Theory Regular_Tree_Relations.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])

(*