theory GTT_Compose
imports GTT
begin
inductive_set Δ⇩ε_set :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for 𝒜 ℬ where
Δ⇩ε_set_cong: "TA_rule f ps p |∈| rules 𝒜 ⟹ TA_rule f qs q |∈| rules ℬ ⟹ length ps = length qs ⟹
(⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ⇩ε_set 𝒜 ℬ) ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ"
| Δ⇩ε_set_eps1: "(p, p') |∈| eps 𝒜 ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ ⟹ (p', q) ∈ Δ⇩ε_set 𝒜 ℬ"
| Δ⇩ε_set_eps2: "(q, q') |∈| eps ℬ ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ ⟹ (p, q') ∈ Δ⇩ε_set 𝒜 ℬ"
lemma Δ⇩ε_states: "Δ⇩ε_set 𝒜 ℬ ⊆ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
proof -
{fix p q assume "(p, q) ∈ Δ⇩ε_set 𝒜 ℬ" then have "(p, q) ∈ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
by (induct) (auto dest: rule_statesD eps_statesD simp flip: fmember.rep_eq)}
then show ?thesis by auto
qed
lemma finite_Δ⇩ε [simp]: "finite (Δ⇩ε_set 𝒜 ℬ)"
using finite_subset[OF Δ⇩ε_states]
by simp
context
includes fset.lifting
begin
lift_definition Δ⇩ε :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) fset" is Δ⇩ε_set by simp
lemmas Δ⇩ε_cong = Δ⇩ε_set_cong [Transfer.transferred]
lemmas Δ⇩ε_eps1 = Δ⇩ε_set_eps1 [Transfer.transferred]
lemmas Δ⇩ε_eps2 = Δ⇩ε_set_eps2 [Transfer.transferred]
lemmas Δ⇩ε_cases = Δ⇩ε_set.cases[Transfer.transferred]
lemmas Δ⇩ε_induct [consumes 1, case_names Δ⇩ε_cong Δ⇩ε_eps1 Δ⇩ε_eps2] = Δ⇩ε_set.induct[Transfer.transferred]
lemmas Δ⇩ε_intros = Δ⇩ε_set.intros[Transfer.transferred]
lemmas Δ⇩ε_simps = Δ⇩ε_set.simps[Transfer.transferred]
end
lemma finite_alt_def [simp]:
"finite {(α, β). (∃t. ground t ∧ α |∈| ta_der 𝒜 t ∧ β |∈| ta_der ℬ t)}" (is "finite ?S")
by (auto dest: ground_ta_der_states[THEN fsubsetD] simp flip: fmember.rep_eq
intro!: finite_subset[of ?S "fset (𝒬 𝒜 |×| 𝒬 ℬ)"])
lemma Δ⇩ε_def':
"Δ⇩ε 𝒜 ℬ = {|(α, β). (∃t. ground t ∧ α |∈| ta_der 𝒜 t ∧ β |∈| ta_der ℬ t)|}"
proof (intro fset_eqI iffI, goal_cases lr rl)
case (lr x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
have "∃t. ground t ∧ p |∈| ta_der 𝒜 t ∧ q |∈| ta_der ℬ t" using lr unfolding x
proof (induct rule: Δ⇩ε_induct)
case (Δ⇩ε_cong f ps p qs q)
obtain ts where ts: "ground (ts i) ∧ ps ! i |∈| ta_der 𝒜 (ts i) ∧ qs ! i |∈| ta_der ℬ (ts i)"
if "i < length qs" for i using Δ⇩ε_cong(5) by metis
then show ?case using Δ⇩ε_cong(1-3)
by (auto intro!: exI[of _ "Fun f (map ts [0..<length qs])"]) blast+
qed (meson ta_der_eps)+
then show ?case by auto
next
case (rl x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
obtain t where "ground t" "p |∈| ta_der 𝒜 t" "q |∈| ta_der ℬ t" using rl by auto
then show ?case unfolding x
proof (induct t arbitrary: p q)
case (Fun f ts)
obtain p' ps where p': "TA_rule f ps p' |∈| rules 𝒜" "p' = p ∨ (p', p) |∈| (eps 𝒜)|⇧+|" "length ps = length ts"
"⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (ts ! i)" using Fun(3) by auto
obtain q' qs where q': "f qs → q' |∈| rules ℬ" "q' = q ∨ (q', q) |∈| (eps ℬ)|⇧+|" "length qs = length ts"
"⋀i. i < length ts ⟹ qs ! i |∈| ta_der ℬ (ts ! i)" using Fun(4) by auto
have st: "(p', q') |∈| Δ⇩ε 𝒜 ℬ"
using Fun(1)[OF nth_mem _ p'(4) q'(4)] Fun(2) p'(3) q'(3)
by (intro Δ⇩ε_cong[OF p'(1) q'(1)]) auto
{assume "(p', p) |∈| (eps 𝒜)|⇧+|" then have "(p, q') |∈| Δ⇩ε 𝒜 ℬ" using st
by (induct rule: ftrancl_induct) (auto intro: Δ⇩ε_eps1)}
from st this p'(2) have st: "(p, q') |∈| Δ⇩ε 𝒜 ℬ" by auto
{assume "(q', q) |∈| (eps ℬ)|⇧+|" then have "(p, q) |∈| Δ⇩ε 𝒜 ℬ" using st
by (induct rule: ftrancl_induct) (auto intro: Δ⇩ε_eps2)}
from st this q'(2) show "(p, q) |∈| Δ⇩ε 𝒜 ℬ" by auto
qed auto
qed
lemma Δ⇩ε_fmember:
"(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟷ (∃t. ground t ∧ p |∈| ta_der 𝒜 t ∧ q |∈| ta_der ℬ t)"
by (auto simp: Δ⇩ε_def')
definition GTT_comp :: "('q, 'f) gtt ⇒ ('q, 'f) gtt ⇒ ('q, 'f) gtt" where
"GTT_comp 𝒢⇩1 𝒢⇩2 = (TA (gtt_rules (fst 𝒢⇩1, fst 𝒢⇩2))
(eps (fst 𝒢⇩1) |∪| eps (fst 𝒢⇩2) |∪| (Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2))),
TA (gtt_rules (snd 𝒢⇩1, snd 𝒢⇩2))
(eps (snd 𝒢⇩1) |∪| eps (snd 𝒢⇩2) |∪| (Δ⇩ε (fst 𝒢⇩2) (snd 𝒢⇩1))))"
lemma gtt_syms_GTT_comp:
"gtt_syms (GTT_comp A B) = gtt_syms A |∪| gtt_syms B"
by (auto simp: GTT_comp_def ta_sig_def)
lemma Δ⇩ε_statesD:
"(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟹ p |∈| 𝒬 𝒜"
"(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟹ q |∈| 𝒬 ℬ"
using subsetD[OF Δ⇩ε_states, of "(p, q)" 𝒜 ℬ]
by (auto simp flip: Δ⇩ε.rep_eq fmember.rep_eq)
lemma Δ⇩ε_statesD':
"q |∈| eps_states (Δ⇩ε 𝒜 ℬ) ⟹ q |∈| 𝒬 𝒜 |∪| 𝒬 ℬ"
by (auto simp: eps_states_def fmember.abs_eq dest: Δ⇩ε_statesD)
lemma Δ⇩ε_swap:
"prod.swap p |∈| Δ⇩ε 𝒜 ℬ ⟷ p |∈| Δ⇩ε ℬ 𝒜"
by (auto simp: Δ⇩ε_def')
lemma gtt_states_comp_union:
"gtt_states (GTT_comp 𝒢⇩1 𝒢⇩2) |⊆| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
proof (intro fsubsetI, goal_cases lr)
case (lr q) then show ?case
by (auto simp: GTT_comp_def gtt_states_def 𝒬_def dest: Δ⇩ε_statesD')
qed
lemma GTT_comp_swap [simp]:
"GTT_comp (prod.swap 𝒢⇩2) (prod.swap 𝒢⇩1) = prod.swap (GTT_comp 𝒢⇩1 𝒢⇩2)"
by (simp add: GTT_comp_def ac_simps)
lemma gtt_comp_complete_semi:
assumes s: "q |∈| gta_der (fst 𝒢⇩1) s" and u: "q |∈| gta_der (snd 𝒢⇩1) u" and ut: "gtt_accept 𝒢⇩2 u t"
shows "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
proof (goal_cases L R)
let ?𝒢 = "GTT_comp 𝒢⇩1 𝒢⇩2"
have sub1l: "rules (fst 𝒢⇩1) |⊆| rules (fst ?𝒢)" "eps (fst 𝒢⇩1) |⊆| eps (fst ?𝒢)"
and sub1r: "rules (snd 𝒢⇩1) |⊆| rules (snd ?𝒢)" "eps (snd 𝒢⇩1) |⊆| eps (snd ?𝒢)"
and sub2r: "rules (snd 𝒢⇩2) |⊆| rules (snd ?𝒢)" "eps (snd 𝒢⇩2) |⊆| eps (snd ?𝒢)"
by (auto simp: GTT_comp_def)
{ case L then show ?case using s ta_der_mono[OF sub1l]
by (auto simp: gta_der_def)
next
case R then show ?case using ut u
proof (induct arbitrary: q s rule: gtt_accept.induct)
case (refl t) then show ?case using ta_der_mono[OF sub1r] by (auto simp: gta_der_def)
next
case (join p t u)
have "(p, q) |∈| eps (snd ?𝒢)" using join
by (simp add: fmember.abs_eq GTT_comp_def)
(force simp: Δ⇩ε_def' gta_der_def)
from ta_der_eps[OF this] join(2) ta_der_mono[OF sub2r]
show ?case by (auto simp: gta_der_def)
next
case (ctxt ts us f)
from ctxt(3) obtain ps p where "TA_rule f ps p |∈| rules (snd 𝒢⇩1)" "p = q ∨ (p, q) |∈| (eps (snd 𝒢⇩1))|⇧+|"
"length ps = length ts" "⋀i. i < length ts ⟹ ps ! i |∈| gta_der (snd 𝒢⇩1) (ts ! i)"
by (auto simp: gta_der_def)
then show ?case using ctxt(1, 2) sub1r(1) ftrancl_mono[OF _ sub1r(2)]
by (auto simp: gta_der_def intro!: exI[of _ p] exI[of _ ps])
qed}
qed
lemmas gtt_comp_complete_semi' = gtt_comp_complete_semi[of _ "prod.swap 𝒢⇩2" _ _ "prod.swap 𝒢⇩1" for 𝒢⇩1 𝒢⇩2,
unfolded fst_swap snd_swap GTT_comp_swap gtt_accept_swap]
lemma gtt_comp_acomplete:
"gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2) ⊆ agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2)"
proof (intro subrelI, goal_cases LR)
case (LR s t)
then consider
q u where "q |∈| gta_der (fst 𝒢⇩1) s" "q |∈| gta_der (snd 𝒢⇩1) u" "gtt_accept 𝒢⇩2 u t"
| q u where "q |∈| gta_der (snd 𝒢⇩2) t" "q |∈| gta_der (fst 𝒢⇩2) u" "gtt_accept 𝒢⇩1 s u"
apply (auto simp: gcomp_rel_def dest!: gtt_lang_from_agtt_lang[THEN equalityD2, THEN subsetD, of "(s, t)", simplified])
apply (auto simp: lift_root_step.simps gmctxtex_onp_gtt_accpet)
apply (auto simp: agtt_lang_def)
done
then show ?case
proof (cases)
case 1 show ?thesis using gtt_comp_complete_semi[OF 1]
by (auto simp: agtt_lang_def gta_der_def)
next
case 2 show ?thesis using gtt_comp_complete_semi'[OF 2]
by (auto simp: agtt_lang_def gta_der_def)
qed
qed
lemma Δ⇩ε_steps_from_𝒢⇩2:
assumes "(q, q') |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "q |∈| gtt_states 𝒢⇩2"
"gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
shows "(q, q') |∈| (eps (fst 𝒢⇩2))|⇧+| ∧ q' |∈| gtt_states 𝒢⇩2"
using assms(1-2)
proof (induct rule: converse_ftrancl_induct)
case (Base y)
then show ?case using assms(3)
by (fastforce simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD Δ⇩ε_statesD(1))
next
case (Step q p)
have "(q, p) |∈| (eps (fst 𝒢⇩2))|⇧+|" "p |∈| gtt_states 𝒢⇩2"
using Step(1, 4) assms(3)
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD Δ⇩ε_statesD(1))
then show ?case using Step(3)
by (auto intro: ftrancl_trans)
qed
lemma Δ⇩ε_steps_from_𝒢⇩1:
assumes "(p, r) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "p |∈| gtt_states 𝒢⇩1"
"gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
obtains "r |∈| gtt_states 𝒢⇩1" "(p, r) |∈| (eps (fst 𝒢⇩1))|⇧+|"
| q p' where "r |∈| gtt_states 𝒢⇩2" "p = p' ∨ (p, p') |∈| (eps (fst 𝒢⇩1))|⇧+|" "(p', q) |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)"
"q = r ∨ (q, r) |∈| (eps (fst 𝒢⇩2))|⇧+|"
using assms(1,2)
proof (induct arbitrary: thesis rule: converse_ftrancl_induct)
case (Base p)
from Base(1) consider (a) "(p, r) |∈| eps (fst 𝒢⇩1)" | (b) "(p, r) |∈| eps (fst 𝒢⇩2)" |
(c) "(p, r) |∈| (Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2))"
by (auto simp: GTT_comp_def fmember.abs_eq)
then show ?case using assms(3) Base
by cases (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD Δ⇩ε_statesD)
next
case (Step q p)
consider "(q, p) |∈| (eps (fst 𝒢⇩1))|⇧+|" "p |∈| gtt_states 𝒢⇩1"
| "(q, p) |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "p |∈| gtt_states 𝒢⇩2" using assms(3) Step(1, 6)
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD Δ⇩ε_statesD)
then show ?case
proof (cases)
case 1 note a = 1 show ?thesis
proof (cases rule: Step(3))
case (2 p' q)
then show ?thesis using assms a
by (auto intro: Step(5) ftrancl_trans)
qed (auto simp: a(2) intro: Step(4) ftrancl_trans[OF a(1)])
next
case 2 show ?thesis using Δ⇩ε_steps_from_𝒢⇩2[OF Step(2) 2(2) assms(3)] Step(5)[OF _ _ 2(1)] by auto
qed
qed
lemma Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2:
assumes "(q, q') |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "q |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
"gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
obtains "q |∈| gtt_states 𝒢⇩1" "q' |∈| gtt_states 𝒢⇩1" "(q, q') |∈| (eps (fst 𝒢⇩1))|⇧+|"
| p p' where "q |∈| gtt_states 𝒢⇩1" "q' |∈| gtt_states 𝒢⇩2" "q = p ∨ (q, p) |∈| (eps (fst 𝒢⇩1))|⇧+|"
"(p, p') |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "p' = q' ∨ (p', q') |∈| (eps (fst 𝒢⇩2))|⇧+|"
| "q |∈| gtt_states 𝒢⇩2" "(q, q') |∈| (eps (fst 𝒢⇩2))|⇧+| ∧ q' |∈| gtt_states 𝒢⇩2"
using assms Δ⇩ε_steps_from_𝒢⇩1 Δ⇩ε_steps_from_𝒢⇩2
by (metis funion_iff)
lemma GTT_comp_eps_fst_statesD:
"(p, q) |∈| eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) ⟹ p |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
"(p, q) |∈| eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) ⟹ q |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD Δ⇩ε_statesD)
lemma GTT_comp_eps_ftrancl_fst_statesD:
"(p, q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+| ⟹ p |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
"(p, q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+| ⟹ q |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
using GTT_comp_eps_fst_statesD[of _ _ 𝒢⇩1 𝒢⇩2]
by (meson converse_ftranclE ftranclE)+
lemma GTT_comp_first:
assumes "q |∈| ta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q |∈| gtt_states 𝒢⇩1"
"gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
shows "q |∈| ta_der (fst 𝒢⇩1) t"
using assms(1,2)
proof (induct t arbitrary: q)
case (Var q')
have "q ≠ q' ⟹ q' |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" using Var
by (auto dest: GTT_comp_eps_ftrancl_fst_statesD)
then show ?case using Var assms(3)
by (auto elim: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2)
next
case (Fun f ts)
obtain q' qs where q': "TA_rule f qs q' |∈| rules (fst (GTT_comp 𝒢⇩1 𝒢⇩2))"
"q' = q ∨ (q', q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "length qs = length ts"
"⋀i. i < length ts ⟹ qs ! i |∈| ta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) (ts ! i)"
using Fun(2) by auto
have "q' |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" using q'(1)
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
then have st: "q' |∈| gtt_states 𝒢⇩1" and eps:"q' = q ∨ (q', q) |∈| (eps (fst 𝒢⇩1))|⇧+|"
using q'(2) Fun(3) assms(3)
by (auto elim!: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2)
from st have rule: "TA_rule f qs q' |∈| rules (fst 𝒢⇩1)" using assms(3) q'(1)
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
have "i < length ts ⟹ qs ! i |∈| ta_der (fst 𝒢⇩1) (ts ! i)" for i
using rule q'(3, 4)
by (intro Fun(1)[OF nth_mem]) (auto simp: gtt_states_def dest!: rule_statesD(4))
then show ?case using q'(3) rule eps
by auto
qed
lemma GTT_comp_second:
assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}" "q |∈| gtt_states 𝒢⇩2"
"q |∈| ta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
shows "q |∈| ta_der (snd 𝒢⇩2) t"
using assms GTT_comp_first[of q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1"]
by (auto simp: gtt_states_def)
lemma gtt_comp_sound_semi:
fixes 𝒢⇩1 𝒢⇩2 :: "('f, 'q) gtt"
assumes as2: "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
and 1: "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q |∈| gtt_states 𝒢⇩1"
shows "∃u. q |∈| gta_der (snd 𝒢⇩1) u ∧ gtt_accept 𝒢⇩2 u t" using 1(2,3) unfolding gta_der_def
proof (induct rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
show ?case
proof (cases "p |∈| gtt_states 𝒢⇩1")
case True
then have *: "TA_rule f ps p |∈| rules (snd 𝒢⇩1)" using GFun(1, 6) as2
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
moreover have st: "i < length ps ⟹ ps ! i |∈| gtt_states 𝒢⇩1" for i using *
by (force simp: gtt_states_def dest: rule_statesD)
moreover have "i < length ps ⟹ ∃u. ps ! i |∈| ta_der (snd 𝒢⇩1) (term_of_gterm u) ∧ gtt_accept 𝒢⇩2 u (ts ! i)" for i
using st GFun(2) by (intro GFun(5)) simp
then obtain us where
"⋀i. i < length ps ⟹ ps ! i |∈| ta_der (snd 𝒢⇩1) (term_of_gterm (us i)) ∧ gtt_accept 𝒢⇩2 (us i) (ts ! i)"
by metis
moreover have "p = q ∨ (p, q) |∈| (eps (snd 𝒢⇩1))|⇧+|" using GFun(3, 6) True as2
by (auto simp: gtt_states_def elim!: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of p q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1", simplified])
ultimately show ?thesis using GFun(2)
by (intro exI[of _ "GFun f (map us [0..<length ts])"])
(auto intro!: exI[of _ ps] exI[of _ p])
next
case False note nt_st = this
then have False: "p ≠ q" using GFun(6) by auto
then have eps: "(p, q) |∈| (eps (snd (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" using GFun(3) by simp
show ?thesis using Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of p q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1", simplified, OF eps]
proof (cases, goal_cases)
case 1 then show ?case using False GFun(3)
by (metis GTT_comp_eps_ftrancl_fst_statesD(1) GTT_comp_swap fst_swap funion_iff)
next
case 2 then show ?case using as2 by (auto simp: gtt_states_def)
next
case 3 then show ?case using as2 GFun(6) by (auto simp: gtt_states_def)
next
case (4 r p')
have meet: "r |∈| ta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (Fun f (map term_of_gterm ts))"
using GFun(1 - 4) 4(3) False
by (auto simp: GTT_comp_def in_ftrancl_UnI intro!: exI[ of _ ps] exI[ of _ p])
then obtain u where wit: "ground u" "p' |∈| ta_der (snd 𝒢⇩1) u" "r |∈| ta_der (fst 𝒢⇩2) u"
using 4(4-) unfolding Δ⇩ε_def' by blast
from wit(1, 3) have "gtt_accept 𝒢⇩2 (gterm_of_term u) (GFun f ts)"
using GTT_comp_second[OF as2 _ meet]
by (intro gtt_accept.join[of r 𝒢⇩2 "gterm_of_term u" "GFun f ts"])
(auto simp add: gta_der_def gtt_states_def simp del: ta_der_Fun dest: ground_ta_der_states)
then show ?case using 4(5) wit(1, 2)
by (intro exI[of _ "gterm_of_term u"]) (auto simp add: ta_der_trancl_eps)
next
case 5
then show ?case using nt_st as2
by (simp add: gtt_states_def)
qed
qed
qed
lemma gtt_comp_asound:
assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
shows "agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) ⊆ gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
proof (intro subrelI, goal_cases LR)
case (LR s t)
obtain q where q: "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
using LR by (auto simp: agtt_lang_def)
{
fix 𝒢⇩1 𝒢⇩2 s t assume as2: "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
and 1: "q |∈| ta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) (term_of_gterm s)"
"q |∈| ta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (term_of_gterm t)" "q |∈| gtt_states 𝒢⇩1"
note st = GTT_comp_first[OF 1(1,3) as2]
obtain u where u: "q |∈| ta_der (snd 𝒢⇩1) (term_of_gterm u)" "gtt_accept 𝒢⇩2 u t"
using gtt_comp_sound_semi[OF as2 1[folded gta_der_def]] by (auto simp: gta_der_def)
have "(s, u) ∈ agtt_lang 𝒢⇩1" using st u(1)
by (auto simp: agtt_lang_def gta_der_def)
moreover have "(u, t) ∈ gtt_lang 𝒢⇩2" using u(2) by auto
then have "(u, t) ∈ lift_root_step UNIV PAny EParallel (agtt_lang 𝒢⇩2)"
by (auto simp: gtt_lang_from_agtt_lang)
ultimately have "(s, t) ∈ agtt_lang 𝒢⇩1 O lift_root_step UNIV PAny EParallel (agtt_lang 𝒢⇩2)"
by auto}
note base = this
consider "q |∈| gtt_states 𝒢⇩1" | "q |∈| gtt_states 𝒢⇩2" | "q |∉| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" by blast
then show ?case using q assms
proof (cases, goal_cases)
case 1 then show ?case using base[of 𝒢⇩1 𝒢⇩2 s t]
by (auto simp: gcomp_rel_def gta_der_def lift_root_step.simps)
next
case 2 then show ?case using base[of "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1" t s, THEN converseI]
by (auto simp: lift_root_step.simps gcomp_rel_def converse_relcomp converse_agtt_lang converse_lift_root_step gta_der_def gtt_states_def)
(simp add: converse_agtt_lang converse_gmctxtex_onp inf_commute sup_commute)+
next
case 3 then show ?case using fsubsetD[OF gtt_states_comp_union[of 𝒢⇩1 𝒢⇩2], of q]
by (auto simp: gta_der_def gtt_states_def)
qed
qed
lemma gtt_comp_lang_complete:
shows "gtt_lang 𝒢⇩1 O gtt_lang 𝒢⇩2 ⊆ gtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2)"
by (simp only: gtt_lang_from_agtt_lang map_both_relcomp[OF inj_term_of_gterm]
image_mono gcomp_rel[symmetric, unfolded lift_root_step.simps]
lift_root_step_incr gtt_comp_acomplete lift_root_step.simps
gmctxtex_onp_rel_mono)
lemma gtt_comp_alang:
assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
shows "agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) = gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
by (intro equalityI gtt_comp_asound[OF assms] gtt_comp_acomplete)
lemma gtt_comp_lang:
assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
shows "gtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) = gtt_lang 𝒢⇩1 O gtt_lang 𝒢⇩2"
by (simp only: gtt_lang_from_agtt_lang map_both_relcomp[OF inj_term_of_gterm]
image_mono gcomp_rel[symmetric, unfolded lift_root_step.simps]
lift_root_step_incr gtt_comp_alang[OF assms] lift_root_step.simps)
abbreviation GTT_comp' where
"GTT_comp' 𝒢⇩1 𝒢⇩2 ≡ GTT_comp (fmap_states_gtt Inl 𝒢⇩1) (fmap_states_gtt Inr 𝒢⇩2)"
lemma gtt_comp'_alang:
shows "agtt_lang (GTT_comp' 𝒢⇩1 𝒢⇩2) = gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
proof -
have [simp]: "finj_on Inl (gtt_states 𝒢⇩1)" "finj_on Inr (gtt_states 𝒢⇩2)"
by (auto simp add: finj_on.rep_eq)
then show ?thesis
by (subst gtt_comp_alang) (auto simp: agtt_lang_fmap_states_gtt)
qed
end