Theory Regular_Tree_Relations.GTT_Compose

theory GTT_Compose
  imports GTT
begin

subsection ‹GTT closure under composition›

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)}
  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]
           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 =
    (let Δ = Δε (snd 𝒢1) (fst 𝒢2) in
    (TA (gtt_rules (fst 𝒢1, fst 𝒢2)) (eps (fst 𝒢1) |∪| eps (fst 𝒢2) |∪| Δ),
     TA (gtt_rules (snd 𝒢1, snd 𝒢2)) (eps (snd 𝒢1) |∪| eps (snd 𝒢2) |∪| (Δ|¯|))))"

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 Let_def)

lemma Δε_statesD:
  "(p, q) |∈| Δε 𝒜   p |∈| 𝒬 𝒜"
  "(p, q) |∈| Δε 𝒜   q |∈| 𝒬 "
  using subsetD[OF Δε_states, of "(p, q)" 𝒜 ]
  by (auto simp flip: Δε.rep_eq)

lemma Δε_statesD':
  "q |∈| eps_states (Δε 𝒜 )  q |∈| 𝒬 𝒜 |∪| 𝒬 "
  by (auto simp: eps_states_def dest: Δε_statesD)

lemma Δε_swap:
  "prod.swap p |∈| Δε 𝒜   p |∈| Δε  𝒜"
  by (auto simp: Δε_def')

lemma Δε_inverse [simp]:
  "(Δε 𝒜 )|¯| = Δε  𝒜"
  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 unfolding gtt_accept_def
    proof (induct arbitrary: q s)
      case (base s t)
      from base(1) obtain p where p: "p |∈| gta_der (fst 𝒢2) s" "p |∈| gta_der (snd 𝒢2) t"
        by (auto simp: agtt_lang_def)
      then have "(p, q) |∈| eps (snd (GTT_comp 𝒢1 𝒢2))"
        using Δε_fmember[of p q "fst 𝒢2" "snd 𝒢1"] base(2)
        by (auto simp: GTT_comp_def gta_der_def)
      from ta_der_eps[OF this] show ?case using p ta_der_mono[OF sub2r]
        by (auto simp add: gta_der_def)
    next
      case (step ss ts f)
      from step(1, 4) 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) (ss ! i)"
        unfolding gta_der_def by auto
      then show ?case using step(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"
    by (auto simp: gcomp_rel_def gtt_accept_def elim!: agtt_langE)
  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 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 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)
  then show ?case using assms(3) Base
    by cases (auto simp: GTT_comp_def gtt_states_def 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 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 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 simp: gtt_accept_def 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] unfolding gtt_accept_def
        by (intro gmctxt_cl.base agtt_langI[of r])
           (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)
  { (* prepare symmetric cases: q |∈| gtt_states 𝒢1 and q |∈| gtt_states 𝒢2 *)
    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 simp: gtt_accept_def)
    ultimately have "(s, t)  agtt_lang 𝒢1 O gmctxt_cl UNIV (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)
  next
    case 2 then show ?case using base[of "prod.swap 𝒢2" "prod.swap 𝒢1" t s, THEN converseI]
      by (auto simp: gcomp_rel_def converse_relcomp converse_agtt_lang gta_der_def gtt_states_def)
         (simp add: finter_commute funion_commute gtt_lang_swap prod.swap_def)+
  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)"
  using gmctxt_cl_mono_rel[OF gtt_comp_acomplete, of UNIV 𝒢1 𝒢2]
  by (simp only: gcomp_rel[symmetric])

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: arg_cong[OF gtt_comp_alang[OF assms], of "gmctxt_cl UNIV"] gcomp_rel)

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