Theory RR2_Infinite_Q_infinity
theory RR2_Infinite_Q_infinity
imports RR2_Infinite
begin
lemma if_cong':
"b = c ⟹ x = u ⟹ y = v ⟹ (if b then x else y) = (if c then u else v)"
by auto
fun ta_der_strict :: "('q,'f) ta ⇒ ('f,'q) term ⇒ 'q fset" where
"ta_der_strict 𝒜 (Var q) = {|q|}"
| "ta_der_strict 𝒜 (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_strict 𝒜 (ts ! i))|}"
lemma ta_der_strict_Var:
"q |∈| ta_der_strict 𝒜 (Var x) ⟷ x = q"
unfolding ta_der.simps by auto
lemma ta_der_strict_Fun:
"q |∈| ta_der_strict 𝒜 (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_strict 𝒜 (ts ! i)))" (is "?Ls ⟷ ?Rs")
unfolding ta_der_strict.simps
by (intro iffI fCollect_memberI finite_Collect_less_eq[OF _ finite_eps[of 𝒜]]) auto
declare ta_der_strict.simps[simp del]
lemmas ta_der_strict_simps [simp] = ta_der_strict_Var ta_der_strict_Fun
lemma ta_der_strict_sub_ta_der:
"ta_der_strict 𝒜 t |⊆| ta_der 𝒜 t"
proof (induct t)
case (Fun f ts)
then show ?case
by auto (metis fsubsetD nth_mem)+
qed auto
lemma ta_der_strict_ta_der_eq_on_ground:
assumes"ground t"
shows "ta_der 𝒜 t = ta_der_strict 𝒜 t"
proof
{fix q assume "q |∈| ta_der 𝒜 t" then have "q |∈| ta_der_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_der 𝒜 t |⊆| ta_der_strict 𝒜 t"
by auto
next
show "ta_der_strict 𝒜 t |⊆| ta_der 𝒜 t" using ta_der_strict_sub_ta_der .
qed
lemma ta_der_to_ta_strict:
assumes "q |∈| ta_der A C⟨Var p⟩" and "ground_ctxt C"
shows "∃ q'. (p = q' ∨ (p, q') |∈| (eps A)|⇧+|) ∧ q |∈| ta_der_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: "TA_rule f qs q' |∈| rules A" "length qs = Suc (length ss + length ts)" "q' = q ∨ (q', q) |∈| (eps A)|⇧+|" and
rec: "∀ i < length qs. qs ! i |∈| ta_der 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'' ∨ (p, q'') |∈| (eps A)|⇧+|) ∧ qs ! length ss |∈| ta_der_strict A C⟨Var q''⟩"
by auto (metis length_map less_add_Suc1 nth_append_length)
then have "∀ i < length qs. qs ! i |∈| ta_der_strict A ((ss @ C⟨Var q''⟩ # ts) ! i)"
using rec r(2) More(3)
using ta_der_strict_ta_der_eq_on_ground[of _ A]
by (auto simp: nth_append_Cons all_Suc_conv 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])
qed auto
fun root_ctxt where
"root_ctxt (More f ss C ts) = f"
| "root_ctxt □ = undefined"
lemma root_to_root_ctxt [simp]:
assumes "C ≠ □"
shows "fst (the (root C⟨t⟩)) ⟷ root_ctxt C"
using assms by (cases C) auto
inductive_set Q_inf for 𝒜 where
trans: "(p, q) ∈ Q_inf 𝒜 ⟹ (q, r) ∈ Q_inf 𝒜 ⟹ (p, r) ∈ Q_inf 𝒜"
| rule: "(None, Some f) qs → q |∈| rules 𝒜 ⟹ i < length qs ⟹ (qs ! i, q) ∈ Q_inf 𝒜"
| eps: "(p, q) ∈ Q_inf 𝒜 ⟹ (q, r) |∈| eps 𝒜 ⟹ (p, r) ∈ Q_inf 𝒜"
abbreviation "Q_inf_e 𝒜 ≡ {q | p q. (p, p) ∈ Q_inf 𝒜 ∧ (p, q) ∈ Q_inf 𝒜}"
lemma Q_inf_states_ta_states:
assumes "(p, q) ∈ Q_inf 𝒜"
shows "p |∈| 𝒬 𝒜" "q |∈| 𝒬 𝒜"
using assms by (induct) (auto simp: rule_statesD eps_statesD)
lemma Q_inf_finite:
"finite (Q_inf 𝒜)" "finite (Q_inf_e 𝒜)"
proof -
have *: "Q_inf 𝒜 ⊆ fset (𝒬 𝒜 |×| 𝒬 𝒜)" "Q_inf_e 𝒜 ⊆ fset (𝒬 𝒜)"
by (auto simp add: Q_inf_states_ta_states(1, 2) subrelI)
show "finite (Q_inf 𝒜)"
by (intro finite_subset[OF *(1)]) simp
show "finite (Q_inf_e 𝒜)"
by (intro finite_subset[OF *(2)]) simp
qed
context
includes fset.lifting
begin
lift_definition fQ_inf :: "('a, 'b option × 'c option) ta ⇒ ('a × 'a) fset" is Q_inf
by (simp add: Q_inf_finite(1))
lift_definition fQ_inf_e :: "('a, 'b option × 'c option) ta ⇒ 'a fset" is Q_inf_e
using Q_inf_finite(2) .
end
lemma Q_inf_ta_eps_Q_inf:
assumes "(p, q) ∈ Q_inf 𝒜" and "(q, q') |∈| (eps 𝒜)|⇧+|"
shows "(p, q') ∈ Q_inf 𝒜" using assms(2, 1)
by (induct rule: ftrancl_induct) (auto simp add: Q_inf.eps)
lemma lhs_state_rule:
assumes "(p, q) ∈ Q_inf 𝒜"
shows "∃ f qs r. (None, Some f) qs → r |∈| rules 𝒜 ∧ p |∈| fset_of_list qs"
using assms by induct (force intro: nth_mem)+
lemma Q_inf_reach_state_rule:
assumes "(p, q) ∈ Q_inf 𝒜" and "𝒬 𝒜 |⊆| ta_reachable 𝒜"
shows "∃ ss ts f C. q |∈| ta_der 𝒜 (More (None, Some f) ss C ts)⟨Var p⟩ ∧ ground_ctxt (More (None, Some f) ss C ts)"
(is "∃ ss ts f C. ?P ss ts f C q p")
using assms
proof (induct)
case (trans p q r)
then obtain f1 f2 ss1 ts1 ss2 ts2 C1 C2 where
C: "?P ss1 ts1 f1 C1 q p" "?P ss2 ts2 f2 C2 r q" by blast
then show ?case
apply (rule_tac x = "ss2" in exI, rule_tac x = "ts2" in exI, rule_tac x = "f2" in exI,
rule_tac x = "C2 ∘⇩c (More (None, Some f1) ss1 C1 ts1)" in exI)
apply (auto simp del: intp_actxt.simps)
apply (metis Subterm_and_Context.ctxt_ctxt_compose actxt_compose.simps(2) ta_der_ctxt)
done
next
case (rule f qs q i)
have "∀ i < length qs. ∃ t. qs ! i |∈| ta_der 𝒜 t ∧ ground t"
using rule(1, 2) fset_mp[OF rule(3), of "qs ! i" for i]
by auto (meson fnth_mem rule_statesD(4) ta_reachableE)
then obtain ts where wit: "length ts = length qs"
"∀ i < length qs. qs ! i |∈| ta_der 𝒜 (ts ! i) ∧ ground (ts ! i)"
using Ex_list_of_length_P[of "length qs" "λ x i. qs ! i |∈| ta_der 𝒜 x ∧ ground x"] by blast
{fix j assume "j < length qs"
then have "qs ! j |∈| ta_der 𝒜 ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)"
using wit by (cases "j < i") (auto simp: min_def nth_append_Cons)}
then have "∀ i < length qs. qs ! i |∈| (map (ta_der 𝒜) (take i ts @ Var (qs ! i) # drop (Suc i) ts)) ! i"
using wit rule(2) by (auto simp: nth_append_Cons)
then have res: "q |∈| ta_der 𝒜 (Fun (None, Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))"
using rule(1, 2) wit by (auto simp: min_def nth_append_Cons intro!: exI[of _ q] exI[of _ qs])
then show ?case using rule(1, 2) wit
apply (rule_tac x = "take i ts" in exI, rule_tac x = "drop (Suc i) ts" in exI)
apply (auto simp: take_map drop_map dest!: in_set_takeD in_set_dropD simp del: ta_der_simps intro!: exI[of _ f] exI[of _ Hole])
apply (metis all_nth_imp_all_set)+
done
next
case (eps p q r)
then show ?case by (meson r_into_rtrancl ta_der_eps)
qed
lemma rule_target_Q_inf:
assumes "(None, Some f) qs → q' |∈| rules 𝒜" and "i < length qs"
shows "(qs ! i, q') ∈ Q_inf 𝒜" using assms
by (intro rule) auto
lemma rule_target_eps_Q_inf:
assumes "(None, Some f) qs → q' |∈| rules 𝒜" "(q', q) |∈| (eps 𝒜)|⇧+|"
and "i < length qs"
shows "(qs ! i, q) ∈ Q_inf 𝒜"
using assms(2, 1, 3) by (induct rule: ftrancl_induct) (auto intro: rule eps)
lemma step_in_Q_inf:
assumes "q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (Fun f (ss @ Var p # ts)))"
shows "(p, q) ∈ Q_inf 𝒜"
using assms rule_target_eps_Q_inf[of f _ _ 𝒜 q] rule_target_Q_inf[of f _ q 𝒜]
by (auto simp: comp_def nth_append_Cons split!: if_splits)
lemma ta_der_Q_inf:
assumes "q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (C⟨Var p⟩))" and "C ≠ Hole"
shows "(p, q) ∈ Q_inf 𝒜" using assms
proof (induct C arbitrary: q)
case (More f ss C ts)
then show ?case
proof (cases "C = Hole")
case True
then show ?thesis using More(2) by (auto simp: step_in_Q_inf)
next
case False
then obtain q' where q: "q' |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) C⟨Var p⟩)"
"q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (Fun f (ss @ Var q' # ts)))"
using More(2) length_map
by (auto simp: comp_def nth_append_Cons split: if_splits cong: if_cong')
(smt (verit) nat_neq_iff nth_map ta_der_strict_simps)+
have "(p, q') ∈ Q_inf 𝒜" using More(1)[OF q(1) False] .
then show ?thesis using step_in_Q_inf[OF q(2)] by (auto intro: trans)
qed
qed auto
lemma Q_inf_e_infinite_terms_res:
assumes "q ∈ Q_inf_e 𝒜" and "𝒬 𝒜 |⊆| ta_reachable 𝒜"
shows "infinite {t. q |∈| ta_der 𝒜 (term_of_gterm t) ∧ fst (groot_sym t) = None}"
proof -
let ?P ="λ u. ground u ∧ q |∈| ta_der 𝒜 u ∧ fst (fst (the (root u))) = None"
have groot[simp]: "fst (fst (the (root (term_of_gterm t)))) = fst (groot_sym t)" for t by (cases t) auto
have [simp]: "C ≠ □ ⟹ fst (fst (the (root C⟨t⟩))) = fst (root_ctxt C)" for C t by (cases C) auto
from assms(1) obtain p where cycle: "(p, p) ∈ Q_inf 𝒜" "(p, q) ∈ Q_inf 𝒜" by auto
from Q_inf_reach_state_rule[OF cycle(1) assms(2)] obtain C where
ctxt: "C ≠ □" "ground_ctxt C" and reach: "p |∈| ta_der 𝒜 C⟨Var p⟩"
by blast
obtain C2 where
closing_ctxt: "C2 ≠ □" "ground_ctxt C2" "fst (root_ctxt C2) = None" and cl_reach: "q |∈| ta_der 𝒜 C2⟨Var p⟩"
by (metis (full_types) Q_inf_reach_state_rule[OF cycle(2) assms(2)] actxt.distinct(1) fst_conv root_ctxt.simps(1))
from assms(2) obtain t where t: "p |∈| ta_der 𝒜 t" and gr_t: "ground t"
by (meson Q_inf_states_ta_states(1) cycle(1) fsubsetD ta_reachableE)
let ?terms = "λ n. (C ^ Suc n)⟨t⟩" let ?S = "{?terms n | n. p |∈| ta_der 𝒜 (?terms n) ∧ ground (?terms n)}"
have "ground (?terms n)" for n using ctxt(2) gr_t by auto
moreover have "p |∈| ta_der 𝒜 (?terms n)" for n using reach t(1)
by (auto simp: ta_der_ctxt) (meson ta_der_ctxt ta_der_ctxt_n_loop)
ultimately have inf: "infinite ?S" using ctxt_comp_n_lower_bound[OF ctxt(1)]
using no_upper_bound_infinite[of _ depth, of ?S] by blast
from infinite_inj_image_infinite[OF this] have inf:"infinite (ctxt_apply_term C2 ` ?S)"
by (smt (verit) ctxt_eq inj_on_def)
{fix u assume "u ∈ (ctxt_apply_term C2 ` ?S)"
then have "?P u" unfolding image_Collect using closing_ctxt cl_reach
by (auto simp: ta_der_ctxt)}
from this have inf: "infinite {u. ground u ∧ q |∈| ta_der 𝒜 u ∧ fst (fst (the (root u))) = None}"
by (intro infinite_super[OF _ inf] subsetI) fast
have inf: "infinite (gterm_of_term ` {u. ground u ∧ q |∈| ta_der 𝒜 u ∧ fst (fst (the (root u))) = None})"
by (intro infinite_inj_image_infinite[OF inf] gterm_of_term_inj) auto
show ?thesis
by (intro infinite_super[OF _ inf]) (auto dest: groot_sym_gterm_of_term)
qed
lemma gfun_at_after_hole_pos:
assumes "ghole_pos C ≤⇩p p"
shows "gfun_at C⟨t⟩⇩G p = gfun_at t (p -⇩p ghole_pos C)" using assms
proof (induct C arbitrary: p)
case (GMore f ss C ts) then show ?case
by (cases p) auto
qed auto
lemma pos_diff_0 [simp]: "p -⇩p p = []"
by (auto simp: pos_diff_def)
lemma Max_suffI: "finite A ⟹ A = B ⟹ Max A = Max B"
by (intro Max_eq_if) auto
lemma nth_args_depth_eqI:
assumes "length ss = length ts"
and "⋀ i. i < length ts ⟹ depth (ss ! i) = depth (ts ! i)"
shows "depth (Fun f ss) = depth (Fun g ts)"
proof -
from assms(1, 2) have "depth ` set ss = depth ` set ts"
using nth_map_conv[OF assms(1), of depth depth]
by (simp flip: set_map)
from Max_suffI[OF _ this] show ?thesis using assms(1)
by (cases ss; cases ts) auto
qed
lemma subt_at_ctxt_apply_hole_pos [simp]: "C⟨s⟩ |_ hole_pos C = s"
by (induct C) auto
lemma ctxt_at_pos_ctxt_apply_hole_poss [simp]: "ctxt_at_pos C⟨s⟩ (hole_pos C) = C"
by (induct C) auto
abbreviation "map_funs_ctxt f ≡ map_ctxt f (λ x. x)"
lemma map_funs_term_ctxt_apply [simp]:
"map_funs_term f C⟨s⟩ = (map_funs_ctxt f C)⟨map_funs_term f s⟩"
by (induct C) auto
lemma map_funs_term_ctxt_decomp:
assumes "map_funs_term fg t = C⟨s⟩"
shows "∃ D u. C = map_funs_ctxt fg D ∧ s = map_funs_term fg u ∧ t = D⟨u⟩"
using assms
proof (induct C arbitrary: t)
case Hole
show ?case
by (rule exI[of _ Hole], rule exI[of _ t], insert Hole, auto)
next
case (More g bef C aft)
from More(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
from More(2)[unfolded t] have f: "fg f = g" and ts: "map (map_funs_term fg) ts = bef @ C⟨s⟩ # aft" (is "?ts = ?bca") by auto
from ts have "length ?ts = length ?bca" by auto
then have len: "length ts = length ?bca" by auto
note id = ts[unfolded map_nth_eq_conv[OF len], THEN spec, THEN mp]
let ?i = "length bef"
from len have i: "?i < length ts" by auto
from id[of ?i] have "map_funs_term fg (ts ! ?i) = C⟨s⟩" by auto
from More(1)[OF this] obtain D u where D: "C = map_funs_ctxt fg D" and
u: "s = map_funs_term fg u" and id: "ts ! ?i = D⟨u⟩" by auto
from ts have "take ?i ?ts = take ?i ?bca" by simp
also have "... = bef" by simp
finally have bef: "map (map_funs_term fg) (take ?i ts) = bef" by (simp add: take_map)
from ts have "drop (Suc ?i) ?ts = drop (Suc ?i) ?bca" by simp
also have "... = aft" by simp
finally have aft: "map (map_funs_term fg) (drop (Suc ?i) ts) = aft" by (simp add:drop_map)
let ?bda = "take ?i ts @ D⟨u⟩ # drop (Suc ?i) ts"
show ?case
proof (rule exI[of _ "More f (take ?i ts) D (drop (Suc ?i) ts)"],
rule exI[of _ u], simp add: u f D bef aft t)
have "ts = take ?i ts @ ts ! ?i # drop (Suc ?i) ts"
by (rule id_take_nth_drop[OF i])
also have "... = ?bda" by (simp add: id)
finally show "ts = ?bda" .
qed
qed
lemma prod_automata_from_none_root_dec:
assumes "gta_lang Q 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ ℱ ∧ funas_gterm t ⊆ ℱ}"
and "q |∈| ta_der 𝒜 (term_of_gterm t)" and "fst (groot_sym t) = None"
and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "q |∈| ta_productive Q 𝒜"
shows "∃ u. t = gterm_to_None_Some u ∧ funas_gterm u ⊆ ℱ"
proof -
have *: "gfun_at t [] = Some (groot_sym t)" by (cases t) auto
from assms(4, 5) obtain C q⇩f where ctxt: "ground_ctxt C" and
fin: "q⇩f |∈| ta_der 𝒜 C⟨Var q⟩" "q⇩f |∈| Q"
by (auto simp: ta_productive_def'[OF assms(4)])
then obtain s v where gp: "gpair s v = (gctxt_of_ctxt C)⟨t⟩⇩G" and
funas: "funas_gterm v ⊆ ℱ"
using assms(1, 2) gta_langI[OF fin(2), of 𝒜 "(gctxt_of_ctxt C)⟨t⟩⇩G"]
by (auto simp: ta_der_ctxt ground_gctxt_of_ctxt_apply_gterm)
from gp have mem: "hole_pos C ∈ gposs s ∪ gposs v"
by auto (metis Un_iff ctxt ghole_pos_in_apply gposs_of_gpair ground_hole_pos_to_ghole)
from this have "hole_pos C ∉ gposs s" using assms(3)
using arg_cong[OF gp, of "λ t. gfun_at t (hole_pos C)"]
using ground_hole_pos_to_ghole[OF ctxt]
using gfun_at_after_hole_pos[OF position_less_refl, of "gctxt_of_ctxt C"]
by (auto simp: gfun_at_gpair * split: if_splits)
(metis fstI gfun_at_None_ngposs_iff)+
from subst_at_gpair_nt_poss_None_Some[OF _ this, of v] this
have "t = gterm_to_None_Some (gsubt_at v (hole_pos C)) ∧ funas_gterm (gsubt_at v (hole_pos C)) ⊆ ℱ"
using funas mem funas_gterm_gsubt_at_subseteq
by (auto simp: gp intro!: exI[of _ "gsubt_at v (hole_pos C)"])
(metis ctxt ground_hole_pos_to_ghole gsubt_at_gctxt_apply_ghole)
then show ?thesis by blast
qed
lemma infinite_set_dec_infinite:
assumes "infinite S" and "⋀ s. s ∈ S ⟹ ∃ t. f t = s ∧ P t"
shows "infinite {t | t s. s ∈ S ∧ f t = s ∧ P t}" (is "infinite ?T")
proof (rule ccontr)
assume ass: "¬ infinite ?T"
have "S ⊆ f ` {x . P x}" using assms(2) by auto
then show False using ass assms(1)
by (auto simp: subset_image_iff)
(metis (mono_tags, lifting) Ball_Collect finite_imageI image_eqI infinite_super)
qed
lemma Q_inf_exec_impl_Q_inf:
assumes "gta_lang Q 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ fset ℱ ∧ funas_gterm t ⊆ fset ℱ}"
and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "𝒬 𝒜 |⊆| ta_productive Q 𝒜"
and "q ∈ Q_inf_e 𝒜"
shows "q |∈| Q_infty 𝒜 ℱ"
proof -
let ?S = "{t. q |∈| ta_der 𝒜 (term_of_gterm t) ∧ fst (groot_sym t) = None}"
let ?P = "λ t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))"
let ?F = "(λ(f, n). ((None, Some f), n)) |`| ℱ"
from Q_inf_e_infinite_terms_res[OF assms(4, 2)] have inf: "infinite ?S" by auto
{fix t assume "t ∈ ?S"
then have "∃ u. t = gterm_to_None_Some u ∧ funas_gterm u ⊆ fset ℱ"
using prod_automata_from_none_root_dec[OF assms(1)] assms(2, 3)
using fin_mono by fastforce}
then show ?thesis using infinite_set_dec_infinite[OF inf, of gterm_to_None_Some ?P]
by (auto simp: Q_infty_fmember) blast
qed
lemma Q_inf_impl_Q_inf_exec:
assumes "q |∈| Q_infty 𝒜 ℱ"
shows "q ∈ Q_inf_e 𝒜"
proof -
let ?t_of_g = "λ t. term_of_gterm t :: ('b option × 'b option, 'a) term"
let ?t_og_g2 = "λ t. term_of_gterm t :: ('b, 'a) term"
let ?inf = "(?t_og_g2 :: 'b gterm ⇒ ('b, 'a) term) ` {t |t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some t))}"
obtain n where card_st: "fcard (𝒬 𝒜) < n" by blast
from assms(1) have "infinite {t |t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some t))}"
unfolding Q_infty_def by blast
from infinite_inj_image_infinite[OF this, of "?t_og_g2"] have inf: "infinite ?inf" using inj_term_of_gterm by blast
{fix s assume "s ∈ ?inf" then have "ground s" "funas_term s ⊆ fset ℱ" by (auto simp: funas_term_of_gterm_conv subsetD)}
from infinte_no_depth_limit[OF inf, of "fset ℱ"] this obtain u where
funas: "funas_gterm u ⊆ fset ℱ" and card_d: "n < depth (?t_og_g2 u)" and reach: "q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some u))"
by auto blast
have "depth (?t_og_g2 u) = depth (?t_of_g (gterm_to_None_Some u))"
proof (induct u)
case (GFun f ts) then show ?case
by (auto simp: comp_def intro: nth_args_depth_eqI)
qed
from this pigeonhole_tree_automata[OF _ reach] card_st card_d obtain C2 C s v p where
ctxt: "C2 ≠ □" "C⟨s⟩ = term_of_gterm (gterm_to_None_Some u)" "C2⟨v⟩ = s" and
loop: "p |∈| ta_der 𝒜 v ∧ p |∈| ta_der 𝒜 C2⟨Var p⟩ ∧ q |∈| ta_der 𝒜 C⟨Var p⟩"
by auto
from ctxt have gr: "ground_ctxt C2" "ground_ctxt C" by auto (metis ground_ctxt_apply ground_term_of_gterm)+
from ta_der_to_ta_strict[OF _ gr(1)] loop obtain q' where
to_strict: "(p = q' ∨ (p, q') |∈| (eps 𝒜)|⇧+|) ∧ p |∈| ta_der_strict 𝒜 C2⟨Var q'⟩" by fastforce
have *: "∃ C. C2 = map_funs_ctxt lift_None_Some C ∧ C ≠ □" using ctxt(1, 2)
apply (auto simp flip: ctxt(3))
by (smt (verit, ccfv_threshold) map_ctxt.simps(1) map_funs_term_ctxt_decomp map_term_of_gterm)
then have q_p: "(q', p) ∈ Q_inf 𝒜" using to_strict ta_der_Q_inf[of p 𝒜 _ q'] ctxt
by auto
then have cycle: "(q', q') ∈ Q_inf 𝒜" using to_strict by (auto intro: Q_inf_ta_eps_Q_inf)
show ?thesis
proof (cases "C = □")
case True then show ?thesis
using cycle q_p loop by (auto intro: Q_inf_ta_eps_Q_inf)
next
case False
obtain q'' where r: "p = q'' ∨ (p, q'') |∈| (eps 𝒜)|⇧+|" "q |∈| ta_der_strict 𝒜 C⟨Var q''⟩"
using ta_der_to_ta_strict[OF conjunct2[OF conjunct2[OF loop]] gr(2)] by auto
then have "(q'', q) ∈ Q_inf 𝒜" using ta_der_Q_inf[of q 𝒜 _ q''] ctxt False
by auto (metis (mono_tags, lifting) map_ctxt.simps(1) map_funs_term_ctxt_decomp map_term_of_gterm)+
then show ?thesis using r(1) cycle q_p
by (auto simp: Q_inf_ta_eps_Q_inf intro!: exI[of _ q'])
(meson Q_inf.trans Q_inf_ta_eps_Q_inf)+
qed
qed
lemma Q_infty_fQ_inf_e_conv:
assumes "gta_lang Q 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ fset ℱ ∧ funas_gterm t ⊆ fset ℱ}"
and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "𝒬 𝒜 |⊆| ta_productive Q 𝒜"
shows "Q_infty 𝒜 ℱ = fQ_inf_e 𝒜"
using Q_inf_impl_Q_inf_exec Q_inf_exec_impl_Q_inf[OF assms]
by (auto simp: fQ_inf_e.rep_eq) fastforce
definition Inf_reg_impl where
"Inf_reg_impl R = Inf_reg R (fQ_inf_e (ta R))"
lemma Inf_reg_impl_sound:
assumes "ℒ 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ fset ℱ ∧ funas_gterm t ⊆ fset ℱ}"
and "𝒬⇩r 𝒜 |⊆| ta_reachable (ta 𝒜)" and "𝒬⇩r 𝒜 |⊆| ta_productive (fin 𝒜) (ta 𝒜)"
shows "ℒ (Inf_reg_impl 𝒜) = ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))"
using Q_infty_fQ_inf_e_conv[of "fin 𝒜" "ta 𝒜" ℱ] assms[unfolded ℒ_def]
by (simp add: Inf_reg_impl_def)
end