Theory GTT

theory GTT
  imports TR.Tree_Automata FOR.Lift_Root_Step
begin

(* A GTT 𝒢 consists of a set of interface states and
   a set of rules for automaton 𝒜 and one for ℬ. *)
type_synonym ('q, 'f) gtt = "('q, 'f) ta × ('q, 'f) ta"

abbreviation gtt_rules where
  "gtt_rules 𝒢 ≡ rules (fst 𝒢) |∪| rules (snd 𝒢)"
abbreviation gtt_eps where
  "gtt_eps 𝒢 ≡ eps (fst 𝒢) |∪| eps (snd 𝒢)"
definition gtt_states where
  "gtt_states 𝒢 = 𝒬 (fst 𝒢) |∪| 𝒬 (snd 𝒢)"
abbreviation gtt_syms where
  "gtt_syms 𝒢 ≡ ta_sig (fst 𝒢) |∪| ta_sig (snd 𝒢)"
definition gtt_interface where
  "gtt_interface 𝒢 = 𝒬 (fst 𝒢) |∩| 𝒬 (snd 𝒢)"

(* We define two notions of GTT acceptance, and show equivalence of them *)

inductive gtt_accept :: "('q, 'f) gtt ⇒ 'f gterm ⇒ 'f gterm ⇒ bool" for 𝒢 where
  refl [intro]: "gtt_accept 𝒢 t t"
| join [intro]: "q |∈| gta_der (fst 𝒢) s ⟹ q |∈| gta_der (snd 𝒢) t ⟹ gtt_accept 𝒢 s t"
| ctxt [intro]: "length ss = length ts ⟹
                 ∀i < length ss. gtt_accept 𝒢 (ss ! i) (ts ! i) ⟹
                 gtt_accept 𝒢 (GFun f ss) (GFun f ts)"

hide_fact (open) refl (* don't shadow HOL.refl *)

inductive gtt_accept' :: "('q, 'f) gtt ⇒ 'f gterm ⇒ 'f gterm ⇒ bool"
  for 𝒢 where
  mctxt [intro]: "length ss = length ts ⟹ num_gholes C = length ss ⟹
    ∀i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i) ⟹
    gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)"


text ‹language accepted by a GTT›

abbreviation gtt_lang :: "('q, 'f) gtt ⇒ 'f gterm rel" where
  "gtt_lang 𝒢 ≡ {(s, t). gtt_accept 𝒢 s t}"

abbreviation gtt_lang_terms :: "('q, 'f) gtt ⇒ ('f, 'q) term rel" where
  "gtt_lang_terms 𝒢 ≡ {(s, t). gtt_accept 𝒢 (gterm_of_term s) (gterm_of_term t) ∧ ground s ∧ ground t}"

lemma term_of_gterm_gtt_lang_gtt_lang_terms_conv:
  "map_both term_of_gterm ` gtt_lang 𝒢 = gtt_lang_terms 𝒢"
  by auto (metis CollectI case_prodI gterm_of_term_inv map_prod_imageI)

text ‹*anchored* language accepted by a GTT›

definition agtt_lang :: "('q, 'f) gtt ⇒ 'f gterm rel" where
  "agtt_lang 𝒢 = {(t, u) |t u q. q |∈| gta_der (fst 𝒢) t ∧ q |∈| gta_der (snd 𝒢) u}"

lemma converse_agtt_lang:
  "(agtt_lang 𝒢)¯ = agtt_lang (prod.swap 𝒢)"
  by (auto simp: agtt_lang_def)

lemma agtt_lang_swap:
  "agtt_lang (prod.swap 𝒢) = prod.swap ` agtt_lang 𝒢"
  by (auto simp: agtt_lang_def)

(* Lemmas about gtt_accept' *)
lemma gtt_accept'_refl [simp]:
  "gtt_accept' 𝒢 t t"
proof -
  have "gtt_accept' 𝒢 (fill_gholes (gmctxt_of_gterm t) [])
                      (fill_gholes (gmctxt_of_gterm t) [])" by fastforce
  thus ?thesis by simp
qed

lemma gtt_accept'_join [simp]:
  assumes "q |∈| gta_der (fst 𝒢) s" "q |∈| gta_der (snd 𝒢) t"
  shows "gtt_accept' 𝒢 s t"
proof -
  have "gtt_accept' 𝒢 (fill_gholes GMHole [s]) (fill_gholes GMHole [t])"
    using assms by (intro gtt_accept'.intros) auto
  thus ?thesis by simp
qed

lemma gtt_cont_extrct:
  assumes "gtt_accept' 𝒢 s t"
  shows "∃C ss ts. s =⇩G⇩f (C, ss) ∧ t =⇩G⇩f (C, ts) ∧
         (∀i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧
                              q |∈| gta_der (snd 𝒢) (ts ! i))"
  using assms by (auto elim!: gtt_accept'.cases) (metis eq_gfill.intros)

lemma gtt_accept'E [elim]:
  assumes "gtt_accept' 𝒢 s t"
  obtains C ss ts where "s = fill_gholes C ss" "t = fill_gholes C ts"
    "num_gholes C = length ss" "num_gholes C = length ts"
    "∀ i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
  using gtt_cont_extrct[OF assms] eqgfE
  by blast 

lemma gtt_accept'_closed:
  assumes "length ss = length ts" "∀ i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
  shows " gtt_accept' 𝒢 (GFun f ss) (GFun f ts)"
proof -
  let ?Prop = "λ (C, ss',ts') i. ss ! i =⇩G⇩f (C, ss') ∧ ts ! i =⇩G⇩f (C, ts') ∧
        (∀j < length ts'. ∃q. q |∈| gta_der (fst 𝒢) (ss' ! j) ∧
                              q |∈| gta_der (snd 𝒢) (ts' ! j)) ∧
        gtt_accept' 𝒢 (fill_gholes C ss') (fill_gholes C ts')"
  from assms gtt_cont_extrct[of 𝒢 "ss ! i" "ts ! i" for i]
  have "∀ i < length ts. ∃ C ss' ts'. ?Prop (C, ss', ts') i" for i
    by auto (metis eqgfE(1))
  then obtain xs where inv: "length ts = length xs" "∀ i < length xs. ?Prop (xs ! i) i"
    using Ex_list_of_length_P[of "length ts" ?Prop]
    by fastforce
  define Ds where "Ds ≡ map fst xs" define sss where "sss ≡ map (fst ∘ snd) xs"
  define tss where "tss ≡ map (snd ∘ snd) xs" note unf = Ds_def sss_def tss_def
  let ?C = "GMFun f (replicate (length Ds) GMHole)"
  have len: "length ts = length Ds" "length Ds = length sss" "length sss = length tss"
    using inv(1) by (auto simp: unf comp_def)
  then have eq: "∀ i < length tss. ss ! i =⇩G⇩f (Ds ! i, sss ! i)" "∀ i < length tss. ts ! i =⇩G⇩f (Ds ! i, tss ! i)"
    using len inv by (auto simp: unf)
  then have len_inn: "∀ i < length tss. length (sss ! i) = length (tss ! i)"
    using len by auto (metis eqgfE(2))
  have mem: "∀ i < length (concat tss). ∃ q. q |∈| gta_der (fst 𝒢) (concat sss ! i) ∧ q |∈| gta_der (snd 𝒢) (concat tss ! i)"
    using len len_inn inv by (intro concat_nth_nthI) (auto simp: unf comp_def case_prod_unfold)
  have *: "fill_gholes ?C ss = GFun f ss" "fill_gholes ?C ts = GFun f ts"
    using len assms(1) by (auto simp del: fill_gholes.simps)
  have s: "GFun f ss =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat sss)"
    using assms(1) eq len_inn len inv(1) unfolding *[symmetric]
    by (intro fill_gholes_gmctxt_sound) (auto simp add: assms(1))
  have t: "GFun f ts =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat tss)"
    using assms(1) eq len_inn len inv(1) unfolding *[symmetric]
    by (intro fill_gholes_gmctxt_sound) (auto simp add: assms(1))
  show ?thesis unfolding eqgfE[OF s] eqgfE[OF t]
    using mem len inv(1) len_inn eq eqgfE(2)[OF s] eqgfE(2)[OF t]
    by (intro gtt_accept'.mctxt[of "concat sss" "concat tss" "fill_gholes_gmctxt ?C Ds" 𝒢])
     (auto simp del: fill_gholes_gmctxt.simps fill_gholes.simps)
qed

(* The following lemma proves that the two definitions of gtt_accept are equivalent *)

lemma gtt_accept_equiv:
  "gtt_accept 𝒢 s t ⟷ gtt_accept' 𝒢 s t"
proof (rule iffI)
  assume "gtt_accept 𝒢 s t"
  then show "gtt_accept' 𝒢 s t"
  proof (induction rule: gtt_accept.induct)
    case (ctxt ss ts f)
    then show ?case using gtt_accept'_closed[OF ctxt(1), of 𝒢]
      by auto
  qed auto
next
  assume "gtt_accept' 𝒢 s t"
  then show "gtt_accept 𝒢 s t"
  proof (induction rule: gtt_accept'.induct)
    case (mctxt ss ts C) thus ?case
    proof (induction C arbitrary: ss ts)
      case GMHole
      then obtain s' t' where "ss = [s']" "ts = [t']" by (cases ss; cases ts) fastforce+
      thus ?case using GMHole(3) by auto
    next
      case (GMFun f Cs)
      moreover { fix i
        assume asm: "i < length Cs"
        hence lengths_eq: "length (partition_gholes ss Cs ! i) = length (partition_gholes ts Cs ! i)"
          by (metis calculation(2, 3) length_map length_partition_by_nth num_gholes.simps(2))
        have num_holes_length: "num_gholes (Cs ! i) = length (partition_gholes ss Cs ! i)"
          using asm GMFun(3) by (simp add: length_partition_by_nth) 
        have join: "∀j<length (partition_gholes ts Cs ! i).
              ∃q. q |∈| gta_der (fst 𝒢) ((partition_gholes ss Cs ! i) ! j) ∧
                  q |∈| gta_der (snd 𝒢) ((partition_gholes ts Cs ! i) ! j)"
          using GMFun(2,3,4)
          by (simp add: asm length_partition_by_nth partition_by_nth_nth(1) partition_by_nth_nth(2))
        have "gtt_accept 𝒢 (fill_gholes (Cs ! i) (partition_gholes ss Cs ! i))
                            (fill_gholes (Cs ! i) (partition_gholes ts Cs ! i))"
          using asm GMFun(1)[OF _ lengths_eq num_holes_length join] by auto
      }
      ultimately show ?case using length_upt[of 0 "length Cs"] unfolding fill_gholes.simps
        by (intro gtt_accept.intros(3)) auto
    qed
  qed
qed

lemma accept'_closed_ctxt:
  assumes "length ss = length ts"
  and "∀i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
  and "num_gholes C = length ss"
  shows "gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)" using assms
proof (induction C arbitrary: ss ts)
  case GMHole
  then show ?case
    by (cases ss; cases ts) auto
next
  case (GMFun f Cs)
  let ?sss = "(partition_gholes ss Cs)"
  let ?tss = "(partition_gholes ts Cs)"
  obtain Css Cts where Css_Cts:"fill_gholes (GMFun f Cs) ss = GFun f Css"
    "fill_gholes (GMFun f Cs) ts = GFun f Cts" "length Cts = length Css"
    by simp
  {fix i
   assume loc_asm: "i < length Cs"
   hence "length (?sss ! i) = length (?tss ! i)" using assms(1) GMFun
     by (simp add: length_partition_by_nth)
   moreover have "num_gholes (Cs ! i) = length (?sss ! i)" using assms(2) loc_asm GMFun
     by (simp add: length_partition_by_nth)
   moreover have "∀j < length (?tss ! i). gtt_accept' 𝒢 ((?sss ! i) ! j)  ((?tss ! i) ! j)"
     using loc_asm GMFun assms(3)
     by (simp add: calculation(1, 2) partition_by_nth_nth(1, 2))
   ultimately have "gtt_accept' 𝒢 (fill_gholes (Cs ! i) (?sss ! i)) (fill_gholes (Cs ! i) (?tss ! i))"
     using GMFun(1) loc_asm by force
   hence "gtt_accept 𝒢 (fill_gholes (Cs!i) (?sss!i)) (fill_gholes (Cs ! i) (?tss ! i))"
     using gtt_accept_equiv by blast}
  hence "∀i < length Cts. gtt_accept 𝒢 (Css ! i) (Cts ! i)" using Css_Cts by fastforce
  hence "gtt_accept 𝒢 (GFun f Css) (GFun f Cts)" using Css_Cts(3) by auto
  then show ?case using gtt_accept_equiv Css_Cts by metis
qed


lemma gtt_lang_from_agtt_lang:
  "gtt_lang 𝒢 = lift_root_step UNIV PAny EParallel (agtt_lang 𝒢)"
  by (auto simp: lift_root_step.simps gtt_accept_equiv agtt_lang_def elim!: gtt_accept'E gmctxtex_onpE)

text ‹Inverse of GTTs.›

lemma gtt_accept_swap [simp]:
  "gtt_accept (prod.swap 𝒢) s t ⟷ gtt_accept 𝒢 t s"
  unfolding gtt_accept_equiv
  by (intro iffI; elim gtt_accept'.cases; metis gtt_accept'.intros fst_swap snd_swap)

lemma gtt_lang_swap:
  "(gtt_lang (A, B))¯ = gtt_lang (B, A)"
  using gtt_accept_swap[of "(A, B)"] by auto

lemma gmctxtex_onp_gtt_accpet:
  "gmctxtex_onp (λC. True) (agtt_lang 𝒢)= gtt_lang 𝒢"
  using gtt_lang_from_agtt_lang[ unfolded lift_root_step.simps, of 𝒢]
  unfolding agtt_lang_def
  by force

lemma gtt_lang_signature_closed:
  "signature_closed UNIV (gtt_lang 𝒢)"
  unfolding gmctxtex_onp_gtt_accpet[symmetric]
  by (intro gmctxtex_onp_sig_closed) simp

(* The following Lemmas are about ta_res' *)

abbreviation mctxt_of_terms where
  "mctxt_of_terms s t ≡ (mctxt_of_term s) ⊓ (mctxt_of_term t)"
abbreviation residuals where
  "residuals s t ≡ inf_mctxt_args (mctxt_of_term s) (mctxt_of_term t)"

lemma term_mctxt [simp]:
  "term_of_mctxt (MFun f (map mctxt_of_term ts)) = Fun f ts"
  by (metis term_of_mctxt_mctxt_of_term_id mctxt_of_term.simps(2))

lemma map_zip_fun:
  assumes "length xs = length ys"
  shows "map (λ(x,y). f x y) (zip (map g xs) (map g ys)) =
         map (λ(x,y). f (g x) (g y)) (zip xs ys)"
  by (simp add: map_nth_eq_conv)

lemma terms_to_common_residuals:
  fixes s t :: "('f, 'v) term"
  shows "s = fill_holes (mctxt_of_terms s t) (map term_of_mctxt (residuals s t)) ∧
         t = fill_holes (mctxt_of_terms s t) (map term_of_mctxt (residuals t s))"
proof (induction s arbitrary: t)
  case (Var x) thus ?case
  proof (induction t)
    case (Var y)
    have "num_holes (MVar y ⊓ MVar x) = num_holes (MVar x ⊓ MVar y)" by simp
    define n_holes where "n_holes = (λ (x::'v) y. num_holes (MVar x ⊓ MVar y))"
    have "(n_holes y x = n_holes x y ∧ Var y = Var x) ∨
          (n_holes y x = n_holes x y ∧ y ≠ x)" using n_holes_def by simp
    thus ?case by fastforce
  next
    case (Fun f ts)
    have "Fun f ts = term_of_mctxt (MFun f (map mctxt_of_term ts))"
      by (metis mctxt_of_term.simps(2) term_of_mctxt_mctxt_of_term_id)
    hence "Fun f ts = fill_holes (mctxt_of_terms (Var x) (Fun f ts))
                  (map term_of_mctxt (residuals (Fun f ts) (Var x)))"
      using term_mctxt[of f ts] by fastforce
    thus ?case by auto
  qed
next
  case (Fun g ss) thus ?case
  proof (induction t arbitrary: g ss)
    case (Var y)
    have "Fun g ss = fill_holes (mctxt_of_terms (Var y) (Fun g ss))
                  (map term_of_mctxt (residuals (Fun g ss) (Var y)))"
      using term_mctxt[of g ss] by fastforce
    thus ?case using term_mctxt[of g ss] by fastforce
  next
    case (Fun f ts) thus ?case
    proof (cases "f = g ∧ length ts = length ss")
      case True
      hence "mctxt_of_terms (Fun g ss) (Fun f ts) =
               MFun f (map (λ(s',t'). mctxt_of_terms s' t') (zip ss ts))"
        using True by (simp add: zip_nth_conv)
      let ?Cs = "map (λ(s',t'). mctxt_of_terms s' t') (zip ss ts)" and
          ?ts = "residuals (Fun g ss) (Fun f ts)" and
          ?ts' = "map (λ(s',t'). inf_mctxt_args s' t') (zip (map mctxt_of_term ss) (map mctxt_of_term ts))" and
          ?ts'' = "map (λ(s',t'). residuals s' t') (zip ss ts)" and
          ?ss = "residuals (Fun f ts) (Fun g ss)" and
          ?ss' = "map (λ(t',s'). inf_mctxt_args t' s') (zip (map mctxt_of_term ts) (map mctxt_of_term ss))" and
          ?ss'' = "map (λ(t',s'). residuals t' s') (zip ts ss)"
      { fix s' t' :: "('f, 'v) Term.term" and  ss' ts'
        assume "s' ∈ set ss'" "t' ∈ set ts'"
        hence "length (residuals s' t') = num_holes (mctxt_of_terms s' t')"
              "length (residuals s' t') = num_holes (mctxt_of_terms t' s')"
          using num_holes_inf_mctxt by (metis, metis inf_mctxt_comm)
      } note residuals_num_holes = this
      have "i < length (map num_holes ?Cs) ⟹
             length (?ts'' ! i) = (map num_holes ?Cs) ! i" for i
        using residuals_num_holes(1)[of _ ss _ ts] True by force
      hence "partition_by ?ts (map num_holes ?Cs) = ?ts'"
        using partition_by_concat_id[of ?ts' "map num_holes ?Cs"] True by simp
      hence part1: "map (λ(s', t'). residuals s' t') (zip ss ts) = partition_holes ?ts ?Cs"
        using True map_zip_fun by metis
      have "i < length (map num_holes ?Cs) ⟹
             length (?ss'' ! i) = (map num_holes ?Cs) ! i" for i
        using residuals_num_holes(2)[of _ ts _ ss] True by force
      hence "partition_by ?ss (map num_holes ?Cs) = ?ss'"
        using partition_by_concat_id[of ?ss' "map num_holes ?Cs"] True by simp
      hence part2: "map (λ(t', s'). residuals t' s') (zip ts ss) = partition_holes ?ss ?Cs"
        using True map_zip_fun by metis
      have push_map_inside: "(map term_of_mctxt) ∘ (λ(x, y). residuals x y) =
            (λ(x, y). map term_of_mctxt (residuals x y))" by auto
      { fix i
        assume "i < length ss"
        hence ith_in_set: "ss ! i ∈ set ss" using True by simp+
        hence IH': "ss ! i = fill_holes (mctxt_of_terms (ss ! i) (ts ! i))
                                   (map term_of_mctxt (residuals (ss ! i) (ts ! i)))"
              "ts ! i = fill_holes (mctxt_of_terms (ss ! i) (ts ! i))
                                   (map term_of_mctxt (residuals (ts ! i) (ss ! i)))"
          using Fun(2)[of "ss ! i" "ts ! i"] True by (meson set_zip_leftD)+
        have "ss ! i = fill_holes (map (λ(x, y). mctxt_of_terms x y) (zip ss ts) ! i)
                         (map (λ(x, y). map term_of_mctxt (residuals x y)) (zip ss ts) ! i)"
             "ts ! i = fill_holes (map (λ(x, y). mctxt_of_terms x y) (zip ss ts) ! i)
                         (map (λ(x, y). map term_of_mctxt (residuals x y)) (zip ts ss) ! i)"
          using IH' True nth_map[of i "zip ss ts"] ‹i < length ss› by force+
      } note inner = this
      have "Fun g ss = fill_holes (mctxt_of_terms (Fun g ss) (Fun f ts))
                                  (map term_of_mctxt (residuals (Fun g ss) (Fun f ts)))"
        using True part1[symmetric]
        by (simp add: map_map_partition_by[symmetric] map_zip_fun push_map_inside)
           (smt inner(1) atLeastLessThan_iff map_eq_conv map_nth set_upt) (*TODO*)
      moreover have "Fun f ts = fill_holes (mctxt_of_terms (Fun g ss) (Fun f ts))
                                  (map term_of_mctxt (residuals (Fun f ts) (Fun g ss)))"
        using True part2[symmetric]
        by (simp add: map_map_partition_by[symmetric] map_zip_fun push_map_inside)
           (smt inner(2) atLeastLessThan_iff map_eq_conv map_nth set_upt) (*TODO*)
      ultimately show ?thesis using True by blast
    next
      case False
      thus ?thesis using term_mctxt[of f ts] term_mctxt[of g ss] by fastforce
    qed
  qed
qed

lemma gtt_accept_exI:
  assumes "gtt_accept 𝒢 s t"
  shows "∃ u. u |∈| ta_der' (fst 𝒢) (term_of_gterm s) ∧ u |∈| ta_der' (snd 𝒢) (term_of_gterm t)" using assms
proof (induction)
  case (refl t)
  then show ?case using ta_der'_refl by blast
next
  case (join q s t)
  then show ?case
    by (metis gta_der_def ta_der_to_ta_der') 
next
  case (ctxt ss ts f)
  then have inner: "∃ us. length us = length ss ∧
    (∀i < length ss. (us ! i) |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧
    (us ! i) |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i)))"
    using Ex_list_of_length_P[of "length ss" "λ u i. u |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧
      u |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i))"]
    by auto
  then obtain us where "length us = length ss ∧ (∀i < length ss.
            (us ! i) |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧ (us ! i) |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i)))"
    by blast
  then have "Fun f us |∈| ta_der' (fst 𝒢) (Fun f (map term_of_gterm ss)) ∧
         Fun f us |∈| ta_der' (snd 𝒢) (Fun f (map term_of_gterm ts))" using ctxt(1) by fastforce
  then show ?case by (metis term_of_gterm.simps) 
qed


lemma agtt_lang_mono:
  assumes "rules (fst 𝒢) |⊆| rules (fst 𝒢')" "eps (fst 𝒢) |⊆| eps (fst 𝒢')"
    "rules (snd 𝒢) |⊆| rules (snd 𝒢')" "eps (snd 𝒢) |⊆| eps (snd 𝒢')"
  shows "agtt_lang 𝒢 ⊆ agtt_lang 𝒢'"
  using fsubsetD[OF ta_der_mono[OF assms(1, 2)]] ta_der_mono[OF assms(3, 4)]
  by (auto simp: agtt_lang_def gta_der_def dest!: fsubsetD[OF ta_der_mono[OF assms(1, 2)]] fsubsetD[OF ta_der_mono[OF assms(3, 4)]])

lemma gtt_accept_mono:
  assumes "rules (fst 𝒢) |⊆| rules (fst 𝒢')" "eps (fst 𝒢) |⊆| eps (fst 𝒢')" 
    "rules (snd 𝒢) |⊆| rules (snd 𝒢')" "eps (snd 𝒢) |⊆| eps (snd 𝒢')"
    "gtt_accept 𝒢 s t"
  shows "gtt_accept 𝒢' s t"
  using ta_der_mono[OF assms(1, 2)] ta_der_mono[OF assms(3, 4)]
  using assms(5) unfolding gtt_accept_equiv
  by (auto simp: gta_der_def elim!: gtt_accept'.cases intro!: mctxt) (meson fin_mono)

definition fmap_states_gtt where
  "fmap_states_gtt f ≡ map_both (fmap_states_ta f)"

lemma ground_map_vars_term_simp:
  "ground t ⟹ map_term f g t = map_term f (λ_. undefined) t"
  by (induct t) auto

lemma ground_map_vars_mctxt_simp:
  "ground_mctxt C ⟹ map_vars_mctxt f C = map_vars_mctxt (λ_. undefined) C"
  by (induct C) auto

lemma states_fmap_states_gtt [simp]:
  "gtt_states (fmap_states_gtt f 𝒢) = f |`| gtt_states 𝒢"
  by (simp add: fimage_funion gtt_states_def fmap_states_gtt_def)

lemma agtt_lang_fmap_states_gtt:
  assumes "finj_on f (gtt_states 𝒢)"
  shows "agtt_lang (fmap_states_gtt f 𝒢) = agtt_lang 𝒢" (is "?Ls = ?Rs")
proof -
  from assms have inj: "finj_on f (𝒬 (fst 𝒢) |∪| 𝒬 (snd 𝒢))" "finj_on f (𝒬 (fst 𝒢))" "finj_on f (𝒬 (snd 𝒢))"
    by (auto simp: gtt_states_def finj_on_fUn)
  then have "?Ls ⊆ ?Rs" using ta_der_fmap_states_inv_superset[OF _ inj(1)]
    by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def)
  moreover have "?Rs ⊆ ?Ls"
    by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def elim!: ta_der_to_fmap_states_der)
  ultimately show ?thesis by blast
qed

lemma agtt_lang_Inl_Inr_states_agtt:
  "agtt_lang (fmap_states_gtt Inl 𝒢) = agtt_lang 𝒢"
  "agtt_lang (fmap_states_gtt Inr 𝒢) = agtt_lang 𝒢"
  by (auto simp: finj_Inl_Inr intro!: agtt_lang_fmap_states_gtt)

lemma gtt_lang_fmap_states_gtt:
  assumes "finj_on f (gtt_states 𝒢)"
  shows "gtt_lang (fmap_states_gtt f 𝒢) = gtt_lang 𝒢" (is "?Ls = ?Rs")
  unfolding fmap_states_gtt_def
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x)
  obtain C ss ts where x: "x = (fill_gholes C ss, fill_gholes C ts)"
       "length ss = num_gholes C" "length ts = num_gholes C"
       "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fmap_states_ta f (fst 𝒢)) (ss ! i) ∧
          q |∈| gta_der (fmap_states_ta f (snd 𝒢)) (ts ! i)"
    using lr by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  { fix i assume i: "i < num_gholes C"
    obtain q where q: "q |∈| gta_der (fmap_states_ta f (fst 𝒢)) (ss ! i)"
      "q |∈| gta_der (fmap_states_ta f (snd 𝒢)) (ts ! i)" using x(4)[OF i] by blast
    then have "the_finv_into (gtt_states 𝒢) f q |∈| gta_der (fst 𝒢) (ss ! i) ∧
      the_finv_into (gtt_states 𝒢) f q |∈| gta_der (snd 𝒢) (ts ! i)"
      using assms by (simp add: gta_der_def gtt_states_def ta_der_fmap_states_inv_superset)
    then have "∃ p. p |∈| gta_der (fst 𝒢) (ss ! i) ∧ p |∈| gta_der (snd 𝒢) (ts ! i)"
      using assms by blast}
  then have "gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)"
    using x(2,3) by (auto simp: adapt_vars_def map_vars_term_fill_holes)
  then show ?case using x
    by (simp add: gtt_accept_equiv)
next
  case (rl x)
  obtain C ss ts where x: "x = (fill_gholes C ss, fill_gholes C ts)"
    "length ss = num_gholes C" "length ts = num_gholes C"
    "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
    using rl by (auto 0 0 simp: gtt_accept_equiv image_def elim!: gtt_accept'.cases)
  from x(4) obtain qs where qs: "qs i |∈| gta_der (fst 𝒢) (ss ! i) ∧ qs i |∈| gta_der (snd 𝒢) (ts ! i)"
    if "i < num_gholes C" for i by metis
  have "gtt_accept' (fmap_states_gtt f 𝒢) (fst x) (snd x)"
    using gtt_accept'.intros[of ss ts C "fmap_states_gtt f 𝒢"] x
    using ta_der_fmap_states_ta[OF conjunct1[OF qs, unfolded gta_der_def], where h = f]
    using ta_der_fmap_states_ta[OF conjunct2[OF qs, unfolded gta_der_def], where h = f]
    by (metis fmap_states_gtt_def fst_map_prod gta_der_def map_vars_term_term_of_gterm prod.sel(1, 2) snd_map_prod)
  then show ?case using x by (auto simp: gtt_accept_equiv fmap_states_gtt_def)
qed

definition gtt_only_reach where
  "gtt_only_reach = map_both ta_only_reach"

lemma gtt_only_reach_lang:
  "gtt_lang (gtt_only_reach 𝒢) = gtt_lang 𝒢"
proof (intro equalityI subrelI, goal_cases LR RL)
  case (LR s t)
  then obtain C ss ts qs where
    s: "s = fill_gholes C ss" "length ss = num_gholes C" and
    t: "t = fill_gholes C ts" "length ts = num_gholes C" and
    q: "⋀i. i < num_gholes C ⟹ ∃ q. q |∈| gta_der (fst (gtt_only_reach 𝒢)) (ss ! i) ∧
                        q |∈| gta_der (snd (gtt_only_reach 𝒢)) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃ q . q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)" if "i < num_gholes C" for i
    using q[of i] that
    by (auto simp: gta_der_def gtt_only_reach_def simp flip: ta_der_gterm_only_reach)
  then show ?case using s t by (auto simp: gtt_accept_equiv)
next
  case (RL s t)
  then obtain C ss ts qs where
    s: "s = fill_gholes C ss" "length ss = num_gholes C" and
    t: "t = fill_gholes C ts" "length ts = num_gholes C" and
    q: "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃ q. q |∈| gta_der (fst (gtt_only_reach 𝒢)) (ss ! i) ∧ q |∈| gta_der (snd (gtt_only_reach 𝒢)) (ts ! i)"
    if "i < num_gholes C" for i
    using q[of i] that s t
    by (auto simp add: gta_der_def gtt_only_reach_def simp flip: ta_der_gterm_only_reach)
  then show ?case using s t by (auto simp: gtt_accept_equiv)
qed

lemma gtt_only_reach_syms:
  "gtt_syms (gtt_only_reach 𝒢) |⊆| gtt_syms 𝒢"
  by (auto simp: gtt_only_reach_def ta_restrict_def ta_sig_def)

definition gtt_only_prod where
  "gtt_only_prod 𝒢 = (let iface = gtt_interface 𝒢 in
     map_both (ta_only_prod iface) 𝒢)"
                   
lemma gtt_only_prod_lang:
  "gtt_lang (gtt_only_prod 𝒢) = gtt_lang 𝒢"
proof (intro equalityI subrelI, goal_cases LR RL)
  case (LR s t)
  then obtain C ss ts qs where
    s: "s = fill_gholes C ss" "length ss = num_gholes C" and
    t: "t = fill_gholes C ts" "length ts = num_gholes C" and
    q: "⋀i. i < num_gholes C ⟹ ∃ q. q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i) ∧
          q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)" if "i < num_gholes C" for i using q[OF that]
    by (auto simp: gta_der_def gtt_only_prod_def Let_def intro: ta_der_ta_only_prod_ta_der)
  then show ?case using s t by (auto simp: gtt_accept_equiv)
next
  case (RL s t)
  then obtain C ss ts qs where
    s: "s = fill_gholes C ss" "length ss = num_gholes C" and
    t: "t = fill_gholes C ts" "length ts = num_gholes C" and
    q: "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  {fix i assume i: "i < num_gholes C"
    guess q using q[OF i] by (elim exE conjE) note q = this
    have "q |∈| gtt_interface 𝒢" using q
      by (simp add: gta_der_def gtt_interface_def)
    then have "q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i)" "q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
      using q
      by (auto simp: gta_der_def gtt_only_prod_def Let_def gtt_interface_def ta_der_only_prod ta_productive_setI)
    then have "∃q. q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i) ∧ q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
      by auto}
  then show ?case using s t by (auto simp: gtt_accept_equiv)
qed

lemma gtt_only_prod_syms:
  "gtt_syms (gtt_only_prod 𝒢) |⊆| gtt_syms 𝒢"
  by (auto simp: gtt_only_prod_def ta_restrict_def ta_sig_def Let_def)

definition trim_gtt where
  "trim_gtt = gtt_only_prod ∘ gtt_only_reach"

lemma trim_gtt_lang:
  "gtt_lang (trim_gtt G) = gtt_lang G"
  unfolding trim_gtt_def comp_def gtt_only_prod_lang gtt_only_reach_lang ..

lemma trim_gtt_prod_syms:
  "gtt_syms (trim_gtt G) |⊆| gtt_syms G"
  unfolding trim_gtt_def using fsubset_trans[OF gtt_only_prod_syms gtt_only_reach_syms] by simp

subsection ‹root-cleanliness›

text ‹A GTT is root-clean if none of its interface states can occur in a non-root positions
  in the accepting derivations corresponding to its anchored GTT relation.›

definition ta_nr_states :: "('q, 'f) ta ⇒ 'q fset" where
  "ta_nr_states A = |⋃| ((fset_of_list ∘ r_lhs_states) |`| (rules A))"

definition gtt_nr_states where
  "gtt_nr_states G = ta_nr_states (fst G) |∪| ta_nr_states (snd G)"

definition gtt_root_clean where
  "gtt_root_clean G ⟷ gtt_nr_states G |∩| gtt_interface G = {||}"


subsection ‹Relabeling›

definition relabel_gtt :: "('q :: linorder, 'f) gtt ⇒ (nat, 'f) gtt" where
  "relabel_gtt G = fmap_states_gtt (map_fset_to_nat (gtt_states G)) G"

lemma relabel_agtt_lang [simp]:
  "agtt_lang (relabel_gtt G) = agtt_lang G"
  by (simp add: agtt_lang_fmap_states_gtt map_fset_to_nat_inj relabel_gtt_def)

lemma agtt_lang_sig:
  "fset (gtt_syms G) ⊆ ℱ ⟹ agtt_lang G ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  by (auto simp: agtt_lang_def gta_der_def 𝒯⇩G_equivalent_def)
     (metis ffunas_gterm.rep_eq less_eq_fset.rep_eq subset_iff ta_der_gterm_sig)+
   

end