theory RR2_Infinite_Q_infinity imports RR2_Infinite begin (* This section constructs an executable membership check for Q infinity, since Inf_automata is already executable (for all sets Q where checking membership is executable) *) lemma if_cong': "b = c ⟹ x = u ⟹ y = v ⟹ (if b then x else y) = (if c then u else v)" by auto (* The reachable terms where eps transitions can only occur after the rule *) 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 (* Q_inf section *) 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: ctxt_apply_term.simps) apply (metis Subterm_and_Context.ctxt_ctxt_compose ctxt_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 (* SLOW *) by (auto simp: comp_def nth_append_Cons split: if_splits cong: if_cong') (smt 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)] ctxt.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 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) (smt Ball_Collect finite_imageI image_subset_iff infinite_iff_countable_subset subset_eq) 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) by (auto simp flip: ctxt(3)) (smt ctxt.simps(8) 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 (smt (z3) ctxt.simps(8) 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