Theory RR2_Infinite

(*
  Author:  Alexander Lochmann <alexander.lochmann@uibk.ac.at> (2019)
  License: LGPL (see file COPYING.LESSER)
*)

theory RR2_Infinite
  imports RRn_Automata Tree_Automata_Pumping GTT_Impl
begin

lemma ground_ctxt_map_vars_to_adpat:
  assumes "ground_ctxt C"
  shows "map_vars_ctxt f C = adapt_vars_ctxt C" using assms
  by (induct C, auto) (metis adapt_vars_def ground_map_vars_term_simp)+

lemma [simp]: "map_ta_rule f id r = (r_root r) (map f (r_lhs_states r)) → (f (r_rhs r))" for f r
  by (simp add: ta_rule.expand ta_rule.map_sel(1 - 3))

primrec is_Inl where
  "is_Inl (Inl q) ⟷ True"
| "is_Inl (Inr q) ⟷ False"

primrec is_Inr where
  "is_Inr (Inr q) ⟷ True"
| "is_Inr (Inl q) ⟷ False"

lemma is_InrE:
  assumes "is_Inr q"
  obtains p where "q = Inr p"
  using assms by (cases q) auto

lemma is_InlE:
  assumes "is_Inl q"
  obtains p where "q = Inl p"
  using assms by (cases q) auto

lemma not_is_Inr_is_Inl [simp]:
  "¬ is_Inl t ⟷ is_Inr t"
  "¬ is_Inr t ⟷ is_Inl t"
  by (cases t, auto)+

fun remove_sum where
  "remove_sum (Inl q) = q"
|"remove_sum (Inr q) = q"

lemma [simp]: "remove_sum ∘ Inl = id" by auto

(* Finitness/Infinitness facts *)
lemma unbound_nat_map:
  assumes "∀ t ∈ S. ∃ u ∈ S. f t < f u" and "S ≠ {}"
  shows "∀(n::nat). ∃t ∈ S. n < f t"
proof -
  obtain x where x: "x ∈ S" using ‹S≠{}› by blast
  from bchoice[of S "λ x y. y ∈ S ∧ f x < f y"] assms obtain g where
    g: "∀ t ∈ S. g t ∈ S ∧ f t < f (g t)" by blast
  define h where "h n = (g^^ (Suc n)) x" for n
  have "n < f (h n) ∧ h n ∈ S" for n
  proof (induct n)
    case 0
    then show ?case using g[THEN bspec, OF x] by (auto simp: h_def)
  next
    case (Suc n) then show ?case using g[THEN bspec, OF conjunct2[OF Suc]]
      by (auto simp: h_def)
  qed
  then show ?thesis by auto
qed

lemma no_upper_bound_infinite:
  assumes "∀(n::nat). ∃t ∈ S. n < f t"
  shows "infinite S"
proof (rule ccontr, simp)
  assume "finite S"
  then obtain n where "n = Max (f ` S)" "∀ t ∈ S. f t ≤ n" by auto
  then show False using assms linorder_not_le by blast
qed

lemma set_constr_finite:
  assumes "finite F"
  shows "finite {h x | x. x ∈ F ∧ P x}" using assms
  by (induct) auto

lemma bounded_depth_finite:
  assumes fin_F: "finite ℱ" and "⋃ (funas_term ` S) ⊆ ℱ"
    and "∀t ∈ S. depth t ≤ n" and "∀t ∈ S. ground t"
  shows "finite S" using assms(2-)
proof (induction n arbitrary: S)
  case 0
  {fix t assume elem: "t ∈ S"
    from 0 have "depth t = 0" "ground t" "funas_term t ⊆ ℱ" using elem by auto
    then have "∃ f. (f, 0) ∈ ℱ ∧ t = Fun f []" by (cases t rule: depth.cases) auto}
  then have "S ⊆ {Fun f [] |f . (f, 0) ∈ ℱ}" by (auto simp add: image_iff)
  from finite_subset[OF this] show ?case
    using set_constr_finite[OF fin_F, of "λ (f, n). Fun f []" "λ x. snd x = 0"]
    by auto
next
  case (Suc n)
  from Suc obtain S' where
    S: "S' = {t :: ('a, 'b) term . ground t ∧ funas_term t ⊆ ℱ ∧ depth t ≤ n}" "finite S'"
    by (auto simp add: SUP_le_iff)
  then obtain L F where L: "set L = S'" "set F = ℱ" using fin_F by (meson finite_list)
  let ?Sn = "{Fun f ts | f ts. (f, length ts) ∈ ℱ ∧ set ts ⊆ S'}"
  let ?Ln = "concat (map (λ (f, n). map (λ ts. Fun f ts) (list_of_permutation_n L n)) F)"
  {fix t assume elem: "t ∈ S"
    from Suc have "depth t ≤ Suc n" "ground t" "funas_term t ⊆ ℱ" using elem by auto
    then have "funas_term t ⊆ ℱ ∧ (∀ x ∈ set (args t). depth x ≤ n) ∧ ground t"
      by (cases t rule: depth.cases) auto
    then have "t ∈ ?Sn ∪ S'"
      using S by (cases t) auto} note sub = this
  {fix t assume elem: "t ∈ ?Sn"
    then obtain f ts where [simp]: "t = Fun f ts" and invar: "(f, length ts) ∈ ℱ" "set ts ⊆ S'"
      by blast
    then have "Fun f ts ∈ set (map (λ ts. Fun f ts) (list_of_permutation_n L (length ts)))"
      using list_fun_sym_eq_set[of L "length ts"] L by (auto simp: image_iff) 
    then have "t ∈ set ?Ln" using invar(1) L(2) by auto}
  from this sub have sub: "?Sn ⊆ set ?Ln" "S ⊆ ?Sn ∪ S'" by blast+
  from finite_subset[OF sub(1)] finite_subset[OF sub(2)] finite_UnI[of ?Sn, OF _ S(2)]
  show ?case 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 infinite_inj_image_infinite:
  assumes "infinite S" and "inj_on f S"
  shows "infinite (f ` S)"
  using assms finite_image_iff by blast

lemma infinite_set_restrict_to_property:
  assumes "⋀ x. x ∈ S ⟹ P x" "infinite S"
  shows "infinite {t| t. P t}" using assms
  by (metis (mono_tags, lifting) Ball_Collect in_mono infinite_iff_countable_subset)

lemma infinite_presev_remove_prop:
  assumes "infinite {t. P t ∧ Q t}"
  shows "infinite {t. P t}"
  using assms by auto

(*The following lemma tells us that number of terms greater than a certain depth are infinite*)
lemma infinte_no_depth_limit:
  assumes "infinite S" and "finite ℱ"
    and "∀t ∈ S. funas_term t ⊆ ℱ" and "∀t ∈ S. ground t"
  shows "∀(n::nat). ∃t ∈ S. n < (depth t)"
proof(rule allI, rule ccontr)
  fix n::nat
  assume "¬ (∃t ∈ S. (depth t) >  n)"
  hence "∀t ∈ S. depth t ≤ n" by auto
  from bounded_depth_finite[OF assms(2) _ this] show False using assms
    by auto
qed

lemma inf_ground_terms_to_gterms:
  assumes "infinite {t . ground t ∧ P t}" (is "infinite ?T")
  shows "infinite {t .  P (term_of_gterm t)}" (is "infinite ?S")
proof -
  have "inj_on gterm_of_term {t. ground t ∧ P t}" using gterm_of_term_inv by (fastforce simp: inj_on_def)
  from infinite_inj_image_infinite[OF assms this] show ?thesis unfolding image_Collect
    by auto (smt Collect_cong ground_term_of_gterm gterm_of_term_inv term_of_gterm_inv)
qed


lemma depth_gterm_conv:
  shows "depth (term_of_gterm t) = depth (term_of_gterm t)"
  by (metis leD nat_neq_iff poss_gposs_conv poss_length_bounded_by_depth poss_length_depth)

lemma funs_term_ctxt [simp]:
  "funs_term C⟨s⟩ = funs_ctxt C ∪ funs_term s"
  by (induct C) auto


definition "rule_st t 𝒜 q = (∃ qs. (fst (the (root t))) qs → q ∈ ta_rules 𝒜 ∧
  length qs = length (args t) ∧
  (∀ i < length (args t). qs ! i ∈ ta_res 𝒜 (args t ! i)))"

lemma ta_res_to_rule_st:
  assumes "q ∈ ta_res 𝒜 t" and "is_Fun t"
  obtains p where "rule_st t 𝒜 p" "(p, q) ∈ (ta_eps 𝒜)⇧*"
  using assms by (cases t) (auto simp: rule_st_def)

lemma ta_res_to_rule_st_ground:
  assumes "q ∈ ta_res 𝒜 t" and "ground t"
  obtains p where "rule_st t 𝒜 p" "(p, q) ∈ (ta_eps 𝒜)⇧*"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_res:
  assumes "rule_st t 𝒜 p" and "is_Fun t"
  shows "p ∈ ta_res 𝒜 t"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_res_ground:
  assumes "rule_st t 𝒜 p" and "ground t"
  shows "p ∈ ta_res 𝒜 t"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_ctxt:
  assumes "rule_st C⟨Var q⟩ 𝒜 p" "q ∈ ta_res 𝒜 t" and "C ≠ □"
  shows "rule_st C⟨t⟩ 𝒜 p" using assms
proof (induct C)
  case (More f ss C ts)
  then show ?case by (auto simp: rule_st_def) (metis append_Cons_nth_not_middle nth_append_length ta_res_ctxt)
qed auto

lemma pigeonhole_ta_infinit_terms:
  assumes "card (ta_states 𝒜) < depth t" and "finite (ta_states 𝒜)" and "q ∈ ta_res 𝒜 t"
    and "ground t" and "P (funas_term t)"
  shows "infinite {t . q ∈ ta_res 𝒜 t ∧ ground t ∧ P (funas_term t)}"
proof -
  from pigeonhole_tree_automata[OF assms(1 - 4)]
  obtain C C2 s v p where ctxt: "C2 ≠ □" "C⟨s⟩ = t" "C2⟨v⟩ = s" and
    loop: "p ∈ ta_res 𝒜 v" "p ∈ ta_res 𝒜 C2⟨Var p⟩" "q ∈ ta_res 𝒜 C⟨Var p⟩" by blast
  let ?terms = "λ n. C⟨(C2 ^n)⟨v⟩⟩" let ?inner = "λ n. (C2 ^n)⟨v⟩"
  have gr: "ground_ctxt C2" "ground_ctxt C" "ground v" using ctxt assms(4) by (metis ground_ctxt_apply)+
  have "q ∈ ta_res 𝒜  (C ∘⇩c C2)⟨Var p⟩" "is_Fun (C ∘⇩c C2)⟨Var p⟩" using ctxt loop assms(3)
    by (auto simp: ta_res_ctxt) (metis Var_supt ctxt.cop_add ctxt_comp_rhs_not_hole is_Var_def nectxt_imp_supt_ctxt) 
  let ?P = "λ t. q ∈ ta_res 𝒜 t ∧ ground t ∧ P (funas_term t)"
  from ctxt have "t ⊳ v" using ctxt_comp_rhs_not_hole ctxt_ctxt by blast
  moreover have "P (funas_term (?terms (Suc n)))" for n using ctxt assms(5)
    by  (auto simp: vars_term_ctxt_apply) (metis Un_absorb2 ctxt_comp_n_pres_funas sup.idem sup.orderI sup_assoc)
  moreover have "q ∈ ta_res 𝒜 (?terms (Suc n))" for n using loop
    by auto (meson ta_res_ctxt ta_res_ctxt_n_loop)
  ultimately have "?P (?terms (Suc n))" for n using gr
    by (metis ctxt_comp_n_pres_ground ground_ctxt_apply)
  then show ?thesis
    using order.strict_trans2[OF ctxt_comp_n_lower_bound[OF ctxt(1)] depth_ctxt_less_eq[of "?inner (Suc n)" C for n]]
    using no_upper_bound_infinite[of _ depth, of "{t. q ∈ ta_res 𝒜 t ∧ ground t ∧ P (funas_term t)}"]
     by blast
qed


lemma gterm_to_None_Some_funas [simp]:
  "funas_gterm (gterm_to_None_Some t) ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ ⟷ funas_gterm t ⊆ ℱ"
  by (induct t) (auto simp: funas_gterm_def, blast)

lemma funas_gterm_bot_some_decomp:
  assumes "funas_gterm s ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ"
  shows "∃ t. gterm_to_None_Some t = s" using assms
proof (induct s)
  case (GFun f ts)
  from GFun(1)[OF nth_mem] obtain ss where "length ss = length ts ∧ (∀i<length ts. gterm_to_None_Some (ss ! i) = ts ! i)"
    using Ex_list_of_length_P[of "length ts" "λ s i. gterm_to_None_Some s = ts ! i"] GFun(2-)
    by (auto simp: funas_gterm_def) (meson UN_subset_iff nth_mem) 
  then show ?case using GFun(2-)
    by (cases f) (auto simp: funas_gterm_def map_nth_eq_conv intro: exI[of _ "GFun (the (snd f)) ss"])
qed

(* Definition INF, Q_infinity and automata construction *)

abbreviation CInl :: "'q ⇒ 'q + 'q" where "CInl ≡ Inl"
abbreviation CInr :: "'q ⇒ 'q + 'q" where "CInr ≡ Inr"

lemma inj_CInl: "inj CInl" using inj_Inl by blast

definition "Inf_branching_terms ℛ ℱ = {t . infinite {u. (t, u) ∈ ℛ ∧ funas_gterm u ⊆ ℱ} ∧ funas_gterm t ⊆ ℱ}"

definition "Q_infty 𝒜 ℱ = {q | q. infinite {t | t. funas_gterm t ⊆ ℱ ∧ q ∈ ta_res 𝒜 (term_of_gterm (gterm_to_None_Some t))}}"

abbreviation q_inf_dash_intro_rules where
  "q_inf_dash_intro_rules Q r ≡ if (r_rhs r) ∈ Q ∧ fst (r_root r) = None then {(r_root r) (map CInl (r_lhs_states r)) → CInr (r_rhs r)} else {}"

abbreviation args :: "'a list ⇒ nat ⇒ ('a + 'a) list" where
  "args ≡ λ qs i. map CInl (take i qs) @ CInr (qs ! i) # map CInl (drop (Suc i) qs)"

abbreviation q_inf_dash_closure_rules :: "('q, 'f) ta_rule ⇒ ('q + 'q, 'f) ta_rule list" where
  "q_inf_dash_closure_rules r ≡ (let (f, qs, q) = (r_root r, r_lhs_states r, r_rhs r) in
   (map (λ i. f (args qs i) → CInr q) [0 ..< length qs]))"

definition Inf_automata :: "('q, 'f option × 'f option) ta ⇒ 'q set ⇒ ('q + 'q, 'f option × 'f option) ta" where
  "Inf_automata 𝒜 𝒬 = ta.make (Inr ` ta_final 𝒜)
  (⋃ (q_inf_dash_intro_rules 𝒬 ` ta_rules 𝒜) ∪ ⋃ ((set ∘ q_inf_dash_closure_rules) ` ta_rules 𝒜) ∪
   map_ta_rule CInl id ` ta_rules 𝒜) (map_both Inl ` ta_eps 𝒜 ∪ map_both CInr ` ta_eps 𝒜)"

lemma Inr_Inl_rel_comp:
  "map_both CInr ` S O map_both CInl ` S = {}" by auto

lemmas eps_split = rtrancl_Un2_separatorE[OF Inr_Inl_rel_comp]

lemma Inf_automata_eps_simp [simp]:
  shows "(map_both Inl ` ta_eps 𝒜 ∪ map_both CInr ` ta_eps 𝒜)⇧* =
      (map_both CInl ` ta_eps 𝒜)⇧* ∪ (map_both CInr ` ta_eps 𝒜)⇧*"
  by (auto simp: Inf_automata_def eps_split elim: converse_rtranclE rtranclE)

lemma Inf_automata_Inl_to_eps [simp]:
  "(CInl p, CInl q) ∈ (map_both CInl ` ta_eps 𝒜)⇧* ⟷ (p, q) ∈ (ta_eps 𝒜)⇧*"
  "(CInr p, CInr q) ∈ (map_both CInr ` ta_eps 𝒜)⇧* ⟷ (p, q) ∈ (ta_eps 𝒜)⇧*"
  "(CInr q, CInr p) ∈ (map_both CInl ` ta_eps 𝒜)⇧* ⟷ q = p"
  "(CInl q, CInl p) ∈ (map_both CInr ` ta_eps 𝒜)⇧* ⟷ q = p"
  by (auto simp: rtrancl_eq_or_trancl trancl_map_both)

lemma Inl_eps_Inr:
  "(CInl q, CInl p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧* ⟷ (CInr q, CInr p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧*"
  by (auto simp: Inf_automata_def)

lemma Inr_rhs_eps_Inr_lhs:
  assumes "(q, CInr p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧*"
  obtains q' where "q = CInr q'" using assms
  by (cases q) (auto simp: Inf_automata_def rtrancl_eq_or_trancl trancl_map_both)

lemma Inl_rhs_eps_Inl_lhs:
  assumes "(q, CInl p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧*"
  obtains q' where "q = CInl q'" using assms
  by (cases q) (auto simp: Inf_automata_def rtrancl_eq_or_trancl trancl_map_both)

lemma Inf_automata_eps [simp]:
  "(CInl q, CInr p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧* ⟷ False"
  "(CInr q, CInl p) ∈ (ta_eps (Inf_automata 𝒜 𝒬))⇧* ⟷ False"
  by (auto elim: Inr_rhs_eps_Inr_lhs Inl_rhs_eps_Inl_lhs)

lemma ta_res_fmap_states_final_mono:
  "CInl ` ta_final 𝒜 = ta_final (fmap_states_ta CInl 𝒜)"
  by (simp add: fmap_states_ta_def')

lemma Inl_A_res_Inf_automata:
  "ta_res (fmap_states_ta CInl 𝒜) t ⊆ ta_res (Inf_automata 𝒜 𝒬) t"
  by (intro ta_res_mono') (auto simp: Inf_automata_def fmap_states_ta_def')

lemma Inl_res_A_res_Inf_automata:
  "CInl ` ta_res 𝒜 (term_of_gterm t) ⊆ ta_res (Inf_automata 𝒜 𝒬) (term_of_gterm t)"
  by (intro subset_trans[OF ta_res_fmap_states_ta_mono[of CInl 𝒜 t]]) (auto simp: Inl_A_res_Inf_automata)

lemma r_rhs_CInl_args_A_rule:
  assumes "f qs → CInl q ∈ ta_rules (Inf_automata 𝒜 𝒬)"
  obtains qs' where "qs = map CInl qs'" "f qs' → q ∈ ta_rules 𝒜" using assms
  by (auto simp: Inf_automata_def)

lemma A_rule_to_dash_closure:
  assumes "f qs → q ∈ ta_rules 𝒜" and "i < length qs"
  shows "f (args qs i) → CInr q ∈ ta_rules (Inf_automata 𝒜 𝒬)"
  using assms by (auto simp add: Inf_automata_def) fastforce


lemma Inf_automata_reach_to_dash_reach:
  assumes "CInl p ∈ ta_res (Inf_automata 𝒜 𝒬) C⟨Var (CInl q)⟩"
  shows "CInr p ∈ ta_res (Inf_automata 𝒜 𝒬) C⟨Var (CInr q)⟩" (is "_ ∈ ta_res ?A _")
  using assms
proof (induct C arbitrary: p)
  case (More f ss C ts)
  from More(2) obtain qs q' where
    rule: "f qs → q' ∈ ta_rules ?A" "length qs = Suc (length ss + length ts)" and
    eps: "(q', CInl p) ∈ (ta_eps ?A)⇧*" and
    reach: "∀ i <  Suc (length ss + length ts). qs ! i ∈ ta_res ?A ((ss @ C⟨Var (CInl q)⟩ # ts) ! i)"
    by (auto simp: map_append_Cons_nth)
  from eps obtain q'' where [simp]: "q' = CInl q''"
    by (cases q') (auto simp add: Inf_automata_def eps_split elim: rtranclE converse_rtranclE)
  from rule obtain qs' where args: "qs = map CInl qs'" "f qs' → q'' ∈ ta_rules 𝒜"
    using r_rhs_CInl_args_A_rule by (metis ‹q' = CInl q''›)
  then have "CInl (qs' ! length ss) ∈ ta_res (Inf_automata 𝒜 𝒬) C⟨Var (CInl q)⟩" using reach
    by (auto simp: all_Suc_conv nth_append_Cons) (metis length_map less_add_Suc1 local.rule(2) nth_append_length nth_map reach) 
  from More(1)[OF this] More(2) show ?case
    using rule args eps reach A_rule_to_dash_closure[OF args(2), of "length ss" 𝒬]
    by (auto simp: map_append_Cons_nth Inl_eps_Inr id_take_nth_drop all_Suc_conv
        intro!: exI[of _ "CInr q''"] exI[of _ "map CInl (take (length ss) qs') @ CInr (qs' ! length ss) # map CInl (drop (Suc (length ss)) qs')"])
      (auto simp: nth_append_Cons min_def)
qed (auto simp: Inf_automata_def)

lemma res_rule_st_Inf_automata_dash:
  assumes "rule_st (term_of_gterm (gterm_to_None_Some t)) 𝒜 p" and "p ∈ 𝒬"
  shows "CInr p ∈ ta_res (Inf_automata 𝒜 𝒬) (term_of_gterm (gterm_to_None_Some t))" (is "CInr p ∈ ta_res ?A _")
proof (cases t)
  case [simp]: (GFun f ts)
  from rule_st_res[OF assms(1)] assms(1) obtain qs where
    rule: "(None, Some f) qs → p ∈ ta_rules 𝒜" "length qs = length ts" and
    reach: "∀ i < length ts. qs ! i ∈ ta_res 𝒜 (term_of_gterm (gterm_to_None_Some (ts  ! i)))"
    by (auto simp: map_append_Cons_nth rule_st_def)
  from rule assms(2) have "(None, Some f) (map CInl qs) → CInr p ∈ ta_rules ?A"
    by (auto simp: Inf_automata_def) force
  then show ?thesis using reach rule Inl_res_A_res_Inf_automata[of 𝒜 "gterm_to_None_Some (ts ! i)" 𝒬 for i]
    by (auto intro!: exI[of _ "CInr p"]  exI[of _ "map CInl qs"]) blast
qed

lemma Inf_automata_dash_reach_to_reach:
  assumes "p ∈ ta_res (Inf_automata 𝒜 𝒬) t" (is "_ ∈ ta_res ?A _")
  shows "remove_sum p ∈ ta_res 𝒜 (map_vars_term remove_sum t)" using assms
proof (induct t arbitrary: p)
  case (Fun f ss)
  from Fun(2) obtain qs q' where
    rule: "f qs → q' ∈ ta_rules ?A" "length qs = length ss" and
    eps: "(q', p) ∈ (ta_eps ?A)⇧*" and
    reach: "∀ i <  length ss. qs ! i ∈ ta_res ?A (ss ! i)" by auto
  from rule have r: "f (map (remove_sum) qs) → (remove_sum q') ∈ ta_rules 𝒜"
    by (auto simp: comp_def Inf_automata_def min_def id_take_nth_drop[symmetric] simp flip: drop_map take_map)
  moreover have "(remove_sum q', remove_sum p) ∈ (ta_eps 𝒜)⇧*" using eps
    by (cases "is_Inl q'"; cases "is_Inl p") (auto elim!: is_InlE is_InrE, auto simp: Inf_automata_def)
  ultimately show ?case using reach rule(2) Fun(1)[OF nth_mem, of i "qs ! i" for i]
    by auto (metis (mono_tags, lifting) length_map map_nth_eq_conv)
qed (auto simp: Inf_automata_def rtrancl_eq_or_trancl trancl_map_both)

lemma depth_poss_split:
  assumes "Suc (depth (term_of_gterm t) + n) < depth (term_of_gterm u)"
  shows "∃ p q. p @ q ∈ gposs u ∧ n < length q ∧ p ∉ gposs t"
proof -
  from poss_length_depth obtain p m where p: "p ∈ gposs u" "length p = m" "depth (term_of_gterm u) = m"  using poss_gposs_conv by blast
  then obtain m' where dt: "depth (term_of_gterm t) = m'" by blast
  have nt: "take (Suc m') p ∉ gposs t" using poss_length_bounded_by_depth dt depth_gterm_conv
    by (metis Suc_leI add_Suc_right add_lessD1 assms leD length_take lessI min.absorb2 p(2, 3))
  moreover have "n < length (drop (Suc m') p)" using assms depth_gterm_conv dt p(2-)
    by (metis add_Suc diff_diff_left length_drop zero_less_diff) 
  ultimately show ?thesis by (metis append_take_drop_id p(1))
qed

lemma gpair_poss_lang_split_ctxt_rule_st:
  assumes "p ∈ gposs (gpair t u)" and "gpair t u ∈ gta_lang 𝒜"
  shows "∃ q q'. CInl q ∈ ta_final (fmap_states_ta CInl 𝒜) ∧
    CInl q ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gpair t u)) ∧
    rule_st (term_of_gterm (gsubt_at (gpair t u) p)) 𝒜 q' ∧
    CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p)) ∧
    CInl q ∈ ta_res (fmap_states_ta CInl 𝒜) (ctxt_of_pos_term p (term_of_gterm (gpair t u)))⟨Var (CInl q')⟩"
proof -
  let ?t_of_g = "λ t. term_of_gterm t :: ('a option × 'b option, 'c + 'c) term"
  define C where "(C :: ('a option × 'b option, 'c + 'c) ctxt) = ctxt_of_pos_term p (?t_of_g (gpair t u))"
  then have gp_ctxt: "gterm_of_term C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩ = gpair t u"
    using assms(1) ctxt_of_pos_gterm_gsubt_at_to_gterm gpair_poss_args_poss poss_append_poss by blast
  then have gr_ctxt: "ground_ctxt C" using assms(1) unfolding C_def
    by (metis ctxt_supt_id ground_ctxt_apply ground_term_of_gterm poss_gposs_conv)
  then have gr_term: "ground C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩"
    using ground_ctxt_apply ground_term_of_gterm by blast
  obtain q' where lang: "CInl q' ∈ ta_final (fmap_states_ta CInl 𝒜)"  
    "CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gpair t u))"
    using assms(2) ta_res_fmap_states_ta_mono[of CInl 𝒜 "gpair t u"] ta_res_fmap_states_final_mono[of 𝒜]
    by (auto elim!: gta_langE)
  from lang(2) have reach_fin: "CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩"
    using gp_ctxt gr_term gterm_of_term_inv by fastforce
  obtain q where reach_CInl: "CInl q ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))"
    "CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) C⟨Var (CInl q)⟩"
    using ta_res_ctxt_decompose[OF reach_fin]
    by auto (metis image_iff ta_res_gterm_states ta_states_fmap_states_ta)
  then have "q ∈ ta_res 𝒜 (term_of_gterm (gsubt_at (gpair t u) p))"
    using ta_res_fmap_states_ta_mono2[OF inj_CInl] by blast
  from ta_res_to_rule_st_ground[OF this] obtain q'' where
    rule_st: "rule_st (term_of_gterm (gsubt_at (gpair t u) p)) 𝒜 q''" and
    eps: "(q'', q) ∈ (ta_eps 𝒜)⇧*" by auto
  from rule_st_res_ground[OF rule_st] have reach: "q'' ∈ ta_res 𝒜 (term_of_gterm (gsubt_at (gpair t u) p))" by auto
  then have r: "CInl q'' ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))"
    "(CInl q'', CInl q) ∈ (ta_eps (fmap_states_ta CInl 𝒜))⇧*"
    using ta_res_fmap_states_ta_mono[of CInl 𝒜 "gsubt_at (gpair t u) p"]
    by blast (auto simp: fmap_states_ta_def' eps) 
  then show ?thesis using lang reach_CInl C_def rule_st ta_res_eps_ctxt[OF _ r(2)] by blast
qed

lemma Inf_to_automata:
  assumes "RR2_spec 𝒜 ℛ" and "finite ℱ" and "finite (ta_states 𝒜)" and "t ∈ Inf_branching_terms ℛ ℱ"
  shows "∃ u. gpair t u ∈ gta_lang (Inf_automata 𝒜 (Q_infty 𝒜 ℱ))" (is "∃ u. gpair t u ∈ gta_lang ?A")
proof -
  let ?t_of_g = "λ t. term_of_gterm t :: ('b, 'a) term"
  let ?t_of_gp = "λ t. term_of_gterm t :: ('b option × 'b option, 'a) term"
  let ?none_t = "λ t. term_of_gterm (gterm_to_None_Some t) :: ('b option × 'b option, 'a) term"
  from assms(3) obtain n where depth_card: "depth (?t_of_g t) + card (ta_states 𝒜) < n" by auto
  from assms(1, 4) have fin: "infinite {u. gpair t u ∈ gta_lang 𝒜 ∧ funas_gterm u ⊆ ℱ}"
    by (auto simp: RR2_spec_def Inf_branching_terms_def)
  from infinte_no_depth_limit[of "?t_of_g ` {u. gpair t u ∈ gta_lang 𝒜 ∧ funas_gterm u ⊆ ℱ}", OF _ assms(2)] this
  have "∀ n. ∃t ∈ ?t_of_g ` {u. gpair t u ∈ gta_lang 𝒜 ∧ funas_gterm u ⊆ ℱ}. n < depth t"
    by (simp add: infinite_inj_image_infinite[OF fin] funas_term_of_gterm_conv inj_term_of_gterm)
  from this depth_card obtain u where funas: "funas_gterm u ⊆ ℱ" and
    depth: "Suc n < depth (?t_of_g u)" and lang: "gpair t u ∈ gta_lang 𝒜" by auto
  have "Suc (depth (term_of_gterm t) + card (ta_states 𝒜)) < depth (term_of_gterm u)"
    using depth depth_card by (metis Suc_less_eq2 depth_gterm_conv less_trans)
  from depth_poss_split[OF this] obtain p q where
    pos: "p @ q ∈ gposs u ∧ card (ta_states 𝒜) < length q ∧ p ∉ gposs t" by auto
  then have gp: "gsubt_at (gpair t u) p = gterm_to_None_Some (gsubt_at u p)" by auto
  define C where "(C :: ('b option × 'b option, 'a + 'a) ctxt) = ctxt_of_pos_term p (term_of_gterm (gpair t u))"
  have gp_split: "gterm_of_term C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩ = gpair t u" unfolding C_def
    using ctxt_of_pos_gterm_gsubt_at_to_gterm gpair_poss_args_poss poss_append_poss pos by blast
  have gr_ctxt: "ground_ctxt C" using pos unfolding C_def
    by (metis ctxt_supt_id gpair_poss_args_poss ground_ctxt_apply ground_term_of_gterm poss_append_poss poss_gposs_conv)
  from pos gpair_poss_lang_split_ctxt_rule_st[OF _ lang] obtain q' q'' where
    lang: "CInl q' ∈ ta_final (fmap_states_ta CInl 𝒜)" "CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gpair t u))" and
    rule_st: "rule_st (term_of_gterm (gsubt_at (gpair t u) p)) 𝒜 q''" and
    reach_rule_st: "CInl q'' ∈ ta_res (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))" and
    reach_fin: "CInl q' ∈ ta_res (fmap_states_ta CInl 𝒜) C⟨Var (CInl q'')⟩"
    by (auto simp: C_def) force
  from reach_fin have reach_fin: "CInl q' ∈ ta_res ?A C⟨Var (CInl q'')⟩"
    using Inl_A_res_Inf_automata[of 𝒜 "C⟨Var (CInl q'')⟩"] by blast
  from lang(1) have fin: "CInr q' ∈ ta_final ?A" using ta_res_fmap_states_final_mono
    by (auto simp: Inf_automata_def) fastforce
  from reach_rule_st have reach: "q'' ∈ ta_res 𝒜 (term_of_gterm (gsubt_at (gpair t u) p))"
    using ta_res_fmap_states_ta_mono2[OF inj_CInl, of 𝒜] by blast
  have c: "card (ta_states 𝒜) < depth (?none_t (gsubt_at u p))" using pos
    by (smt gposs_gsubst_at_subst_at_eq gposs_map_gterm le_trans not_le poss_append_poss poss_gposs_conv poss_length_bounded_by_depth)
  have "funas_term (?none_t (gsubt_at u p)) ⊆ (λ(f, n). ((None, Some f), n)) ` ℱ"
    using funas pos funas_poss_presv[OF funas, of p] by (auto simp: funas_term_of_gterm_conv)
  from this pigeonhole_ta_infinit_terms[OF c assms(3), of _ "λ t. t ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ"]
  have "infinite {t. ground t ∧ q'' ∈ ta_res 𝒜 t  ∧ funas_term t ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ}"
    using reach by (auto simp: gp) (metis (mono_tags, lifting) Collect_cong) 
  then have "infinite {t. q'' ∈ ta_res 𝒜 (term_of_gterm t) ∧ funas_gterm t ⊆ (λ(f, n). ((None, Some f), n)) ` ℱ}"
    using inf_ground_terms_to_gterms[of "λ t. q'' ∈ ta_res 𝒜 t ∧ funas_term t ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ"]
    by (auto simp: funas_term_of_gterm_conv)
  from infinite_set_dec_infinite[OF this, of gterm_to_None_Some "λ t. funas_gterm t ⊆ ℱ"]
  have "q'' ∈ Q_infty 𝒜 ℱ" using funas_gterm_bot_some_decomp unfolding Q_infty_def
    by auto (smt Collect_cong funas_gterm_bot_some_decomp gterm_to_None_Some_funas)
  from res_rule_st_Inf_automata_dash rule_st this Inf_automata_reach_to_dash_reach[OF reach_fin]
  have "CInr q' ∈ ta_res (Inf_automata 𝒜 (Q_infty 𝒜 ℱ)) (term_of_gterm (gpair t u))"
    using gp_split gr_ctxt by (metis gp ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv ta_res_ctxt)  
  then show ?thesis using fin by (auto intro!: exI[of _ u] elim!: gta_langI)
qed

lemma CInr_Inf_automata_to_q_state:
  assumes "CInr p ∈ ta_res (Inf_automata 𝒜 𝒬) t" and "ground t"
  shows "∃ C s q. C⟨s⟩ = t ∧ CInr q ∈ ta_res (Inf_automata 𝒜 𝒬) s ∧ q ∈ 𝒬 ∧ CInr p ∈ ta_res (Inf_automata 𝒜 𝒬) C⟨Var (CInr q)⟩ ∧
    (fst ∘ fst ∘ the ∘ root) s = None" using assms
proof (induct t arbitrary: p)
  case (Fun f ts)
  let ?A = "(Inf_automata 𝒜 𝒬)"
  from Fun(2) obtain qs q' where
    rule: "f qs → CInr q' ∈ ta_rules ?A" "length qs = length ts" and
    eps: "(CInr q', CInr p) ∈ (ta_eps ?A)⇧*" and
    reach: "∀ i < length ts. qs ! i ∈ ta_res ?A (ts ! i)"
    by auto (metis Inr_rhs_eps_Inr_lhs)
  consider (a) "⋀ i. i < length qs ⟹ ∃ q''. qs ! i = CInl q''" | (b) "∃ i < length qs. ∃ q''. qs ! i = CInr q''"
    by (meson remove_sum.cases)
  then show ?case
  proof cases
    case a
    then have "f qs → CInr q' ∈ ⋃ (q_inf_dash_intro_rules 𝒬 ` ta_rules 𝒜)" using rule
      by (auto simp: Inf_automata_def min_def) (metis (no_types, lifting) Inl_Inr_False length_map length_take less_imp_le_nat min.absorb2 nth_append_length) 
    then show ?thesis using reach eps rule(2)
      apply (auto intro!: exI[of _ Hole])
      using rule reach by blast
  next
    case b
    then obtain i q'' where b: "i < length ts" "qs ! i = CInr q''" using rule(2) by auto
    then have "CInr q'' ∈ ta_res ?A (ts ! i)" using rule(2) reach by auto 
    from Fun(3) Fun(1)[OF nth_mem, OF b(1) this] b rule(2) obtain C s q''' where
      ctxt: "C⟨s⟩ = ts ! i" and
      qinf: "CInr q''' ∈ ta_res (Inf_automata 𝒜 𝒬) s ∧ q''' ∈ 𝒬" and
      reach2: "CInr q'' ∈ ta_res (Inf_automata 𝒜 𝒬) C⟨Var (CInr q''')⟩" and
      "(fst ∘ fst ∘ the ∘ root) s = None"
      by auto
    then show ?thesis using rule eps reach ctxt qinf reach2 b(1) b(2)[symmetric]
      by (auto simp: min_def nth_append_Cons simp flip: map_append id_take_nth_drop[OF b(1)]
        intro!: exI[of _ "More f (take i ts) C (drop (Suc i) ts)"] exI[of _ "s"] exI[of _ "q'''"] exI[of _ "CInr q'"] exI[of _ "qs"])
  qed
qed auto

lemma aux_lemma:
  assumes "RR2_spec 𝒜 ℛ" and "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
    and "infinite {u | u. gpair t u ∈ gta_lang 𝒜}"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
  using assms unfolding RR2_spec_def Inf_branching_terms_def
  apply (auto) apply (smt Collect_cong basic_trans_rules(31) mem_Collect_eq mem_Sigma_iff)
  using not_finite_existsD by fastforce

lemma Inf_automata_to_Inf:
  assumes "RR2_spec 𝒜 ℛ" and "finite ℱ" and "finite (ta_states 𝒜)"
    and "ℛ ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
    and "gpair t u ∈ gta_lang (Inf_automata 𝒜 (Q_infty 𝒜 ℱ))"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
proof -
  let ?g_to_term = "λ t. term_of_gterm t :: ('b, unit) term"
  let ?t_to_germ = "λ t. gterm_of_term t :: 'b gterm"
  let ?A = "Inf_automata 𝒜 (Q_infty 𝒜 ℱ)"
  from assms(5) obtain q where fin: "CInr q ∈ ta_final ?A" and
    reach_fin: "CInr q ∈ ta_res ?A (term_of_gterm (gpair t u))"
    by (auto simp: Inf_automata_def elim!: gta_langE) blast
  from CInr_Inf_automata_to_q_state[OF reach_fin] obtain C s p where
    ctxt: "C⟨s⟩ = term_of_gterm (gpair t u)" and
    q_inf_st: "CInr p ∈ ta_res ?A s" "p ∈ Q_infty 𝒜 ℱ" and
    reach: "CInr q ∈ ta_res ?A C⟨Var (CInr p)⟩" and
    none: "(fst ∘ fst ∘ the ∘ root) s = None" by auto
  let ?C = "ctxt_of_pos_term (hole_pos C) (term_of_gterm u :: ('b, unit) term)"
  from ctxt have gr_ctxt: "ground_ctxt C" and gr_term: "ground s"
    by (metis ground_ctxt_apply ground_term_of_gterm)+
  {assume ass: "hole_pos C ∈ gposs t"
    then have "∃ f h. gfun_at (gpair t u) (hole_pos C) = Some (Some f, h)"
      using fun_at_gfun_at_conv poss_gposs_conv gfun_at_poss by auto
    moreover have "gfun_at (gpair t u) (hole_pos C) = fun_at C⟨s⟩ (hole_pos C)"
      using fun_at_gfun_at_conv ctxt by (metis hole_pos_poss poss_gposs_conv)
    ultimately have False using ctxt[symmetric] none by (cases s) (auto)}
  then have nt_pos_t [simp]: "hole_pos C ∉ gposs t" and pos_u [simp]: "hole_pos C ∈ gposs u"
    using ctxt by auto (metis gpair_poss_args_poss hole_pos_poss poss_gposs_conv)
  have  fun_gr_C': "ground_ctxt ?C" by auto
  from nt_pos_t pos_u ctxt have [simp]: "s = term_of_gterm (gterm_to_None_Some (gsubt_at u (hole_pos C)))"
    by (metis gr_term gsubt_at_ctxt_pos gterm_of_term_inv subst_at_gpair_nt_poss_None_Some term_of_gterm_inv)
  let ?S = "{t. funas_gterm t ⊆ ℱ ∧ p ∈ ta_res 𝒜 (term_of_gterm (gterm_to_None_Some t))}"
  let ?S' = "{(gctxt_apply (ctxt_of_pos_term (hole_pos C) (term_of_gterm u)) w) | w.
    p ∈ ta_res 𝒜 (term_of_gterm (gterm_to_None_Some w)) ∧ funas_gterm w ⊆ ℱ}"
  from infinite_inj_image_infinite have  "infinite (?g_to_term ` ?S)" using inj_term_of_gterm q_inf_st(2)
    by (auto simp: Q_infty_def)
  from infinite_inj_image_infinite[OF this] have "infinite (ctxt_apply_term ?C ` ?g_to_term ` ?S)" by (smt ctxt_eq inj_on_def)
  from infinite_inj_image_infinite[OF this] have "infinite (?t_to_germ ` ctxt_apply_term ?C ` ?g_to_term ` ?S)"
    using fun_gr_C' by (smt ground_ctxt_apply ground_term_of_gterm gterm_of_term_inj imageE)
  then have inf: "infinite ?S'" unfolding image_comp
    by (auto simp add: image_Collect) (smt Collect_cong finite_Collect_conjI) 
  {fix u assume "u ∈ ?S'" then obtain w where u: "u = gctxt_apply ?C w" and
      fun_r: "funas_gterm w ⊆ ℱ ∧ p ∈ ta_res 𝒜 (term_of_gterm (gterm_to_None_Some w))"
      by (auto simp add: image_Collect image_comp)
    have conv: "gpair t (gctxt_apply ?C w) = gterm_of_term C⟨term_of_gterm (gterm_to_None_Some w)⟩" for w
      using ctxt[symmetric] by simp (metis gpair_ctxt_decomposition_2 gr_ctxt nt_pos_t term_of_gterm_inv)  
    from fun_r have "q ∈ ta_res 𝒜 (term_of_gterm (gpair t u))" unfolding u conv
      using Inf_automata_dash_reach_to_reach[OF reach] gr_ctxt 
      by (auto simp: map_vars_term_ctxt_commute ground_ctxt_map_vars_to_adpat gterm_of_term_inv' adapt_vars_term_of_gterm ta_res_ctxt)
    then have "gpair t u ∈ gta_lang 𝒜" using conjunct1[OF fun_r] fin
      by (auto simp: Inf_automata_def gta_langI)}
  from this infinite_set_restrict_to_property[OF _ inf, of "λ u. gpair t u ∈ gta_lang 𝒜"]
  have "infinite {u. gpair t u ∈ gta_lang 𝒜}" by auto
  from aux_lemma[OF assms(1, 4), of t] this show ?thesis by auto
qed

end