section ‹Stuff about tree automata›
theory Tree_Automata_Utils
imports TA.Tree_Automata Ground_Terms Basic_Utils
begin
lemma if_cong':
"b = c ⟹ x = u ⟹ y = v ⟹ (if b then x else y) = (if c then u else v)"
by auto
subsection ‹Trivialities›
lemma ta_lang_imp_ground [simp]:
"t ∈ ta_lang A ⟹ ground t"
by (elim ta_langE2)
lemma ta_res_adapt_vars_ground [simp]:
"ground t ⟹ ta_res A (adapt_vars t) = ta_res 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
subsection ‹Alternative definition of @{const ta_productive}›
lemma ta_productive_aux:
assumes "ta_states A ⊆ ta_reachable A" "q ∈ ta_res A (C⟨t⟩)"
shows "∃C'. ground_ctxt C' ∧ q ∈ ta_res A (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' ∈ ta_rules A" "(q', q) ∈ (ta_eps A)⇧*"
"qs ! length ts1 ∈ ta_res A (C⟨t⟩)" "length qs = Suc (length ts1 + length ts2)"
by simp (metis length_map less_add_Suc1 nth_append_length)
{ fix i assume "i < length qs"
then have "qs ! i ∈ ta_states A" using q'(1)
by (simp add: ta_states_def r_states_def r_lhs_states_def) (metis nth_mem)
then have "∃t. ground t ∧ qs ! i ∈ ta_res A t" using assms(1) by (metis rev_subsetD ta_reachableE) }
then obtain ts where ts: "i < length qs ⟹ ground (ts i) ∧ qs ! i ∈ ta_res A (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_res.simps
by (intro CollectI exI[of _ q, OF exI[of _ q', OF exI[of _ qs]]])
(auto simp: nth_append_Cons not_le not_less Suc_le_eq elim: less_SucE)
qed
lemma ta_productive_def':
assumes "ta_states A ⊆ ta_reachable A"
shows "ta_productive A = {q |q q' C. ground_ctxt C ∧ q' ∈ ta_res A (C⟨Var q⟩) ∧ q' ∈ ta_final A}"
using ta_productive_aux[OF assms] by (fastforce simp: ta_productive_def)
text ‹Properties of @{term adapt_vars}›
lemma adapt_vars_inj [simp]:
assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
shows "x = y"
using adapt_vars_adapt_vars assms by metis
lemma funs_term_adapt_vars [simp]:
"funs_term (adapt_vars t) = funs_term t"
by (induct t) (auto simp: adapt_vars_def)
lemma adapt_vars_idemp:
"ground t ⟹ adapt_vars (adapt_vars t) = adapt_vars t"
by (induct t) auto
lemma adapt_vars_id:
"ground t ⟹ adapt_vars t = t"
by (induct t) (auto intro!: nth_equalityI)
lemma adapt_vars_in_ta_lang_conv [simp]:
"adapt_vars t ∈ ta_lang A ⟷ t ∈ ta_lang A"
unfolding ta_lang_def
using adapt_vars_idemp adapt_vars_reverse ground_adapt_vars by blast
hide_const (open) make
lemma ta_make_simps [simp]:
"ta_rules (ta.make Q⇩f Δ ℰ) = Δ"
"ta_eps (ta.make Q⇩f Δ ℰ) = ℰ"
"ta_final (ta.make Q⇩f Δ ℰ) = Q⇩f"
"ta.make Q⇩f Δ ℰ = ta.make Q⇩f' Δ' ℰ' ⟷ Q⇩f = Q⇩f' ∧ Δ = Δ' ∧ ℰ = ℰ'"
by (simp_all add: ta.make_def)
subsection ‹Renaming automata symbols›
definition fmap_funs_ta :: "('f ⇒ 'g) ⇒ ('a, 'f) ta ⇒ ('a, 'g) ta" where
"fmap_funs_ta h A = ta.make (ta_final A) {(h f) qs → q |f qs q. f qs → q ∈ ta_rules A} (ta_eps A)"
definition funs_ta :: "('q, 'f) ta ⇒ 'f set" where
"funs_ta A = {f |f qs q. f qs → q ∈ ta_rules A}"
lemma fmap_funs_ta_cong [cong]:
"(⋀x. x ∈ funs_ta A ⟹ h x = k x) ⟹ A = B ⟹ fmap_funs_ta h A = fmap_funs_ta k B"
by (force simp: fmap_funs_ta_def funs_ta_def)
lemma fmap_funs_ta_id [simp]:
"fmap_funs_ta id A = A"
proof -
have [simp]: "{f qs → q |f qs q. f qs → q ∈ X} = X" for X by (intro set_eqI; case_tac x) auto
show ?thesis by (simp add: fmap_funs_ta_def)
qed
lemma fmap_states_ta_def':
"fmap_states_ta f A = ta.make (f ` ta_final A) (map_ta_rule f id ` ta_rules A) (map_prod f f ` ta_eps A)"
proof -
have [simp]: "map_ta_rule f id = case_ta_rule (λg qs q. g (map f qs) → f q)"
by (auto split: ta_rule.splits)
show ?thesis
by (auto simp: fmap_states_ta_def ta.make_def[symmetric])
qed
lemma fmap_states_ta_id [simp]:
"fmap_states_ta id A = A"
by (cases A) (auto simp: fmap_states_ta_def split: ta_rule.splits)
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"
by (auto simp: fmap_funs_ta_def)
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 image_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_def fmap_funs_ta_def)
lemma ta_states_fmap_states_ta [simp]:
"ta_states (fmap_states_ta f A) = f ` ta_states A"
by (cases A) (simp add: fmap_states_ta_def ta_states_def image_Un case_prod_eta prod.case_distrib
image_UN r_states_def ta_rule.case_distrib r_rhs_def r_lhs_states_def cong: ta_rule.case_cong)
lemma ta_res_funs_ta:
"q ∈ ta_res A t ⟹ funs_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 subsetD] Fun(2) by (auto dest!: in_set_idx)
qed auto
lemma ta_lang_funs_ta:
"t ∈ ta_lang A ⟹ funs_term t ⊆ funs_ta A"
by (elim ta_langE) (simp add: ta_res_funs_ta)
lemma ta_res_fmap_funs_ta:
"q ∈ ta_res A t ⟹ q ∈ ta_res (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_res_fmap_states_ta:
assumes "q ∈ ta_res A t"
shows "h q ∈ ta_res (fmap_states_ta h A) (map_vars_term h t)"
proof -
have [intro]: "(q, q') ∈ (ta_eps A)⇧* ⟹ (h q, h q') ∈ (ta_eps (fmap_states_ta h A))⇧*" for q q'
by (force intro!: rtrancl_map[of "ta_eps A"] simp: fmap_states_ta_def)
show ?thesis using assms
proof (induct t arbitrary: q)
case (Fun f ts)
obtain q' qs where *: "f qs → q' ∈ ta_rules A" "(q', q) ∈ (ta_eps A)⇧*" "length qs = length ts"
"⋀i. i < length ts ⟹ qs ! i ∈ ta_res A (ts ! i)" using Fun(2) by auto
have "f (map h qs) → h q' ∈ ta_rules (fmap_states_ta h A)"
using *(1) by (force simp: fmap_states_ta_def)
then show ?case using Fun(1)[OF nth_mem *(4)] *(2,3) by (auto 0 4)
qed auto
qed
lemma ta_res_fmap_states_ta_mono:
shows "f ` ta_res A (term_of_gterm s) ⊆ ta_res (fmap_states_ta f A) (term_of_gterm s)"
using ta_res_fmap_states_ta[of _ A "term_of_gterm s" f]
by (metis image_subsetI map_vars_term_term_of_gterm)
lemma ta_res_fmap_states_ta_mono2:
assumes "inj f"
shows "ta_res (fmap_states_ta f A) (term_of_gterm s) ⊆ f ` ta_res A (term_of_gterm s)"
using ta_res_fmap_states_inv[of f A "term_of_gterm s"]
by (smt adapt_vars_term_of_gterm assms ground_term_of_gterm image_eqI inj_on_by_inj subsetI)
lemma fmap_funs_ta_res':
"q ∈ ta_res (fmap_funs_ta h A) t ⟹ ∃t'. q ∈ ta_res A t' ∧ map_funs_term h t' = t"
proof (induct t arbitrary: q)
case (Var x) then show ?case by (auto simp: fmap_funs_ta_def intro!: exI[of _ "Var x"])
next
case (Fun f ts)
obtain f' qs q' where f': "f = h f'" "f' qs → q' ∈ ta_rules A" "(q', q) ∈ (ta_eps A)⇧*"
"length qs = length ts" "⋀i. i < length ts ⟹ qs ! i ∈ ta_res (fmap_funs_ta h A) (ts ! i)"
using Fun(2) by (auto simp: fmap_funs_ta_def)
obtain ts' where "⋀i. i < length ts ⟹ qs ! i ∈ ta_res A (ts' i) ∧ map_funs_term h (ts' i) = ts ! i"
using Fun(1)[OF nth_mem f'(5)] by metis
note [simp] = conjunct1[OF this] conjunct2[OF this, unfolded id_def]
show ?case by (auto simp: comp_def f'(1,2,3,4)
intro!: exI[of _ "Fun f' (map ts' [0..<length ts])"] exI[of _ qs] exI[of _ q'] nth_equalityI)
qed
lemma fmap_funs_ta_lang:
"ta_lang (fmap_funs_ta h A) = map_funs_term h ` ta_lang A"
proof ((intro set_eqI iffI; elim imageE ta_langE2), goal_cases lr rl)
case (lr t q)
obtain t' where t': "q ∈ ta_res A t'" "adapt_vars t = map_funs_term h t'"
using lr(3) by (auto dest!: fmap_funs_ta_res')
have [simp]: "adapt_vars (map_funs_term h t') = map_funs_term h (adapt_vars t')"
by (simp add: adapt_vars_def term.map_comp comp_def)
have "t' ∈ ta_lang A" using t'(1) lr(1,2)
arg_cong[OF t'(2), of ground, unfolded id_def, symmetric]
by (auto simp: fmap_funs_ta_def adapt_vars_id intro!: ta_langI[where q = q])
then show ?case using lr(1) arg_cong[OF t'(2), of "adapt_vars :: _ ⇒ ('a, 'b) term"]
by (auto intro!: rev_image_eqI[of "adapt_vars t'"])
next
case (rl t t' q)
have "q ∈ ta_res (fmap_funs_ta h A) (adapt_vars (map_funs_term h t'))"
using ta_res_fmap_funs_ta[OF rl(4), of h] by (simp add: adapt_vars_def term.map_comp comp_def)
then show ?case using rl(2,3) unfolding rl(1)
by (intro ta_langI2[of "map_funs_term h t'" q]) (auto simp: id_def fmap_funs_ta_def)
qed
lemma ta_states_fmap_funs_ta [simp]:
"ta_states (fmap_funs_ta f A) = ta_states A"
by (auto 0 4 simp: fmap_funs_ta_def ta_states_def r_states_def r_rhs_def r_lhs_states_def split: ta_rule.splits)
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_res' ta_res_fmap_funs_ta ground_map_funs_term)
lemma ta_res_gterm_states:
"q ∈ ta_res 𝒜 (term_of_gterm t) ⟹ q ∈ ta_states 𝒜"
by (meson ground_term_of_gterm subsetD ta_res_states)
subsection ‹epsilon-closure of tree automata›
definition eps_closure :: "('q, 'f) ta ⇒ 'q ⇒ 'q set" where
"eps_closure 𝒜 q = { q'. (q,q') ∈ (ta_eps 𝒜)^* }"
definition eps_elim :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
"eps_elim 𝒜 = (ta.make (ta_final 𝒜)
(ta_rules 𝒜 ∪ { rule . (∃fs qs q' q. rule = fs qs → q' ∧
fs qs → q ∈ ta_rules 𝒜 ∧ q' ∈ eps_closure 𝒜 q) }) {})"
text ‹The following theorem shows that epsilon-elimination of a
tree automaton preserves its language.›
lemma ta_lang_eps_elim:
fixes 𝒜 :: "('q, 'f) ta"
shows "ta_lang (eps_elim 𝒜) = ta_lang 𝒜"
proof -
{ fix q t
assume asm: "q ∈ ta_res (eps_elim 𝒜) t" "ground t"
hence "q ∈ ta_res 𝒜 t"
proof (induction t arbitrary: q)
case (Fun f ts)
then obtain q' qs where seq_props: "(f qs → q') ∈ ta_rules (eps_elim 𝒜)"
"(q',q) ∈ ((ta_eps (eps_elim 𝒜))^*)" "length qs = length ts"
"∀ i < length ts. qs ! i ∈ (map (ta_res (eps_elim 𝒜)) ts) ! i"
using asm by auto
have "ta_eps (eps_elim 𝒜) = {}" unfolding eps_elim_def make_def by auto
then have "q = q'" using seq_props(2) by simp
then obtain p where rule': "(f qs → p) ∈ ta_rules 𝒜" "(p,q) ∈ ((ta_eps 𝒜)^*)"
using seq_props(1) unfolding eps_elim_def make_def eps_closure_def
by fastforce
{ fix i
assume "i < length ts"
hence "qs ! i ∈ (map (ta_res 𝒜) ts) ! i"
using Fun(1)[of "ts ! i" "qs ! i"] Fun(2-) seq_props(3,4)
by force
}
thus ?case using eps_elim_def rule' seq_props(3) Fun by auto
qed simp
}
moreover { fix q t
assume asm: "q ∈ ta_res 𝒜 t" "ground t"
hence "q ∈ ta_res (eps_elim 𝒜) t"
proof (induction t arbitrary: q)
case (Fun f ts)
then obtain q' qs where seq_props: "(f qs → q') ∈ ta_rules 𝒜"
"(q',q) ∈ ((ta_eps 𝒜)^*)" "length qs = length ts"
"∀ i < length ts. qs ! i ∈ (map (ta_res 𝒜) ts) ! i"
using asm by auto
then have rule': "(f qs → q) ∈ ta_rules (eps_elim 𝒜)"
unfolding eps_elim_def make_def eps_closure_def by auto
{ fix i
assume "i < length ts"
hence "qs ! i ∈ (map (ta_res (eps_elim 𝒜)) ts) ! i"
using Fun(1)[of "ts ! i" "qs ! i"] Fun(2-) seq_props(3,4)
by force
}
thus ?case using eps_elim_def rule' seq_props(3) Fun by auto
qed simp
}
ultimately have res_eq: "ground t ⟶ ta_res 𝒜 t = ta_res (eps_elim 𝒜) t"
for t
by blast
have final_eq: "ta_final (eps_elim 𝒜) = ta_final 𝒜"
unfolding eps_elim_def make_def by auto
{
fix tv :: "('f, 'v) term"
assume asm: "tv ∈ ta_lang 𝒜"
obtain t where t: "tv = adapt_vars (t::('f,'q) term)"
using asm adapt_vars_adapt_vars ta_langE2
by metis
hence ground_t: "ground t" using asm ta_langE3 by blast
hence "ta_final 𝒜 ∩ ta_res 𝒜 t ≠ {}" using t asm unfolding ta_lang_def
using adapt_vars_inj by blast
hence "ta_final (eps_elim 𝒜) ∩ ta_res (eps_elim 𝒜) t ≠ {}"
using ground_t res_eq[of t] final_eq by auto
hence "tv ∈ ta_lang (eps_elim 𝒜)"
using t asm ground_t unfolding ta_lang_def by blast
}
hence lang_incl: "ta_lang 𝒜 ⊆ ta_lang (eps_elim 𝒜)"
using subsetI by auto
{ fix tv :: "('f, 'v) term"
assume asm: "tv ∈ ta_lang (eps_elim 𝒜)"
obtain t where t: "tv = adapt_vars (t::('f,'q) term)"
using asm adapt_vars_adapt_vars ta_langE2
by metis
hence ground_t:"ground t" using asm ta_langE3 by blast
hence "ta_final (eps_elim 𝒜) ∩ ta_res (eps_elim 𝒜) t ≠ {}"
using t asm adapt_vars_inj unfolding ta_lang_def by blast
hence "ta_final 𝒜 ∩ ta_res 𝒜 t ≠ {}"
using ground_t res_eq[of t] final_eq by auto
hence "tv ∈ ta_lang 𝒜"
using t asm ground_t unfolding ta_lang_def by blast
}
hence "ta_lang (eps_elim 𝒜) ⊆ ta_lang 𝒜"
using subsetI by auto
thus ?thesis using lang_incl by blast
qed
lemma ta_res_eps_ctxt:
assumes "p ∈ ta_res A C⟨Var q'⟩" and "(q, q') ∈ (ta_eps A)⇧*"
shows "p ∈ ta_res A C⟨Var q⟩"
using assms by (metis mem_Collect_eq ta_res.simps(1) ta_res_ctxt)
fun ta_res' :: "('q,'f)ta ⇒ ('f,'q)term ⇒ ('f,'q)term set" where
"ta_res' TA (Var q) = {p. ∃q'. p = Var q' ∧ (q, q') ∈ (ta_eps TA)^*}"
| "ta_res' TA (Fun f ts) = {q. ∃q'. q = Var q' ∧ q' ∈ ta_res TA (Fun f ts)} ∪
{t. ∃ss. t = Fun f ss ∧ length ss = length ts ∧
(∀i < length ts. ss ! i ∈ ta_res' TA (ts ! i))}"
lemma ta_res'_ta_res:
assumes "t ∈ ta_res' TA s" "p ∈ ta_res TA t"
shows "p ∈ ta_res TA s"
using assms
proof (induction arbitrary: p t rule: ta_res'.induct)
case (2 TA f ts) show ?case using 2(2-)
proof (induction t)
case (Var q)
show ?thesis using ta_res_ctxt[of q TA "Fun f ts" p □] Var by simp
next
case (Fun g ss)
have ss_props: "g = f" "length ss = length ts" "∀i < length ts. ss ! i ∈ ta_res' TA (ts ! i)"
using Fun(2) by (auto elim!: ta_res'.cases)
obtain qs p' where qs_props: "(g qs → p') ∈ ta_rules TA ∧
(p',p) ∈ (ta_eps TA)⇧* ∧ length qs = length ss ∧
(∀i < length ss. qs ! i ∈ (map (ta_res TA) ss) ! i)"
using Fun(3) by auto
{ fix i
assume asm: "i < length ts"
hence ss_i_ts_i: "ss ! i ∈ ta_res' TA (ts ! i)" using ss_props by blast
have "qs ! i ∈ ta_res TA (ts ! i)"
using Fun(3) 2(1)[OF asm ss_i_ts_i, of "qs ! i"] asm ss_props(2) qs_props by force
}
hence "∀i<length ts. qs ! i ∈ ta_res TA (ts ! i)"
using ss_props(1,2) by blast
thus ?thesis using qs_props unfolding ss_props by auto
qed
qed force
lemma ta_res_ta_res':
assumes "q ∈ ta_res TA s"
shows "Var q ∈ ta_res' TA s"
using assms by (induct s arbitrary: q) auto
lemma ta_res'_varposs_to_ta_res:
assumes "t ∈ ta_res' TA s" and "p ∈ varposs t"
shows "the_Var (subt_at t p) ∈ ta_res TA (subt_at s p)"
using assms by (induct s arbitrary: t p) (auto, blast)
lemma ta_res'_refl[simp]: "t ∈ ta_res' TA t"
by (induction t) fastforce+
lemma ta_res'_eps:
assumes "Var p ∈ ta_res' 𝒜 s" and "(p, q) ∈ (ta_eps 𝒜)⇧*"
shows "Var q ∈ ta_res' 𝒜 s" using assms
by (cases s, auto) (meson rtrancl_trans)
lemma ta_res'_trans:
assumes "t ∈ ta_res' 𝒜 s" and "u ∈ ta_res' 𝒜 t"
shows "u ∈ ta_res' 𝒜 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
next
case [simp]: (Fun g ss)
show ?thesis using IS IH
by auto (meson ta_res'_refl ta_res'_ta_res)
qed
qed (auto simp: ta_res'_eps)
lemma ta_eps_ta_res'_ctxtcl:
assumes "(p, q) ∈ (ta_eps 𝒜)⇧*"
shows "C⟨Var q⟩ ∈ ta_res' 𝒜 C⟨Var p⟩" using assms
by (induct C) (auto simp: nth_append_Cons)
fun ta_res_strict :: "('q,'f)ta ⇒ ('f,'q)term ⇒ 'q set" where
"ta_res_strict TA (Var q) = {q}"
|"ta_res_strict TA (Fun f ts) = {q' | q' q qs. (f qs → q) ∈ ta_rules TA ∧ (q,q') ∈ (ta_eps TA)⇧* ∧
length qs = length ts ∧ (∀ i < length ts. qs ! i ∈ (map (ta_res_strict TA) ts) ! i)}"
lemma ta_res_strict_sub_ta_res:
"ta_res_strict 𝒜 t ⊆ ta_res 𝒜 t"
apply (induct t, auto) using nth_mem by blast
lemma ta_res_strict_ta_res_eq_on_ground:
assumes"ground t"
shows "ta_res 𝒜 t = ta_res_strict 𝒜 t"
proof
{fix q assume "q ∈ ta_res 𝒜 t"
then have "q ∈ ta_res_strict 𝒜 t" using assms
proof (induct t arbitrary: q)
case (Fun f ts)
then show ?case apply auto
using nth_mem by blast
qed auto}
then show "ta_res 𝒜 t ⊆ ta_res_strict 𝒜 t" by auto
next
show "ta_res_strict 𝒜 t ⊆ ta_res 𝒜 t" using ta_res_strict_sub_ta_res .
qed
lemma ta_res_strict_fun:
assumes "q ∈ ta_res_strict 𝒜 t" and "t ⊳ Var p"
shows "p ∈ ⋃ ((set ∘ r_lhs_states) ` ta_rules 𝒜)" using assms
proof (induct t arbitrary: q)
case (Fun f ts)
from Fun(3) obtain u where w: "u ∈ set ts" "u ⊵ Var p" by auto
then show ?case
proof (cases "u ⊳ Var p")
case True
show ?thesis using Fun(1)[OF w(1) _ True] Fun(2) in_set_idx[OF w(1)]
by auto
next
case False
then have [simp]: "u = Var p" using w(2) by auto
then obtain i where w: "i < length ts" "ts ! i = u" using in_set_idx[OF w(1)] by auto
then obtain f qs q' where r: "f qs → q' ∈ ta_rules 𝒜" "length ts = length qs"
"qs ! i ∈ ta_res_strict 𝒜 (ts ! i)" using Fun(2) by auto
moreover have "qs ! i ∈ set (r_lhs_states (f qs → q))" using r(1, 2) w(1) by simp
ultimately show ?thesis using w(1) r(2) by (auto simp add: w(2)) force
qed
qed auto
lemma ta_res_strict_ctxt:
assumes "p ∈ ta_res_strict A t" and "q ∈ ta_res_strict A C⟨Var p⟩"
shows "q ∈ ta_res_strict A C⟨t⟩"
using assms
proof (induct C arbitrary: q)
case (More f ss C ts)
from More(3) obtain qs q1 q' where
r: "f qs → q' ∈ ta_rules A" "length qs = Suc (length ss + length ts)" "(q', q) ∈ (ta_eps A)⇧*" and
wit: "q1 ∈ ta_res_strict A C⟨Var p⟩" "∃ i < length qs. qs ! i = q1" and
rec: "∀ i < length qs. qs ! i ∈ map (ta_res_strict A) (ss @ C⟨Var p⟩ #ts) ! i"
by auto (metis length_map less_add_Suc1 nth_append_length)
from More(1)[OF More(2) wit(1)] wit(2) r rec
show ?case
by (auto intro!: exI[of _ f] exI[of _ q'] exI[of _ qs])
(metis More.hyps append_Cons_nth_not_middle assms(1) nth_append_length)
qed auto
lemma ta_res_to_ta_strict:
assumes "q ∈ ta_res A C⟨Var p⟩" and "ground_ctxt C"
shows "∃ q'. (p, q') ∈ (ta_eps A)⇧* ∧ q ∈ ta_res_strict A C⟨Var q'⟩"
using assms
proof (induct C arbitrary: q p)
case (More f ss C ts)
from More(2) obtain qs q' where
r: "f qs → q' ∈ ta_rules A" "length qs = Suc (length ss + length ts)" "(q', q) ∈ (ta_eps A)⇧*" and
rec: "∀ i < length qs. qs ! i ∈ map (ta_res A) (ss @ C⟨Var p⟩ # ts) ! i"
by auto
from More(1)[of "qs ! length ss" p] More(3) rec r(2) obtain q'' where
mid: "(p, q'') ∈ (ta_eps A)⇧* ∧ qs ! length ss ∈ ta_res_strict A C⟨Var q''⟩"
by auto (metis length_map less_add_Suc1 nth_append_length)
then have "∀ i < length qs. qs ! i ∈ ta_res_strict A ((ss @ C⟨Var q''⟩ # ts) ! i)" using rec r(2) More(3)
by (auto simp: nth_append_Cons all_Suc_conv ta_res_strict_ta_res_eq_on_ground split:if_splits cong: if_cong')
then show ?case using rec r conjunct1[OF mid]
by (rule_tac x = q'' in exI, auto intro!: exI[of _ q'] exI[of _ qs])
(metis add_Suc add_diff_inverse_nat length_map less_antisym nat_add_left_cancel_less nth_append_Cons nth_map)
qed auto
lemma ta_res_strict_ctxt_intermediate_state:
assumes "p ∈ ta_res_strict A C⟨t⟩"
shows "∃ q. q ∈ ta_res_strict A t ∧ p ∈ ta_res_strict A C⟨Var q⟩"
using assms
proof (induct C arbitrary: p)
case (More f ss C ts) note IS = this
have [simp]: "¬ i < length (ss :: ('b, 'a) term list) ⟶ i < Suc (length ss) ⟶ qs ! i = (q :: 'a) ⟷ qs ! length ss = q" for ss i qs q
using less_antisym by blast
show ?case
proof (cases "C = Hole")
case True
then show ?thesis using IS(2) ta_res_strict_ctxt
by (cases ts) (auto simp: add_diff_inverse_nat
nth_append_Cons singleton_iff append_Cons_nth_not_middle split!: if_splits)
next
case False
obtain qs q' where r: "f qs → q' ∈ ta_rules A" "(q', p) ∈ (ta_eps A)⇧*" "length qs = Suc (length ss + length ts)" and
wit: "qs ! length ss ∈ ta_res_strict A C⟨t⟩" and
reach: "∀ i < length qs. qs ! i ∈ map (ta_res_strict A) (ss @ C⟨t⟩ # ts) ! i" using IS(2)
by (auto simp: add_diff_inverse_nat nth_append_Cons singleton_iff append_Cons_nth_not_middle)
(metis length_map less_add_Suc1 nat_neq_iff)
then show ?thesis using IS(1)[OF wit] r
by auto (metis append_Cons_nth_not_middle length_map nth_append_length)
qed
qed auto
lemma ta_eps_states: "ta_eps 𝒜 ⊆ ta_states 𝒜 × ta_states 𝒜"
unfolding ta_states_def by auto
lemma finite_ta_statesI:
assumes "finite (ta_final TA)" and "finite (ta_rules TA)" and "finite (ta_eps TA)"
shows "finite (ta_states TA)"
using assms unfolding ta_states_def r_states_def insert_def by auto
definition eps_free :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
"eps_free TA = ta.make (ta_final TA) {f qs → q' |f qs q q'. f qs → q ∈ ta_rules TA ∧ (q, q') ∈ (ta_eps TA)⇧*} {}"
lemma ta_res_eps_free [simp]:
"ground t ⟹ ta_res (eps_free TA) t = ta_res TA t"
by (induct t) (auto simp: eps_free_def)
lemma ta_lang_eps_free [simp]:
"ta_lang (eps_free TA) = ta_lang TA"
by (simp only: ta_lang_def ta_res_eps_free cong: conj_cong) (simp add: eps_free_def)
subsection ‹ta_lang for gterms›
definition gta_res where
"gta_res = (λA t. ta_res A (term_of_gterm t))"
definition gta_lang where
"gta_lang = (λA :: ('q, _) ta. gterm_of_term ` (ta_lang A :: (_, 'q) term set))"
lemma gta_lang_to_ta_lang:
"term_of_gterm ` gta_lang A = ta_lang A"
unfolding image_comp gta_lang_def
apply (auto simp: gterm_of_term_inv' image_def comp_def)
by (metis adapt_vars_adapt_vars ta_lang_imp_ground adapt_vars_in_ta_lang_conv)
lemma term_of_gterm_in_ta_lang_conv:
"term_of_gterm t ∈ ta_lang A ⟷ t ∈ gta_lang A"
by (smt gta_lang_to_ta_lang image_iff term_of_gterm_inv)
lemma gta_lang_def_sym:
"gterm_of_term ` ta_lang A = gta_lang A"
unfolding gta_lang_def image_def
by (intro Collect_cong) (metis gta_lang_def gterm_of_term_inv ta_lang_imp_ground
term_of_gterm_in_ta_lang_conv imageI term_of_gterm_inv)
lemma fmap_funs_gta_lang:
shows "gta_lang (fmap_funs_ta f A) = map_gterm f ` gta_lang A"
unfolding gta_lang_def arg_cong[OF fmap_funs_ta_lang, of "λT. gterm_of_term ` T"]
by (simp add: image_comp comp_def cong: image_cong)
lemma gta_langI:
assumes "q ∈ ta_final 𝒜" and "q ∈ ta_res 𝒜 (term_of_gterm t)"
shows "t ∈ gta_lang 𝒜" 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:
assumes "t ∈ gta_lang 𝒜"
obtains q where "q ∈ ta_final 𝒜" and "q ∈ ta_res 𝒜 (term_of_gterm t)"
using assms
by (metis adapt_vars_term_of_gterm ta_langE2 term_of_gterm_in_ta_lang_conv)
lemma gta_lang_mono:
assumes "⋀ t. ta_res 𝒜 t ⊆ ta_res 𝔅 t"
and "ta_final 𝒜 ⊆ ta_final 𝔅"
shows "gta_lang 𝒜 ⊆ gta_lang 𝔅"
using assms by (auto elim!: gta_langE intro!: gta_langI)
lemma inj_fmap_states_presv_gta_lang:
assumes "inj_on f (ta_states 𝒜)"
shows "gta_lang (fmap_states_ta f 𝒜) = gta_lang 𝒜" (is "gta_lang ?A = _")
proof -
{fix t assume "t ∈ gta_lang ?A"
then obtain q where "q ∈ ta_final ?A" "q ∈ ta_res ?A (term_of_gterm t)"
by (auto elim: gta_langE)
then have "t ∈ gta_lang 𝒜" using ta_res_fmap_states_inv[OF assms, of "term_of_gterm t" q]
by (auto simp add: fmap_states_ta_def' intro!: gta_langI)
(smt Un_iff adapt_vars_term_of_gterm assms ground_term_of_gterm inj_onD subsetD ta_res_states ta_states_def)}
moreover
{fix t assume "t ∈ gta_lang 𝒜"
then have "t ∈ gta_lang ?A"
by (metis assms fmap_ta(2) gta_lang_def_sym)}
ultimately show ?thesis by auto
qed
subsection ‹Relabeling›
definition relabel_ta :: "('q :: linorder, 'f) ta ⇒ (nat, 'f) ta" where
"relabel_ta A = fmap_states_ta (map_set_to_nat (ta_states A)) A"
lemma relabel_gta_lang [simp]:
"finite (ta_states A) ⟹ gta_lang (relabel_ta A) = gta_lang A"
unfolding relabel_ta_def gta_lang_def
by (simp add: fmap_ta(2) map_set_to_nat_inj gta_lang_def_sym)
lemma finite_relabel_ta [simp]:
"finite (ta_states A) ⟹ finite (ta_states (relabel_ta A))"
unfolding relabel_ta_def by simp
lemma ta_states_trim_ta:
"ta_states (trim_ta A) ⊆ ta_states A"
unfolding trim_ta_def using ta_prod_reach_states .
lemmas finite_trim_ta [simp] = finite_subset[OF ta_states_trim_ta]
lemma empty_ta_lang:
"gta_lang (ta.make {} {} {}) = {}"
by (auto simp: gta_lang_def elim!: ta_langE)
lemma const_ta_lang:
"gta_lang (ta.make {q} {f [] → q} {}) = {GFun f []}"
proof -
have [dest]: "q' ∈ ta_res (ta.make {q} {f [] → q} {}) t' ⟹ ground t' ⟹ t' = Fun f []" for t' q'
by (induct t') auto
show ?thesis
by (auto simp: gta_lang_def elim!: ta_langE intro!: rev_image_eqI ta_langI[of "Fun f []"])
qed
lemma ground_set_map_adapt_vars_dist:
assumes "A ⊆ Collect ground × Collect ground"
and "B ⊆ Collect ground × Collect ground"
shows "(map_both adapt_vars ` A) O (map_both adapt_vars ` B) = map_both adapt_vars ` (A O B)" (is "?L = ?R")
proof
show "?L ⊆ ?R" apply (rule) using assms adapt_vars_inj by blast
next
show "?R ⊆ ?L" apply (rule) using assms adapt_vars_inj by blast
qed
lemma reach_poss_term:
assumes "q ∈ ta_res A t" "p ∈ poss t"
shows "∃ q'. q' ∈ ta_res A (t |_ p)"
using assms by (metis subt_at_imp_ctxt ta_res_ctxt_decompose)
lemma reach_poss_gterm:
assumes "q ∈ ta_res A (term_of_gterm t)" "p ∈ gposs t"
shows "∃ q'. q' ∈ ta_res A (term_of_gterm (gsubt_at t p)) ∧ q ∈ ta_res A (ctxt_of_pos_term p (term_of_gterm t))⟨Var q'⟩" using assms
using assms by (metis ctxt_supt_id ground_ctxt_apply ground_term_of_gterm gsubt_at_to_subt_at gterm_of_term_inv poss_gposs_conv ta_res_ctxt_decompose)
lemma funas_poss_presv:
assumes "funas_gterm u ⊆ ℱ" and "p ∈ gposs u"
shows "funas_gterm (gsubt_at u p) ⊆ ℱ" using assms
proof (induct u arbitrary: p)
case (GFun f ts)
then show ?case
proof (cases p)
case [simp]:(Cons a ps) show ?thesis
using GFun(1)[OF nth_mem, of a ps] GFun(2-)
by (auto simp: funas_gterm_def UN_subset_iff in_mono)
qed auto
qed
inductive_set ta_rule_tr :: "('q, 'f) ta_rule set ⇒ ('f, 'q) term rel" for Δ⇩A where
rule: "f qs → q ∈ Δ⇩A ⟹ (C⟨Fun f (map Var qs)⟩, C⟨Var q⟩) ∈ ta_rule_tr Δ⇩A"
forΔ_ε">inductive_set ta_eps_tr for Δ⇩ε where
eps: "(p, q) ∈ Δ⇩ε⇧* ⟹ (C⟨Var p⟩, C⟨Var q⟩) ∈ ta_eps_tr Δ⇩ε"
abbreviation "move_strict Δ⇩A Δ⇩ε ≡ ta_rule_tr Δ⇩A O ta_eps_tr Δ⇩ε"
lemma ta_rule_lhs_Var [simp]:
"(Var x, s) ∈ ta_rule_tr Δ⇩A ⟷ False"
by (metis Term.term.simps(4) ctxt_supteq supteq_Var_id ta_rule_tr.simps)
lemma ta_rule_tr_ctxtcl:
assumes "(s, t) ∈ (ta_rule_tr Δ⇩A)"
shows "(C⟨s⟩, C⟨t⟩) ∈ (ta_rule_tr Δ⇩A)"
using assms by (induct) (metis ctxt_ctxt_compose ta_rule_tr.intros)
lemma ta_eps_tr_ctxtcl:
assumes "(s, t) ∈ (ta_eps_tr Δ⇩ε)"
shows "(C⟨s⟩, C⟨t⟩) ∈ (ta_eps_tr Δ⇩ε)"
using assms by induct (auto simp flip: ctxt_ctxt_compose intro: ta_eps_tr.intros)
lemma move_strict_ctxtcl:
assumes "(s, t) ∈ (move_strict Δ⇩A Δ⇩ε)"
shows "(C⟨s⟩, C⟨t⟩) ∈ (move_strict Δ⇩A Δ⇩ε)"
using assms
proof (induct arbitrary: C)
case (relcompI a b c)
then show ?case using ta_eps_tr_ctxtcl ta_rule_tr_ctxtcl by blast
qed
lemma move_strict_trancl_ctxtcl:
assumes "(s, t) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*"
using assms rtrancl_map[OF move_strict_ctxtcl, of "move_strict Δ⇩A Δ⇩ε" "id"]
by fastforce
lemma move_args_step_imp_step:
assumes "⋀ i. i < length ts ⟹ (ts ! i, qs ! i) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*"
and "length ts = length qs"
shows "(Fun f ts, Fun f qs) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*"
using assms by (simp add: args_steps_imp_steps ctxt.closedI move_strict_ctxtcl)
lemma move_strict_rtrancl_lhs_Var_relf [simp]:
assumes "(s, t) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*" and "s = Var q"
shows "t = Var q" using assms
by induct auto
lemma ta_rule_rhs_Var_args_Vars:
assumes "(s, Var q) ∈ (ta_rule_tr Δ⇩A)"
shows "∀ i < length (args s). is_Var (args s ! i)"
using assms by (cases s, case_tac C) auto
lemma ta_rule_rhs_Var_to_rule:
assumes "(s, Var q) ∈ (ta_rule_tr Δ⇩A)"
shows "fst (the (root s)) (map the_Var (args s)) → q ∈ Δ⇩A"
using assms by (cases s, case_tac C) (auto simp: comp_def)
lemma ta_rule_funs_length:
assumes "(s, t) ∈ ta_rule_tr Δ⇩A"
and "s = Fun f ts" and "t = Fun g ss"
shows "g = f" "length ss = length ts" using assms
by (induct) (case_tac C, auto, case_tac C, auto)
lemma ta_rule_tr_args:
assumes "(s, t) ∈ ta_rule_tr Δ⇩A"
and "s = Fun f ts" and "t = Fun g ss"
obtains bef u v aft where "ts = bef @ u # aft" "ss = bef @ v # aft" "(u, v) ∈ ta_rule_tr Δ⇩A"
using assms by (induct) (case_tac C, auto simp: ta_rule_tr.intros)
lemma ta_rule_tr_ta_res':
assumes "(s, t) ∈ (ta_rule_tr (ta_rules 𝒜))"
shows "t ∈ ta_res' 𝒜 s" using assms
proof (induct s arbitrary: t)
case (Fun f ts) note IH = Fun(1)[OF nth_mem] note IS = Fun(2)
show ?case
proof (cases t)
case (Var x)
have "f (map the_Var ts) → x ∈ ta_rules 𝒜" using ta_rule_rhs_Var_to_rule[OF IS[unfolded Var]]
by auto
moreover
{fix i assume "i < length ts"
then have "the_Var (ts ! i) ∈ ta_res 𝒜 (ts ! i)"
using ta_rule_rhs_Var_args_Vars[OF IS[unfolded Var]]
by (cases "ts ! i") auto}
ultimately show ?thesis unfolding Var
by (auto intro!: exI[of _ x] exI[of _ "map the_Var ts"])
next
case (Fun g ss)
from ta_rule_tr_args[OF IS] obtain bef u v aft where
list: "ts = bef @ u # aft" "ss = bef @ v # aft" and
rule: "(u, v) ∈ (ta_rule_tr (ta_rules 𝒜))" unfolding Fun
by metis
then show ?thesis using IS IH[of "length bef" "ss ! length bef"] ta_rule_funs_length[OF IS, of f ts g ss]
unfolding Fun by (auto simp: nth_append_Cons)
qed
qed auto
lemma ta_eps_tr_ta_res':
assumes "(s, t) ∈ (ta_eps_tr (ta_eps 𝒜))"
shows "t ∈ ta_res' 𝒜 s" using assms
by (induct, case_tac C) (auto simp: ta_eps_ta_res'_ctxtcl nth_append_Cons)
lemma move_strict_to_ta_res':
assumes "(s, t) ∈ move_strict (ta_rules 𝒜) (ta_eps 𝒜)"
shows "t ∈ ta_res' 𝒜 s" using assms
by (auto dest: ta_rule_tr_ta_res' ta_eps_tr_ta_res' intro: ta_res'_trans)
lemma move_strict_rtrancl_to_ta_res':
assumes "(s, t) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*"
shows "t ∈ ta_res' 𝒜 s" using assms
by (induct) (auto dest!: move_strict_to_ta_res' intro: ta_res'_trans)
lemma ta_res_to_move_strict:
assumes "q ∈ ta_res 𝒜 s" and "ground s"
shows "(s, Var q) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*"
using assms
proof (induct s arbitrary: q)
case (Fun f ts)
from Fun(2) obtain qs p where
rule: "f qs → p ∈ ta_rules 𝒜" "length qs = length ts" and
eps: "(p, q) ∈ (ta_eps 𝒜)⇧*" and
reach: "∀ i < length ts. qs ! i ∈ ta_res 𝒜 (ts ! i)" by auto
from Fun(1)[OF nth_mem, of i "qs ! i" for i] reach rule(2) Fun(3)
have "i < length ts ⟹ (ts ! i, Var (qs ! i)) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*" for i by auto
from this rule(2) have "(Fun f ts, Fun f (map Var qs)) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*"
by (simp add: move_args_step_imp_step)
then show ?case using ta_rule_tr.intros[OF rule(1), of □] ta_eps_tr.intros[OF eps, of □]
by (auto intro: rtrancl_into_rtrancl)
qed auto
lemma move_strict_ta_res:
assumes "(s, t) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*" and "t = Var q"
shows "q ∈ ta_res 𝒜 s" using assms
proof (induct arbitrary: q rule: converse_rtrancl_induct)
case (step y z)
from step(3)[OF step(4)] move_strict_to_ta_res'[OF step(1)] show ?case
by (meson ta_res'_ta_res)
qed auto
lemma gterm_move_strict_ta_res_eq:
assumes "ground s"
shows "(s, Var q) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧* ⟷ q ∈ ta_res 𝒜 s"
using assms move_strict_ta_res ta_res_to_move_strict
by metis
lemma ta_res'_to_move_strict:
assumes "t ∈ ta_res' 𝒜 s" and "ground s"
shows "(s, t) ∈ (move_strict (ta_rules 𝒜) (ta_eps 𝒜))⇧*" using assms
proof (induct s arbitrary: t)
case (Fun f ts) note IS = Fun(2-) note IH = Fun(1)[OF nth_mem]
show ?case
proof (cases t)
case [simp]: (Fun g ss)
then show ?thesis using IS IH[of i "ss ! i" for i]
by (auto simp: move_args_step_imp_step)
qed (metis IS move_strict_ta_res rtrancl.rtrancl_refl ta_res'_ta_res ta_res_to_move_strict)
qed auto
lemma poss_ctxt_var_term [simp]:
"poss C⟨Var q⟩ ⊆ poss C⟨Var p⟩"
"poss C⟨Var q⟩ ⊆ poss C⟨Fun f ts⟩"
by (metis less_eq_hole_pos_in_possc less_eq_pos_def par_hole_pos_in_possc parallel_pos poss_imp_possc self_append_conv subsetI subt_at_hole_pos var_pos_maximal)+
lemma ta_rule_tr_poss:
assumes "(s, t) ∈ ta_rule_tr Δ⇩A"
shows "poss t ⊆ poss s" using assms
by (induct) (auto simp: hole_pos_poss_conv)
lemma ta_eps_tr_poss:
assumes "(s, t) ∈ ta_eps_tr Δ⇩ε"
shows "poss t ⊆ poss s" using assms
by (induct) (auto simp: hole_pos_poss_conv)
lemma move_poss:
assumes "(s, t) ∈ (move_strict Δ⇩A Δ⇩ε)"
shows "poss t ⊆ poss s" using assms
by (induct) (auto dest: ta_rule_tr_poss ta_eps_tr_poss intro: subset_trans)
lemma move_rtrancl_poss:
assumes "(s, t) ∈ (move_strict Δ⇩A Δ⇩ε)⇧*"
shows "poss t ⊆ poss s" using assms
by (induct) (auto dest!: move_poss intro: subset_trans)
definition "ta_run 𝒜 t r q ⟷ (∀ p ∈ gposs t.
(groot (gsubt_at t p)) (map (λ i. (snd ∘ r) (p @ [i])) [0 ..< length (gargs (gsubt_at t p))]) → fst (r p) ∈ ta_rules 𝒜 ∧
(fst (r p), snd (r p)) ∈ (ta_eps 𝒜)⇧*) ∧ snd (r []) = q"
lemma ta_res_implies_succesful_run_ex:
assumes "q ∈ ta_res 𝒜 (term_of_gterm t)"
shows "∃ r. ta_run 𝒜 t r q"
using assms
proof (induct t arbitrary: q)
case (GFun f ts)
from GFun(2) obtain qs p where
rule: "f qs → p ∈ ta_rules 𝒜" "length qs = length ts" and
eps: "(p, q) ∈ (ta_eps 𝒜)⇧*" and
reach: "∀ i < length ts. qs ! i ∈ ta_res 𝒜 (term_of_gterm (ts ! i))" by auto
from reach GFun(1)[OF nth_mem, of i "qs ! i" for i] obtain rs where
r: "length rs = length ts" "∀ i < length ts. ta_run 𝒜 (ts ! i) (rs ! i) (qs ! i)"
using Ex_list_of_length_P[of "length ts" "λ r i. ta_run 𝒜 (ts ! i) r (qs ! i)"] rule(2)
by blast
then have [simp]: "map (λi. snd ((rs ! i) [])) [0..<length ts] = qs" using rule(2)
by (auto simp: ta_run_def intro!: nth_equalityI)
then show ?case using r rule eps reach unfolding ta_run_def
by (rule_tac x = "λ l. case l of [] ⇒ (p, q) | (i # xs) ⇒ (rs ! i) xs" in exI)
(auto simp flip: atomize_all)
qed
lemma ta_run_implies_ta_res:
assumes "ta_run 𝒜 t r q"
shows "q ∈ ta_res 𝒜 (term_of_gterm t)"
using assms
proof (induct t arbitrary: q r)
case (GFun f ts)
{fix i assume "i < length ts"
then have "ta_run 𝒜 (ts ! i) (λa. r (i # a)) (snd (r [i]))"
using GFun(2) by (auto simp: ta_run_def) fastforce}
from this GFun(2) show ?case
using GFun(1)[OF nth_mem, of i "λ p. r (i # p)" "snd (r [i])" for i]
by (auto simp: ta_run_def intro!: exI[of _ "fst (r [])"] exI[of _ "map (λi. snd (r [i])) [0..<length ts]"])
qed
end