theory GTT_Transitive_Closure
imports GTT_Compose Basic_Utils
begin
"step_Δ_ε 𝒜 ℬ ≡">abbreviation "step_Δ⇩ε 𝒜 ℬ ≡
(ta.make {} (ta_rules 𝒜) (ta_eps 𝒜 ∪ Δ⇩ε ℬ 𝒜),
ta.make {} (ta_rules ℬ) (ta_eps ℬ ∪ Δ⇩ε 𝒜 ℬ))"
primrec make_Δ⇩ε :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ nat ⇒ ('q, 'f) ta × ('q, 'f) ta" where
"make_Δ⇩ε 𝒜 ℬ 0 = (𝒜, ℬ)"
| "make_Δ⇩ε 𝒜 ℬ (Suc n) = (let (𝒜⇩n, ℬ⇩n) = make_Δ⇩ε 𝒜 ℬ n in step_Δ⇩ε 𝒜⇩n ℬ⇩n)"
"states 𝒜 ℬ ≡ ta_states 𝒜 ∪ ta_states ℬ"">abbreviation "states 𝒜 ℬ ≡ ta_states 𝒜 ∪ ta_states ℬ"
"ε_ext1 𝒜 ℬ n ≡ ta_eps (fst (make_Δ_ε 𝒜 ℬ n))"">abbreviation "ε_ext1 𝒜 ℬ n ≡ ta_eps (fst (make_Δ⇩ε 𝒜 ℬ n))"
"ε_ext2 𝒜 ℬ n ≡ ta_eps (snd (make_Δ_ε 𝒜 ℬ n))"">abbreviation "ε_ext2 𝒜 ℬ n ≡ ta_eps (snd (make_Δ⇩ε 𝒜 ℬ n))"
lemma Δ⇩ε_subset1: "Δ⇩ε 𝒜 ℬ ⊆ ta_states 𝒜 × ta_states ℬ"
unfolding Δ⇩ε_def using ta_res_states by blast
lemma Δ⇩ε_subset:
assumes "ta_states 𝒜' ⊆ states 𝒜 ℬ" "ta_states ℬ' ⊆ states 𝒜 ℬ"
shows "Δ⇩ε 𝒜' ℬ' ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
using assms Δ⇩ε_subset1 by blast
lemma Δ⇩ε_states:
assumes "(q, q') ∈ Δ⇩ε 𝒜 ℬ"
shows "q ∈ states 𝒜 ℬ" "q' ∈ states 𝒜 ℬ"
using assms Δ⇩ε_subset1 by blast+
lemma make_Δ⇩ε_ta_rules':
"ta_rules (fst (make_Δ⇩ε 𝒜 ℬ (Suc n))) = ta_rules (fst (make_Δ⇩ε 𝒜 ℬ n))"
"ta_rules (snd (make_Δ⇩ε 𝒜 ℬ (Suc n))) = ta_rules (snd (make_Δ⇩ε 𝒜 ℬ n))"
unfolding ta.make_def make_Δ⇩ε.simps
by (metis (no_types, lifting) case_prod_unfold ext_inject fst_conv snd_conv surjective)+
lemma make_Δ⇩ε_ta_rules:
"ta_rules (fst (make_Δ⇩ε 𝒜 ℬ n)) = ta_rules (fst (make_Δ⇩ε 𝒜 ℬ 0))"
"ta_rules (snd (make_Δ⇩ε 𝒜 ℬ n)) = ta_rules (snd (make_Δ⇩ε 𝒜 ℬ 0))"
using make_Δ⇩ε_ta_rules' by (induction n) fast+
lemma make_Δ⇩ε_ta_eps':
"ε_ext1 𝒜 ℬ n ⊆ ε_ext1 𝒜 ℬ (Suc n)" "ε_ext2 𝒜 ℬ n ⊆ ε_ext2 𝒜 ℬ (Suc n)"
unfolding ta.make_def make_Δ⇩ε.simps using fst_conv snd_conv
by (metis (no_types, lifting) Un_upper1 case_prod_beta' select_convs(3))+
lemma make_Δ⇩ε_ta_eps:
assumes "m ≥ n"
shows "ε_ext1 𝒜 ℬ n ⊆ ε_ext1 𝒜 ℬ m" "ε_ext2 𝒜 ℬ n ⊆ ε_ext2 𝒜 ℬ m"
using assms make_Δ⇩ε_ta_eps' fst_conv snd_conv le_Suc_eq
by (induction m) fastforce+
lemma subset_states_compose:
assumes "⋃ (r_states ` ta_rules 𝒜) ⊆ Q" "ta_eps 𝒜 ⊆ Q × Q" "ta_final 𝒜 ⊆ Q"
shows "ta_states 𝒜 ⊆ Q"
using assms unfolding ta_states_def by blast
lemma make_Δ⇩ε_states_subset:
"ta_states (fst (make_Δ⇩ε 𝒜 ℬ n)) ⊆ states 𝒜 ℬ ∧
ta_states (snd (make_Δ⇩ε 𝒜 ℬ n)) ⊆ states 𝒜 ℬ"
unfolding make_Δ⇩ε.simps ta.make_def
proof (induction n)
case (Suc n)
obtain 𝒜⇩n ℬ⇩n where nth: "make_Δ⇩ε 𝒜 ℬ n = (𝒜⇩n, ℬ⇩n)" by fastforce
hence "ta_eps 𝒜⇩n ⊆ states 𝒜 ℬ × states 𝒜 ℬ" "ta_eps ℬ⇩n ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
using Suc by (auto simp: ta_states_def)
moreover have "Δ⇩ε ℬ⇩n 𝒜⇩n ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
"Δ⇩ε 𝒜⇩n ℬ⇩n ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
using Suc by (simp_all add: Δ⇩ε_subset nth)
ultimately have eps: "ta_eps (fst (make_Δ⇩ε 𝒜 ℬ (Suc n))) ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
"ta_eps (snd (make_Δ⇩ε 𝒜 ℬ (Suc n))) ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
unfolding make_Δ⇩ε.simps ta.make_def nth by auto
have final: "ta_final (fst (make_Δ⇩ε 𝒜 ℬ (Suc n))) ⊆ states 𝒜 ℬ"
"ta_final (snd (make_Δ⇩ε 𝒜 ℬ (Suc n))) ⊆ states 𝒜 ℬ"
by (auto simp: ta.make_def nth)
have "⋃ (r_states ` ta_rules 𝒜⇩n) ⊆ states 𝒜 ℬ"
"⋃ (r_states ` ta_rules ℬ⇩n) ⊆ states 𝒜 ℬ"
using make_Δ⇩ε_ta_rules[of 𝒜 ℬ n] nth
unfolding make_Δ⇩ε.simps fst_conv snd_conv ta_states_def by auto
hence rules: "⋃ (r_states ` ta_rules (fst (make_Δ⇩ε 𝒜 ℬ (Suc n)))) ⊆ states 𝒜 ℬ"
"⋃ (r_states ` ta_rules (snd (make_Δ⇩ε 𝒜 ℬ (Suc n)))) ⊆ states 𝒜 ℬ"
using nth unfolding make_Δ⇩ε.simps ta.make_def by auto
show ?case using subset_states_compose[OF rules(1) eps(1) final(1)]
subset_states_compose[OF rules(2) eps(2) final(2)] by blast
qed simp
lemma ε_ext1_subset: "ε_ext1 𝒜 ℬ n ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
using make_Δ⇩ε_states_subset[of 𝒜 ℬ n] unfolding ta_states_def by auto
lemma ε_ext2_subset: "ε_ext2 𝒜 ℬ n ⊆ states 𝒜 ℬ × states 𝒜 ℬ"
using make_Δ⇩ε_states_subset[of 𝒜 ℬ n] unfolding ta_states_def by auto
text ‹The following lemma shows that there exists a
saturated GTT obtained by iteratively adding ε-transitions.›
lemma trans_closure_fixpoint:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
shows "∃N. ∀n≥N. make_Δ⇩ε 𝒜 ℬ n = make_Δ⇩ε 𝒜 ℬ N"
proof -
define S where "S = states 𝒜 ℬ × states 𝒜 ℬ"
have "finite S" using assms finite_subset S_def by blast
have sub: "∀n. ε_ext1 𝒜 ℬ n ⊆ S ∧ ε_ext2 𝒜 ℬ n ⊆ S"
using ε_ext1_subset ε_ext2_subset S_def by blast
have "∃n. ∀m≥n. (ε_ext1 𝒜 ℬ m) = (ε_ext1 𝒜 ℬ n) ∧
(ε_ext2 𝒜 ℬ m) = (ε_ext2 𝒜 ℬ n)"
using inc_set_fixpoint2[OF _ sub ‹finite S›] make_Δ⇩ε_ta_eps by fast
then obtain n where "∀m≥n. (ε_ext1 𝒜 ℬ m) = (ε_ext1 𝒜 ℬ n) ∧
(ε_ext2 𝒜 ℬ m) = (ε_ext2 𝒜 ℬ n)" by blast
from this this[THEN spec[of _ "Suc n"]] have
"∀m≥Suc n. (ε_ext1 𝒜 ℬ m) = (ε_ext1 𝒜 ℬ (Suc n)) ∧ (ε_ext2 𝒜 ℬ m) = (ε_ext2 𝒜 ℬ (Suc n))"
using Suc_leD le_SucI[OF le_refl] by blast
moreover have "∀m≥Suc n. ta_final (fst (make_Δ⇩ε 𝒜 ℬ m)) = ta_final (fst (make_Δ⇩ε 𝒜 ℬ (Suc n))) ∧
ta_final (snd (make_Δ⇩ε 𝒜 ℬ m)) = ta_final (snd (make_Δ⇩ε 𝒜 ℬ (Suc n)))"
by (auto split: prod.splits simp: ta.make_def dest: Suc_le_D)
moreover have "∀m≥Suc n. ta_rules (fst (make_Δ⇩ε 𝒜 ℬ m)) = ta_rules (fst (make_Δ⇩ε 𝒜 ℬ (Suc n))) ∧
ta_rules (snd (make_Δ⇩ε 𝒜 ℬ m)) = ta_rules (snd (make_Δ⇩ε 𝒜 ℬ (Suc n)))"
using make_Δ⇩ε_ta_rules[of 𝒜 ℬ]
by (auto split: prod.splits simp del: make_Δ⇩ε.simps) blast+
ultimately have "∀m≥Suc n. make_Δ⇩ε 𝒜 ℬ m = make_Δ⇩ε 𝒜 ℬ (Suc n)"
using prod_eqI ta.equality unfolding make_Δ⇩ε.simps ta.make_def
by (metis (mono_tags, lifting) old.unit.exhaust)
thus ?thesis by blast
qed
"least_fp_N 𝒜 ℬ ≡ LEAST N. ∀n≥N. make_Δ_ε 𝒜 ℬ n = make_Δ_ε 𝒜 ℬ N"">definition "least_fp_N 𝒜 ℬ ≡ LEAST N. ∀n≥N. make_Δ⇩ε 𝒜 ℬ n = make_Δ⇩ε 𝒜 ℬ N"
definition 𝒢⇩N :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta × ('q, 'f) ta" where
"𝒢⇩N 𝒜 ℬ = make_Δ⇩ε 𝒜 ℬ (least_fp_N 𝒜 ℬ)"
lemma 𝒢⇩N_is_fixpoint:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
shows "step_Δ⇩ε (fst (𝒢⇩N 𝒜 ℬ)) (snd (𝒢⇩N 𝒜 ℬ)) = 𝒢⇩N 𝒜 ℬ"
using LeastI_ex[OF trans_closure_fixpoint[OF assms], THEN spec[of _ "Suc (least_fp_N 𝒜 ℬ)"]]
by (cases "make_Δ⇩ε 𝒜 ℬ (least_fp_N 𝒜 ℬ)") (auto simp: 𝒢⇩N_def least_fp_N_def)
lemma 𝒢⇩N_GTT_comp:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
shows "GTT_comp (𝒢⇩N 𝒜 ℬ) (𝒢⇩N 𝒜 ℬ) = 𝒢⇩N 𝒜 ℬ"
using 𝒢⇩N_is_fixpoint[OF assms] by (auto simp: GTT_comp_def)
lemma 𝒢⇩N_GTT_trans:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
"(s, u) ∈ gtt_lang (𝒢⇩N 𝒜 ℬ)" "(u, t) ∈ gtt_lang (𝒢⇩N 𝒜 ℬ)"
shows "(s, t) ∈ gtt_lang (𝒢⇩N 𝒜 ℬ)"
using gtt_comp_lang_complete[of "𝒢⇩N 𝒜 ℬ" "𝒢⇩N 𝒜 ℬ"] assms(3,4)
by (auto simp: 𝒢⇩N_GTT_comp[OF assms(1,2)])
lemma 𝒢⇩N_GTT_step:
assumes "(s, t) ∈ gtt_lang (𝒜, ℬ)"
shows "(s, t) ∈ gtt_lang (𝒢⇩N 𝒜 ℬ)"
using make_Δ⇩ε_ta_eps[of 0 "least_fp_N 𝒜 ℬ", of 𝒜 ℬ, THEN subsetD] assms(1)
by (auto intro!: gtt_accept_mono[of "(𝒜, ℬ)"] simp: 𝒢⇩N_def make_Δ⇩ε_ta_rules)
lemma 𝒢⇩N_complete:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
shows "Restr ((gtt_lang (𝒜, ℬ))⇧*) {t. ground t} ⊆ gtt_lang (𝒢⇩N 𝒜 ℬ)"
unfolding rtrancl_trancl_reflcl Int_Un_distrib2
proof (intro Un_least, goal_cases)
case 1
have "gtt_lang (𝒜, ℬ) ⊆ gtt_lang (𝒢⇩N 𝒜 ℬ)" using 𝒢⇩N_GTT_step[of _ _ 𝒜 ℬ] by auto
note trancl_mono[OF _ this]
moreover have "(gtt_lang (𝒢⇩N 𝒜 ℬ))⇧+ = gtt_lang (𝒢⇩N 𝒜 ℬ)" using 𝒢⇩N_GTT_trans[OF assms]
by (intro trancl_id transI)
ultimately show ?case by blast
next
case 2 then show ?case using gtt_accept.refl by blast
qed
lemma make_Δ⇩ε_by_GTT_comp:
"make_Δ⇩ε 𝒜 ℬ (Suc n) = GTT_comp (make_Δ⇩ε 𝒜 ℬ n) (make_Δ⇩ε 𝒜 ℬ n)"
by (cases "make_Δ⇩ε 𝒜 ℬ n") (auto simp: GTT_comp_def)
lemma gtt_lang_ground_ctxt_closed:
assumes "ground_ctxt C" "(s, t) ∈ gtt_lang 𝒢"
shows "(C⟨s⟩, C⟨t⟩) ∈ gtt_lang 𝒢"
proof -
{ fix i s and ss1 ss2 :: "('f, 'v) term list" assume "i < Suc (length ss1 + length ss2)"
then have "fill_holes ((map mctxt_of_term ss1 @ MHole # map mctxt_of_term ss2) ! i)
((replicate (length ss1) [] @ [s] # replicate (length ss2) []) ! i) = (ss1 @ s # ss2) ! i"
by (cases "i = length ss1") (auto simp del: upt_Suc simp: nth_append)
} note [simp] = this
have *: "fill_holes (MFun f (map mctxt_of_term ss1 @ MHole # map mctxt_of_term ss2)) [s] = Fun f (ss1 @ s # ss2)"
for f ss1 s ss2 by (auto simp del: upt_Suc intro!: nth_equalityI)
then have "ctxt.closed {(s, t). gtt_accept 𝒢 s t}"
using accept'_closed_ctxt[of "[_]" "[_]" 𝒢 "MFun _ ((map mctxt_of_term _) @ MHole # (map mctxt_of_term _))"]
unfolding * by (auto simp: gtt_accept_equiv intro!: one_imp_ctxt_closed)
then show ?thesis using assms by auto
qed
lemma gtt_langs_ground_ctxt_closed:
assumes "ground_ctxt C" "(s, t) ∈ (gtt_lang 𝒢)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (gtt_lang 𝒢)⇧*"
using assms(2) gtt_lang_ground_ctxt_closed[OF assms(1), of _ _ 𝒢]
by (induct rule: rtrancl_induct) (auto intro: rtrancl.intros(2))
lemma ground_ctxt_closed_imp_ground_mctxt_closed:
assumes "⋀C s t. ground_ctxt C ⟹ (s, t) ∈ R⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ R⇧*"
"length ss = num_holes C" "length ts = num_holes C" "ground_mctxt C"
"⋀i. i < num_holes C ⟹ (ss ! i, ts ! i) ∈ Restr (R⇧*) {t. ground t}"
shows "(fill_holes C ss, fill_holes C ts) ∈ R⇧*"
proof -
have "i ≤ num_holes C ⟹ (fill_holes C ss, fill_holes C (take i ts @ drop i ss)) ∈ R⇧*" for i
proof (induct i)
case (Suc i)
have "num_holes C = Suc (length (take i ts) + length (drop (Suc i) ss))"
using Suc(2) assms(2,3) by auto
from fill_holes_ctxt_main[OF this]
obtain D where [simp]: "⋀s. D⟨s⟩ = fill_holes C (take i ts @ s # drop (Suc i) ss)" by metis
have [simp]: "take i ts @ ss ! i # drop (Suc i) ss = take i ts @ drop i ss"
"take i ts @ ts ! i # drop (Suc i) ss = take (Suc i) ts @ drop (Suc i) ss"
using Suc(2) assms(2,3)
by (simp_all add: Cons_nth_drop_Suc Suc.prems Suc_le_lessD assms(3) take_Suc_conv_app_nth)
have "ground D⟨ss ! i⟩" using assms(2-5) by (auto simp: ground_fill_holes in_set_conv_nth)
then have "ground_ctxt D" by (metis ground_ctxt_apply)
then show ?case using Suc(1,2) assms(1)[of D "ss ! i" "ts ! i"] assms(5) by auto
qed auto
from this[of "num_holes C"] show ?thesis using assms(2,3) by auto
qed
lemma partition_by_singles:
"length xs = n ⟹ partition_by xs (replicate n (Suc 0)) = map (λx. [x]) xs"
by (induct xs arbitrary: n) auto
lemma map_nth':
"length xs = n ⟹ map (op ! xs) [0..<n] = xs"
by (auto simp: map_nth)
lemma ground_ctxt_closed_imp_arg_closed:
assumes "⋀C s t. ground_ctxt C ⟹ (s, t) ∈ R⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ R⇧*"
"length ss = length ts"
"⋀i. i < length ts ⟹ (ss ! i, ts ! i) ∈ Restr (R⇧*) {t. ground t}"
shows "(Fun f ss, Fun f ts) ∈ R⇧*"
using ground_ctxt_closed_imp_ground_mctxt_closed[of R ss "MFun f (replicate (length ts) MHole)" ts]
assms(2,3) by (auto simp: assms(1) partition_by_singles map_nth' cong: list.map_cong_simp)
lemma rtrancl_gtt_lang_ground_mctxt_closed:
assumes "length ss = num_holes C" "length ts = num_holes C" "ground_mctxt C"
"∀i < num_holes C. (ss ! i, ts ! i) ∈ Restr ((gtt_lang 𝒢)⇧*) {t. ground t}"
shows "(fill_holes C ss, fill_holes C ts) ∈ (gtt_lang 𝒢)⇧*"
using assms(4) ground_ctxt_closed_imp_ground_mctxt_closed[OF _ assms(1,2,3), of "gtt_lang 𝒢"]
by (auto simp: gtt_langs_ground_ctxt_closed)
lemma rtrancl_gtt_lang_arg_closed:
assumes "length ss = length ts" "∀i < length ts. (ss ! i, ts ! i) ∈ Restr ((gtt_lang 𝒢)⇧*) {t. ground t}"
shows "(Fun f ss, Fun f ts) ∈ (gtt_lang 𝒢)⇧*"
using assms(2) ground_ctxt_closed_imp_arg_closed[OF _ assms(1), of "gtt_lang 𝒢"]
by (auto simp: gtt_langs_ground_ctxt_closed)
lemma GTT_comp_𝒢_𝒢_in_rtrancl:
"gtt_lang (GTT_comp 𝒢 𝒢) ⊆ (gtt_lang 𝒢)⇧*"
proof -
{ fix q t 𝒢 assume "q ∈ ta_res (fst (GTT_comp 𝒢 𝒢)) t" "ground t"
then have "∃s. ground s ∧ (t, s) ∈ (gtt_lang 𝒢)⇧* ∧ q ∈ ta_res (fst 𝒢) s"
proof (induct t arbitrary: q)
case (Fun f ts)
obtain qs q' where q': "f qs → q' ∈ ta_rules (fst (GTT_comp 𝒢 𝒢))"
"(q', q) ∈ (ta_eps (fst (GTT_comp 𝒢 𝒢)))⇧*" "length qs = length ts"
"⋀i. i<length ts ⟹ qs ! i ∈ ta_res (fst (GTT_comp 𝒢 𝒢)) (ts ! i)"
using Fun(2) by auto
{ fix i assume i: "i < length ts"
then have "∃s. ground s ∧ (ts ! i, s) ∈ (gtt_lang 𝒢)⇧* ∧ qs ! i ∈ ta_res (fst 𝒢) s"
using Fun(1)[OF nth_mem q'(4), of i] Fun(3) by auto
}
then obtain ss where ss: "i < length ts ⟹ ground (ss i) ∧ (ts ! i, ss i) ∈ (gtt_lang 𝒢)⇧* ∧
qs ! i ∈ ta_res (fst 𝒢) (ss i)" for i by metis
define s where "s = Fun f (map ss [0..<length ts])"
have "ground s" using ss(1) by (auto simp: s_def)
moreover have "(Fun f ts, s) ∈ (gtt_lang 𝒢)⇧*" using ss(1) Fun(3)
by (auto intro!: rtrancl_gtt_lang_arg_closed simp: s_def)
moreover have "q' ∈ ta_res (fst 𝒢) s" using q'(1,3) ss by (auto simp: GTT_comp_def s_def)
moreover show ?case using q'(2) calculation
proof (induct arbitrary: s rule: converse_rtrancl_induct)
case (step q' p)
consider "(q', p) ∈ ta_eps (fst 𝒢)" | "(q', p) ∈ Δ⇩ε (snd 𝒢) (fst 𝒢)"
using step(1) by (auto simp: GTT_comp_def)
then show ?case
proof (cases)
case 1 then show ?thesis using step(3)[of s] step(4,5,6) by (auto intro: ta_res_eps)
next
case 2
obtain s' where "(s, s') ∈ gtt_lang 𝒢" "ground s'" "p ∈ ta_res (fst 𝒢) s'"
using 2 step(4,6) by (auto simp: Δ⇩ε_def)
then show ?thesis using step(5) rtrancl.rtrancl_into_rtrancl step.hyps(3) by force
qed
qed auto
qed auto
} note * = this
have "gtt_accept' (GTT_comp 𝒢 𝒢) s t ⟹ ground s ⟹ ground t ⟹ (s, t) ∈ (gtt_lang 𝒢)⇧*" for s t
proof (induct rule: gtt_accept'.cases)
case (mctxt ss ts C)
{ fix i assume i: "i < num_holes C"
then obtain q where q: "q ∈ ta_res (fst (GTT_comp 𝒢 𝒢)) (ss ! i)" "q ∈ ta_res (snd (GTT_comp 𝒢 𝒢)) (ts ! i)"
using mctxt(5) by (auto simp: mctxt(3,4))
have [simp]: "ground (ss ! i)" "ground (ts ! i)" using i mctxt(3,4,6,7)
by (auto simp add: ground_fill_holes mctxt(1,2))
obtain s' where s': "ground s'" "q ∈ ta_res (fst 𝒢) s'" "(ss ! i, s') ∈ (gtt_lang 𝒢)⇧*"
using *[of q 𝒢 "ss ! i"] q(1) by auto
obtain t' where t': "ground t'" "q ∈ ta_res (snd 𝒢) t'" "(ts ! i, t') ∈ (gtt_lang (prod.swap 𝒢))⇧*"
using *[of q "prod.swap 𝒢" "ts ! i"] q(2) by auto
have "(gtt_lang (prod.swap 𝒢))¯ = gtt_lang 𝒢" by auto
then have "(t', ts ! i) ∈ (gtt_lang 𝒢)⇧*" using converseI[OF t'(3)] unfolding converse_inward(1) by metis
moreover have "(s', t') ∈ gtt_lang 𝒢" using s'(1,2) t'(1,2) by auto
ultimately have "(ss ! i, ts ! i) ∈ (gtt_lang 𝒢)⇧*" using s'(3)
by (meson rtrancl.rtrancl_into_rtrancl rtrancl_trans)
}
then show ?case using mctxt(6,7)
by (auto simp: ground_fill_holes mctxt(1-4) intro!: rtrancl_gtt_lang_ground_mctxt_closed)
qed
then show ?thesis by (auto simp: gtt_accept_equiv)
qed
lemma make_Δ⇩ε_sound:
"gtt_lang (make_Δ⇩ε 𝒜 ℬ n) ⊆ (gtt_lang (𝒜, ℬ))⇧*"
proof (induct n)
case (Suc n) show ?case using rtrancl_mono[OF Suc] GTT_comp_𝒢_𝒢_in_rtrancl[of "make_Δ⇩ε 𝒜 ℬ n"]
by (simp del: make_Δ⇩ε.simps add: make_Δ⇩ε_by_GTT_comp)
qed auto
lemma 𝒢⇩N_sound:
"gtt_lang (𝒢⇩N 𝒜 ℬ) ⊆ Restr ((gtt_lang (𝒜, ℬ))⇧*) {t. ground t}"
by (auto simp: 𝒢⇩N_def make_Δ⇩ε_sound)
lemma 𝒢⇩N_lang:
assumes "finite (ta_states 𝒜)" "finite (ta_states ℬ)"
shows "gtt_lang (𝒢⇩N 𝒜 ℬ) = Restr ((gtt_lang (𝒜, ℬ))⇧*) {t. ground t}"
using 𝒢⇩N_sound 𝒢⇩N_complete[OF assms] by auto
lemma Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang:
"Restr ((gtt_lang (𝒜, ℬ))⇧*) {t. ground t} = (gtt_lang (𝒜, ℬ))⇧+"
by (auto simp: rtrancl_trancl_reflcl simp del: reflcl_trancl dest: tranclD tranclD2)
"GTT_rtrancl G ≡ 𝒢_N (fst G) (snd G)"">abbreviation "GTT_rtrancl G ≡ 𝒢⇩N (fst G) (snd G)"
end