Theory Tree_Automata

section ‹Tree automaton›

theory Tree_Automata
  imports FSet_Utils
    "HOL-Library.Product_Lexorder"
    "HOL-Library.Option_ord"
begin

subsection ‹Tree automaton definition and functionality›

datatype ('q, 'f) ta_rule = TA_rule (r_root: 'f) (r_lhs_states: "'q list") (r_rhs: 'q) (‹_ _ → _› [51, 51, 51] 52)
datatype ('q, 'f) ta = TA (rules: "('q, 'f) ta_rule fset") (eps: "('q × 'q) fset")

text ‹In many application we are interested in specific subset of all terms. If these
  can be captured by a tree automaton (identified by a state) then we say the set is regular.
  This gives the motivation for the following definition›
datatype ('q, 'f) reg = Reg (fin: "'q fset") (ta: "('q, 'f) ta")


text ‹The state set induced by a tree automaton is implicit in our representation.
  We compute it based on the rules and epsilon transitions of a given tree automaton›

abbreviation rule_arg_states where "rule_arg_states Δ ≡ |⋃| ((fset_of_list ∘ r_lhs_states) |`| Δ)"
abbreviation rule_target_states where "rule_target_states Δ ≡ (r_rhs |`| Δ)"
definition rule_states where "rule_states Δ ≡ rule_arg_states Δ |∪| rule_target_states Δ"

definition eps_states where "eps_states Δ⇩ε ≡ (fst |`| Δ⇩ε) |∪| (snd |`| Δ⇩ε)"
definition "𝒬 𝒜 = rule_states (rules 𝒜) |∪| eps_states (eps 𝒜)"
abbreviation "𝒬⇩r 𝒜 ≡ 𝒬 (ta 𝒜)"

definition ta_rhs_states :: "('q, 'f) ta ⇒ 'q fset" where
  "ta_rhs_states 𝒜 ≡ {| q | p q. (p |∈| rule_target_states (rules 𝒜)) ∧ (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)|}"

definition "ta_sig 𝒜 = (λ r. (r_root r, length (r_lhs_states r))) |`| (rules 𝒜)"

subsubsection ‹Rechability of a term induced by a tree automaton›
(* The reachable states of some term. *)
fun ta_der :: "('q, 'f) ta ⇒ ('f, 'q) term ⇒ 'q fset" where
  "ta_der 𝒜 (Var q) = {|q' | q'. q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+| |}"
| "ta_der 𝒜 (Fun f ts) = {|q' | q' q qs.
    TA_rule f qs q |∈| (rules 𝒜) ∧ (q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+|) ∧ length qs = length ts ∧ 
    (∀ i < length ts. qs ! i |∈| ta_der 𝒜 (ts ! i))|}"

(* The reachable mixed terms of some term. *)
fun ta_der' :: "('q,'f) ta ⇒ ('f,'q) term ⇒ ('f,'q) term fset" where
  "ta_der' 𝒜 (Var p) = {|Var q | q. p = q ∨  (p, q) |∈| (eps 𝒜)|⇧+| |}"
| "ta_der' 𝒜 (Fun f ts) = {|Var q | q. q |∈| ta_der 𝒜 (Fun f ts)|} |∪|
    {|Fun f ss | ss. length ss = length ts ∧
      (∀i < length ts. ss ! i |∈| ta_der' 𝒜 (ts ! i))|}"

text ‹Sometimes it is useful to analyse a concrete computation done by a tree automaton.
  To do this we introduce the notion of run which keeps track which states are computed in each
  subterm to reach a certain state.›

abbreviation "ex_rule_state ≡ fst ∘ groot_sym"
abbreviation "ex_comp_state ≡ snd ∘ groot_sym"

inductive run for 𝒜 where
  step: "length qs = length ts ⟹ (∀ i < length ts. run 𝒜 (qs ! i) (ts ! i)) ⟹
    TA_rule f (map ex_comp_state qs) q |∈| (rules 𝒜) ⟹ (q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+|) ⟹ 
    run 𝒜 (GFun (q, q') qs) (GFun f ts)"


subsubsection ‹Language acceptance›

definition ta_lang :: "'q fset ⇒ ('q, 'f) ta ⇒ ('f, 'v) terms" where
  [code del]: "ta_lang Q 𝒜 = {adapt_vars t | t. ground t ∧ Q |∩| ta_der 𝒜 t ≠ {||}}"

definition gta_der where
  "gta_der 𝒜 t = ta_der 𝒜 (term_of_gterm t)"

definition gta_lang where
  "gta_lang Q 𝒜 = {t. Q |∩| gta_der 𝒜 t ≠ {||}}"

definition ℒ where
  "ℒ 𝒜 = gta_lang (fin 𝒜) (ta 𝒜)"

definition reg_Restr_Q⇩f where
  "reg_Restr_Q⇩f R = Reg (fin R |∩| 𝒬⇩r R) (ta R)"

subsubsection ‹Trimming›

definition ta_restrict where
  "ta_restrict 𝒜 Q = TA {| TA_rule f qs q| f qs q. TA_rule f qs q |∈| rules 𝒜 ∧ fset_of_list qs |⊆| Q ∧ q |∈| Q |} (fRestr (eps 𝒜) Q)"

definition ta_reachable :: "('q, 'f) ta ⇒ 'q fset" where
  "ta_reachable 𝒜 = {|q| q. ∃ t. ground t ∧ q |∈| ta_der 𝒜 t |}"

definition ta_productive :: "'q fset ⇒ ('q,'f) ta ⇒ 'q fset" where
  "ta_productive P 𝒜 ≡ {|q| q q' C. q' |∈| ta_der 𝒜 (C⟨Var q⟩) ∧ q' |∈| P |}"

text ‹An automaton is trim if all its states are reachable and productive.›
definition ta_is_trim :: "'q fset ⇒ ('q, 'f) ta ⇒ bool" where
  "ta_is_trim P 𝒜 ≡ ∀ q. q |∈| 𝒬 𝒜 ⟶ q |∈| ta_reachable 𝒜 ∧ q |∈| ta_productive P 𝒜"

definition reg_is_trim :: "('q, 'f) reg ⇒ bool" where
  "reg_is_trim R ≡ ta_is_trim (fin R) (ta R)"

text ‹We obtain a trim automaton by restriction it to reachable and productive states.›
abbreviation ta_only_reach :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
  "ta_only_reach 𝒜 ≡ ta_restrict 𝒜 (ta_reachable 𝒜)"

abbreviation ta_only_prod :: "'q fset ⇒ ('q,'f) ta ⇒ ('q,'f) ta" where
  "ta_only_prod P 𝒜 ≡ ta_restrict 𝒜 (ta_productive P 𝒜)"

definition reg_reach where
  "reg_reach R = Reg (fin R) (ta_only_reach (ta R))"

definition reg_prod where
  "reg_prod R = Reg (fin R) (ta_only_prod (fin R) (ta R))"

definition trim_ta :: "'q fset ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta" where
  "trim_ta P 𝒜 = ta_only_prod P (ta_only_reach 𝒜)"

definition trim_reg where
  "trim_reg R = Reg (fin R) (trim_ta (fin R) (ta R))"

subsubsection ‹Mapping over tree automata›

definition fmap_states_ta ::  "('a ⇒ 'b) ⇒ ('a, 'f) ta ⇒ ('b, 'f) ta" where
  "fmap_states_ta f 𝒜 = TA (map_ta_rule f id |`| rules 𝒜) (map_both f |`| eps 𝒜)"

definition fmap_funs_ta :: "('f ⇒ 'g) ⇒ ('a, 'f) ta ⇒ ('a, 'g) ta" where
  "fmap_funs_ta f 𝒜 = TA (map_ta_rule id f |`| rules 𝒜) (eps 𝒜)"

definition fmap_states_reg ::  "('a ⇒ 'b) ⇒ ('a, 'f) reg ⇒ ('b, 'f) reg" where
  "fmap_states_reg f R = Reg (f |`| fin R) (fmap_states_ta f (ta R))"

definition fmap_funs_reg :: "('f ⇒ 'g) ⇒ ('a, 'f) reg ⇒ ('a, 'g) reg" where
  "fmap_funs_reg f R = Reg (fin R) (fmap_funs_ta f (ta R))"

subsubsection ‹Product construction (language intersection)›

definition prod_ta_rules :: "('q1,'f) ta ⇒ ('q2,'f) ta ⇒ ('q1 × 'q2, 'f) ta_rule fset" where
  "prod_ta_rules 𝒜 ℬ = {| TA_rule f qs q | f qs q. TA_rule f (map fst qs) (fst q) |∈| rules 𝒜 ∧
     TA_rule f (map snd qs) (snd q) |∈| rules ℬ|}"
declare prod_ta_rules_def [simp]


definition prod_epsLp where
  "prod_epsLp 𝒜 ℬ = (λ (p, q). (fst p, fst q) |∈| eps 𝒜 ∧ snd p = snd q ∧ snd q |∈| 𝒬 ℬ)"
definition prod_epsRp where
  "prod_epsRp 𝒜 ℬ = (λ (p, q). (snd p, snd q) |∈| eps ℬ ∧ fst p = fst q ∧ fst q |∈| 𝒬 𝒜)"

definition prod_ta :: "('q1,'f) ta ⇒ ('q2,'f) ta ⇒ ('q1 × 'q2, 'f) ta" where
  "prod_ta 𝒜 ℬ = TA (prod_ta_rules 𝒜 ℬ)
    (fCollect (prod_epsLp 𝒜 ℬ) |∪| fCollect (prod_epsRp 𝒜 ℬ))"

definition reg_intersect where
  "reg_intersect R L = Reg (fin R |×| fin L) (prod_ta (ta R) (ta L))"

subsubsection ‹Union construction (language union)›

definition ta_union where
  "ta_union 𝒜 ℬ = TA (rules 𝒜 |∪| rules ℬ) (eps 𝒜 |∪| eps ℬ)"

definition reg_union where
  "reg_union R L = Reg (Inl |`| (fin R |∩| 𝒬⇩r R) |∪| Inr |`| (fin L |∩| 𝒬⇩r L))
    (ta_union (fmap_states_ta Inl (ta R)) (fmap_states_ta Inr (ta L)))"


subsubsection ‹Epsilon free and tree automaton accepting empty language›

definition eps_free_rulep where
  "eps_free_rulep 𝒜 = (λ r. ∃ f qs q q'. r = TA_rule f qs q' ∧ TA_rule f qs q |∈| rules 𝒜 ∧ (q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+|))"

definition eps_free :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
  "eps_free 𝒜 = TA (fCollect (eps_free_rulep 𝒜)) {||}"

definition is_ta_eps_free :: "('q, 'f) ta ⇒ bool" where
  "is_ta_eps_free 𝒜 ⟷ eps 𝒜 = {||}"

definition ta_empty :: "'q fset ⇒ ('q,'f) ta ⇒ bool" where
  "ta_empty Q 𝒜 ⟷ ta_reachable 𝒜 |∩| Q |⊆| {||}"

definition eps_free_reg where
  "eps_free_reg R = Reg (fin R) (eps_free (ta R))"

definition reg_empty where
  "reg_empty R = ta_empty (fin R) (ta R)"


subsubsection ‹Relabeling tree automaton states to natural numbers›

definition map_fset_to_nat :: "('a :: linorder) fset ⇒ 'a ⇒ nat" where
  "map_fset_to_nat X = (λx. the (mem_idx x (sorted_list_of_fset X)))"

definition map_fset_fset_to_nat :: "('a :: linorder) fset fset ⇒ 'a fset ⇒ nat" where
  "map_fset_fset_to_nat X = (λx. the (mem_idx (sorted_list_of_fset x) (sorted_list_of_fset (sorted_list_of_fset |`| X))))"

definition relabel_ta :: "('q :: linorder, 'f) ta ⇒ (nat, 'f) ta" where
  "relabel_ta 𝒜 = fmap_states_ta (map_fset_to_nat (𝒬 𝒜)) 𝒜"

definition relabel_Q⇩f :: "('q :: linorder) fset ⇒ ('q :: linorder, 'f) ta ⇒ nat fset" where
  "relabel_Q⇩f Q 𝒜 = map_fset_to_nat (𝒬 𝒜) |`| (Q |∩| 𝒬 𝒜)"
definition relabel_reg  :: "('q :: linorder, 'f) reg ⇒ (nat, 'f) reg" where
  "relabel_reg R = Reg (relabel_Q⇩f (fin R) (ta R)) (relabel_ta (ta R))"

― ‹The instantiation of $<$ and $\leq$ for finite sets are $\mid \subset \mid$ and $\mid \subseteq \mid$
  which don't give rise to a total order and therefore it cannot be an instance of the type class linorder.
  However taking the lexographic order of the sorted list of each finite set gives rise
  to a total order. Therefore we provide a relabeling for tree automata where the states
  are finite sets. This allows us to relabel the well known power set construction.›

definition relabel_fset_ta :: "(('q :: linorder) fset, 'f) ta ⇒ (nat, 'f) ta" where
  "relabel_fset_ta 𝒜 = fmap_states_ta (map_fset_fset_to_nat (𝒬 𝒜)) 𝒜"

definition relabel_fset_Q⇩f :: "('q :: linorder) fset fset ⇒ (('q :: linorder) fset, 'f) ta ⇒ nat fset" where
  "relabel_fset_Q⇩f Q 𝒜 = map_fset_fset_to_nat (𝒬 𝒜) |`| (Q |∩| 𝒬 𝒜)"

definition relable_fset_reg  :: "(('q :: linorder) fset, 'f) reg ⇒ (nat, 'f) reg" where
  "relable_fset_reg R = Reg (relabel_fset_Q⇩f (fin R) (ta R)) (relabel_fset_ta (ta R))"


definition "srules 𝒜 = fset (rules 𝒜)"
definition "seps 𝒜 = fset (eps 𝒜)"

lemma rules_transfer [transfer_rule]:
  "rel_fun (=) (pcr_fset (=)) srules rules" unfolding rel_fun_def
  by (auto simp add: cr_fset_def fset.pcr_cr_eq srules_def)

lemma eps_transfer [transfer_rule]:
  "rel_fun (=) (pcr_fset (=)) seps eps" unfolding rel_fun_def
  by (auto simp add: cr_fset_def fset.pcr_cr_eq seps_def)

lemma TA_equalityI:
  "rules 𝒜 = rules ℬ ⟹ eps 𝒜 = eps ℬ ⟹ 𝒜 = ℬ"
  using ta.expand by blast

lemma rule_states_code [code]:
  "rule_states Δ = |⋃| ((λ r. finsert (r_rhs r) (fset_of_list (r_lhs_states r))) |`| Δ)"
  unfolding rule_states_def
  by fastforce

lemma eps_states_code [code]:
  "eps_states Δ⇩ε = |⋃| ((λ (q,q'). {|q,q'|}) |`| Δ⇩ε)" (is "?Ls = ?Rs")
  unfolding eps_states_def
  by (force simp add: case_prod_beta')

lemma rule_states_empty [simp]:
  "rule_states {||} = {||}"
  by (auto simp: rule_states_def)

lemma eps_states_empty [simp]:
  "eps_states {||} = {||}"
  by (auto simp: eps_states_def)

lemma rule_states_union [simp]:
  "rule_states (Δ |∪| Γ) = rule_states Δ |∪| rule_states Γ"
  unfolding rule_states_def
  by fastforce

lemma rule_states_mono:
  "Δ |⊆| Γ ⟹ rule_states Δ |⊆| rule_states Γ"
  unfolding rule_states_def
  by force

lemma eps_states_union [simp]:
  "eps_states (Δ |∪| Γ) = eps_states Δ |∪| eps_states Γ"
  unfolding eps_states_def
  by auto

lemma eps_states_image [simp]:
  "eps_states (map_both f |`| Δ⇩ε) = f |`| eps_states Δ⇩ε"
  unfolding eps_states_def map_prod_def
  by (force simp: fimage_iff)

lemma eps_states_mono:
  "Δ |⊆| Γ ⟹ eps_states Δ |⊆| eps_states Γ"
  unfolding eps_states_def
  by transfer auto

lemma eps_statesI [intro]:
  "(p, q) |∈| Δ ⟹ p |∈| eps_states Δ"
  "(p, q) |∈| Δ ⟹ q |∈| eps_states Δ"
  unfolding eps_states_def
  by (auto simp add: rev_image_eqI)

lemma eps_statesE [elim]:
  assumes "p |∈| eps_states Δ"
  obtains q where "(p, q) |∈| Δ ∨ (q, p) |∈| Δ" using assms
  unfolding eps_states_def
  by (transfer, auto)+

lemma rule_statesE [elim]:
  assumes "q |∈| rule_states Δ"
  obtains f ps p where "TA_rule f ps p |∈| Δ" "q |∈| (fset_of_list ps) ∨ q = p" using assms
proof -
  assume ass: "(⋀f ps p. f ps → p |∈| Δ ⟹ q |∈| fset_of_list ps ∨ q = p ⟹ thesis)"
  from assms obtain r where "r |∈| Δ" "q |∈| fset_of_list (r_lhs_states r) ∨ q = r_rhs r"
    by (auto simp: rule_states_def)
  then show thesis using ass
    by (cases r) auto
qed

lemma rule_statesI [intro]:
  assumes "r |∈| Δ" "q |∈| finsert (r_rhs r) (fset_of_list (r_lhs_states r))"
  shows "q |∈| rule_states Δ" using assms
  by (auto simp: rule_states_def)


text ‹Destruction rule for states›

lemma rule_statesD:
  "r |∈| (rules 𝒜) ⟹ r_rhs r |∈| 𝒬 𝒜" "f qs → q |∈| (rules 𝒜) ⟹ q |∈| 𝒬 𝒜"
  "r |∈| (rules 𝒜) ⟹ p |∈| fset_of_list (r_lhs_states r) ⟹ p |∈| 𝒬 𝒜"
  "f qs → q |∈| (rules 𝒜) ⟹ p |∈| fset_of_list qs ⟹ p |∈| 𝒬 𝒜"
  by (force simp: 𝒬_def rule_states_def fimage_iff)+

lemma eps_states [simp]: "(eps 𝒜) |⊆| 𝒬 𝒜 |×| 𝒬 𝒜"
  unfolding 𝒬_def eps_states_def rule_states_def
  by (auto simp add: rev_image_eqI)

lemma eps_statesD: "(p, q) |∈| (eps 𝒜) ⟹ p |∈| 𝒬 𝒜 ∧ q |∈| 𝒬 𝒜"
  using eps_states by (auto simp add: 𝒬_def)

lemma eps_trancl_statesD:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ p |∈| 𝒬 𝒜 ∧ q |∈| 𝒬 𝒜"
  by (induct rule: ftrancl_induct) (auto dest: eps_statesD)

lemmas eps_dest_all = eps_statesD eps_trancl_statesD

text ‹Mapping over function symbols/states›

lemma finite_Collect_ta_rule:
  "finite {TA_rule f qs q | f qs q. TA_rule f qs q |∈| rules 𝒜}" (is "finite ?S")
proof -
  have "{f qs → q |f qs q. f qs → q |∈| rules 𝒜} ⊆ fset (rules 𝒜)"
    by auto
  from finite_subset[OF this] show ?thesis by simp
qed

lemma map_ta_rule_finite:
  "finite Δ ⟹ finite {TA_rule (g h) (map f qs) (f q) | h qs q. TA_rule h qs q ∈ Δ}"
proof (induct rule: finite.induct)
  case (insertI A a)
  have union: "{TA_rule (g h) (map f qs) (f q) |h qs q. TA_rule h qs q ∈ insert a A} =
    {TA_rule (g h) (map f qs) (f q) | h qs q. TA_rule h qs q = a} ∪ {TA_rule (g h) (map f qs) (f q) |h qs q. TA_rule h qs q ∈ A}"
    by auto
  have "finite {g h map f qs → f q |h qs q. h qs → q = a}"
    by (cases a) auto
  from finite_UnI[OF this insertI(2)] show ?case unfolding union .
qed auto

lemmas map_ta_rule_fset_finite [simp] = map_ta_rule_finite[of "fset Δ" for Δ, simplified]
lemmas map_ta_rule_states_finite [simp] = map_ta_rule_finite[of "fset Δ" id for Δ, simplified]
lemmas map_ta_rule_funsym_finite [simp] = map_ta_rule_finite[of "fset Δ" _ id for Δ, simplified]

lemma map_ta_rule_comp:
  "map_ta_rule f g ∘ map_ta_rule f' g' = map_ta_rule (f ∘ f') (g ∘ g')"
  using ta_rule.map_comp[of f g]
  by (auto simp: comp_def)

lemma map_ta_rule_cases:
  "map_ta_rule f g r = TA_rule (g (r_root r)) (map f (r_lhs_states r)) (f (r_rhs r))"
  by (cases r) auto

lemma map_ta_rule_prod_swap_id [simp]:
  "map_ta_rule prod.swap prod.swap (map_ta_rule prod.swap prod.swap r) = r"
  by (auto simp: map_ta_rule_cases)


lemma rule_states_image [simp]:
  "rule_states (map_ta_rule f g |`| Δ) = f |`| rule_states Δ" (is "?Ls = ?Rs")
proof -
  {fix q assume "q |∈| ?Ls"
    then obtain r where "r |∈| Δ"
      "q |∈| finsert (r_rhs (map_ta_rule f g r)) (fset_of_list (r_lhs_states (map_ta_rule f g r)))"
      by (auto simp: rule_states_def)
    then have "q |∈| ?Rs" by (cases r) (force simp: fimage_iff)}
  moreover
  {fix q assume "q |∈| ?Rs"
    then obtain r p where "r |∈| Δ" "f p = q"
      "p |∈| finsert (r_rhs r) (fset_of_list (r_lhs_states r))"
      by (auto simp: rule_states_def)
    then have "q |∈| ?Ls" by (cases r) (force simp: fimage_iff)}
  ultimately show ?thesis by blast
qed

lemma 𝒬_mono:
  "(rules 𝒜) |⊆| (rules ℬ) ⟹ (eps 𝒜) |⊆| (eps ℬ) ⟹ 𝒬 𝒜 |⊆| 𝒬 ℬ"
  using rule_states_mono eps_states_mono unfolding 𝒬_def
  by blast

lemma 𝒬_subseteq_I:
  assumes "⋀ r. r |∈| rules 𝒜 ⟹ r_rhs r |∈| S"
    and "⋀ r. r |∈| rules 𝒜 ⟹ fset_of_list (r_lhs_states r) |⊆| S"
    and "⋀ e. e |∈| eps 𝒜 ⟹ fst e |∈| S ∧ snd e |∈| S"
  shows "𝒬 𝒜 |⊆| S" using assms unfolding 𝒬_def
  by (auto simp: rule_states_def) blast

lemma finite_states:
  "finite {q. ∃ f p ps. f ps → p |∈| rules 𝒜 ∧ (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)}" (is "finite ?set")
proof -
  have "?set ⊆ fset (𝒬 𝒜)"
    by (intro subsetI, drule CollectD)
       (metis eps_trancl_statesD rule_statesD(2))
  from finite_subset[OF this] show ?thesis by auto
qed

text ‹Collecting all states reachable from target of rules›

lemma finite_ta_rhs_states [simp]:
  "finite {q. ∃p. p |∈| rule_target_states (rules 𝒜) ∧ (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)}" (is "finite ?Set")
proof -
  have "?Set ⊆ fset (𝒬 𝒜)"
    by (auto dest: rule_statesD)
       (metis eps_trancl_statesD rule_statesD(1))+
  from finite_subset[OF this] show ?thesis
    by auto
qed

text ‹Computing the signature induced by the rule set of given tree automaton›



lemma ta_sigI [intro]:
  "TA_rule f qs q |∈| (rules 𝒜) ⟹ length qs = n ⟹ (f, n) |∈| ta_sig 𝒜" unfolding ta_sig_def
  using mk_disjoint_finsert by fastforce

lemma ta_sig_mono:
  "(rules 𝒜) |⊆| (rules ℬ) ⟹ ta_sig 𝒜 |⊆| ta_sig ℬ"
  by (auto simp: ta_sig_def)

lemma finite_eps:
  "finite {q. ∃ f ps p. f ps → p |∈| rules 𝒜 ∧ (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)}" (is "finite ?S")
  by (intro finite_subset[OF _ finite_ta_rhs_states[of 𝒜]]) (auto intro!: bexI)

lemma collect_snd_trancl_fset:
  "{p. (q, p) |∈| (eps 𝒜)|⇧+|} = fset (snd |`| (ffilter (λ x. fst x = q) ((eps 𝒜)|⇧+|)))"
  by (auto simp: image_iff) force

lemma ta_der_Var:
  "q |∈| ta_der 𝒜 (Var x) ⟷ x = q ∨ (x, q) |∈| (eps 𝒜)|⇧+|"
  by (auto simp: collect_snd_trancl_fset)

lemma ta_der_Fun:
  "q |∈| ta_der 𝒜 (Fun f ts) ⟷ (∃ ps p. TA_rule f ps p |∈| (rules 𝒜) ∧
      (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|) ∧ length ps = length ts ∧ 
      (∀ i < length ts. ps ! i |∈| ta_der 𝒜 (ts ! i)))" (is "?Ls ⟷ ?Rs")
  unfolding ta_der.simps
  by (intro iffI fCollect_memberI finite_Collect_less_eq[OF _ finite_eps[of 𝒜]]) auto

declare ta_der.simps[simp del]
declare ta_der.simps[code del]
lemmas ta_der_simps [simp] = ta_der_Var ta_der_Fun

lemma ta_der'_Var:
  "Var q |∈| ta_der' 𝒜 (Var x) ⟷ x = q ∨ (x, q) |∈| (eps 𝒜)|⇧+|"
  by (auto simp: collect_snd_trancl_fset)

lemma ta_der'_Fun:
  "Var q |∈| ta_der' 𝒜 (Fun f ts) ⟷ q |∈| ta_der 𝒜 (Fun f ts)"
  unfolding ta_der'.simps
  by (intro iffI funionI1 fCollect_memberI)
     (auto simp del: ta_der_Fun ta_der_Var simp: fset_image_conv)

lemma ta_der'_Fun2:
  "Fun f ps |∈| ta_der' 𝒜 (Fun g ts) ⟷ f = g ∧ length ps = length ts ∧ (∀i<length ts. ps ! i |∈| ta_der' 𝒜 (ts ! i))"
proof -
  have f: "finite {ss. set ss ⊆ fset ( |⋃| (fset_of_list (map (ta_der' 𝒜) ts))) ∧ length ss = length ts}"
    by (intro finite_lists_length_eq) auto
  have "finite {ss. length ss = length ts ∧ (∀i<length ts. ss ! i |∈| ta_der' 𝒜 (ts ! i))}"
    by (intro finite_subset[OF _ f])
       (force simp: in_fset_conv_nth simp flip: fset_of_list_elem)
  then show ?thesis unfolding ta_der'.simps
    by (intro iffI funionI2 fCollect_memberI)
       (auto simp del: ta_der_Fun ta_der_Var)
qed

declare ta_der'.simps[simp del]
declare ta_der'.simps[code del]
lemmas ta_der'_simps [simp] = ta_der'_Var ta_der'_Fun ta_der'_Fun2

text ‹Induction schemes for the most used cases›

lemma ta_der_induct[consumes 1, case_names Var Fun]:
  assumes reach: "q |∈| ta_der 𝒜 t"
  and VarI: "⋀ q v. v = q ∨ (v, q) |∈| (eps 𝒜)|⇧+| ⟹ P (Var v) q"
  and FunI: "⋀f ts ps p q. f ps → p |∈| rules 𝒜 ⟹ length ts = length ps ⟹ p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+| ⟹
    (⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (ts ! i)) ⟹
    (⋀i. i < length ts ⟹ P (ts ! i) (ps ! i)) ⟹ P (Fun f ts) q"
  shows "P t q" using assms(1)
  by (induct t arbitrary: q) (auto simp: VarI FunI)

lemma ta_der_gterm_induct[consumes 1, case_names GFun]:
  assumes reach: "q |∈| ta_der 𝒜 (term_of_gterm t)"
  and Fun: "⋀f ts ps p q. TA_rule f ps p |∈| rules 𝒜 ⟹ length ts = length ps ⟹ p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+| ⟹
    (⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (term_of_gterm (ts ! i))) ⟹
    (⋀i. i < length ts ⟹ P (ts ! i) (ps ! i)) ⟹ P (GFun f ts) q"
  shows "P t q" using assms(1)
  by (induct t arbitrary: q) (auto simp: Fun)

lemma ta_der_rule_empty:
  assumes "q |∈| ta_der (TA {||} Δ⇩ε) t"
  obtains p where "t = Var p" "p = q ∨ (p, q) |∈| Δ⇩ε|⇧+|"
  using assms by (cases t) auto

lemma ta_der_eps:
  assumes "(p, q) |∈| (eps 𝒜)" and "p |∈| ta_der 𝒜 t"
  shows "q |∈| ta_der 𝒜 t" using assms
  by (cases t) (auto intro: ftrancl_into_trancl)

lemma ta_der_trancl_eps:
  assumes "(p, q) |∈| (eps 𝒜)|⇧+|" and "p |∈| ta_der 𝒜 t"
  shows "q |∈| ta_der 𝒜 t" using assms
  by (induct rule: ftrancl_induct) (auto intro: ftrancl_into_trancl ta_der_eps)

lemma ta_der_mono:
  "(rules 𝒜) |⊆| (rules ℬ) ⟹ (eps 𝒜) |⊆| (eps ℬ) ⟹ ta_der 𝒜 t |⊆| ta_der ℬ t"
proof (induct t)
  case (Var x) then show ?case
    by (auto dest: ftrancl_mono[of _ "eps 𝒜" "eps ℬ"])
next
  case (Fun f ts)
  show ?case using Fun(1)[OF nth_mem Fun(2, 3)]
    by (auto dest!: fsubsetD[OF Fun(2)] ftrancl_mono[OF _ Fun(3)]) blast+
qed

lemma ta_der_el_mono:
  "(rules 𝒜) |⊆| (rules ℬ) ⟹ (eps 𝒜) |⊆| (eps ℬ) ⟹ q |∈| ta_der 𝒜 t ⟹ q |∈| ta_der ℬ t"
  using ta_der_mono by blast

lemma ta_der'_ta_der:
  assumes "t |∈| ta_der' 𝒜 s" "p |∈| ta_der 𝒜 t"
  shows "p |∈| ta_der 𝒜 s" using assms
proof (induction arbitrary: p t rule: ta_der'.induct)
  case (2 𝒜 f ts) show ?case using 2(2-)
  proof (induction t)
    case (Var x) then show ?case
      by auto (meson ftrancl_trans)
  next
    case (Fun g ss)
    have ss_props: "g = f" "length ss = length ts" "∀i < length ts. ss ! i |∈| ta_der' 𝒜 (ts ! i)"
      using Fun(2) by auto
    then show ?thesis using Fun(1)[OF nth_mem] Fun(2-)
      by (auto simp: ss_props)
         (metis (no_types, lifting) "2.IH" ss_props(3))+  
  qed
qed (auto dest: ftrancl_trans simp: ta_der'.simps)

lemma ta_der'_empty:
  assumes "t |∈| ta_der' (TA {||} {||}) s"
  shows "t = s" using assms
  by (induct s arbitrary: t) (auto simp add: ta_der'.simps nth_equalityI)

lemma ta_der'_to_ta_der:
  "Var q |∈| ta_der' 𝒜 s ⟹ q |∈| ta_der 𝒜 s"
  using ta_der'_ta_der by fastforce

lemma ta_der_to_ta_der':
  "q |∈| ta_der 𝒜 s ⟷ Var q |∈| ta_der' 𝒜 s "
  by (induct s arbitrary: q) auto

lemma ta_der'_poss:
  assumes "t |∈| ta_der' 𝒜 s"
  shows "poss t ⊆ poss s" using assms
proof (induct s arbitrary: t)
  case (Fun f ts)
  show ?case using Fun(2) Fun(1)[OF nth_mem, of i "args t ! i" for i]
    by (cases t) auto
qed (auto simp: ta_der'.simps)

lemma ta_der'_refl[simp]: "t |∈| ta_der' 𝒜 t"
  by (induction t) fastforce+

lemma ta_der'_eps:
  assumes "Var p |∈| ta_der' 𝒜 s" and "(p, q) |∈| (eps 𝒜)|⇧+|"
  shows "Var q |∈| ta_der' 𝒜 s" using assms
  by (cases s, auto dest: ftrancl_trans) (meson ftrancl_trans)

lemma ta_der'_trans:
  assumes "t |∈| ta_der' 𝒜 s" and "u |∈| ta_der' 𝒜 t"
  shows "u |∈| ta_der' 𝒜 s" using assms
proof (induct t arbitrary: u s)
  case (Fun f ts) note IS = Fun(2-) note IH = Fun(1)[OF nth_mem, of i "args s ! i" for i]
  show ?case
  proof (cases s)
    case (Var x1)
    then show ?thesis using IS by (auto simp: ta_der'.simps)
  next
    case [simp]: (Fun g ss)
    show ?thesis using IS IH
      by (cases u, auto) (metis ta_der_to_ta_der')+
  qed
qed (auto simp: ta_der'.simps ta_der'_eps)

text ‹Connecting contexts to derivation definition›

lemma ta_der_ctxt:
  assumes p: "p |∈| ta_der 𝒜 t" "q |∈| ta_der 𝒜 C⟨Var p⟩"
  shows "q |∈| ta_der 𝒜 C⟨t⟩" using assms(2)
proof (induct C arbitrary: q)
  case Hole then show ?case using assms
    by (auto simp: ta_der_trancl_eps)
next
  case (More f ss C ts)
  from More(2) obtain qs r where
    rule: "f qs → r |∈| rules 𝒜" "length qs = Suc (length ss + length ts)" and
    reach: "∀ i < Suc (length ss + length ts). qs ! i |∈| ta_der 𝒜 ((ss @ C⟨Var p⟩ # ts) ! i)" "r = q ∨ (r, q) |∈| (eps 𝒜)|⇧+|"
    by auto
  have "i < Suc (length ss + length ts) ⟹ qs ! i |∈| ta_der 𝒜 ((ss @ C⟨t⟩ # ts) ! i)" for i
    using More(1)[of "qs ! length ss"] assms rule(2) reach(1)
    unfolding nth_append_Cons by presburger
  then show ?case using rule reach(2) by auto
qed

lemma ta_der_eps_ctxt:
  assumes "p |∈| ta_der A C⟨Var q'⟩" and "(q, q') |∈| (eps A)|⇧+|"
  shows "p |∈| ta_der A C⟨Var q⟩"
  using assms by (meson ta_der_Var ta_der_ctxt) 

lemma rule_reachable_ctxt_exist:
  assumes rule: "f qs → q |∈| rules 𝒜" and "i < length qs"
  shows "∃ C. q |∈| ta_der 𝒜 (C ⟨Var (qs ! i)⟩)" using assms
  by (intro exI[of _ "More f (map Var (take i qs)) □ (map Var (drop (Suc i) qs))"])
     (auto simp: min_def nth_append_Cons intro!: exI[of _ q] exI[of _ qs])

lemma ta_der_ctxt_decompose:
  assumes "q |∈| ta_der 𝒜 C⟨t⟩"
  shows "∃ p . p |∈| ta_der 𝒜 t ∧ q |∈| ta_der 𝒜 C⟨Var p⟩" using assms
proof (induct C arbitrary: q)
  case (More f ss C ts)
  from More(2) obtain qs r where
    rule: "f qs → r |∈| rules 𝒜" "length qs = Suc (length ss + length ts)" and
    reach: "∀ i < Suc (length ss + length ts). qs ! i |∈| ta_der 𝒜 ((ss @ C⟨t⟩ # ts) ! i)"
       "r = q ∨ (r, q) |∈| (eps 𝒜)|⇧+|"
    by auto
  obtain p where p: "p |∈| ta_der 𝒜 t" "qs ! length ss |∈| ta_der 𝒜 C⟨Var p⟩"
    using More(1)[of "qs ! length ss"] reach(1) rule(2)
    by (metis less_add_Suc1 nth_append_length)
  have "i < Suc (length ss + length ts) ⟹ qs ! i |∈| ta_der 𝒜 ((ss @ C⟨Var p⟩ # ts) ! i)" for i
    using reach rule(2) p by (auto simp: p(2) nth_append_Cons)
  then have "q |∈| ta_der 𝒜 (More f ss C ts)⟨Var p⟩" using rule reach
    by auto
  then show ?case using p(1) by (intro exI[of _ p]) blast
qed auto

― ‹Relation between reachable states and states of a tree automaton›

lemma ta_der_states:
  "ta_der 𝒜 t |⊆| 𝒬 𝒜 |∪| fvars_term t"
proof (induct t)
  case (Var x) then show ?case
    by (auto simp: eq_onp_same_args) 
       (metis eps_trancl_statesD)
  case (Fun f ts) then show ?case
    by (auto simp: rule_statesD(2) eps_trancl_statesD)
qed

lemma ground_ta_der_states:
  "ground t ⟹ ta_der 𝒜 t |⊆| 𝒬 𝒜"
  using ta_der_states[of 𝒜 t] by auto

lemmas ground_ta_der_statesD = fsubsetD[OF ground_ta_der_states]

lemma gterm_ta_der_states [simp]:
  "q |∈| ta_der 𝒜 (term_of_gterm t) ⟹ q |∈| 𝒬 𝒜"
  by (intro ground_ta_der_states[THEN fsubsetD, of "term_of_gterm t"]) simp

lemma ta_der_states':
  "q |∈| ta_der 𝒜 t ⟹ q |∈| 𝒬 𝒜 ⟹ fvars_term t |⊆| 𝒬 𝒜"
proof (induct rule: ta_der_induct)
  case (Fun f ts ps p r)
  then have "i < length ts ⟹ fvars_term (ts ! i) |⊆| 𝒬 𝒜" for i
    by (auto simp: in_fset_conv_nth dest!: rule_statesD(3))
  then show ?case by (force simp: in_fset_conv_nth)
qed (auto simp: eps_trancl_statesD)

lemma ta_der_not_stateD:
  "q |∈| ta_der 𝒜 t ⟹ q |∉| 𝒬 𝒜 ⟹ t = Var q"
  using fsubsetD[OF ta_der_states, of q 𝒜 t]
  by (cases t) (auto dest: rule_statesD eps_trancl_statesD)

lemma ta_der_is_fun_stateD:
  "is_Fun t ⟹ q |∈| ta_der 𝒜 t ⟹ q |∈| 𝒬 𝒜"
  using ta_der_not_stateD[of q 𝒜 t]
  by (cases t) auto

lemma ta_der_is_fun_fvars_stateD:
  "is_Fun t ⟹ q |∈| ta_der 𝒜 t ⟹ fvars_term t |⊆| 𝒬 𝒜"
  using ta_der_is_fun_stateD[of t q 𝒜]
  using ta_der_states'[of q 𝒜 t]
  by (cases t) auto

lemma ta_der_not_reach:
  assumes "⋀ r. r |∈| rules 𝒜 ⟹ r_rhs r ≠ q"
    and "⋀ e. e |∈| eps 𝒜 ⟹ snd e ≠ q"
  shows "q |∉| ta_der 𝒜 (term_of_gterm t)" using assms
  by (cases t) (fastforce dest!: assms(1) ftranclD2[of _ q])


lemma ta_rhs_states_subset_states: "ta_rhs_states 𝒜 |⊆| 𝒬 𝒜"
  by (auto simp: ta_rhs_states_def dest: rtranclD rule_statesD eps_trancl_statesD)

(* a resulting state is always some rhs of a rule (or epsilon transition) *)
lemma ta_rhs_states_res: assumes "is_Fun t" 
  shows "ta_der 𝒜 t |⊆| ta_rhs_states 𝒜"
proof
  fix q assume q: "q |∈| ta_der 𝒜 t"
  from ‹is_Fun t› obtain f ts where t: "t = Fun f ts" by (cases t, auto)
  from q[unfolded t] obtain q' qs where "TA_rule f qs q' |∈| rules 𝒜" 
    and q: "q' = q ∨ (q', q) |∈| (eps 𝒜)|⇧+|" by auto
  then show "q |∈| ta_rhs_states 𝒜" unfolding ta_rhs_states_def
    by (auto intro!: bexI)
qed

text ‹Reachable states of ground terms are preserved over the @{const adapt_vars} function›

lemma ta_der_adapt_vars_ground [simp]:
  "ground t ⟹ ta_der A (adapt_vars t) = ta_der A t"
  by (induct t) auto

lemma gterm_of_term_inv':
  "ground t ⟹ term_of_gterm (gterm_of_term t) = adapt_vars t"
  by (induct t) (auto 0 0 intro!: nth_equalityI)

lemma map_vars_term_term_of_gterm:
  "map_vars_term f (term_of_gterm t) = term_of_gterm t"
  by (induct t) auto

lemma adapt_vars_term_of_gterm:
  "adapt_vars (term_of_gterm t) = term_of_gterm t"
  by (induct t) auto

(* a term can be reduced to a state, only if all symbols appear in the automaton *)
lemma ta_der_term_sig:
  "q |∈| ta_der 𝒜 t ⟹ ffunas_term t |⊆| ta_sig 𝒜"
proof (induct rule: ta_der_induct)
  case (Fun f ts ps p q)
  show ?case using Fun(1 - 4) Fun(5)[THEN fsubsetD]
    by (auto simp: in_fset_conv_nth)
qed auto

lemma ta_der_gterm_sig:
  "q |∈| ta_der 𝒜 (term_of_gterm t) ⟹ ffunas_gterm t |⊆| ta_sig 𝒜"
  using ta_der_term_sig ffunas_term_of_gterm_conv
  by fastforce

text ‹@{const ta_lang} for terms with arbitrary variable type›

lemma ta_langE: assumes "t ∈ ta_lang Q 𝒜"
  obtains t' q where "ground t'" "q |∈| Q" "q |∈| ta_der 𝒜 t'" "t = adapt_vars t'"
  using assms unfolding ta_lang_def by blast

lemma ta_langI: assumes "ground t'" "q |∈| Q" "q |∈| ta_der 𝒜 t'" "t = adapt_vars t'"
  shows "t ∈ ta_lang Q 𝒜"
  using assms unfolding ta_lang_def by blast

lemma ta_lang_def2: "(ta_lang Q (𝒜 :: ('q,'f)ta) :: ('f,'v)terms) = {t. ground t ∧ Q |∩| ta_der 𝒜 (adapt_vars t) ≠ {||}}"
  by (auto elim!: ta_langE) (metis adapt_vars_adapt_vars ground_adapt_vars ta_langI)

text ‹@{const ta_lang} for @{const gterms}›

lemma ta_lang_to_gta_lang [simp]:
  "ta_lang Q 𝒜 = term_of_gterm ` gta_lang Q 𝒜" (is "?Ls = ?Rs")
proof -
  {fix t assume "t ∈ ?Ls"
    from ta_langE[OF this] obtain q t' where "ground t'" "q |∈| Q" "q |∈| ta_der 𝒜 t'" "t = adapt_vars t'"
      by blast
    then have "t ∈ ?Rs" unfolding gta_lang_def gta_der_def
      by (auto simp: image_iff gterm_of_term_inv' intro!: exI[of _ "gterm_of_term t'"])}
  moreover
  {fix t assume "t ∈ ?Rs" then have "t ∈ ?Ls"
      using ta_langI[OF ground_term_of_gterm _ _  gterm_of_term_inv'[OF ground_term_of_gterm]]
      by (force simp: gta_lang_def gta_der_def)}
  ultimately show ?thesis by blast
qed

lemma term_of_gterm_in_ta_lang_conv:
  "term_of_gterm t ∈ ta_lang Q 𝒜 ⟷ t ∈ gta_lang Q 𝒜"
  by (metis (mono_tags, lifting) image_iff ta_lang_to_gta_lang term_of_gterm_inv)

lemma gta_lang_def_sym:
  "gterm_of_term ` ta_lang Q 𝒜 = gta_lang Q 𝒜"
  (* this is nontrivial because the lhs has a more general type than the rhs of gta_lang_def *)
  unfolding gta_lang_def image_def
  by (intro Collect_cong) (simp add: gta_lang_def)

lemma gta_langI [intro]:
  assumes "q |∈| Q" and "q |∈| ta_der 𝒜 (term_of_gterm t)"
  shows "t ∈ gta_lang Q 𝒜" using assms
  by (metis adapt_vars_term_of_gterm ground_term_of_gterm ta_langI term_of_gterm_in_ta_lang_conv)

lemma gta_langE [elim]:
  assumes "t ∈ gta_lang Q 𝒜"
  obtains q where "q |∈| Q" and "q |∈| ta_der 𝒜 (term_of_gterm t)" using assms
  by (metis adapt_vars_adapt_vars adapt_vars_term_of_gterm ta_langE term_of_gterm_in_ta_lang_conv) 

lemma gta_lang_mono:
  assumes "⋀ t. ta_der 𝒜 t |⊆| ta_der 𝔅 t" and "Q⇩𝒜 |⊆| Q⇩𝔅"
  shows "gta_lang Q⇩𝒜 𝒜 ⊆ gta_lang Q⇩𝔅 𝔅"
  using assms by (auto elim!: gta_langE intro!: gta_langI)

lemma gta_lang_term_of_gterm [simp]:
  "term_of_gterm t ∈ term_of_gterm ` gta_lang Q 𝒜 ⟷ t ∈ gta_lang Q 𝒜"
  by (auto elim!: gta_langE intro!: gta_langI) (metis term_of_gterm_inv)

(* terms can be accepted, only if all their symbols appear in the automaton *)
lemma gta_lang_subset_rules_funas:
  "gta_lang Q 𝒜 ⊆ 𝒯⇩G (fset (ta_sig 𝒜))"
  using ta_der_gterm_sig[THEN fsubsetD]
  by (force simp: 𝒯⇩G_equivalent_def ffunas_gterm.rep_eq)

lemma reg_funas:
  "ℒ 𝒜 ⊆ 𝒯⇩G (fset (ta_sig (ta 𝒜)))" using gta_lang_subset_rules_funas
  by (auto simp: ℒ_def)

lemma ta_syms_lang: "t ∈ ta_lang Q 𝒜 ⟹ ffunas_term t |⊆| ta_sig 𝒜"
  using gta_lang_subset_rules_funas ffunas_gterm_gterm_of_term ta_der_gterm_sig ta_lang_def2
  by fastforce

lemma gta_lang_Rest_states_conv:
  "gta_lang Q 𝒜 = gta_lang (Q |∩| 𝒬 𝒜) 𝒜"
  by (auto elim!: gta_langE)

lemma reg_Rest_fin_states [simp]:
  "ℒ (reg_Restr_Q⇩f 𝒜) = ℒ 𝒜"
  using gta_lang_Rest_states_conv
  by (auto simp: ℒ_def reg_Restr_Q⇩f_def)

text ‹Deterministic tree automatons›

definition ta_det :: "('q,'f) ta ⇒ bool" where
  "ta_det 𝒜 ⟷ eps 𝒜 = {||} ∧ 
    (∀ f qs q q'. TA_rule f qs q |∈| rules 𝒜 ⟶ TA_rule f qs q' |∈| rules 𝒜 ⟶ q = q')"

definition "ta_subset 𝒜 ℬ ⟷ rules 𝒜 |⊆| rules ℬ ∧ eps 𝒜 |⊆| eps ℬ"

(* determinism implies unique results *)
lemma ta_detE[elim, consumes 1]: assumes det: "ta_det 𝒜"
  shows "q |∈| ta_der 𝒜 t ⟹ q' |∈| ta_der 𝒜 t ⟹ q = q'" using assms
  by (induct t arbitrary: q q') (auto simp: ta_det_def, metis nth_equalityI nth_mem)


lemma ta_subset_states: "ta_subset 𝒜 ℬ ⟹ 𝒬 𝒜 |⊆| 𝒬 ℬ"
  using 𝒬_mono by (auto simp: ta_subset_def)

lemma ta_subset_refl[simp]: "ta_subset 𝒜 𝒜" 
  unfolding ta_subset_def by auto

lemma ta_subset_trans: "ta_subset 𝒜 ℬ ⟹ ta_subset ℬ ℭ ⟹ ta_subset 𝒜 ℭ"
  unfolding ta_subset_def by auto

lemma ta_subset_det: "ta_subset 𝒜 ℬ ⟹ ta_det ℬ ⟹ ta_det 𝒜"
  unfolding ta_det_def ta_subset_def by blast

lemma ta_der_mono': "ta_subset 𝒜 ℬ ⟹ ta_der 𝒜 t |⊆| ta_der ℬ t"
  using ta_der_mono unfolding ta_subset_def by auto

lemma ta_lang_mono': "ta_subset 𝒜 ℬ ⟹ Q⇩𝒜 |⊆| Q⇩ℬ ⟹ ta_lang Q⇩𝒜 𝒜 ⊆ ta_lang Q⇩ℬ ℬ"
  using gta_lang_mono[of 𝒜 ℬ] ta_der_mono'[of 𝒜 ℬ]
  by auto blast

(* the restriction of an automaton to a given set of states *)
lemma ta_restrict_subset: "ta_subset (ta_restrict 𝒜 Q) 𝒜"
  unfolding ta_subset_def ta_restrict_def
  by auto

lemma ta_restrict_states_Q: "𝒬 (ta_restrict 𝒜 Q) |⊆| Q"
  by (auto simp: 𝒬_def ta_restrict_def rule_states_def eps_states_def dest!: fsubsetD)

lemma ta_restrict_states: "𝒬 (ta_restrict 𝒜 Q) |⊆| 𝒬 𝒜"
  using ta_subset_states[OF ta_restrict_subset] by fastforce 

lemma ta_restrict_states_eq_imp_eq [simp]:
  assumes eq: "𝒬 (ta_restrict 𝒜 Q) = 𝒬 𝒜"
  shows "ta_restrict 𝒜 Q = 𝒜" using assms
  apply (auto simp: ta_restrict_def
              intro!: ta.expand finite_subset[OF _ finite_Collect_ta_rule, of _ 𝒜])
  apply (metis (no_types, lifting) eq fsubsetD fsubsetI rule_statesD(1) rule_statesD(4) ta_restrict_states_Q ta_rule.collapse)
  apply (metis eps_statesD eq fin_mono ta_restrict_states_Q)
  by (metis eps_statesD eq fsubsetD ta_restrict_states_Q)

lemma ta_der_ta_derict_states:
  "fvars_term t |⊆| Q ⟹ q |∈| ta_der (ta_restrict 𝒜 Q) t ⟹ q |∈| Q"
  by (induct t arbitrary: q) (auto simp: ta_restrict_def elim: ftranclE)

lemma ta_derict_ruleI [intro]:
  "TA_rule f qs q |∈| rules 𝒜 ⟹ fset_of_list qs |⊆| Q ⟹ q |∈| Q ⟹ TA_rule f qs q |∈| rules (ta_restrict 𝒜 Q)"
  by (auto simp: ta_restrict_def intro!: ta.expand finite_subset[OF _ finite_Collect_ta_rule, of _ 𝒜])

text ‹Reachable and productive states: There always is a trim automaton›

lemma finite_ta_reachable [simp]:
  "finite {q. ∃t. ground t ∧ q |∈| ta_der 𝒜 t}"
proof -
  have "{q. ∃t. ground t ∧ q |∈| ta_der 𝒜 t} ⊆ fset (𝒬 𝒜)"
    using ground_ta_der_states[of _ 𝒜]
    by auto
  from finite_subset[OF this] show ?thesis by auto
qed

lemma ta_reachable_states:
  "ta_reachable 𝒜 |⊆| 𝒬 𝒜"
  unfolding ta_reachable_def using ground_ta_der_states
  by force

lemma ta_reachableE:
  assumes "q |∈| ta_reachable 𝒜"
  obtains t where "ground t" "q |∈| ta_der 𝒜 t"
  using assms[unfolded ta_reachable_def] by auto

lemma ta_reachable_gtermE [elim]:
  assumes "q |∈| ta_reachable 𝒜"
  obtains t where "q |∈| ta_der 𝒜 (term_of_gterm t)"
  using ta_reachableE[OF assms]
  by (metis ground_term_to_gtermD) 

lemma ta_reachableI [intro]:
  assumes "ground t" and "q |∈| ta_der 𝒜 t"
  shows "q |∈| ta_reachable 𝒜"
  using assms finite_ta_reachable
  by (auto simp: ta_reachable_def)

lemma ta_reachable_gtermI [intro]:
  "q |∈| ta_der 𝒜 (term_of_gterm t) ⟹ q |∈| ta_reachable 𝒜"
  by (intro ta_reachableI[of "term_of_gterm t"]) simp

lemma ta_reachableI_rule:
  assumes sub: "fset_of_list qs |⊆| ta_reachable 𝒜"
    and rule: "TA_rule f qs q |∈| rules 𝒜"
  shows "q |∈| ta_reachable 𝒜"
    "∃ ts. length qs = length ts ∧ (∀ i < length ts. ground (ts ! i)) ∧
      (∀ i < length ts. qs ! i |∈| ta_der 𝒜 (ts ! i))" (is "?G")
proof -
  {
    fix i
    assume i: "i < length qs"
    then have "qs ! i |∈| fset_of_list qs" by auto
    with sub have "qs ! i |∈| ta_reachable 𝒜" by auto
    from ta_reachableE[OF this] have "∃ t. ground t ∧ qs ! i |∈| ta_der 𝒜 t" by auto
  }
  then have "∀ i. ∃ t. i < length qs ⟶ ground t ∧ qs ! i |∈| ta_der 𝒜 t" by auto
  from choice[OF this] obtain ts where ts: "⋀ i. i < length qs ⟹ ground (ts i) ∧ qs ! i |∈| ta_der 𝒜 (ts i)" by blast
  let ?t = "Fun f (map ts [0 ..< length qs])"
  have gt: "ground ?t" using ts by auto
  have r: "q |∈| ta_der 𝒜 ?t" unfolding ta_der_Fun using rule ts
    by (intro exI[of _ qs] exI[of _ q]) simp
  with gt show "q |∈| ta_reachable 𝒜" by blast
  from gt ts show ?G by (intro exI[of _ "map ts [0..<length qs]"]) simp
qed

lemma ta_reachable_rule_gtermE:
  assumes "𝒬 𝒜 |⊆| ta_reachable 𝒜"
    and "TA_rule f qs q |∈| rules 𝒜"
  obtains t where "groot t = (f, length qs)" "q |∈| ta_der 𝒜 (term_of_gterm t)"
proof -
  assume *: "⋀t. groot t = (f, length qs) ⟹ q |∈| ta_der 𝒜 (term_of_gterm t) ⟹ thesis"
  from assms have "fset_of_list qs |⊆| ta_reachable 𝒜"
    by (auto dest: rule_statesD(3))
  from ta_reachableI_rule[OF this assms(2)] obtain ts where args: "length qs = length ts"
    "∀ i < length ts. ground (ts ! i)" "∀ i < length ts. qs ! i |∈| ta_der 𝒜 (ts ! i)"
    using assms by force
  then show ?thesis using assms(2)
    by (intro *[of "GFun f (map gterm_of_term ts)"]) auto
qed

lemma ta_reachableI_eps':
  assumes reach: "q |∈| ta_reachable 𝒜"
    and eps: "(q, q') |∈| (eps 𝒜)|⇧+|"  
  shows "q' |∈| ta_reachable 𝒜"
proof -
  from ta_reachableE[OF reach] obtain t where g: "ground t" and res: "q |∈| ta_der 𝒜 t" by auto
  from ta_der_trancl_eps[OF eps res] g show ?thesis by blast
qed

lemma ta_reachableI_eps:
  assumes reach: "q |∈| ta_reachable 𝒜"
    and eps: "(q, q') |∈| eps 𝒜"  
  shows "q' |∈| ta_reachable 𝒜"
  by (rule ta_reachableI_eps'[OF reach], insert eps, auto)

― ‹Automata are productive on a set P if all states can reach a state in P›


lemma finite_ta_productive:
  "finite {p. ∃q q' C. p = q ∧ q' |∈| ta_der 𝒜 C⟨Var q⟩ ∧ q' |∈| P}"
proof -
  {fix x q C assume ass: "x ∉ fset P" "q |∈| P" "q |∈| ta_der 𝒜 C⟨Var x⟩"
    then have "x ∈ fset (𝒬 𝒜)"
    proof (cases "is_Fun C⟨Var x⟩")
      case True
      then show ?thesis using ta_der_is_fun_fvars_stateD[OF _ ass(3)]
        by auto
    next
      case False
      then show ?thesis using ass
        by (cases C, auto, (metis eps_trancl_statesD)+)
    qed}
  then have "{q | q q' C. q' |∈| ta_der 𝒜 (C⟨Var q⟩) ∧ q' |∈| P} ⊆ fset (𝒬 𝒜) ∪ fset P" by auto
  from finite_subset[OF this] show ?thesis by auto
qed

lemma ta_productiveE: assumes "q |∈| ta_productive P 𝒜"
  obtains q' C where "q' |∈| ta_der 𝒜 (C⟨Var q⟩)" "q' |∈| P" 
  using assms[unfolded ta_productive_def] by auto

lemma ta_productiveI:
  assumes "q' |∈| ta_der 𝒜 (C⟨Var q⟩)" "q' |∈| P" 
  shows "q |∈| ta_productive P 𝒜"
  using assms unfolding ta_productive_def
  using finite_ta_productive
  by auto

lemma ta_productiveI': 
  assumes "q |∈| ta_der 𝒜 (C⟨Var p⟩)" "q |∈| ta_productive P 𝒜" 
  shows "p |∈| ta_productive P 𝒜"
  using assms unfolding ta_productive_def
  by auto (metis (mono_tags, lifting) ctxt_ctxt_compose ta_der_ctxt)

lemma ta_productive_setI:
  "q |∈| P ⟹ q |∈| ta_productive P 𝒜"
  using ta_productiveI[of q 𝒜 □ q]
  by simp


lemma ta_reachable_empty_rules [simp]:
  "rules 𝒜 = {||} ⟹ ta_reachable 𝒜 = {||}"
  by (auto simp: ta_reachable_def)
     (metis ground.simps(1) ta.exhaust_sel ta_der_rule_empty)

lemma ta_reachable_mono:
  "ta_subset 𝒜 ℬ ⟹ ta_reachable 𝒜 |⊆| ta_reachable ℬ" using ta_der_mono'
  by (auto simp: ta_reachable_def) blast

lemma ta_reachabe_rhs_states: 
  "ta_reachable 𝒜 |⊆| ta_rhs_states 𝒜"
proof -
  {fix q assume "q |∈| ta_reachable 𝒜"
    then obtain t where "ground t" "q |∈| ta_der 𝒜 t"
      by (auto simp: ta_reachable_def)
    then have "q |∈| ta_rhs_states 𝒜"
      by (cases t) (auto simp: ta_rhs_states_def intro!: bexI)}
  then show ?thesis by blast
qed

lemma ta_reachable_eps:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ p |∈| ta_reachable 𝒜 ⟹ (p, q) |∈| (fRestr (eps 𝒜) (ta_reachable 𝒜))|⇧+|"
proof (induct rule: ftrancl_induct)
  case (Base a b)
  then show ?case
    by (metis fSigmaI finterI fr_into_trancl ta_reachableI_eps)
next
  case (Step p q r)
  then have "q |∈| ta_reachable 𝒜" "r |∈| ta_reachable 𝒜"
    by (metis ta_reachableI_eps ta_reachableI_eps')+
  then show ?case using Step
    by (metis fSigmaI finterI ftrancl_into_trancl)
qed

(* major lemma to show that one can restrict to reachable states *)
lemma ta_der_only_reach:
  assumes "fvars_term t |⊆| ta_reachable 𝒜"
  shows "ta_der 𝒜 t = ta_der (ta_only_reach 𝒜) t" (is "?LS = ?RS")
proof -
  have "?RS |⊆| ?LS" using ta_der_mono'[OF ta_restrict_subset]
    by fastforce
  moreover
  {fix q assume "q |∈| ?LS"
    then have "q |∈| ?RS" using assms
    proof (induct rule: ta_der_induct)
      case (Fun f ts ps p q)
      from Fun(2, 6) have ta_reach [simp]: "i < length ps ⟹ fvars_term (ts ! i) |⊆| ta_reachable 𝒜" for i
        by auto (metis ffUnionI fimage_fset fnth_mem funionI2 length_map nth_map sup.orderE) 
      from Fun have r: "i < length ts ⟹ ps ! i |∈| ta_der (ta_only_reach 𝒜) (ts ! i)"
        "i < length ts ⟹ ps ! i |∈| ta_reachable 𝒜" for i
        by (auto) (metis ta_reach ta_der_ta_derict_states)+
      then have "f ps → p |∈| rules (ta_only_reach 𝒜)"
        using Fun(1, 2)
        by (intro ta_derict_ruleI)
           (fastforce simp: in_fset_conv_nth intro!: ta_reachableI_rule[OF _ Fun(1)])+
      then show ?case using ta_reachable_eps[of p q] ta_reachableI_rule[OF _ Fun(1)] r Fun(2, 3)
        by (auto simp: ta_restrict_def intro!: exI[of _ p] exI[of _ ps])
    qed (auto simp: ta_restrict_def intro: ta_reachable_eps)}
  ultimately show ?thesis by blast
qed

lemma ta_der_gterm_only_reach:
  "ta_der 𝒜 (term_of_gterm t) = ta_der (ta_only_reach 𝒜) (term_of_gterm t)"
  using ta_der_only_reach[of "term_of_gterm t" 𝒜]
  by simp

lemma ta_reachable_ta_only_reach [simp]:
  "ta_reachable (ta_only_reach 𝒜) = ta_reachable 𝒜"  (is "?LS = ?RS")
proof -
  have "?LS |⊆| ?RS" using ta_der_mono'[OF ta_restrict_subset]
    by (auto simp: ta_reachable_def) fastforce
  moreover
  {fix t assume "ground (t :: ('b, 'a) term)"
    then have "ta_der 𝒜 t = ta_der (ta_only_reach 𝒜) t" using ta_der_only_reach[of t 𝒜]
      by simp}
  ultimately show ?thesis unfolding ta_reachable_def
    by auto
qed

lemma ta_only_reach_reachable:
  "𝒬 (ta_only_reach 𝒜) |⊆| ta_reachable (ta_only_reach 𝒜)"
  using ta_restrict_states_Q[of 𝒜 "ta_reachable 𝒜"]
  by auto

(* It is sound to restrict to reachable states. *)
lemma gta_only_reach_lang:
  "gta_lang Q (ta_only_reach 𝒜) = gta_lang Q 𝒜"
  using ta_der_gterm_only_reach
  by (auto elim!: gta_langE intro!: gta_langI) force+


lemma ℒ_only_reach: "ℒ (reg_reach R) = ℒ R"
  using gta_only_reach_lang
  by (auto simp: ℒ_def reg_reach_def)

lemma ta_only_reach_lang:
  "ta_lang Q (ta_only_reach 𝒜) = ta_lang Q 𝒜"
  using gta_only_reach_lang
  by (metis ta_lang_to_gta_lang)


lemma ta_prod_epsD:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ q |∈| ta_productive P 𝒜 ⟹ p |∈| ta_productive P 𝒜"
  using ta_der_ctxt[of q 𝒜 "□⟨Var p⟩"]
  by (auto simp: ta_productive_def ta_der_trancl_eps)

lemma ta_only_prod_eps:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ q |∈| ta_productive P 𝒜 ⟹ (p, q) |∈| (eps (ta_only_prod P 𝒜))|⇧+|"
proof (induct rule: ftrancl_induct)
  case (Base p q)
  then show ?case
    by (metis (no_types, lifting) fSigmaI finterI fr_into_trancl ta.sel(2) ta_prod_epsD ta_restrict_def)
next
  case (Step p q r) note IS = this
  show ?case using IS(2 - 4) ta_prod_epsD[OF fr_into_trancl[OF IS(3)] IS(4)] 
    by (auto simp: ta_restrict_def) (simp add: ftrancl_into_trancl)
qed

(* Major lemma to show that it is sound to restrict to productive states. *)
lemma ta_der_only_prod: 
  "q |∈| ta_der 𝒜 t ⟹ q |∈| ta_productive P 𝒜 ⟹ q |∈| ta_der (ta_only_prod P 𝒜) t"
proof (induct rule: ta_der_induct)
  case (Fun f ts ps p q)
  let ?𝒜 = "ta_only_prod P 𝒜"
  have pr: "p |∈| ta_productive P 𝒜" "i < length ts ⟹ ps ! i |∈| ta_productive P 𝒜" for i
    using Fun(2) ta_prod_epsD[of p q] Fun(3, 6) rule_reachable_ctxt_exist[OF Fun(1)]
    using ta_productiveI'[of p 𝒜 _ "ps ! i" P]
    by auto
  then have "f ps → p |∈| rules ?𝒜" using Fun(1, 2) unfolding ta_restrict_def
    by (auto simp: in_fset_conv_nth intro: finite_subset[OF _ finite_Collect_ta_rule, of _ 𝒜])
  then show ?case using pr Fun ta_only_prod_eps[of p q 𝒜 P] Fun(3, 6)
    by auto
qed (auto intro: ta_only_prod_eps)

lemma ta_der_ta_only_prod_ta_der:
  "q |∈| ta_der (ta_only_prod P 𝒜) t ⟹ q |∈| ta_der 𝒜 t"
  by (meson ta_der_el_mono ta_restrict_subset ta_subset_def)


(* It is sound to restrict to productive states. *)
lemma gta_only_prod_lang:
  "gta_lang Q (ta_only_prod Q 𝒜) = gta_lang Q 𝒜" (is "gta_lang Q ?𝒜 = _")
proof
  show "gta_lang Q ?𝒜 ⊆ gta_lang Q 𝒜"
    using gta_lang_mono[OF ta_der_mono'[OF ta_restrict_subset]]
    by blast
next
  {fix t assume "t ∈ gta_lang Q 𝒜"
    from gta_langE[OF this] obtain q where
      reach: "q |∈| ta_der 𝒜 (term_of_gterm t)" "q |∈| Q" .
    from ta_der_only_prod[OF reach(1) ta_productive_setI[OF reach(2)]] reach(2)
    have "t ∈ gta_lang Q ?𝒜" by (auto intro: gta_langI)}
  then show "gta_lang Q 𝒜 ⊆ gta_lang Q ?𝒜" by blast
qed

lemma ℒ_only_prod: "ℒ (reg_prod R) = ℒ R"
  using gta_only_prod_lang
  by (auto simp: ℒ_def reg_prod_def)

lemma ta_only_prod_lang:
  "ta_lang Q (ta_only_prod Q 𝒜) = ta_lang Q 𝒜"
  using gta_only_prod_lang
  by (metis ta_lang_to_gta_lang)

(* the productive states are also productive w.r.t. the new automaton *)
lemma ta_prodictive_ta_only_prod [simp]:
  "ta_productive P (ta_only_prod P 𝒜) = ta_productive P 𝒜"  (is "?LS = ?RS")
proof -
  have "?LS |⊆| ?RS" using ta_der_mono'[OF ta_restrict_subset]
    using finite_ta_productive[of 𝒜 P]
    by (auto simp: ta_productive_def) fastforce
  moreover have "?RS |⊆| ?LS" using ta_der_only_prod
    by (auto elim!: ta_productiveE)
       (smt (z3) ta_der_only_prod ta_productiveI ta_productive_setI)
  ultimately show ?thesis by blast
qed

lemma ta_only_prod_productive:
  "𝒬 (ta_only_prod P 𝒜) |⊆| ta_productive P (ta_only_prod P 𝒜)"
  using ta_restrict_states_Q by force

lemma ta_only_prod_reachable:
  assumes all_reach: "𝒬 𝒜 |⊆| ta_reachable 𝒜"
  shows "𝒬 (ta_only_prod P 𝒜) |⊆| ta_reachable (ta_only_prod P 𝒜)" (is "?Ls |⊆| ?Rs")
proof -
  {fix q assume "q |∈| ?Ls"
    then obtain t where "ground t" "q |∈| ta_der 𝒜 t" "q |∈| ta_productive P 𝒜"
      using fsubsetD[OF ta_only_prod_productive[of 𝒜 P]]
      using fsubsetD[OF fsubset_trans[OF ta_restrict_states all_reach, of "ta_productive P 𝒜"]]
      by (auto elim!: ta_reachableE)
    then have "q |∈| ?Rs"
      by (intro ta_reachableI[where ?𝒜 = "ta_only_prod P 𝒜" and ?t = t]) (auto simp: ta_der_only_prod)}
  then show ?thesis by blast
qed

lemma ta_prod_reach_subset:
  "ta_subset (ta_only_prod P (ta_only_reach 𝒜)) 𝒜"
  by (rule ta_subset_trans, (rule ta_restrict_subset)+)

lemma ta_prod_reach_states:
  "𝒬 (ta_only_prod P (ta_only_reach 𝒜)) |⊆| 𝒬 𝒜"
  by (rule ta_subset_states[OF ta_prod_reach_subset])

(* If all states are reachable then there exists a ground context for all productive states *)
lemma ta_productive_aux:
  assumes "𝒬 𝒜 |⊆| ta_reachable 𝒜" "q |∈| ta_der 𝒜 (C⟨t⟩)"
  shows "∃C'. ground_ctxt C' ∧ q |∈| ta_der 𝒜 (C'⟨t⟩)" using assms(2)
proof (induct C arbitrary: q)
  case Hole then show ?case by (intro exI[of _ "□"]) auto
next
  case (More f ts1 C ts2)
  from More(2) obtain qs q' where q': "f qs → q' |∈| rules 𝒜" "q' = q ∨ (q', q) |∈| (eps 𝒜)|⇧+|"
    "qs ! length ts1 |∈| ta_der 𝒜 (C⟨t⟩)" "length qs = Suc (length ts1 + length ts2)"
    by simp (metis less_add_Suc1 nth_append_length)
  { fix i assume "i < length qs"
    then have "qs ! i |∈| 𝒬 𝒜" using q'(1)
      by (auto dest!: rule_statesD(4))
    then have "∃t. ground t ∧ qs ! i |∈| ta_der 𝒜 t" using assms(1)
      by (simp add: ta_reachable_def) force}
  then obtain ts where ts: "i < length qs ⟹ ground (ts i) ∧ qs ! i |∈| ta_der 𝒜 (ts i)" for i by metis
  obtain C' where C: "ground_ctxt C'" "qs ! length ts1 |∈| ta_der 𝒜 C'⟨t⟩" using More(1)[OF q'(3)] by blast
  define D where "D ≡ More f (map ts [0..<length ts1]) C' (map ts [Suc (length ts1)..<Suc (length ts1 + length ts2)])"
  have "ground_ctxt D" unfolding D_def using ts C(1) q'(4) by auto
  moreover have "q |∈| ta_der 𝒜 D⟨t⟩" using ts C(2) q' unfolding D_def
    by (auto simp: nth_append_Cons not_le not_less le_less_Suc_eq Suc_le_eq intro!: exI[of _ qs] exI[of _ q'])
  ultimately show ?case by blast
qed

lemma ta_productive_def':
  assumes "𝒬 𝒜 |⊆| ta_reachable 𝒜"
  shows "ta_productive Q 𝒜 = {| q| q q' C. ground_ctxt C ∧ q' |∈| ta_der 𝒜 (C⟨Var q⟩) ∧ q' |∈| Q |}"
  using ta_productive_aux[OF assms]
  by (auto simp: ta_productive_def intro!: finite_subset[OF _ finite_ta_productive, of _ 𝒜 Q]) force+

(* turn a finite automaton into a trim one, by removing
   first all unreachable and then all non-productive states *)

lemma trim_gta_lang: "gta_lang Q (trim_ta Q 𝒜) = gta_lang Q 𝒜"
  unfolding trim_ta_def gta_only_reach_lang gta_only_prod_lang ..

lemma trim_ta_subset: "ta_subset (trim_ta Q 𝒜) 𝒜"
  unfolding trim_ta_def by (rule ta_prod_reach_subset)

theorem trim_ta: "ta_is_trim Q (trim_ta Q 𝒜)" unfolding ta_is_trim_def
  by (metis fin_mono ta_only_prod_reachable ta_only_reach_reachable
      ta_prodictive_ta_only_prod ta_restrict_states_Q trim_ta_def)


lemma reg_is_trim_trim_reg [simp]: "reg_is_trim (trim_reg R)"
  unfolding reg_is_trim_def trim_reg_def
  by (simp add: trim_ta)

lemma trim_reg_reach [simp]:
  "𝒬⇩r (trim_reg A) |⊆| ta_reachable (ta (trim_reg A))"
  by (auto simp: trim_reg_def) (meson ta_is_trim_def trim_ta)

lemma trim_reg_prod [simp]:
  "𝒬⇩r (trim_reg A) |⊆| ta_productive (fin (trim_reg A)) (ta (trim_reg A))"
  by (auto simp: trim_reg_def) (meson ta_is_trim_def trim_ta)

(* Proposition 7: every tree automaton can be turned into an  equivalent trim one *)
lemmas obtain_trimmed_ta = trim_ta trim_gta_lang ta_subset_det[OF trim_ta_subset]

(* Trim tree automaton signature *)
lemma ℒ_trim_ta_sig:
  assumes "reg_is_trim R" "ℒ R ⊆ 𝒯⇩G (fset ℱ)"
  shows "ta_sig (ta R) |⊆| ℱ"
proof -
  {fix r assume r: "r |∈| rules (ta R)"
    then obtain f ps p where [simp]: "r = f ps → p" by (cases r) auto
    from r assms(1) have "fset_of_list ps |⊆| ta_reachable (ta R)"
      by (auto simp add: rule_statesD(4) reg_is_trim_def ta_is_trim_def)
    from ta_reachableI_rule[OF this, of f p] r
    obtain ts where ts: "length ts = length ps" "∀ i < length ps. ground (ts ! i)"
      "∀ i < length ps. ps ! i |∈| ta_der (ta R) (ts ! i)"
      by auto
    obtain C q where ctxt: "ground_ctxt C" "q |∈| ta_der (ta R) (C⟨Var p⟩)" "q |∈| fin R"
      using assms(1) unfolding reg_is_trim_def
      by (metis ‹r = f ps → p› fsubsetI r rule_statesD(2) ta_productiveE ta_productive_aux ta_is_trim_def)
    from ts ctxt r have reach: "q |∈| ta_der (ta R) C⟨Fun f ts⟩"
      by auto (metis ta_der_Fun ta_der_ctxt)
    have gr: "ground C⟨Fun f ts⟩" using ts(1, 2) ctxt(1)
      by (auto simp: in_set_conv_nth)
    then have "C⟨Fun f ts⟩ ∈ ta_lang (fin R) (ta R)" using ctxt(1, 3) ts(1, 2)
      apply (intro ta_langI[OF _ _ reach, of "fin R" "C⟨Fun f ts⟩"])
      apply (auto simp del: adapt_vars_ctxt)
      by (metis gr adapt_vars2 adapt_vars_adapt_vars)
    then have *: "gterm_of_term C⟨Fun f ts⟩ ∈ ℒ R" using gr
      by (auto simp: ℒ_def)
    then have "funas_gterm (gterm_of_term C⟨Fun f ts⟩) ⊆ fset ℱ" using assms(2) gr
      by (auto simp: 𝒯⇩G_equivalent_def)
    moreover have "(f, length ps) ∈ funas_gterm (gterm_of_term C⟨Fun f ts⟩)"
      using ts(1) by (auto simp: funas_gterm_gterm_of_term[OF gr])
    ultimately have "(r_root r, length (r_lhs_states r)) |∈| ℱ"
      by auto}
  then show ?thesis
    by (auto simp: ta_sig_def)
qed

text ‹Map function over TA rules which change states/signature›

lemma map_ta_rule_iff:
  "map_ta_rule f g |`| Δ = {|TA_rule (g h) (map f qs) (f q) | h qs q. TA_rule h qs q |∈| Δ|}"
  apply (intro fequalityI fsubsetI)
  apply (auto simp add: rev_image_eqI)
  apply (metis map_ta_rule_cases ta_rule.collapse)
  done

lemma ℒ_trim: "ℒ (trim_reg R) = ℒ R"
  by (auto simp: trim_gta_lang ℒ_def trim_reg_def)


lemma fmap_funs_ta_def':
  "fmap_funs_ta h 𝒜 = TA {|(h f) qs → q |f qs q. f qs → q |∈| rules 𝒜|} (eps 𝒜)"
  unfolding fmap_funs_ta_def map_ta_rule_iff by auto

lemma fmap_states_ta_def':
  "fmap_states_ta h 𝒜 = TA {|f (map h qs) → h q |f qs q. f qs → q |∈| rules 𝒜|} (map_both h |`| eps 𝒜)"
  unfolding fmap_states_ta_def map_ta_rule_iff by auto

lemma fmap_states [simp]:
  "𝒬 (fmap_states_ta h 𝒜) = h |`| 𝒬 𝒜"
  unfolding fmap_states_ta_def 𝒬_def
  by auto

lemma fmap_states_ta_sig [simp]:
  "ta_sig (fmap_states_ta f 𝒜) = ta_sig 𝒜"
  by (auto simp: fmap_states_ta_def ta_sig_def ta_rule.map_sel intro: fset.map_cong0)

lemma fmap_states_ta_eps_wit:
  assumes "(h p, q) |∈| (map_both h |`| eps 𝒜)|⇧+|" "finj_on h (𝒬 𝒜)" "p |∈| 𝒬 𝒜"
  obtains q' where "q = h q'" "(p, q') |∈| (eps 𝒜)|⇧+|" "q' |∈| 𝒬 𝒜"
  using assms(1)[unfolded ftrancl_map_both_fsubset[OF assms(2), of "eps 𝒜", simplified]]
  using ‹finj_on h (𝒬 𝒜)›[unfolded finj_on_def', rule_format, OF ‹p |∈| 𝒬 𝒜›]
  by (metis Pair_inject eps_trancl_statesD prod_fun_fimageE)

lemma ta_der_fmap_states_inv_superset:
  assumes "𝒬 𝒜 |⊆| ℬ" "finj_on h ℬ"
    and  "q |∈| ta_der (fmap_states_ta h 𝒜) (term_of_gterm t)"
  shows "the_finv_into ℬ h q |∈| ta_der 𝒜 (term_of_gterm t)" using assms(3)
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  from assms(1, 2) have inj: "finj_on h (𝒬 𝒜)" using fsubset_finj_on by blast
  have "x |∈| 𝒬 𝒜 ⟹ the_finv_into (𝒬 𝒜) h (h x) = the_finv_into ℬ h (h x)" for x
    using assms(1, 2) by (metis fsubsetD inj the_finv_into_f_f) 
  then show ?case using GFun the_finv_into_f_f[OF inj] assms(1)
    by (auto simp: fmap_states_ta_def' finj_on_def' rule_statesD eps_statesD
      elim!: fmap_states_ta_eps_wit[OF _ inj]
      intro!: exI[of _ "the_finv_into ℬ h p"])
qed

lemma ta_der_fmap_states_inv:
  assumes "finj_on h (𝒬 𝒜)" "q |∈| ta_der (fmap_states_ta h 𝒜) (term_of_gterm t)"
  shows "the_finv_into (𝒬 𝒜) h q |∈| ta_der 𝒜 (term_of_gterm t)"
  by (simp add: ta_der_fmap_states_inv_superset assms)

lemma ta_der_to_fmap_states_der:
  assumes "q |∈| ta_der 𝒜 (term_of_gterm t)"
  shows "h q |∈| ta_der (fmap_states_ta h 𝒜) (term_of_gterm t)" using assms
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  then show ?case
    using ftrancl_map_prod_mono[of h "eps 𝒜"]
    by (auto simp: fmap_states_ta_def' intro!: exI[of _ "h p"] exI[of _ "map h ps"])
qed

lemma ta_der_fmap_states_conv:
  assumes "finj_on h (𝒬 𝒜)"
  shows "ta_der (fmap_states_ta h 𝒜) (term_of_gterm t) =  h |`| ta_der 𝒜 (term_of_gterm t)"
  using ta_der_to_fmap_states_der[of _ 𝒜 t] ta_der_fmap_states_inv[OF assms]
  using f_the_finv_into_f[OF assms] finj_on_the_finv_into[OF assms]
  using gterm_ta_der_states
  by (auto intro!: rev_fimage_eqI) fastforce

lemma fmap_states_ta_det:
  assumes "finj_on f (𝒬 𝒜)"
  shows "ta_det (fmap_states_ta f 𝒜) = ta_det 𝒜" (is "?Ls = ?Rs")
proof
  {fix g ps p q assume ass: "?Ls" "TA_rule g ps p |∈| rules 𝒜" "TA_rule g ps q |∈| rules 𝒜"
    then have "TA_rule g (map f ps) (f p) |∈| rules (fmap_states_ta f 𝒜)"
       "TA_rule g (map f ps) (f q) |∈| rules (fmap_states_ta f 𝒜)"
      by (force simp: fmap_states_ta_def)+
    then have "p = q" using ass finj_on_eq_iff[OF assms]
      by (auto simp: ta_det_def) (meson rule_statesD(2))} 
  then show "?Ls ⟹ ?Rs"
    by (auto simp: ta_det_def fmap_states_ta_def')
next
  {fix g ps qs p q assume ass: "?Rs" "TA_rule g ps p |∈| rules 𝒜" "TA_rule g qs q |∈| rules 𝒜"
    then have "map f ps = map f qs ⟹ ps = qs" using finj_on_eq_iff[OF assms]
      by (auto simp: map_eq_nth_conv in_fset_conv_nth dest!: rule_statesD(4) intro!: nth_equalityI)}
  then show "?Rs ⟹ ?Ls" using finj_on_eq_iff[OF assms]
    by (auto simp: ta_det_def fmap_states_ta_def') blast
qed

lemma fmap_states_ta_lang:
  "finj_on f (𝒬 𝒜) ⟹ Q |⊆| 𝒬 𝒜 ⟹ gta_lang (f |`| Q) (fmap_states_ta f 𝒜) = gta_lang Q 𝒜"
  using ta_der_fmap_states_conv[of f 𝒜]
  by (auto simp: finj_on_def' finj_on_eq_iff fsubsetD elim!: gta_langE intro!: gta_langI)

lemma fmap_states_ta_lang2:
  "finj_on f (𝒬 𝒜 |∪| Q) ⟹ gta_lang (f |`| Q) (fmap_states_ta f 𝒜) = gta_lang Q 𝒜"
  using ta_der_fmap_states_conv[OF fsubset_finj_on[of f "𝒬 𝒜 |∪| Q" "𝒬 𝒜"]] 
  by (auto simp: finj_on_def' elim!: gta_langE intro!: gta_langI) fastforce


definition funs_ta :: "('q, 'f) ta ⇒ 'f fset" where
  "funs_ta 𝒜 = {|f |f qs q. TA_rule f qs q |∈| rules 𝒜|}"

lemma funs_ta[code]:
  "funs_ta 𝒜 = (λ r. case r of TA_rule f ps p ⇒ f) |`| (rules 𝒜)" (is "?Ls = ?Rs")
  by (force simp: funs_ta_def rev_fimage_eqI simp flip: fset.set_map
     split!: ta_rule.splits intro!: finite_subset[of "{f. ∃qs q. TA_rule f qs q |∈| rules 𝒜}" "fset ?Rs"])

lemma finite_funs_ta [simp]:
  "finite {f. ∃qs q. TA_rule f qs q |∈| rules 𝒜}"
  by (intro finite_subset[of "{f. ∃qs q. TA_rule f qs q |∈| rules 𝒜}" "fset (funs_ta 𝒜)"])
     (auto simp: funs_ta rev_fimage_eqI simp flip: fset.set_map split!: ta_rule.splits)

lemma funs_taE [elim]:
  assumes "f |∈| funs_ta 𝒜"
  obtains ps p where "TA_rule f ps p |∈| rules 𝒜" using assms
  by (auto simp: funs_ta_def)

lemma funs_taI [intro]:
  "TA_rule f ps p |∈| rules 𝒜 ⟹ f |∈| funs_ta 𝒜"
  by (auto simp: funs_ta_def)

lemma fmap_funs_ta_cong:
  "(⋀x. x |∈| funs_ta 𝒜 ⟹ h x = k x) ⟹ 𝒜 = ℬ ⟹ fmap_funs_ta h 𝒜 = fmap_funs_ta k ℬ"
  by (force simp: fmap_funs_ta_def')

lemma [simp]: "{|TA_rule f qs q |f qs q. TA_rule f qs q |∈| X|} = X"
  by (intro fset_eqI; case_tac x) auto

lemma fmap_funs_ta_id [simp]:
  "fmap_funs_ta id 𝒜 = 𝒜" by (simp add: fmap_funs_ta_def')

lemma fmap_states_ta_id [simp]:
  "fmap_states_ta id 𝒜 = 𝒜"
  by (auto simp: fmap_states_ta_def map_ta_rule_iff prod.map_id0)

lemmas fmap_funs_ta_id' [simp] = fmap_funs_ta_id[unfolded id_def]

lemma fmap_funs_ta_comp:
  "fmap_funs_ta h (fmap_funs_ta k A) = fmap_funs_ta (h ∘ k) A"
proof -
  have "r |∈| rules A ⟹ map_ta_rule id h (map_ta_rule id k r) = map_ta_rule id (λx. h (k x)) r" for r
    by (cases r) (auto)
  then show ?thesis
    by (force simp: fmap_funs_ta_def fimage_iff cong: fmap_funs_ta_cong)
qed

lemma fmap_funs_reg_comp:
  "fmap_funs_reg h (fmap_funs_reg k A) = fmap_funs_reg (h ∘ k) A"
  using fmap_funs_ta_comp unfolding fmap_funs_reg_def
  by auto

lemma fmap_states_ta_comp:
  "fmap_states_ta h (fmap_states_ta k A) = fmap_states_ta (h ∘ k) A"
  by (auto simp: fmap_states_ta_def ta_rule.map_comp comp_def id_def prod.map_comp)

lemma funs_ta_fmap_funs_ta [simp]:
  "funs_ta (fmap_funs_ta f A) = f |`| funs_ta A"
  by (auto simp: funs_ta fmap_funs_ta_def' comp_def fimage_iff
    split!: ta_rule.splits) force+

lemma ta_der_funs_ta:
  "q |∈| ta_der A t ⟹ ffuns_term t |⊆| funs_ta A"
proof (induct t arbitrary: q)
  case (Fun f ts)
  then have "f |∈| funs_ta A" by (auto simp: funs_ta_def)
  then show ?case using Fun(1)[OF nth_mem, THEN fsubsetD] Fun(2)
    by (auto simp: in_fset_conv_nth) blast+
qed auto

lemma ta_der_fmap_funs_ta:
  "q |∈| ta_der A t ⟹ q |∈| ta_der (fmap_funs_ta f A) (map_funs_term f t)"
  by (induct t arbitrary: q) (auto 0 4 simp: fmap_funs_ta_def')

lemma ta_der_fmap_states_ta:
  assumes "q |∈| ta_der A t"
  shows "h q |∈| ta_der (fmap_states_ta h A) (map_vars_term h t)"
proof -
  have [intro]: "(q, q') |∈| (eps A)|⇧+| ⟹ (h q, h q') |∈| (eps (fmap_states_ta h A))|⇧+|" for q q'
    by (force intro!: ftrancl_map[of "eps A"] simp: fmap_states_ta_def)
  show ?thesis using assms
  proof (induct rule: ta_der_induct)
    case (Fun f ts ps p q)
    have "f (map h ps) → h p |∈| rules (fmap_states_ta h A)"
      using Fun(1) by (force simp: fmap_states_ta_def')
    then show ?case using Fun by (auto 0 4)
  qed auto
qed

lemma ta_der_fmap_states_ta_mono:
  shows "f |`| ta_der A (term_of_gterm s) |⊆| ta_der (fmap_states_ta f A) (term_of_gterm s)"
  using ta_der_fmap_states_ta[of _ A "term_of_gterm s" f]
  by (simp add: fimage_fsubsetI ta_der_to_fmap_states_der)

lemma ta_der_fmap_states_ta_mono2:
  assumes "finj_on f (𝒬 A)"
  shows "ta_der (fmap_states_ta f A) (term_of_gterm s) |⊆| f |`| ta_der A (term_of_gterm s)"
  using ta_der_fmap_states_conv[OF assms] by auto

lemma fmap_funs_ta_der':
  "q |∈| ta_der (fmap_funs_ta h A) t ⟹ ∃t'. q |∈| ta_der A t' ∧ map_funs_term h t' = t"
proof (induct rule: ta_der_induct)
  case (Var q v)
  then show ?case by (auto simp: fmap_funs_ta_def intro!: exI[of _ "Var v"])
next
  case (Fun f ts ps p q)
  obtain f' ts' where root: "f = h f'" "f' ps → p |∈| rules A" and
    "⋀i. i < length ts ⟹ ps ! i |∈| ta_der A (ts' i) ∧ map_funs_term h (ts' i) = ts ! i"
    using Fun(1, 5) unfolding fmap_funs_ta_def'
    by auto metis
  note [simp] = conjunct1[OF this(3)] conjunct2[OF this(3), unfolded id_def]
  have [simp]: "p = q ⟹ f' ps → q |∈| rules A" using root(2) by auto
  show ?case using Fun(3)
    by (auto simp: comp_def Fun root fmap_funs_ta_def'
      intro!: exI[of _ "Fun f' (map ts' [0..<length ts])"] exI[of _ ps] exI[of _ p] nth_equalityI)
qed

lemma fmap_funs_gta_lang:
  "gta_lang Q (fmap_funs_ta h 𝒜) = map_gterm h ` gta_lang Q 𝒜" (is "?Ls = ?Rs")
proof -
  {fix s assume "s ∈ ?Ls" then obtain q where
    lang: "q |∈| Q" "q |∈| ta_der (fmap_funs_ta h 𝒜) (term_of_gterm s)"
      by auto
    from fmap_funs_ta_der'[OF this(2)] obtain t where
    t: "q |∈| ta_der 𝒜 t" "map_funs_term h t = term_of_gterm s" "ground t"
      by (metis ground_map_term ground_term_of_gterm)
    then have "s ∈ ?Rs" using map_gterm_of_term[OF t(3), of h id] lang
      by (auto simp: gta_lang_def gta_der_def image_iff)
         (metis fempty_iff finterI ground_term_to_gtermD map_term_of_gterm term_of_gterm_inv)}
  moreover have "?Rs ⊆ ?Ls" using ta_der_fmap_funs_ta[of _ 𝒜 _ h]
    by (auto elim!: gta_langE intro!: gta_langI) fastforce
  ultimately show ?thesis by blast
qed

lemma fmap_funs_ℒ:
  "ℒ (fmap_funs_reg h R) =  map_gterm h ` ℒ R"
  using fmap_funs_gta_lang[of "fin R" h]
  by (auto simp: fmap_funs_reg_def ℒ_def)

lemma ta_states_fmap_funs_ta [simp]: "𝒬 (fmap_funs_ta f A) = 𝒬 A"
  by (auto simp: fmap_funs_ta_def 𝒬_def)
 
lemma ta_reachable_fmap_funs_ta [simp]:
  "ta_reachable (fmap_funs_ta f A) = ta_reachable A" unfolding ta_reachable_def
  by (metis (mono_tags, lifting) fmap_funs_ta_der' ta_der_fmap_funs_ta ground_map_term)


lemma fin_in_states:
  "fin (reg_Restr_Q⇩f R) |⊆| 𝒬⇩r (reg_Restr_Q⇩f R)"
  by (auto simp: reg_Restr_Q⇩f_def)

lemma fmap_states_reg_Restr_Q⇩f_fin:
  "finj_on f (𝒬 𝒜) ⟹ fin (fmap_states_reg f (reg_Restr_Q⇩f R)) |⊆| 𝒬⇩r (fmap_states_reg f (reg_Restr_Q⇩f R))"
  by (auto simp: fmap_states_reg_def reg_Restr_Q⇩f_def)

lemma ℒ_fmap_states_reg_Inl_Inr [simp]:
  "ℒ (fmap_states_reg Inl R) = ℒ R"
  "ℒ (fmap_states_reg Inr R) = ℒ R"
  unfolding ℒ_def fmap_states_reg_def
  by (auto simp: finj_Inl_Inr intro!: fmap_states_ta_lang2)

lemma finite_Collect_prod_ta_rules:
  "finite {f qs → (a, b) |f qs a b. f map fst qs → a |∈| rules 𝒜 ∧ f map snd qs → b |∈| rules 𝔅}" (is "finite ?set")
proof -
  have "?set ⊆ (λ (ra, rb). case ra of f ps → p ⇒ case rb of g qs → q ⇒ f (zip ps qs) → (p, q)) ` (srules 𝒜 × srules 𝔅)"
    by (auto simp: srules_def image_iff split!: ta_rule.splits)
       (metis ta_rule.inject zip_map_fst_snd)
  from finite_imageI[of "srules 𝒜 × srules 𝔅", THEN finite_subset[OF this]]
  show ?thesis by (auto simp: srules_def)
qed

― ‹The product automaton of the automata A and B is constructed
 by applying the rules on pairs of states›

lemmas prod_eps_def = prod_epsLp_def prod_epsRp_def

lemma finite_prod_epsLp:
  "finite (Collect (prod_epsLp 𝒜 ℬ))"
  by (intro finite_subset[of "Collect (prod_epsLp 𝒜 ℬ)" "fset ((𝒬 𝒜 |×| 𝒬 ℬ) |×| 𝒬 𝒜 |×| 𝒬 ℬ)"])
     (auto simp: prod_epsLp_def dest: eps_statesD)

lemma finite_prod_epsRp:
  "finite (Collect (prod_epsRp 𝒜 ℬ))"
  by (intro finite_subset[of "Collect (prod_epsRp 𝒜 ℬ)" "fset ((𝒬 𝒜 |×| 𝒬 ℬ) |×| 𝒬 𝒜 |×| 𝒬 ℬ)"])
     (auto simp: prod_epsRp_def dest: eps_statesD)
lemmas finite_prod_eps [simp] = finite_prod_epsLp[unfolded prod_epsLp_def] finite_prod_epsRp[unfolded prod_epsRp_def]

lemma [simp]: "f qs → q |∈| rules (prod_ta 𝒜 ℬ) ⟷ f qs → q |∈| prod_ta_rules 𝒜 ℬ"
  "r |∈| rules (prod_ta 𝒜 ℬ) ⟷ r |∈| prod_ta_rules 𝒜 ℬ"
  by (auto simp: prod_ta_def)

lemma prod_ta_states:
  "𝒬 (prod_ta 𝒜 ℬ) |⊆| 𝒬 𝒜 |×| 𝒬 ℬ"
proof -
  {fix q assume "q |∈| rule_states (rules (prod_ta 𝒜 ℬ))"
    then obtain f ps p where "f ps → p |∈| rules (prod_ta 𝒜 ℬ)" and "q |∈| fset_of_list ps ∨ p = q"
      by (metis rule_statesE)
    then have "fst q |∈| 𝒬 𝒜 ∧ snd q |∈| 𝒬 ℬ"
      using rule_statesD(2, 4)[of f "map fst ps" "fst p" 𝒜]
      using rule_statesD(2, 4)[of f "map snd ps" "snd p" ℬ]
      by auto}
  moreover
  {fix q assume "q |∈| eps_states (eps (prod_ta 𝒜 ℬ))" then have "fst q |∈| 𝒬 𝒜 ∧ snd q |∈| 𝒬 ℬ"
      by (auto simp: eps_states_def prod_ta_def prod_eps_def dest: eps_statesD)}
  ultimately show ?thesis
    by (auto simp: 𝒬_def) blast+
qed

lemma prod_ta_det:
  assumes "ta_det 𝒜" and "ta_det ℬ"
  shows "ta_det (prod_ta 𝒜 ℬ)"
  using assms unfolding ta_det_def prod_ta_def prod_eps_def
  by auto

lemma prod_ta_sig:
  "ta_sig (prod_ta 𝒜 ℬ) |⊆| ta_sig 𝒜 |∪| ta_sig ℬ"
proof (rule fsubsetI)
  fix x
  assume "x |∈| ta_sig (prod_ta 𝒜 ℬ)"
  hence "x |∈| ta_sig 𝒜 ∨ x |∈| ta_sig ℬ"
    unfolding ta_sig_def prod_ta_def
    using image_iff by fastforce
  thus "x |∈| ta_sig (prod_ta 𝒜 ℬ) ⟹ x |∈| ta_sig 𝒜 |∪| ta_sig ℬ"
    by simp
qed

lemma from_prod_eps:
  "(p, q) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+| ⟹ (snd p, snd q) |∉| (eps ℬ)|⇧+| ⟹ snd p = snd q ∧ (fst p, fst q) |∈| (eps 𝒜)|⇧+|"
  "(p, q) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+| ⟹ (fst p, fst q) |∉| (eps 𝒜)|⇧+| ⟹ fst p = fst q ∧ (snd p, snd q) |∈| (eps ℬ)|⇧+|"
  apply (induct rule: ftrancl_induct) 
  apply (auto simp: prod_ta_def prod_eps_def intro: ftrancl_into_trancl )
  apply (simp add: fr_into_trancl not_ftrancl_into)+
  done

lemma to_prod_eps𝒜:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ r |∈| 𝒬 ℬ ⟹ ((p, r), (q, r)) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|"
  by (induct rule: ftrancl_induct)
     (auto simp: prod_ta_def prod_eps_def intro: fr_into_trancl ftrancl_into_trancl)

lemma to_prod_epsℬ:
  "(p, q) |∈| (eps ℬ)|⇧+| ⟹ r |∈| 𝒬 𝒜 ⟹ ((r, p), (r, q)) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|"
  by (induct rule: ftrancl_induct)
     (auto simp: prod_ta_def prod_eps_def intro: fr_into_trancl ftrancl_into_trancl)

lemma to_prod_eps:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ (p', q') |∈| (eps ℬ)|⇧+| ⟹ ((p, p'), (q, q')) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|"
proof (induct rule: ftrancl_induct)
  case (Base a b)
  show ?case using Base(2, 1)
  proof (induct rule: ftrancl_induct)
    case (Base c d)
    then have "((a, c), b, c) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|" using finite_prod_eps
      by (auto simp: prod_ta_def prod_eps_def dest: eps_statesD intro!: fr_into_trancl ftrancl_into_trancl)
    moreover have "((b, c), b, d) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|" using finite_prod_eps Base
      by (auto simp: prod_ta_def prod_eps_def dest: eps_statesD intro!: fr_into_trancl ftrancl_into_trancl)
    ultimately show ?case
      by (auto intro: ftrancl_trans)
  next
    case (Step p q r)
    then have "((b, q), b, r) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|" using finite_prod_eps
      by (auto simp: prod_ta_def prod_eps_def dest: eps_statesD intro!: fr_into_trancl)
    then show ?case using Step
      by (auto intro: ftrancl_trans)
  qed
next
  case (Step a b c)
  from Step have "q' |∈| 𝒬 ℬ"
    by (auto dest: eps_trancl_statesD)
  then have "((b, q'), (c,q')) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|" 
    using Step(3) finite_prod_eps
    by (auto simp: prod_ta_def prod_eps_def intro!: fr_into_trancl)
  then show ?case using ftrancl_trans Step
    by auto
qed

lemma prod_ta_der_to_𝒜_ℬ_der1:
  assumes "q |∈| ta_der (prod_ta 𝒜 ℬ) (term_of_gterm t)"
  shows "fst q |∈| ta_der 𝒜 (term_of_gterm t)" using assms
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  then show ?case
    by (auto dest: from_prod_eps intro!: exI[of _ "map fst ps"] exI[of _ "fst p"])
qed

lemma prod_ta_der_to_𝒜_ℬ_der2:
  assumes "q |∈| ta_der (prod_ta 𝒜 ℬ) (term_of_gterm t)"
  shows  "snd q |∈| ta_der ℬ (term_of_gterm t)" using assms
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  then show ?case
    by (auto dest: from_prod_eps intro!: exI[of _ "map snd ps"] exI[of _ "snd p"])
qed

lemma 𝒜_ℬ_der_to_prod_ta:
  assumes "fst q |∈| ta_der 𝒜 (term_of_gterm t)" "snd q |∈| ta_der ℬ (term_of_gterm t)"
  shows "q |∈| ta_der (prod_ta 𝒜 ℬ) (term_of_gterm t)" using assms
proof (induct t arbitrary: q)
  case (GFun f ts)
  from GFun(2, 3) obtain ps qs p q' where
    rules: "f ps → p |∈| rules 𝒜" "f qs → q' |∈| rules ℬ" "length ps = length ts" "length ps = length qs" and
    eps: "p = fst q ∨ (p, fst q) |∈| (eps 𝒜)|⇧+|" "q' = snd q ∨ (q', snd q) |∈| (eps ℬ)|⇧+|" and
    steps: "∀ i < length qs. ps ! i |∈| ta_der 𝒜 (term_of_gterm (ts ! i))"
      "∀ i < length qs. qs ! i |∈| ta_der ℬ (term_of_gterm (ts ! i))"
    by auto
  from rules have st: "p |∈| 𝒬 𝒜" "q' |∈| 𝒬 ℬ" by (auto dest: rule_statesD)
  have "(p, snd q) = q ∨ ((p, q'), q) |∈| (eps (prod_ta 𝒜 ℬ))|⇧+|" using eps st
    using to_prod_epsℬ[of q' "snd q" ℬ "fst q" 𝒜]
    using to_prod_eps𝒜[of p "fst q" 𝒜 "snd q" ℬ]
    using to_prod_eps[of p "fst q" 𝒜 q' "snd q" ℬ]
    by (cases "p = fst q"; cases "q' = snd q") (auto simp: prod_ta_def)
  then show ?case using rules eps steps GFun(1) st
    by (cases "(p, snd q) = q")
       (auto simp: finite_Collect_prod_ta_rules dest: to_prod_epsℬ intro!: exI[of _ p] exI[of _ q'] exI[of _ "zip ps qs"])
qed

lemma prod_ta_der:
  "q |∈| ta_der (prod_ta 𝒜 ℬ) (term_of_gterm t) ⟷
     fst q |∈| ta_der 𝒜 (term_of_gterm t) ∧ snd q |∈| ta_der ℬ (term_of_gterm t)"
  using prod_ta_der_to_𝒜_ℬ_der1 prod_ta_der_to_𝒜_ℬ_der2 𝒜_ℬ_der_to_prod_ta
  by blast

lemma intersect_ta_gta_lang:
 "gta_lang (Q⇩𝒜 |×| Q⇩ℬ) (prod_ta 𝒜 ℬ) = gta_lang Q⇩𝒜 𝒜 ∩ gta_lang Q⇩ℬ ℬ"
  by (auto simp: prod_ta_der elim!: gta_langE intro: gta_langI)


lemma ℒ_intersect: "ℒ (reg_intersect R L) = ℒ R ∩ ℒ L"
  by (auto simp: intersect_ta_gta_lang ℒ_def reg_intersect_def)

lemma intersect_ta_ta_lang:
 "ta_lang (Q⇩𝒜 |×| Q⇩ℬ) (prod_ta 𝒜 ℬ) = ta_lang Q⇩𝒜 𝒜 ∩ ta_lang Q⇩ℬ ℬ"
  using intersect_ta_gta_lang[of Q⇩𝒜 Q⇩ℬ 𝒜 ℬ]
  by auto (metis IntI imageI term_of_gterm_inv)

―  ‹Union of tree automata›

lemma ta_union_ta_subset:
  "ta_subset 𝒜 (ta_union 𝒜 ℬ)" "ta_subset ℬ (ta_union 𝒜 ℬ)"
  unfolding ta_subset_def ta_union_def
  by auto

lemma ta_union_states [simp]:
  "𝒬 (ta_union 𝒜 ℬ) = 𝒬 𝒜 |∪| 𝒬 ℬ"
  by (auto simp: ta_union_def 𝒬_def)

lemma ta_union_sig [simp]:
  "ta_sig (ta_union 𝒜 ℬ) = ta_sig 𝒜 |∪| ta_sig ℬ"
  by (auto simp: ta_union_def ta_sig_def)

lemma ta_union_eps_disj_states:
  assumes "𝒬 𝒜 |∩| 𝒬 ℬ = {||}" and "(p, q) |∈| (eps (ta_union 𝒜 ℬ))|⇧+|"
  shows "(p, q) |∈| (eps 𝒜)|⇧+| ∨ (p, q) |∈| (eps ℬ)|⇧+|" using assms(2, 1)
  by (induct rule: ftrancl_induct)
     (auto simp: ta_union_def ftrancl_into_trancl dest: eps_statesD eps_trancl_statesD)

lemma eps_ta_union_eps [simp]:
  "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ (p, q) |∈| (eps (ta_union 𝒜 ℬ))|⇧+|"
  "(p, q) |∈| (eps ℬ)|⇧+| ⟹ (p, q) |∈| (eps (ta_union 𝒜 ℬ))|⇧+|"
  by (auto simp add: in_ftrancl_UnI ta_union_def)


lemma disj_states_eps [simp]:
  "𝒬 𝒜 |∩| 𝒬 ℬ = {||} ⟹ f ps → p |∈| rules 𝒜 ⟹ (p, q) |∈| (eps ℬ)|⇧+| ⟷ False"
  "𝒬 𝒜 |∩| 𝒬 ℬ = {||} ⟹ f ps → p |∈| rules ℬ ⟹ (p, q) |∈| (eps 𝒜)|⇧+| ⟷  False"
  by (auto simp: rtrancl_eq_or_trancl dest: rule_statesD eps_trancl_statesD)

lemma ta_union_der_disj_states:
  assumes "𝒬 𝒜 |∩| 𝒬 ℬ = {||}" and "q |∈| ta_der (ta_union 𝒜 ℬ) t"
  shows "q |∈| ta_der 𝒜 t ∨ q |∈| ta_der ℬ t" using assms(2)
proof (induct rule: ta_der_induct)
  case (Var q v)
  then show ?case using ta_union_eps_disj_states[OF assms(1)]
    by auto
next
  case (Fun f ts ps p q)
  have dist: "fset_of_list ps |⊆| 𝒬 𝒜 ⟹ i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (ts ! i)"
    "fset_of_list ps |⊆| 𝒬 ℬ ⟹ i < length ts ⟹ ps ! i |∈| ta_der ℬ (ts ! i)" for i
    using Fun(2) Fun(5)[of i] assms(1)
    by (auto dest!: ta_der_not_stateD fsubsetD)
  from Fun(1) consider (a) "fset_of_list ps |⊆| 𝒬 𝒜" | (b) "fset_of_list ps |⊆| 𝒬 ℬ"
    by (auto simp: ta_union_def dest: rule_statesD)
  then show ?case using dist Fun(1, 2) assms(1) ta_union_eps_disj_states[OF assms(1), of p q] Fun(3)
    by (cases) (auto simp: fsubsetI rule_statesD ta_union_def intro!: exI[of _ p] exI[of _ ps])   
qed

lemma ta_union_der_disj_states':
  assumes "𝒬 𝒜 |∩| 𝒬 ℬ = {||}"
  shows "ta_der (ta_union 𝒜 ℬ) t = ta_der 𝒜 t |∪| ta_der ℬ t"
  using ta_union_der_disj_states[OF assms] ta_der_mono' ta_union_ta_subset
  by (auto, fastforce) blast

lemma ta_union_gta_lang:
  assumes "𝒬 𝒜 |∩| 𝒬 ℬ = {||}" and "Q⇩𝒜 |⊆| 𝒬 𝒜" and "Q⇩ℬ |⊆| 𝒬 ℬ"
  shows"gta_lang (Q⇩𝒜 |∪| Q⇩ℬ) (ta_union 𝒜 ℬ) = gta_lang Q⇩𝒜 𝒜 ∪ gta_lang Q⇩ℬ ℬ" (is "?Ls = ?Rs")
proof -
  {fix s assume "s ∈ ?Ls" then obtain q
      where w: "q |∈| Q⇩𝒜 |∪| Q⇩ℬ" "q |∈| ta_der (ta_union 𝒜 ℬ) (term_of_gterm s)"
      by (auto elim: gta_langE)
    from ta_union_der_disj_states[OF assms(1) w(2)] consider
      (a)  "q |∈| ta_der 𝒜 (term_of_gterm s)" | "q |∈| ta_der ℬ (term_of_gterm s)" by blast
    then have "s ∈ ?Rs" using w(1) assms
      by (cases, auto simp: gta_langI)
         (metis fempty_iff finterI funion_iff gterm_ta_der_states sup.orderE)}
  moreover have "?Rs ⊆ ?Ls" using ta_union_der_disj_states'[OF assms(1)]
    by (auto elim!: gta_langE intro!: gta_langI)
  ultimately show ?thesis by blast
qed


lemma ℒ_union: "ℒ (reg_union R L) = ℒ R ∪ ℒ L"
proof -
  let ?inl = "Inl :: 'b ⇒ 'b + 'c" let ?inr = "Inr :: 'c ⇒ 'b + 'c"
  let ?fr = "?inl |`| (fin R |∩| 𝒬⇩r R)" let ?fl = "?inr |`| (fin L |∩| 𝒬⇩r L)"
  have [simp]:"gta_lang (?fr |∪| ?fl) (ta_union (fmap_states_ta ?inl (ta R)) (fmap_states_ta ?inr (ta L))) =
   gta_lang ?fr (fmap_states_ta ?inl (ta R)) ∪ gta_lang ?fl (fmap_states_ta ?inr (ta L))"
    by (intro ta_union_gta_lang) (auto simp: fimage_iff)
  have [simp]: "gta_lang ?fr (fmap_states_ta ?inl (ta R)) = gta_lang (fin R |∩| 𝒬⇩r R) (ta R)"
    by (intro fmap_states_ta_lang) (auto simp: finj_Inl_Inr)
  have [simp]: "gta_lang ?fl (fmap_states_ta ?inr (ta L)) = gta_lang (fin L |∩| 𝒬⇩r L) (ta L)"
    by (intro fmap_states_ta_lang) (auto simp: finj_Inl_Inr)
  show ?thesis
    using gta_lang_Rest_states_conv
    by (auto simp: ℒ_def reg_union_def ta_union_gta_lang) fastforce
qed

lemma reg_union_states:
  "𝒬⇩r (reg_union A B) = (Inl |`| 𝒬⇩r A) |∪| (Inr |`| 𝒬⇩r B)"
  by (auto simp: reg_union_def)

― ‹Deciding emptiness›

lemma ta_empty [simp]:
  "ta_empty Q 𝒜 = (gta_lang Q 𝒜 = {})"
  by (auto simp: ta_empty_def elim!: gta_langE ta_reachable_gtermE
    intro: ta_reachable_gtermI gta_langI)


lemma reg_empty [simp]:
  "reg_empty R = (ℒ R = {})"
  by (simp add: ℒ_def reg_empty_def)

text ‹Epsilon free automaton›

lemma finite_eps_free_rulep [simp]:
  "finite (Collect (eps_free_rulep 𝒜))"
proof -
  let ?par = "(λ r. case r of f qs → q ⇒ (f, qs)) |`| (rules 𝒜)"
  let ?st = "(λ (r, q). case r of (f, qs) ⇒ TA_rule f qs q) |`| (?par |×| 𝒬 𝒜)"
  show ?thesis using rule_statesD eps_trancl_statesD
    by (intro finite_subset[of "Collect (eps_free_rulep 𝒜)" "fset ?st"])
       (auto simp: eps_free_rulep_def fimage_iff
             simp flip: fset.set_map
             split!: ta_rule.splits, fastforce+)
qed

lemmas finite_eps_free_rule [simp] = finite_eps_free_rulep[unfolded eps_free_rulep_def]

lemma ta_res_eps_free:
  "ta_der (eps_free 𝒜) (term_of_gterm t) = ta_der 𝒜 (term_of_gterm t)" (is "?Ls = ?Rs")
proof -
  {fix q assume "q |∈| ?Ls" then have "q |∈| ?Rs"
      by (induct rule: ta_der_gterm_induct)
         (auto simp: eps_free_def eps_free_rulep_def)}
  moreover
  {fix q assume "q |∈| ?Rs" then have "q |∈| ?Ls"
    proof (induct rule: ta_der_gterm_induct)
      case (GFun f ts ps p q)
      then show ?case
        by (auto simp: eps_free_def eps_free_rulep_def intro!: exI[of _ ps])
    qed}
  ultimately show ?thesis by blast
qed

lemma ta_lang_eps_free [simp]:
  "gta_lang Q (eps_free 𝒜) = gta_lang Q 𝒜"
  by (auto simp add: ta_res_eps_free elim!: gta_langE intro: gta_langI)

lemma ℒ_eps_free: "ℒ (eps_free_reg R) = ℒ R"
  by (auto simp: ℒ_def eps_free_reg_def)

text ‹Sufficient criterion for containment›
  (* sufficient criterion to check whether automaton accepts at least T_g(F) where F is a subset of
   the signature *) 

definition ta_contains_aux :: "('f × nat) set ⇒ 'q fset ⇒ ('q, 'f) ta ⇒ 'q fset ⇒ bool" where
  "ta_contains_aux ℱ Q⇩1 𝒜 Q⇩2 ≡ (∀ f qs. (f, length qs) ∈ ℱ ∧ fset_of_list qs |⊆| Q⇩1 ⟶
     (∃ q q'. TA_rule f qs q |∈| rules 𝒜 ∧ q' |∈| Q⇩2 ∧ (q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+|)))"

lemma ta_contains_aux_state_set:
  assumes "ta_contains_aux ℱ Q 𝒜 Q" "t ∈ 𝒯⇩G ℱ"
  shows "∃ q. q |∈| Q ∧ q |∈| ta_der 𝒜 (term_of_gterm t)" using assms(2)
proof (induct rule: 𝒯⇩G.induct)
  case (const a)
  then show ?case using assms(1)
    by (force simp: ta_contains_aux_def)
next
  case (ind f n ss)
  obtain qs where "fset_of_list qs |⊆| Q" "length ss = length qs"
    "∀ i < length qs. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i))"
    using ind(4) Ex_list_of_length_P[of "length ss" "λ q i. q |∈| Q ∧ q |∈| ta_der 𝒜 (term_of_gterm (ss ! i))"]
    by (auto simp: fset_list_fsubset_eq_nth_conv) metis
  then show ?case using ind(1 - 3) assms(1)
    by (auto simp: ta_contains_aux_def) blast
qed

lemma ta_contains_aux_mono:
  assumes "ta_subset 𝒜 ℬ" and "Q⇩2 |⊆| Q⇩2'"
  shows "ta_contains_aux ℱ Q⇩1 𝒜 Q⇩2 ⟹ ta_contains_aux ℱ Q⇩1 ℬ Q⇩2'"
  using assms unfolding ta_contains_aux_def ta_subset_def
  by (meson fin_mono ftrancl_mono)
 
definition ta_contains :: "('f × nat) set ⇒ ('f × nat) set ⇒ ('q, 'f) ta ⇒ 'q fset ⇒ 'q fset ⇒ bool"
  where "ta_contains ℱ 𝒢 𝒜 Q Q⇩f ≡ ta_contains_aux ℱ Q 𝒜 Q ∧ ta_contains_aux 𝒢 Q 𝒜 Q⇩f"

lemma ta_contains_mono:
  assumes "ta_subset 𝒜 ℬ" and "Q⇩f |⊆| Q⇩f'"
  shows "ta_contains ℱ 𝒢 𝒜 Q Q⇩f ⟹ ta_contains ℱ 𝒢 ℬ Q Q⇩f'"
  unfolding ta_contains_def 
  using ta_contains_aux_mono[OF assms(1) fsubset_refl]
  using ta_contains_aux_mono[OF assms]
  by blast

lemma ta_contains_both: 
  assumes contain: "ta_contains ℱ 𝒢 𝒜 Q Q⇩f"
  shows "⋀ t. groot t ∈ 𝒢 ⟹ ⋃ (funas_gterm ` set (gargs t)) ⊆ ℱ ⟹ t ∈ gta_lang Q⇩f 𝒜"
proof -
  fix t :: "'a gterm"
  assume F: "⋃ (funas_gterm ` set (gargs t)) ⊆ ℱ" and G: "groot t ∈ 𝒢"
  obtain g ss where t[simp]: "t = GFun g ss" by (cases t, auto)
  then have "∃ qs. length qs = length ss ∧ (∀ i < length qs. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i)) ∧ qs ! i |∈| Q)"
    using contain ta_contains_aux_state_set[of ℱ Q 𝒜 "ss ! i" for i] F
    unfolding ta_contains_def 𝒯⇩G_funas_gterm_conv
    using Ex_list_of_length_P[of "length ss" "λ q i. q |∈| Q ∧ q |∈| ta_der 𝒜 (term_of_gterm (ss ! i))"]
    by auto (metis SUP_le_iff nth_mem)
  then obtain qs where " length qs = length ss"
    "∀ i < length qs. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i))"
    "∀ i < length qs. qs ! i |∈| Q"
    by blast
  then obtain q where "q |∈| Q⇩f" "q |∈| ta_der 𝒜 (term_of_gterm t)"
    using conjunct2[OF contain[unfolded ta_contains_def]] G
    by (auto simp: ta_contains_def ta_contains_aux_def fset_list_fsubset_eq_nth_conv) metis
  then show "t ∈ gta_lang Q⇩f 𝒜"
    by (intro gta_langI) simp
qed

lemma ta_contains: 
  assumes contain: "ta_contains ℱ ℱ 𝒜 Q Q⇩f"
  shows "𝒯⇩G ℱ ⊆ gta_lang Q⇩f 𝒜" (is "?A ⊆ _")
proof -
  have [simp]: "funas_gterm t ⊆ ℱ ⟹ groot t ∈ ℱ" for t by (cases t) auto
  have [simp]: "funas_gterm t ⊆ ℱ ⟹ ⋃ (funas_gterm ` set (gargs t)) ⊆ ℱ" for t
    by (cases t) auto
  show ?thesis using ta_contains_both[OF contain]
    by (auto simp: 𝒯⇩G_equivalent_def)
qed

text ‹Relabeling, map finite set to natural numbers›


lemma map_fset_to_nat_inj:
  assumes "Y |⊆| X"
  shows "finj_on (map_fset_to_nat X) Y"
proof -
  { fix x y assume "x |∈| X" "y |∈| X"
    then have "x |∈| fset_of_list (sorted_list_of_fset X)" "y |∈| fset_of_list (sorted_list_of_fset X)"
      by simp_all
    note this[unfolded mem_idx_fset_sound]
    then have "x = y" if "map_fset_to_nat X x = map_fset_to_nat X y"
      using that nth_eq_iff_index_eq[OF distinct_sorted_list_of_fset[of X]]
      by (force dest: mem_idx_sound_output simp: map_fset_to_nat_def) }
  then show ?thesis using assms
    by (auto simp add: finj_on_def' fBall_def)
qed

lemma map_fset_fset_to_nat_inj:
  assumes "Y |⊆| X"
  shows "finj_on (map_fset_fset_to_nat X) Y" using assms
proof -
  let ?f = "map_fset_fset_to_nat X"
  { fix x y assume "x |∈| X" "y |∈| X"
    then have "sorted_list_of_fset x |∈| fset_of_list (sorted_list_of_fset (sorted_list_of_fset |`| X))"
      "sorted_list_of_fset y |∈| fset_of_list (sorted_list_of_fset (sorted_list_of_fset |`| X))"
        unfolding map_fset_fset_to_nat_def by auto
    note this[unfolded mem_idx_fset_sound]
    then have "x = y" if "?f x = ?f y"
      using that nth_eq_iff_index_eq[OF distinct_sorted_list_of_fset[of "sorted_list_of_fset |`| X"]]
      by (auto simp: map_fset_fset_to_nat_def)
         (metis mem_idx_sound_output sorted_list_of_fset_simps(1))+}
  then show ?thesis using assms
    by (auto simp add: finj_on_def' fBall_def)
qed


lemma relabel_gta_lang [simp]:
  "gta_lang (relabel_Q⇩f Q 𝒜) (relabel_ta 𝒜) = gta_lang Q 𝒜"
proof -
  have "gta_lang (relabel_Q⇩f Q 𝒜) (relabel_ta 𝒜) = gta_lang (Q |∩| 𝒬 𝒜) 𝒜"
    unfolding relabel_ta_def relabel_Q⇩f_def
    by (intro fmap_states_ta_lang2 map_fset_to_nat_inj) simp
  then show ?thesis by fastforce
qed


lemma ℒ_relable [simp]: "ℒ (relabel_reg R) = ℒ R"
  by (auto simp: ℒ_def relabel_reg_def)

lemma relabel_ta_lang [simp]:
  "ta_lang (relabel_Q⇩f Q 𝒜) (relabel_ta 𝒜) = ta_lang Q 𝒜"
  unfolding ta_lang_to_gta_lang
  using relabel_gta_lang
  by simp



lemma relabel_fset_gta_lang [simp]:
  "gta_lang (relabel_fset_Q⇩f Q 𝒜) (relabel_fset_ta 𝒜) = gta_lang Q 𝒜"
proof -
  have "gta_lang (relabel_fset_Q⇩f Q 𝒜) (relabel_fset_ta 𝒜) = gta_lang (Q |∩| 𝒬 𝒜) 𝒜"
    unfolding relabel_fset_Q⇩f_def relabel_fset_ta_def
    by (intro fmap_states_ta_lang2 map_fset_fset_to_nat_inj) simp
  then show ?thesis by fastforce
qed


lemma ℒ_relable_fset [simp]: "ℒ (relable_fset_reg R) = ℒ R"
  by (auto simp: ℒ_def relable_fset_reg_def)

lemma ta_states_trim_ta:
  "𝒬 (trim_ta Q 𝒜) |⊆| 𝒬 𝒜"
  unfolding trim_ta_def using ta_prod_reach_states .

lemma trim_ta_reach: "𝒬 (trim_ta Q 𝒜) |⊆| ta_reachable (trim_ta Q 𝒜)"
  unfolding trim_ta_def using ta_only_prod_reachable ta_only_reach_reachable
  by metis

lemma trim_ta_prod: "𝒬 (trim_ta Q A) |⊆| ta_productive Q (trim_ta Q A)"
  unfolding trim_ta_def using ta_only_prod_productive
  by metis

lemma empty_gta_lang:
  "gta_lang Q (TA {||} {||}) = {}"
  using ta_reachable_gtermI
  by (force simp: gta_lang_def gta_der_def elim!: ta_langE)

abbreviation empty_reg where
  "empty_reg ≡ Reg {||} (TA {||} {||})"

lemma ℒ_epmty:
  "ℒ empty_reg = {}"
  by (auto simp: ℒ_def empty_gta_lang)

lemma const_ta_lang:
  "gta_lang {|q|} (TA  {| TA_rule f [] q |} {||}) = {GFun f []}"
proof -
  have [dest!]: "q' |∈| ta_der (TA  {| TA_rule f [] q |} {||}) t' ⟹ ground t' ⟹ t' = Fun f []" for t' q'
    by (induct t') auto
  show ?thesis
    by (auto simp: gta_lang_def gta_der_def elim!: gta_langE)
       (metis gterm_of_term.simps list.simps(8) term_of_gterm_inv)
qed


lemma run_argsD:
  "run 𝒜 s t ⟹ length (gargs s) = length (gargs t) ∧ (∀ i < length (gargs t). run 𝒜 (gargs s ! i) (gargs t ! i))"
  using run.cases by fastforce

lemma run_root_rule:
  "run 𝒜 s t ⟹ TA_rule (groot_sym t) (map ex_comp_state (gargs s)) (ex_rule_state s) |∈| (rules 𝒜) ∧
     (ex_rule_state s = ex_comp_state s ∨ (ex_rule_state s, ex_comp_state s) |∈| (eps 𝒜)|⇧+|)"
  by (cases s; cases t) (auto elim: run.cases)

lemma run_poss_eq: "run 𝒜 s t ⟹ gposs s = gposs t"
  by (induct rule: run.induct) auto

lemma run_gsubt_cl:
  assumes "run 𝒜 s t" and "p ∈ gposs t"
  shows "run 𝒜 (gsubt_at s p) (gsubt_at t p)" using assms
proof (induct p arbitrary: s t)
  case (Cons i p) show ?case using Cons(1) Cons(2-)
    by (cases s; cases t) (auto dest: run_argsD)
qed auto

lemma run_replace_at:
  assumes "run 𝒜 s t" and "run 𝒜 u v" and "p ∈ gposs s"
    and "ex_comp_state (gsubt_at s p) = ex_comp_state u"
  shows "run 𝒜 s[p ← u]⇩G t[p ← v]⇩G" using assms
proof (induct p arbitrary: s t)
  case (Cons i p)
  obtain r q qs f ts where [simp]: "s = GFun (r, q) qs" "t = GFun f ts" by (cases s, cases t) auto
  have *: "j < length qs ⟹ ex_comp_state (qs[i := (qs ! i)[p ← u]⇩G] ! j) = ex_comp_state (qs ! j)" for j
    using Cons(5) by (cases "i = j", cases p) auto
  have [simp]: "map ex_comp_state (qs[i := (qs ! i)[p ← u]⇩G]) = map ex_comp_state qs" using Cons(5)
    by (auto simp: *[unfolded comp_def] intro!: nth_equalityI)
  have "run 𝒜 (qs ! i)[p ← u]⇩G (ts ! i)[p ← v]⇩G" using Cons(2-)
    by (intro Cons(1)) (auto dest: run_argsD)
  moreover have "i < length qs" "i < length ts" using Cons(4) run_poss_eq[OF Cons(2)]
    by force+
  ultimately show ?case using Cons(2) run_root_rule[OF Cons(2)]
    by (fastforce simp: nth_list_update dest: run_argsD intro!: run.intros)
qed simp

text ‹relating runs to derivation definition›

lemma run_to_comp_st_gta_der:
  "run 𝒜 s t ⟹ ex_comp_state s |∈| gta_der 𝒜 t"
proof (induct s arbitrary: t)
  case (GFun q qs)
  show ?case using GFun(1)[OF nth_mem, of i "gargs t ! i" for i]
    using run_argsD[OF GFun(2)] run_root_rule[OF GFun(2-)]
    by (cases t) (auto simp: gta_der_def intro!: exI[of _ "map ex_comp_state qs"] exI[of _ "fst q"])
qed

lemma run_to_rule_st_gta_der:
  assumes "run 𝒜 s t" shows "ex_rule_state s |∈| gta_der 𝒜 t"
proof (cases s)
  case [simp]: (GFun q qs)
  have "i < length qs ⟹ ex_comp_state (qs ! i) |∈| gta_der 𝒜 (gargs t ! i)" for i
    using run_to_comp_st_gta_der[of 𝒜] run_argsD[OF assms] by force
  then show ?thesis using conjunct1[OF run_argsD[OF assms]] run_root_rule[OF assms]
    by (cases t) (auto simp: gta_der_def intro!: exI[of _ "map ex_comp_state qs"] exI[of _ "fst q"])
qed

lemma run_to_gta_der_gsubt_at:
  assumes "run 𝒜 s t" and "p ∈ gposs t"
  shows "ex_rule_state (gsubt_at s p) |∈| gta_der 𝒜 (gsubt_at t p)"
    "ex_comp_state (gsubt_at s p) |∈| gta_der 𝒜 (gsubt_at t p)"
  using assms run_gsubt_cl[THEN run_to_comp_st_gta_der] run_gsubt_cl[THEN run_to_rule_st_gta_der]
  by blast+

lemma gta_der_to_run:
  "q |∈| gta_der 𝒜 t ⟹ (∃ p qs. run 𝒜 (GFun (p, q) qs) t)" unfolding gta_der_def
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  from GFun(5) Ex_list_of_length_P[of "length ts" "λ qs i. run 𝒜 (GFun (fst qs, ps ! i) (snd qs)) (ts ! i)"]
  obtain qss where mid: "length qss = length ts" "∀ i < length ts .run 𝒜 (GFun (fst (qss ! i), ps ! i) (snd (qss ! i))) (ts ! i)"
    by auto
  have [simp]: "map (ex_comp_state ∘ (λ(qs, y). GFun (fst y, qs) (snd y))) (zip ps qss) = ps" using GFun(2) mid(1)
    by (intro nth_equalityI) auto
  show ?case using mid GFun(1 - 4)
    by (intro exI[of _ p] exI[of _ "map2 (λ f args. GFun (fst args, f) (snd args)) ps qss"])
       (auto intro: run.intros)
qed

lemma run_ta_der_ctxt_split1:
  assumes "run 𝒜 s t" "p ∈ gposs t"
  shows "ex_comp_state s |∈| ta_der 𝒜 (ctxt_at_pos (term_of_gterm t) p)⟨Var (ex_comp_state (gsubt_at s p))⟩"
  using assms
proof (induct p arbitrary: s t)
  case (Cons i p)
  obtain q f qs ts where [simp]: "s = GFun q qs" "t = GFun f ts" and l: "length qs = length ts"
    using run_argsD[OF Cons(2)] by (cases s, cases t) auto
  from Cons(2, 3) l have "ex_comp_state (qs ! i) |∈| ta_der 𝒜 (ctxt_at_pos (term_of_gterm (ts ! i)) p)⟨Var (ex_comp_state (gsubt_at (qs ! i) p))⟩"
    by (intro Cons(1)) (auto dest: run_argsD)
  then show ?case using Cons(2-) l
    by (fastforce simp: nth_append_Cons min_def dest: run_root_rule run_argsD
    intro!: exI[of _ "map ex_comp_state (gargs s)"]  exI[of _ "ex_rule_state s"]
            run_to_comp_st_gta_der[of 𝒜 "qs ! i" "ts ! i" for i, unfolded comp_def gta_der_def])
qed auto


lemma run_ta_der_ctxt_split2:
  assumes "run 𝒜 s t" "p ∈ gposs t"
  shows "ex_comp_state s |∈| ta_der 𝒜 (ctxt_at_pos (term_of_gterm t) p)⟨Var (ex_rule_state (gsubt_at s p))⟩"
proof (cases "ex_rule_state (gsubt_at s p) = ex_comp_state (gsubt_at s p)")
  case False then show ?thesis
    using run_root_rule[OF run_gsubt_cl[OF assms]]
    by (intro ta_der_eps_ctxt[OF run_ta_der_ctxt_split1[OF assms]]) auto
qed (auto simp: run_ta_der_ctxt_split1[OF assms, unfolded comp_def])

end