Theory GTT

theory GTT
  imports TA.Tree_Automata Tree_Automata_Utils Basic_Utils
begin

abbreviation map_both where
  "map_both f ≡ map_prod f f"

(* A 𝒢 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 𝒢 ≡ ta_rules (fst 𝒢) ∪ ta_rules (snd 𝒢)"
abbreviation gtt_eps where
  "gtt_eps 𝒢 ≡ ta_eps (fst 𝒢) ∪ ta_eps (snd 𝒢)"
abbreviation gtt_states where
  "gtt_states 𝒢 ≡ ta_states (fst 𝒢) ∪ ta_states (snd 𝒢)"
abbreviation gtt_syms where
  "gtt_syms 𝒢 ≡ ta_syms (fst 𝒢) ∪ ta_syms (snd 𝒢)"

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

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

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

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

abbreviation gtt_lang where
  "gtt_lang 𝒢 ≡ Restr {(s, t). gtt_accept 𝒢 s t} {t. ground t}"

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

lemma gtt_accept'_join[simp]:
  assumes "q ∈ ta_res (fst 𝒢) s" "q ∈ ta_res (snd 𝒢) t"
  shows "gtt_accept' 𝒢 s t"
proof -
  have "gtt_accept' 𝒢 (fill_holes MHole [s]) (fill_holes MHole [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 = fill_holes C ss) ∧ (t = fill_holes C ts) ∧
         (length ss = length ts) ∧ (num_holes C = length ss ) ∧
         (∀i < length ts. ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧
                              q ∈ ta_res (snd 𝒢) (ts ! i))"
  using assms by (auto elim!: gtt_accept'.cases)

(* 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"
  thus "gtt_accept' 𝒢 s t"
  proof (induction rule: gtt_accept.induct)
    case (ctxt ss ts f)
    let ?Prop = "λx i. ∃C ss' ts'. x = (C, (ss', ts')) ∧ length ss' = length ts' ∧
        (num_holes C = length ss') ∧
        (ss ! i = fill_holes C ss') ∧ (ts ! i = fill_holes C ts') ∧
        (∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
                              q ∈ ta_res (snd 𝒢) (ts' ! j)) ∧
        gtt_accept' 𝒢 (fill_holes C ss') (fill_holes C ts')"
    { fix i
      assume "i < length ss"
      hence "gtt_accept' 𝒢 (ss ! i) (ts ! i)" using ctxt(2) by blast
      hence "∃x C ss' ts'. x = (C, (ss', ts')) ∧ length ss' = length ts' ∧
        (num_holes C = length ss') ∧
        (ss ! i = fill_holes C ss') ∧ (ts ! i = fill_holes C ts') ∧
        (∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
                              q ∈ ta_res (snd 𝒢) (ts' ! j)) ∧
        gtt_accept' 𝒢 (fill_holes C ss') (fill_holes C ts')"
        by (auto elim!: gtt_accept'.cases)
    } note inner = this
    then obtain xs where xs: "length xs = length ss ∧ (∀i<length ss. ?Prop (xs ! i) i)"
      using construct_exI'[of "length ss" ?Prop] by blast
    hence ss_i_ts_i:
      "∀i<length xs. ss ! i = fill_holes ((map fst xs) ! i) ((map (fst ∘ snd) xs) ! i) ∧
                     ts ! i = fill_holes ((map fst xs) ! i) ((map (snd ∘ snd) xs) ! i) ∧
                     num_holes ((map fst xs) ! i) = length ((map (fst ∘ snd) xs) ! i) ∧
                     num_holes ((map fst xs) ! i) = length ((map (snd ∘ snd) xs) ! i)"
       by (smt comp_apply fst_conv length_map map_nth nth_map snd_conv)
    define ss' ts' where ss': "ss' = concat (map (fst ∘ snd) xs)" and
                         ts': "ts' = concat (map (snd ∘ snd) xs)"
    hence lengths_eq: "length ss' = length ts'" using ss_i_ts_i
      by (metis (no_types, lifting) eq_length_concat_nth length_map)
    have map_eq: "map (num_holes ∘ fst) xs = map (length ∘ (fst ∘ snd)) xs"
      using ss_i_ts_i by (metis (no_types, lifting) List.map.compositionality map_eq_conv')
    hence num_holes: "num_holes (MFun f (map fst xs)) = length ss'"
      using ss' ts' by (auto simp: length_concat nth_map[of _ xs] map_eq)
    have "∀i<length xs. ∀j < length ((map (snd ∘ snd) xs) ! i).
                       ∃q. q ∈ ta_res (fst 𝒢) (((map (fst ∘ snd) xs) ! i) ! j) ∧
                           q ∈ ta_res (snd 𝒢) (((map (snd ∘ snd) xs) ! i) ! j)"
      using xs by (smt comp_apply fst_conv length_map map_nth nth_map snd_conv)
    hence join_state: "∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
                                            q ∈ ta_res (snd 𝒢) (ts' ! j)"
      using ss_i_ts_i (*nth_concat_two_lists[of _ "map (fst ∘ snd) xs" "map (snd ∘ snd) xs"]*)
        unfolding ss' ts' by (smt length_map nth_concat_two_lists ss_i_ts_i)
    have "i < length (map (num_holes ∘ fst) xs) ⟹
          length (map (fst ∘ snd) xs ! i) = map (num_holes ∘ fst) xs ! i" for i
      using ss_i_ts_i by fastforce
    hence f_ss: "Fun f ss = fill_holes (MFun f (map fst xs)) ss'"
      using xs ss_i_ts_i partition_by_concat_id[of "map (fst ∘ snd) xs" "map (num_holes ∘ fst) xs"]
      unfolding ss' by simp (smt atLeastLessThan_iff map_eq_conv map_nth set_upt ss_i_ts_i)
    have "i < length (map (num_holes ∘ fst) xs) ⟹
          length (map (snd ∘ snd) xs ! i) = map (num_holes ∘ fst) xs ! i" for i
      using ss_i_ts_i by fastforce
    hence f_ts: "Fun f ts = fill_holes (MFun f (map fst xs)) ts'"
      using xs ss_i_ts_i partition_by_concat_id[of "map (snd ∘ snd) xs" "map (num_holes ∘ fst) xs"]
      unfolding ss' ts' ‹length ss = length ts›
      by simp (smt atLeastLessThan_iff map_eq_conv map_nth set_upt ss_i_ts_i)
    show ?case using join_state lengths_eq num_holes unfolding f_ss f_ts
      by (intro gtt_accept'.intros) auto
  qed auto
next
  assume "gtt_accept' 𝒢 s t"
  thus "gtt_accept 𝒢 s t"
  proof (induction rule: gtt_accept'.induct)
    case (mctxt ss ts C) thus ?case
    proof (induction C arbitrary: ss ts)
      case MHole
      then obtain s' t' where "ss = [s']" "ts = [t']" by (cases ss; cases ts) fastforce+
      thus ?case using MHole(3) by auto
    next
      case (MFun f Cs)
      moreover { fix i
        assume asm: "i < length Cs"
        hence lengths_eq: "length (partition_holes ss Cs ! i) = length (partition_holes ts Cs ! i)"
          using MFun(2,3) by auto
        have num_holes_length: "num_holes (Cs ! i) = length (partition_holes ss Cs ! i)"
          using asm MFun(3) by auto
        have join: "∀j<length (partition_holes ts Cs ! i).
              ∃q. q ∈ ta_res (fst 𝒢) ((partition_holes ss Cs ! i) ! j) ∧
                  q ∈ ta_res (snd 𝒢) ((partition_holes ts Cs ! i) ! j)"
          using MFun(2,3,4)
          by (smt asm length_map lengths_eq nth_map num_holes.simps(3) num_holes_length
              partition_by_nth_nth)
        have "gtt_accept 𝒢 (fill_holes (Cs ! i) (partition_holes ss Cs ! i))
                            (fill_holes (Cs ! i) (partition_holes ts Cs ! i))"
          using asm MFun(1)[OF _ lengths_eq num_holes_length join] by auto
      }
      ultimately show ?case using length_upt[of 0 "length Cs"] unfolding fill_holes.simps
        by (intro gtt_accept.intros(3)) auto
    qed auto
  qed
qed

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 accept'_closed_ctxt:
  assumes "length ss = length ts"
  and "∀i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
  and "num_holes C = length ss"
  shows "gtt_accept' 𝒢 (fill_holes C ss) (fill_holes C ts)"
  using assms
proof (induction C arbitrary: ss ts)
  case (MVar x)
  then show ?case by auto
next
  case MHole
  then show ?case
    by (metis One_nat_def fill_holes_MHole lessI num_holes.simps(2))
next
  case (MFun f Cs)
  let ?sss = "(partition_holes ss Cs)"
  let ?tss = "(partition_holes ts Cs)"
  obtain Css Cts where Css_Cts:"fill_holes (MFun f Cs) ss = Fun f Css"
    "fill_holes (MFun f Cs) ts = Fun 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) MFun by simp
   moreover have "num_holes (Cs ! i) = length (?sss ! i)" using assms(2) loc_asm MFun by force
   moreover have "∀j < length (?tss ! i). gtt_accept' 𝒢 ((?sss ! i) ! j)  ((?tss ! i) ! j)"
      using loc_asm MFun assms(3) by (metis calculation(1) calculation(2) length_map nth_map
                  num_holes.simps(3) partition_by_nth_nth(1) partition_by_nth_nth(2))
   ultimately have "gtt_accept' 𝒢 (fill_holes (Cs ! i) (?sss ! i)) (fill_holes (Cs ! i) (?tss ! i))"
     using MFun(1) loc_asm by force
   hence "gtt_accept 𝒢 (fill_holes (Cs!i) (?sss!i)) (fill_holes (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 𝒢 (Fun f Css) (Fun f Cts)" using Css_Cts(3) by auto
  then show ?case using gtt_accept_equiv Css_Cts by metis
qed

(* The following Lemmas are about ta_res' *)
lemma ta_res'_id:
  "t ∈ ta_res' 𝒜 t"
  by (induction t) auto

lemma ta_res_res'_inclusion:
  fixes q 𝒜 l
  shows "(q ∈ ta_res 𝒜 l) ⟶ Var q ∈ ta_res' 𝒜 l"
  by (induction "𝒜" "l" rule: ta_res.induct) fastforce+

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 mctxt_of_term.simps(2) term_of_mctxt_mctxt_of_term_id)

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" "ground s" "ground t"
  shows "∃u. u ∈ ta_res' (fst 𝒢) s ∧ u ∈ ta_res' (snd 𝒢) t"
  using assms
proof (induction)
  case (refl t)
  thus ?case using ta_res'_id by blast
next
  case (join q s t)
  thus ?case using ta_res_res'_inclusion by fast
next
  case (ctxt ss ts f)
  { fix i
    assume asm: "i < length ss"
    hence "ground (ts ! i)" "ground (ss ! i)" using ctxt by auto
    hence "gtt_accept 𝒢 (ss ! i) (ts ! i)"
          "∃u⇩i. u⇩i ∈ ta_res' (fst 𝒢) (ss ! i) ∧ u⇩i ∈ ta_res' (snd 𝒢) (ts ! i)"
      using asm ctxt(1,2) by blast+
    hence "∃us. (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i)"
      using asm by (metis nth_list_update_eq)
  }
  hence inner: "∀i < length ss.
           ∃us. (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i)"
    by auto
  have "∃us. length us = length ss ∧ (∀i < length ss.
            (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i))"
    using construct_exI[OF inner] by auto
  then obtain us where "length us = length ss ∧ (∀i < length ss.
            (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i))"
    by blast
  hence "Fun f us ∈ ta_res' (fst 𝒢) (Fun f ss) ∧
         Fun f us ∈ ta_res' (snd 𝒢) (Fun f ts)" using ctxt(1) by fastforce
  thus ?case by blast
qed

lemma ta_res_stable:
  assumes "q ∈ ta_res 𝒜 t" "ta_rules 𝒜 ⊆ ta_rules 𝒜'" "ta_eps 𝒜 ⊆ ta_eps 𝒜'"
  shows "q ∈ ta_res 𝒜' t"
  by (metis assms subsetD[OF ta_res_mono'])

lemma gtt_accept_mono:
  assumes "ta_eps (fst 𝒢) ⊆ ta_eps (fst 𝒢')" "ta_rules (fst 𝒢) ⊆ ta_rules (fst 𝒢')"
    "ta_eps (snd 𝒢) ⊆ ta_eps (snd 𝒢')" "ta_rules (snd 𝒢) ⊆ ta_rules (snd 𝒢')"
    "gtt_accept 𝒢 s t"
  shows "gtt_accept 𝒢' s t"
  using assms(5) unfolding gtt_accept_equiv
  by (elim gtt_accept'.cases) (metis gtt_accept'.intros assms(1-4) subsetD[OF ta_res_mono'])

lemma gtt_accept_stable:
  assumes "gtt_accept (𝒜, ℬ) l r"
    "ta_rules 𝒜 ⊆ ta_rules 𝒜'" "ta_rules ℬ ⊆ ta_rules ℬ'"
    "ta_eps 𝒜 ⊆ ta_eps 𝒜'" "ta_eps ℬ ⊆ ta_eps ℬ'"
  shows "gtt_accept (𝒜', ℬ') l r"
  using gtt_accept_mono[of "(𝒜, ℬ)" "(𝒜', ℬ')" l r] assms by simp

lemma ta_res_ta_final_ignored:
  assumes "q ∈ ta_res (ta.make Q⇩f Δ ℰ) t"
  shows "q ∈ ta_res (ta.make Q⇩f' Δ ℰ) t"
  using assms(1) unfolding ta.make_def
proof (induction "⦇ta_final = Q⇩f, ta_rules = Δ, ta_eps = ℰ⦈" t arbitrary: q rule: ta_res.induct)
  case (2 f ts)
  obtain q' qs where accepted_Δ: "f qs → q' ∈ Δ" "(q', q) ∈ ℰ⇧*" "length qs = length ts"
      "∀i<length ts. qs ! i ∈ ta_res ⦇ta_final = Q⇩f, ta_rules = Δ, ta_eps = ℰ⦈ (ts ! i)"
    using 2(2) by auto
  moreover have "∀i<length ts. qs ! i ∈ ta_res ⦇ta_final = Q⇩f', ta_rules = Δ, ta_eps = ℰ⦈ (ts ! i)"
    using 2(1) accepted_Δ(4) by auto
  ultimately show ?case using accepted_Δ(1-3) by auto
qed simp

abbreviation 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 gtt_lang_fmap_states_gtt:
  assumes "inj_on f (gtt_states 𝒢)"
  shows "gtt_lang (fmap_states_gtt f 𝒢) = map_both adapt_vars ` gtt_lang 𝒢"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x)
  obtain C ss ts where x: "x = (fill_holes C ss, fill_holes C ts)"
       "length ss = num_holes C" "length ts = num_holes C"
       "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fmap_states_ta f (fst 𝒢)) (ss ! i) ∧
          q ∈ ta_res (fmap_states_ta f (snd 𝒢)) (ts ! i)"
       "ground (fill_holes C ss)" "ground (fill_holes C ts)"
    using lr by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  { fix i assume i: "i < num_holes C"
    obtain q where q: "q ∈ ta_res (fmap_states_ta f (fst 𝒢)) (ss ! i)"
      "q ∈ ta_res (fmap_states_ta f (snd 𝒢)) (ts ! i)" using x(4)[OF i] by blast
    have g: "ground (ss ! i)" "ground (ts ! i)" using x(2,3,5,6) by (auto simp: ground_fill_holes i)
    then have "∃p. p ∈ ta_res (fst 𝒢) (adapt_vars (ss ! i)) ∧ p ∈ ta_res (snd 𝒢) (adapt_vars (ts ! i))"
      using assms[unfolded inj_on_Un] assms x(2,3,5,6) q
         ta_res_fmap_states_inv[of f "fst 𝒢" "ss ! i" q] ta_res_fmap_states_inv[of f "snd 𝒢" "ts ! i" q]
        inj_onD[OF assms _ UnI1[OF subsetD[OF ta_res_states]] UnI2[OF subsetD[OF ta_res_states]],
          of _ _ "adapt_vars (ss ! i)" "adapt_vars (ts ! i)"]
      by (auto) }
  then have "gtt_accept' 𝒢 (adapt_vars (fill_holes C ss)) (adapt_vars (fill_holes C ts))"
    using x(2,3) by (auto simp: adapt_vars_def map_vars_term_fill_holes)
  then show ?case using x(1,5,6) by (auto 0 0 simp: image_def prod.map_comp gtt_accept_equiv
      intro!: bexI[of _ "map_prod adapt_vars adapt_vars x"])
next
  case (rl x)
  obtain C ss ts where x: "x = (adapt_vars (fill_holes C ss), adapt_vars (fill_holes C ts))"
    "length ss = num_holes C" "length ts = num_holes C"
    "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧ q ∈ ta_res (snd 𝒢) (ts ! i)"
    "ground (fill_holes C ss)" "ground (fill_holes C ts)"
    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 ∈ ta_res (fst 𝒢) (ss ! i) ∧ qs i ∈ ta_res (snd 𝒢) (ts ! i)"
    if "i < num_holes C" for i by metis
  have "gtt_accept' (fmap_states_gtt f 𝒢) (fst x) (snd x)"
    using gtt_accept'.intros[of "map (map_vars_term f) ss" "map (map_vars_term f) ts"
      "map_vars_mctxt f C" "fmap_states_gtt f 𝒢"] x(2,3,5,6)
      ta_res_fmap_states_ta[OF conjunct1[OF qs], where h = f]
      ta_res_fmap_states_ta[OF conjunct2[OF qs], where h = f]
    by (auto simp: map_vars_term_fill_holes x(1) adapt_vars_def ground_fill_holes
      ground_map_vars_term_simp[of _ _ f] ground_map_vars_mctxt_simp[of _ f]
      cong: map_cong)
  then show ?case using x(1,2,3,5,6) by (auto simp: gtt_accept_equiv)
qed

definition gtt_only_reach where
  "gtt_only_reach = map_both ta_only_reach"

lemma gtt_only_reach_lang:
  "gtt_lang (gtt_only_reach G) = gtt_lang G"
proof (intro equalityI subrelI, goal_cases LR RL)
  case (LR s t)
  then obtain C ss ts qs where
    s: "s = fill_holes C ss" "length ss = num_holes C" "ground s" and
    t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
    q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst (gtt_only_reach G)) (ss ! i) ∧
                        q ∈ ta_res (snd (gtt_only_reach G)) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)" if "i < num_holes C" for i
    using q[of i] subsetD[OF ta_res_mono[OF ta_restrict_subset]] that by (fastforce simp: gtt_only_reach_def)
  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_holes C ss" "length ss = num_holes C" "ground s" and
    t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
    q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃q. q ∈ ta_res (fst (gtt_only_reach G)) (ss ! i) ∧ q ∈ ta_res (snd (gtt_only_reach G)) (ts ! i)"
    if "i < num_holes C" for i
    using q[of i] ta_res_only_reach[OF refl, of "ss ! i" "fst G", THEN conjunct2]
      ta_res_only_reach[OF refl, of "ts ! i" "snd G", THEN conjunct2] that s t
    by (simp add: ground_fill_holes all_set_conv_all_nth)
      (auto simp: ground_vars_term_empty set_conv_nth gtt_only_reach_def)
  then show ?case using s t by (auto simp: gtt_accept_equiv)
qed

lemma gtt_only_reach_syms:
  "gtt_syms (gtt_only_reach G) ⊆ gtt_syms G"
  by (auto simp: gtt_only_reach_def ta_restrict_def)
    (metis (mono_tags, lifting) image_iff mem_Collect_eq select_convs(2) ta_syms_def)+

definition gtt_only_prod where
  "gtt_only_prod G =
    (let iface = ta_states ((fst G)⦇ta_final := {}⦈) ∩ ta_states ((snd G)⦇ta_final := {}⦈) in
    map_both ta_only_prod ((fst G)⦇ta_final := iface⦈, (snd G)⦇ta_final := iface⦈))"

lemma gtt_only_prod_lang:
  "gtt_lang (gtt_only_prod G) = gtt_lang G"
proof (intro equalityI subrelI, goal_cases LR RL)
  case (LR s t)
  then obtain C ss ts qs where
    s: "s = fill_holes C ss" "length ss = num_holes C" "ground s" and
    t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
    q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i) ∧
                        q ∈ ta_res (snd (gtt_only_prod G)) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  have "∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)" if "i < num_holes C" for i
    using q[of i] subsetD[OF ta_res_mono'[of "fst (gtt_only_prod G)" "fst G"]]
      subsetD[OF ta_res_mono'[of "snd (gtt_only_prod G)" "snd G"]] that
      ta_restrict_subset[of "_⦇ ta_final := _ ⦈"]
    by (fastforce simp: gtt_only_prod_def Let_def ta_subset_def)
  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_holes C ss" "length ss = num_holes C" "ground s" and
    t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
    q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)"
    by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
  let ?iface = "ta_states (fst G⦇ta_final := {}⦈) ∩ ta_states (snd G⦇ta_final := {}⦈)"
  { fix i assume i: "i < num_holes C"
    guess q using q[OF i] by (elim exE conjE) note q = this
    have g: "ground (ss ! i)" "ground (ts ! i)" using s t i by (auto simp: ground_fill_holes)
    have "q ∈ ?iface" using q g
      subset_trans[OF ta_res_mono'[of A "A⦇ta_final := {}⦈" for A] ta_res_states[of _ "_⦇ta_final := {} ⦈"], THEN subsetD]
      by fastforce
    have "q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i)" "q ∈ ta_res (snd (gtt_only_prod G)) (ts ! i)"
      using q g by (auto simp: gtt_only_prod_def Let_def intro!: ta_productive_final
        ta_res_only_prod subsetD[OF ta_res_mono'[of A "A⦇ta_final := ?iface⦈" for A]]
        subset_trans[OF ta_res_mono'[of A "A⦇ta_final := {}⦈" for A] ta_res_states[of _ "_⦇ta_final := {} ⦈"], THEN subsetD])
    then have "∃q. q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i) ∧ q ∈ ta_res (snd (gtt_only_prod G)) (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 G) ⊆ gtt_syms G"
  by (auto simp: gtt_only_prod_def ta_restrict_def)
    (smt fst_conv snd_conv image_iff mem_Collect_eq select_convs(2) ta_syms_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 subset_trans[OF gtt_only_prod_syms gtt_only_reach_syms] by simp

end