theory Tree_Automata
imports
Certification_Monads.Check_Monad TRS.Multihole_Context
UL.FSet_Util GR.Ground_Terms
begin
lemma finite_vars_ctxt: "finite (vars_ctxt C)"
by (induct C) auto
context
includes fset.lifting
begin
lemma finite_funs_term:
"finite (funs_term t)"
by (induct t) auto
lift_definition ffuns_term :: "('f, 'v) term ⇒ 'f fset" is funs_term using finite_funs_term
by blast
lift_definition fvars_term :: "('f, 'v) term ⇒ 'v fset" is vars_term by simp
lift_definition fvars_ctxt :: "('f, 'v) ctxt ⇒ 'v fset" is vars_ctxt by (simp add: finite_vars_ctxt)
lemmas fvars_term_ctxt_apply [simp] = vars_term_ctxt_apply[Transfer.transferred]
lemmas fvars_term_of_gterm [simp] = vars_term_of_gterm[Transfer.transferred]
lemmas map_fvars_term_fvars_term = map_vars_term_vars_term[Transfer.transferred]
lemmas fground_vars_term_empty = ground_vars_term_empty[Transfer.transferred]
lemma ffuns_term_Var [simp]: "ffuns_term (Var x) = {||}"
by transfer auto
lemma fffuns_term_Fun [simp]: "ffuns_term (Fun f ts) = |⋃| (ffuns_term |`| fset_of_list ts) |∪| {|f|}"
by transfer auto
lemma fvars_term_Var [simp]: "fvars_term (Var x) = {|x|}"
by transfer auto
lemma fvars_term_Fun [simp]: "fvars_term (Fun f ts) = |⋃| (fvars_term |`| fset_of_list ts)"
by transfer auto
lemmas ground_fvars_term_empty = ground_vars_term_empty[Transfer.transferred]
lift_definition ffunas_term :: "('f, 'v) term ⇒ ('f × nat) fset" is funas_term
by (simp add: finite_funas_term)
lift_definition ffunas_gterm :: "'f gterm ⇒ ('f × nat) fset" is funas_gterm
by (simp add: finite_funas_gterm)
lemmas ffunas_term_simps [simp] = funas_term.simps[Transfer.transferred]
lemmas ffunas_gterm_simps [simp] = funas_gterm.simps[Transfer.transferred]
lemmas ffunas_term_of_gterm_conv = funas_term_of_gterm_conv[Transfer.transferred]
lemmas ffunas_gterm_gterm_of_term = funas_gterm_gterm_of_term[Transfer.transferred]
lemmas ftrancl_map_both_fRestr = trancl_map_both_Restr[Transfer.transferred]
lemma ftrancl_map_both_fsubset:
"finj_on f X ⟹ R |⊆| X |×| X ⟹ (map_both f |`| R)|⇧+| = map_both f |`| R|⇧+|"
using ftrancl_map_both_fRestr[of f X R]
by (simp add: inf_absorb1)
lemmas ftrancl_map_prod_mono = trancl_map_prod_mono[Transfer.transferred]
lemmas ftrancl_map = trancl_map[Transfer.transferred]
subsection ‹Basic definitions and Lemmas›
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")
datatype ('q, 'f) reg = Reg (fin: "'q fset") (ta: "('q, 'f) ta")
"srules 𝒜 = fset (rules 𝒜)"">definition "srules 𝒜 = fset (rules 𝒜)"
"seps 𝒜 = fset (eps 𝒜)"">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 finite_Collect_ta_rule:
"finite {TA_rule f qs q | f qs q. TA_rule f qs q |∈| rules 𝒜}"
proof -
have [simp]: "{TA_rule f qs q | f qs q. TA_rule f qs q |∈| rules 𝒜} = (srules 𝒜)"
apply transfer apply (auto simp: srules_def)
by (metis ta_rule.exhaust)
show ?thesis by (auto simp: srules_def)
qed
lemma TA_equalityI:
"rules 𝒜 = rules ℬ ⟹ eps 𝒜 = eps ℬ ⟹ 𝒜 = ℬ"
using ta.expand by blast
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 Δ⇩ε ≡ |⋃| ((λ (q,q'). {|q,q'|}) |`| Δ⇩ε)"
"𝒬 𝒜 = rule_states (rules 𝒜) |∪| eps_states (eps 𝒜)"">definition "𝒬 𝒜 = rule_states (rules 𝒜) |∪| eps_states (eps 𝒜)"
"𝒬_r 𝒜 ≡ 𝒬 (ta 𝒜)"">abbreviation "𝒬⇩r 𝒜 ≡ 𝒬 (ta 𝒜)"
lemma rule_states [code]:
"rule_states Δ = |⋃| ((λ r. finsert (r_rhs r) (fset_of_list (r_lhs_states r))) |`| Δ)"
unfolding rule_states_def
by transfer auto
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 transfer auto
lemma rule_states_mono:
"Δ |⊆| Γ ⟹ rule_states Δ |⊆| rule_states Γ"
unfolding rule_states_def
by transfer auto
lemma eps_states_union [simp]:
"eps_states (Δ |∪| Γ) = eps_states Δ |∪| eps_states Γ"
unfolding eps_states_def
by transfer auto
lemma eps_states_mono:
"Δ |⊆| Γ ⟹ eps_states Δ |⊆| eps_states Γ"
unfolding eps_states_def
by transfer auto
lemma eps_states_image [simp]:
"eps_states (map_both f |`| Δ⇩ε) = f |`| eps_states Δ⇩ε"
unfolding eps_states_def map_prod_def
by transfer fastforce
lemma eps_statesI [intro, simp]:
"(p, q) |∈| Δ ⟹ p |∈| eps_states Δ"
"(p, q) |∈| Δ ⟹ q |∈| eps_states Δ"
unfolding eps_states_def
by (transfer, auto)+
lemma eps_statesE [elim]:
assumes "p |∈| eps_states Δ"
obtains q where "(p, q) |∈| Δ ∨ (q, p) |∈| Δ" using assms
unfolding eps_states_def
by (transfer, auto)+
declare eps_transfer[transfer_rule del]
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 (auto simp: 𝒬_def rule_states_def fimage_iff)
(transfer, force simp: srules_def)+
declare eps_transfer[transfer_rule]
lemma eps_states [simp]: "(eps 𝒜) |⊆| 𝒬 𝒜 |×| 𝒬 𝒜"
unfolding 𝒬_def eps_states_def rule_states_def
by transfer auto
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
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, unfolded fmember.rep_eq[symmetric]]
lemmas map_ta_rule_states_finite [simp] = map_ta_rule_finite[of "fset Δ" id for Δ, simplified, unfolded fmember.rep_eq[symmetric]]
lemmas map_ta_rule_funsym_finite [simp] = map_ta_rule_finite[of "fset Δ" _ id for Δ, simplified, unfolded fmember.rep_eq[symmetric]]
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
apply (metis ta_rule.collapse ta_rule.simps(4) fimage_eqI ta_rule.map)+
done
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 Δ"
unfolding map_ta_rule_iff rule_states_def
apply transfer apply (auto simp: image_def map_ta_rule_finite)
apply fastforce apply fastforce
apply (metis image_eqI list.set_map ta_rule.collapse ta_rule.sel(2))
by (metis ta_rule.collapse ta_rule.map_sel(3) ta_rule.simps(4))
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 notin_fset rule_statesD(2))
from finite_subset[OF this] show ?thesis by auto
qed
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 𝒜)|⇧+|)|}"
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 notin_fset rule_statesD(1))+
from finite_subset[OF this] show ?thesis
by auto
qed
"ta_sig 𝒜 = (λ r. (r_root r, length (r_lhs_states r))) |`| (rules 𝒜)"">definition "ta_sig 𝒜 = (λ r. (r_root r, length (r_lhs_states r))) |`| (rules 𝒜)"
lemma ta_sigI [intro]:
"TA_rule f qs q |∈| (rules 𝒜) ⟹ length qs = n ⟹ (f, n) |∈| ta_sig 𝒜" unfolding ta_sig_def
by transfer (force simp: srules_def image_def)
lemma ta_sig_mono:
"(rules 𝒜) |⊆| (rules ℬ) ⟹ ta_sig 𝒜 |⊆| ta_sig ℬ"
by (auto simp: ta_sig_def)
subsection ‹Multiple definitions of reachability of states from terms›
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))|}"
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))|}"
lemma finite_eps:
"finite {q. ∃ f ps p. f ps → p |∈| rules 𝒜 ∧ (p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)}"
proof -
have t: "(seps 𝒜)⇧+ `` r_rhs ` srules 𝒜 ∪ r_rhs ` srules 𝒜 = {q. ∃f ps p. f ps → p ∈ srules 𝒜 ∧ (p = q ∨ (p, q) ∈ (seps 𝒜)⇧+)}"
by (auto simp: seps_def srules_def rev_image_eqI)
(metis ta_rule.collapse)+
have "finite (r_rhs ` srules 𝒜)" by (auto simp: srules_def)
then have "finite ((seps 𝒜)⇧+ `` r_rhs ` srules 𝒜 ∪ r_rhs ` srules 𝒜)"
by (auto simp: seps_def)
then show ?thesis unfolding t
by transfer simp
qed
lemma ta_der_Var:
"q |∈| ta_der 𝒜 (Var x) ⟷ x = q ∨ (x, q) |∈| (eps 𝒜)|⇧+|"
unfolding ta_der.simps
by transfer (auto simp: seps_def)
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 𝒜)|⇧+|"
unfolding ta_der'.simps
by transfer (auto simp: seps_def finite_snd)
end
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))}"
apply (intro finite_subset[OF _ f])
apply (auto simp flip: fset_of_list_elem fmember.rep_eq)
by (metis fBexI fset_of_list_elem in_set_idx nth_mem)
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
subsubsection ‹Various kinds of 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"
apply (induct t)
apply (auto dest: ftrancl_mono[of _ "eps 𝒜" "eps ℬ"])
apply (metis fin_mono nth_mem)
by (meson fsubsetD ftrancl_mono nth_mem)
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'_varposs_to_ta_der:
assumes "t |∈| ta_der' 𝒜 s" and "p ∈ varposs t"
shows "the_Var (subt_at t p) |∈| ta_der 𝒜 (subt_at s p)"
using assms
by (induct s arbitrary: t p) (auto simp: ta_der'.simps, blast+)
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)
subsubsection ‹Connecting contexts and multihole contexts to mixed terms›
lemma eps_ta_der'_ctxtcl:
assumes "(p, q) |∈| (eps 𝒜)|⇧+|"
shows "C⟨Var q⟩ |∈| ta_der' 𝒜 C⟨Var p⟩" using assms
by (induct C) (auto simp: nth_append_Cons)
lemma ta_der'_empty_step:
assumes "t |∈| ta_der' 𝒜 (term_of_gterm s)" and "vars_term t = {}"
shows "t = (term_of_gterm s)" using assms
by (induct s arbitrary: t) (auto simp: ta_der'.simps intro!: nth_equalityI)
lemma ta_der'_empty_step_fvars:
assumes "t |∈| ta_der' 𝒜 (term_of_gterm s)" and "fvars_term t = {||}"
shows "t = (term_of_gterm s)"
using ta_der'_empty_step[OF assms(1)] assms(2)
by (metis bot_fset.rep_eq fvars_term.rep_eq)
lemma ta_der'_eps_eq_split_vars:
assumes "t |∈| ta_der' 𝒜 s" and "rules 𝒜 = {||}"
shows "fst (split_vars t) = fst (split_vars s)" using assms
by (induct s arbitrary: t) (auto simp: ta_der'.simps comp_def map_eq_conv')
lemma ta_der'_inf_split_vars:
assumes "t |∈| ta_der' 𝒜 s"
shows "fst (split_vars t) ≤ fst (split_vars s)" using assms
proof (induct s arbitrary: t)
case (Fun f ts) then show ?case
by (cases t) (auto simp: comp_def less_eq_mctxt_prime intro: less_eq_mctxt'.intros)
qed (auto simp: ta_der'.simps)
lemma ta_der'_inf_mctxt:
assumes "t |∈| ta_der' 𝒜 s"
shows "fst (split_vars t) ≤ (mctxt_of_term s)" using assms
proof (induct s arbitrary: t)
case (Fun f ts) then show ?case
by (cases t) (auto simp: comp_def less_eq_mctxt_prime intro: less_eq_mctxt'.intros)
qed (auto simp: ta_der'.simps)
lemma ta_der'_mctxt_args:
assumes "t |∈| ta_der' 𝒜 s"
shows "unfill_holes (fst (split_vars t)) s = map ((|_) s) (varposs_list t)"
using unfill_holes_to_subst_at_hole_poss[OF ta_der'_inf_mctxt[OF assms]]
unfolding hole_poss_split_vars_varposs_list
by auto
lemma ta_der'_fill_holes:
assumes "t |∈| ta_der' 𝒜 s"
shows "fill_holes (fst (split_vars t)) (map ((|_) s) (varposs_list t)) = s"
using ta_der'_mctxt_args[OF assms] fill_unfill_holes[OF ta_der'_inf_mctxt[OF assms]]
by auto
lemma mctxt_args_ta_der':
assumes "num_holes C = length qs" "num_holes C = length ss"
and "∀ i < length ss. qs ! i |∈| ta_der 𝒜 (ss ! i)"
shows "(fill_holes C (map Var qs)) |∈| ta_der' 𝒜 (fill_holes C ss)" using assms
proof (induct rule: fill_holes_induct2)
case MHole then show ?case
by (cases ss; cases qs) (auto simp: ta_der_to_ta_der')
next
case (MFun f ts) then show ?case
by (simp add: partition_by_nth_nth(1, 2))
qed auto
lemma ta_der'_fill_holes_args:
assumes "Var q |∈| ta_der' 𝒜 (fill_holes C ts)"
and len: "num_holes C = length ts"
shows "∃ qs. length qs = length ts ∧ (∀ i < length ts. qs ! i |∈| ta_der 𝒜 (ts ! i)) ∧
Var q |∈| ta_der' 𝒜 (fill_holes C (map Var qs))" using len assms(1)
proof (induct arbitrary: q rule: fill_holes_induct)
case (MHole x) then show ?case
by (auto simp: ta_der_to_ta_der' intro: exI[of _ "[q]"])
next
case (MFun f Cs xs)
let ?Nth = "λ i. fill_holes (Cs ! i) (partition_holes (concat (partition_holes xs Cs)) Cs ! i)"
let ?P = "λ q qs i. length qs = length (partition_holes xs Cs ! i) ∧
(∀j < length (partition_holes xs Cs ! i). qs ! j |∈| ta_der 𝒜 (partition_holes xs Cs ! i ! j)) ∧
Var q |∈| ta_der' 𝒜 (fill_holes (Cs ! i) (map Var qs))"
from MFun (3) obtain ps p where
rule: "f ps → p |∈| rules 𝒜" "length ps = length Cs" and
eps: "p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|" and steps: "∀ i < length ps. ps ! i |∈| ta_der 𝒜 (?Nth i)"
by auto
from MFun have "i < length Cs ⟹ ∃ qs. ?P (ps ! i) qs i" for i
using rule steps unfolding ta_der_to_ta_der'
by auto
from this Ex_list_of_length_P[of "length Cs" "λ qs i. ?P (ps ! i) qs i"] obtain qs where
IH: "length qs = length Cs" "∀ i < length qs. ?P (ps ! i) (qs ! i) i"
by auto
note inv = this[unfolded ta_der_to_ta_der'[symmetric]]
have [simp]: "i < length Cs ⟹ (partition_holes (map Var (concat qs)) Cs ! i) = map Var (qs ! i)" for i using inv
by (metis MFun.hyps(1) length_partition_holes_nth map_partition_holes_nth partition_holes_concat_id)
have "i < length (concat (partition_holes xs Cs)) ⟹ i < length (concat qs)" for i
using IH MFun(1) by (auto, metis length_concat nth_map_conv)
then show ?case using inv
using concat_index_split_sound_bounds[of _ qs]
using concat_index_split_unique[of _ qs "partition_holes xs Cs" 0]
using steps rule eps unfolding partition_holes_fill_holes_conv
apply (intro exI[of _ "concat qs"])
apply (auto simp: concat_index_split_sound eq_length_concat_nth
split: prod.splits intro!: exI[of _ p] exI[of _ ps])
apply blast+
done
qed auto
subsubsection ‹Connecting contexts and multihole contexts to derivation definition›
lemma ta_der_ctxt:
assumes p: "p |∈| ta_der 𝒜 t"
shows "q |∈| ta_der 𝒜 (C ⟨ Var p ⟩) ⟹ q |∈| ta_der 𝒜 (C ⟨ t ⟩)"
apply (induct C arbitrary: q)
apply (auto simp add: p ta_der_trancl_eps)
apply (metis append_Cons_nth_not_middle nth_append_length)+
done
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 take_drop_imp_nth 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 ⟩)"
proof -
from ta_der'_fill_holes_args[OF assms[unfolded ta_der_to_ta_der' eqfE(1)[OF mctxt_of_ctxt[of C]]]]
obtain p where "p |∈| ta_der 𝒜 t ∧ Var q |∈| ta_der' 𝒜 (fill_holes (mctxt_of_ctxt C) [Var p])"
by (auto, case_tac qs, auto)
then show ?thesis using eqfE[OF mctxt_of_ctxt[of C]]
by (metis ta_der'_to_ta_der)
qed
lemma ta_der_fill_holes:
assumes "q |∈| ta_der 𝒜 (fill_holes C ts)"
and len: "num_holes C = length ts"
shows "∃ qs. length qs = length ts ∧ (∀ i < length ts. qs ! i |∈| ta_der 𝒜 (ts ! i)) ∧
q |∈| ta_der 𝒜 (fill_holes C (map Var qs))"
using assms ta_der'_fill_holes_args[OF _ len] unfolding ta_der_to_ta_der'
by blast
lemma fill_holes_ta_der:
assumes "length ss = num_holes C" "length qs = num_holes C"
"⋀i. i < num_holes C ⟹ qs ! i |∈| ta_der 𝒜 (ss ! i)"
"q |∈| ta_der 𝒜 (fill_holes C (map Var qs))"
shows "q |∈| ta_der 𝒜 (fill_holes C ss)"
using assms mctxt_args_ta_der' ta_der'_fill_holes_args unfolding ta_der_to_ta_der'
by (intro ta_der'_trans[OF _ assms(4)[unfolded ta_der_to_ta_der']])
(simp add: assms(3) mctxt_args_ta_der')
lemma ta_der_states:
"ta_der 𝒜 t |⊆| 𝒬 𝒜 |∪| fvars_term t"
proof (induct t)
case (Var x) then show ?case
by auto (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 ground_fvars_term_empty by force
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 |⊆| 𝒬 𝒜"
apply (induct t arbitrary: q rule: term_fset_induct)
apply (auto simp: eps_trancl_statesD dest!: in_fset_idx)
using fnth_mem rule_statesD(4) apply fastforce+
done
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
apply (cases t) apply auto apply force
apply (metis ftranclE)
done
context
includes fset.lifting
begin
lemma r_set_statesI:
assumes "q |∈| rule_states Δ"
obtains h qs q' where "TA_rule h qs q' |∈| Δ" "q = q' ∨ q |∈| fset_of_list qs"
using assms unfolding rule_states_def
apply transfer apply auto
apply (metis ta_rule.collapse)+
done
lemma target_to_rule:
assumes "q |∈| rule_target_states Δ"
obtains f qs where "TA_rule f qs q |∈| Δ" using assms
apply transfer apply auto
apply (metis ta_rule.collapse)
done
lemma ta_rhs_states_subset_states: "ta_rhs_states 𝒜 |⊆| 𝒬 𝒜"
by (auto simp: ta_rhs_states_def dest: rtranclD rule_statesD eps_trancl_statesD)
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
apply transfer apply (auto simp: srules_def seps_def, force)
by (metis ta_rule.sel(3))
qed
end
subsection ‹Reachable states of ground terms are preserved over the 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
lemma ta_der_term_sig:
"q |∈| ta_der 𝒜 t ⟹ ffunas_term t |⊆| ta_sig 𝒜"
by (induct t arbitrary: q rule: term_idx_induct)
(fastforce dest!: in_fset_idx)+
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
subsection ‹ta_lang for terms with arbitrary variable type›
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 ≠ {||}}"
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)
subsection ‹ta_lang for gterms›
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 𝒜)"
lemma ta_lang_to_gta_lang [simp]:
"ta_lang Q 𝒜 = term_of_gterm ` gta_lang Q 𝒜"
unfolding image_comp gta_lang_def
apply (auto simp: adapt_vars2 ta_langI gterm_of_term_inv' image_def comp_def gta_der_def elim!: ta_langE)
apply (metis fempty_iff finterI gterm_of_term_inv gterm_of_term_inv')
by (metis adapt_vars_term_of_gterm ground_term_of_gterm ta_langI)
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 𝒜"
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)
lemma gta_lang_subset_rules_funas:
"gta_lang Q 𝒜 ⊆ 𝒯⇩G (fset (ta_sig 𝒜))"
using ta_der_gterm_sig
by (auto simp: 𝒯⇩G_equivalent_def elim!: gta_langE)
(smt ffunas_gterm.rep_eq in_mono less_eq_fset.rep_eq ta_der_gterm_sig)
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
by (auto simp: 𝒯⇩G_equivalent_def funas_term_of_gterm_conv)
(smt ffunas_term_of_gterm_conv fsubsetD gta_langE ta_der_gterm_sig)
lemma gta_lang_Rest_states_conv:
"gta_lang Q 𝒜 = gta_lang (Q |∩| 𝒬 𝒜) 𝒜"
by (auto elim!: gta_langE)
definition reg_Restr_Q⇩f where
"reg_Restr_Q⇩f R = Reg (fin R |∩| 𝒬⇩r R) (ta R)"
lemma reg_Rest_fin_states:
"ℒ (reg_Restr_Q⇩f 𝒜) = ℒ 𝒜"
using gta_lang_Rest_states_conv
by (auto simp: ℒ_def reg_Restr_Q⇩f_def)
subsection ‹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')"
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)
"ta_subset 𝒜 ℬ ⟷ rules 𝒜 |⊆| rules ℬ ∧ eps 𝒜 |⊆| eps ℬ"">definition "ta_subset 𝒜 ℬ ⟷ rules 𝒜 |⊆| rules ℬ ∧ eps 𝒜 |⊆| eps ℬ"
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
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)"
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 fin_mono 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 _ 𝒜])
subsection ‹Reachable and productive states: There always is a trim automaton›
definition ta_reachable :: "('q, 'f) ta ⇒ 'q fset" where
"ta_reachable 𝒜 = {|q| q. ∃ t. ground t ∧ q |∈| ta_der 𝒜 t |}"
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 (metis fsubsetD notin_fset)
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)
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 |}"
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 (metis notin_fset)
next
case False
then show ?thesis using ass
by (cases C, auto, (metis eps_trancl_statesD notin_fset)+)
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
definition ta_trim :: "'q fset ⇒ ('q, 'f) ta ⇒ bool" where
"ta_trim P 𝒜 ≡ ∀ q. q |∈| 𝒬 𝒜 ⟶ q |∈| ta_reachable 𝒜 ∧ q |∈| ta_productive P 𝒜"
abbreviation ta_only_reach :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
"ta_only_reach 𝒜 ≡ ta_restrict 𝒜 (ta_reachable 𝒜)"
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 𝒜"
apply (auto simp: ta_reachable_def ta_rhs_states_def)
apply (case_tac t) apply auto
done
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
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 (smt ffUnionI fimage_eqI fnth_mem fsubsetD)
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)
(auto simp flip: subseteq_set_conv_nth dest: in_fset_idx 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 add: fground_vars_term_empty)}
ultimately show ?thesis
by (force simp: ta_reachable_def)
qed
lemma ta_only_reach_reachable:
"𝒬 (ta_only_reach 𝒜) |⊆| ta_reachable (ta_only_reach 𝒜)"
using ta_restrict_states_Q[of 𝒜 "ta_reachable 𝒜"]
by auto
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+
definition reg_reach where
"reg_reach R = Reg (fin R) (ta_only_reach (ta R))"
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)
abbreviation ta_only_prod :: "'q fset ⇒ ('q,'f) ta ⇒ ('q,'f) ta" where
"ta_only_prod P 𝒜 ≡ ta_restrict 𝒜 (ta_productive P 𝒜)"
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
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 dest!: in_fset_idx 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)
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
definition reg_prod where
"reg_prod R = Reg (fin R) (ta_only_prod (fin R) (ta R))"
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)
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 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 𝒜)"
using ta_reachableI ta_reachableE ta_der_only_prod ta_only_prod_productive[of 𝒜 P]
using fsubset_trans[OF ta_restrict_states all_reach, of "ta_productive P 𝒜"]
by (smt fsubset_iff ta_prodictive_ta_only_prod)
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])
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
guess C' using More(1)[OF q'(3)] ..
then show ?case using ts q'(1,2,4)
apply (intro exI[of _ "More f (map ts [0..<length ts1]) C' (map ts [Suc (length ts1)..<Suc (length ts1 + length ts2)])"]
conjI)
subgoal by auto
unfolding ctxt_apply_term.simps ta_der.simps
apply (intro fCollect_memberI exI[of _ q, OF exI[of _ q', OF exI[of _ qs]]] finite_subset[OF _ finite_states, of _ 𝒜])
by (auto simp: nth_append_Cons not_le not_less Suc_le_eq elim: less_SucE)
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+
definition trim_ta :: "'q fset ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta" where
"trim_ta P 𝒜 = ta_only_prod P (ta_only_reach 𝒜)"
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_trim Q (trim_ta Q 𝒜)" unfolding ta_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)
definition trim_reg where
"trim_reg R = Reg (fin R) (trim_ta (fin R) (ta R))"
lemma ℒ_trim: "ℒ (trim_reg R) = ℒ R"
by (auto simp: trim_gta_lang ℒ_def trim_reg_def)
lemmas obtain_trimmed_ta = trim_ta trim_gta_lang ta_subset_det[OF trim_ta_subset]
thm obtain_trimmed_ta
subsection ‹Map function over TA rules which change states/signature›
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))"
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: fBex_def fmap_states_ta_def ta_sig_def fimage_iff)
(metis id_def length_map ta_rule.map_sel(1, 2))+
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
by (auto simp: fimage_iff ftrancl_map_both_fsubset[OF assms(2), of "eps 𝒜"] finj_on_def')
(metis (mono_tags, lifting) eps_trancl_statesD fbspec)
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_conv' 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 fmember.rep_eq
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 fmember.rep_eq 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_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 dest!: in_fset_idx) 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]
show ?case using Fun(3)
apply (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)
using root(2) by auto
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_funs_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_funs_term)
definition refin_fin_reg where
"refin_fin_reg R = Reg (fin R |∩| 𝒬⇩r R) (ta R)"
lemma fin_in_states:
"fin (refin_fin_reg R) |⊆| 𝒬⇩r (refin_fin_reg R)"
by (auto simp: refin_fin_reg_def)
lemma fmap_states_reg_refin_fin_reg_fin:
"finj_on f (𝒬 𝒜) ⟹ fin (fmap_states_reg f (refin_fin_reg R)) |⊆| 𝒬⇩r (fmap_states_reg f (refin_fin_reg R))"
by (auto simp: fmap_states_reg_def refin_fin_reg_def)
lemma refin_fin_reg_lang [simp]:
"ℒ (refin_fin_reg R) = ℒ R"
by (metis ℒ_def gta_lang_Rest_states_conv refin_fin_reg_def reg.sel(1, 2))
subsection ‹Product automata›
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]
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 fmember.rep_eq 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
lemma prod_ta_zip [code]:
"prod_ta_rules 𝒜 𝔅 =
(λ (ra, rb). case ra of f ps → p ⇒ case rb of f qs → q ⇒ f (zip ps qs) → (p, q)) |`|
ffilter (λ (ra, rb). case ra of f ps → p ⇒ case rb of g qs → q ⇒ f = g ∧ length ps = length qs)
(rules 𝒜 |×| rules 𝔅)" (is "?Ls = ?Rs")
proof -
{fix r assume ass: "r |∈| ?Ls"
then obtain f qs q where [simp]: "r = f qs → q" by auto
then have "r |∈| ?Rs" using ass
by (auto simp: ffilter_simp fimage_iff zip_map_fst_snd fBex_def simp flip: fmember.rep_eq
intro!: exI[of _ "TA_rule f (map fst qs) (fst q)"] exI[of _ "TA_rule f (map snd qs) (snd q)"]
finite_subset[OF _ finite_fset[of "rules 𝒜 |×| rules 𝔅"]])}
moreover
{fix r assume ass: "r |∈| ?Rs" then have "r |∈| ?Ls"
by (auto simp: ffilter_simp fimage_iff finite_Collect_prod_ta_rules split!: ta_rule.splits)
}
ultimately show ?thesis by blast
qed
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 |∈| 𝒬 𝒜)"
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 simp flip: fmember.rep_eq 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 simp flip: fmember.rep_eq dest: eps_statesD)
lemmas finite_prod_eps [simp] = finite_prod_epsLp[unfolded prod_epsLp_def] finite_prod_epsRp[unfolded prod_epsRp_def]
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 𝒜 ℬ))"
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 r_set_statesI)
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 ℬ"
by (auto simp add: ta_sig_def fimage_iff fBall_def)+
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)
definition reg_intersect where
"reg_intersect R L = Reg (fin R |×| fin L) (prod_ta (ta R) (ta L))"
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)
subsection ‹Union of tree automata›
definition ta_union where
"ta_union 𝒜 ℬ = TA (rules 𝒜 |∪| rules ℬ) (eps 𝒜 |∪| eps ℬ)"
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 simp flip: fsubseteq_fset_conv_nth)
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
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)))"
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)
subsection ‹Deciding emptiness›
definition ta_empty :: "'q fset ⇒ ('q,'f) ta ⇒ bool" where
"ta_empty Q 𝒜 ⟷ ta_reachable 𝒜 |∩| Q |⊆| {||}"
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)
subsection ‹Epsilon free automaton›
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 𝒜)|⇧+|))"
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 fmember.rep_eq
split!: ta_rule.splits, fastforce+)
qed
lemmas finite_eps_free_rule [simp] = finite_eps_free_rulep[unfolded eps_free_rulep_def]
definition eps_free :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
"eps_free 𝒜 = TA (fCollect (eps_free_rulep 𝒜)) {||}"
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)
definition reg_eps_free where
"reg_eps_free R = Reg (fin R) (eps_free (ta R))"
lemma ℒ_eps_free: "ℒ (reg_eps_free R) = ℒ R"
by (auto simp: ℒ_def reg_eps_free_def)
subsection ‹Sufficient criterion for containment›
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 flip: fsubseteq_fset_conv_nth) 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 simp flip: fsubseteq_fset_conv_nth) 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
subsection ‹Basic lemmas for combining tree automata with rewriting›
lemma ta_der_subst:
assumes x: "⋀ x. x |∈| fvars_term t ⟹ σ x |∈| ta_der' 𝒜 (τ x)"
and q: "q |∈| ta_der 𝒜 (t ⋅ σ)"
shows "q |∈| ta_der 𝒜 (t ⋅ τ)" using q x
proof (induct t arbitrary: q)
case (Var x)
then show ?case using ta_der'_trans
by (simp add: ta_der_trancl_eps ta_der_to_ta_der') blast
next
case (Fun f ts) from Fun(2)
obtain ps p where rule: "f ps → p |∈| rules 𝒜"
and len: "length ps = length ts" and eps: "p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|"
and rec: "⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 ((ts ! i) ⋅ σ)"
by auto
from rec len have "i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (ts ! i ⋅ τ)" for i
using Fun(1)[OF nth_mem, of i "ps ! i"] Fun(3)
by (simp add: fBexI)
then show ?case using len rule eps
by (auto intro: exI[of _ p] exI[of _ ps])
qed
context
includes fset.lifting
begin
lemma ta_der_subst_linear:
assumes l: "linear_term t" and q: "q |∈| ta_der 𝒜 (t ⋅ τ)"
obtains σ where "q |∈| ta_der 𝒜 (map_vars_term σ t)" "∀ x |∈| fvars_term t. σ x |∈| ta_der 𝒜 (τ x)"
proof -
assume ass: "(⋀σ. q |∈| ta_der 𝒜 (map_vars_term σ t) ⟹ ∀x|∈|fvars_term t. σ x |∈| ta_der 𝒜 (τ x) ⟹ thesis)"
let ?P = "λ σ p t. p |∈| ta_der 𝒜 (map_vars_term σ t) ∧ (∀ x |∈| fvars_term t. σ x |∈| ta_der 𝒜 (τ x))"
have "∃ σ. ?P σ q t" using l q
proof (induct t arbitrary: q)
case (Fun f ts) from Fun(3)
obtain ps p where rule: "f ps → p |∈| rules 𝒜"
and len: "length ps = length ts" and eps: "p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|"
and rec: "⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 ((ts ! i) ⋅ τ)"
by auto
from Fun(1)[OF nth_mem] Fun(2) rec
have "∀ i. ∃ σ. i < length ts ⟶ ?P σ (ps ! i) (ts ! i)" by auto
from choice[OF this] obtain σ where
ind: "⋀ i. i < length ts ⟹ ?P (σ i) (ps ! i) (ts ! i)"
by auto
from Fun(2) have "is_partition (map vars_term ts)" by auto
from subst_merge[OF this, of σ] obtain σ2 where σ2:
"⋀ i. i < length ts ⟹ ∀ x |∈| fvars_term (ts ! i). σ2 x = σ i x"
by transfer auto
then show ?case using rule len eps rec ind
by (auto simp: fBall_def intro!: exI[of _ σ2] exI[of _ p] exI[of _ ps])
(metis map_fvars_term_fvars_term in_fset_idx)+
qed auto
then show ?thesis using ass by blast
qed
end
lemma ta_der_subst_det: fixes τ 𝒜
defines "σ ≡ (λ x. SOME q. q |∈| ta_der 𝒜 (τ x))"
assumes det: "ta_det 𝒜" and q: "q |∈| ta_der 𝒜 (t ⋅ τ)"
shows "q |∈| ta_der 𝒜 (map_vars_term σ t) ∧ (∀ x |∈| fvars_term t. σ x |∈| ta_der 𝒜 (τ x))" using q
proof (induct t arbitrary: q)
case (Var x)
then show ?case using det
by (auto simp: σ_def intro: someI)
next
case (Fun f ts)
from Fun(2) obtain q' qs where rule: "TA_rule f qs q' |∈| rules 𝒜"
and len: "length qs = length ts"
and rec: "⋀i. i < length ts ⟹ qs ! i |∈| ta_der 𝒜 (ts ! i ⋅ τ)"
and q: "q' = q ∨ (q',q) |∈| (eps 𝒜)|⇧+|"
by auto
then have ind: "i < length ts ⟹ qs ! i |∈| ta_der 𝒜 (map_vars_term σ (ts ! i))"
"i < length ts ⟹ (∀ x |∈| fvars_term (ts ! i). σ x |∈| ta_der 𝒜 (τ x))" for i
using Fun(1)[OF nth_mem, of i "qs ! i" for i]
by auto
then show ?case using rule rec q len
by (auto simp: in_fset_conv_nth fBall_def)
qed
lemma ta_der_subst_linear_det:
assumes ld: "linear_term t ∨ ta_det 𝒜"
and q: "q |∈| ta_der 𝒜 (t ⋅ τ)"
shows "∃ σ. q |∈| ta_der 𝒜 (map_vars_term σ t) ∧ (∀ x |∈| fvars_term t. σ x |∈| ta_der 𝒜 (τ x))" using ld
proof
assume lin: "linear_term t"
from ta_der_subst_linear[OF this q] obtain σ where
"q |∈| ta_der 𝒜 (map_vars_term σ t)" "∀x|∈|fvars_term t. σ x |∈| ta_der 𝒜 (τ x)"
by blast
then show ?thesis by blast
next
assume "ta_det 𝒜"
from ta_der_subst_det[OF this q] show ?thesis by - (rule exI)
qed
subsection ‹Relabeling›
subsection ‹map finite set 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))))"
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 notin_fset sorted_list_of_fset_simps(1))+}
then show ?thesis using assms
by (auto simp add: finj_on_def' fBall_def)
qed
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 |∩| 𝒬 𝒜)"
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
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))"
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
definition relabel_fset_fset_ta :: "(('q :: linorder) fset, 'f) ta ⇒ (nat, 'f) ta" where
"relabel_fset_fset_ta 𝒜 = fmap_states_ta (map_fset_fset_to_nat (𝒬 𝒜)) 𝒜"
definition relabel_fset_fset_Q⇩f :: "('q :: linorder) fset fset ⇒ (('q :: linorder) fset, 'f) ta ⇒ nat fset" where
"relabel_fset_fset_Q⇩f Q 𝒜 = map_fset_fset_to_nat (𝒬 𝒜) |`| (Q |∩| 𝒬 𝒜)"
lemma relabel_fset_fset_gta_lang [simp]:
"gta_lang (relabel_fset_fset_Q⇩f Q 𝒜) (relabel_fset_fset_ta 𝒜) = gta_lang Q 𝒜"
proof -
have "gta_lang (relabel_fset_fset_Q⇩f Q 𝒜) (relabel_fset_fset_ta 𝒜) = gta_lang (Q |∩| 𝒬 𝒜) 𝒜"
unfolding relabel_fset_fset_Q⇩f_def relabel_fset_fset_ta_def
by (intro fmap_states_ta_lang2 map_fset_fset_to_nat_inj) simp
then show ?thesis by fastforce
qed
definition relable_fset_reg :: "(('q :: linorder) fset, 'f) reg ⇒ (nat, 'f) reg" where
"relable_fset_reg R = Reg (relabel_fset_fset_Q⇩f (fin R) (ta R)) (relabel_fset_fset_ta (ta R))"
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
end