# 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

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

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

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

"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

"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) ≠ {||}}"

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

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

(*