Theory RR2_infinite_Impl

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

theory RR2_infinite_Impl
  imports RR2_Infinite GTT_Impl Horn_Autoref
begin

(*Trivial facts about states *)
lemma r_lhs_states:
  assumes "f qs → q ∈ ta_rules 𝒜" "i < length qs"
  shows "qs ! i ∈ ta_states 𝒜"
  using assms unfolding ta_states_def r_states_def by fastforce

lemma ta_eps_single_ta_states:
  assumes "(p, q) ∈ ta_eps 𝒜"
  shows "p ∈ ta_states 𝒜" "q ∈ ta_states 𝒜"
  using assms by (auto simp: ta_states_def)

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 :: "('q, 'f option × 'f option) ta ⇒ ('q × 'q) set" for 𝒜 where
  trans: "(p, q) ∈ Q_inf 𝒜 ⟹ (q, r) ∈ Q_inf 𝒜 ⟹ (p, r) ∈ Q_inf 𝒜"
| rule: "(None, Some f) qs → q ∈ ta_rules 𝒜 ⟹ i < length qs ⟹ (qs ! i, q) ∈ Q_inf 𝒜"
| eps: "(p, q) ∈ Q_inf 𝒜 ⟹ (q, r) ∈ ta_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 ∈ ta_states 𝒜" "q ∈ ta_states 𝒜"
  using assms by (induct) (auto simp: r_rhs_states r_lhs_states ta_eps_single_ta_states)

lemma Q_inf_ta_eps_Q_inf:
  assumes "(p, q) ∈ Q_inf 𝒜" and "(q, q') ∈ (ta_eps 𝒜)⇧*"
  shows "(p, q') ∈ Q_inf 𝒜" using assms(2, 1)
  by (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 ∈ ta_rules 𝒜 ∧ p ∈ set qs"
  using assms by induct (auto intro: nth_mem)

lemma Q_inf_reach_state_rule:
  assumes "(p, q) ∈ Q_inf 𝒜" and "ta_states 𝒜 ⊆ ta_reachable 𝒜"
  shows "∃ ss ts f C. q ∈ ta_res 𝒜 (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:  ta_res.simps ctxt_apply_term.simps)
    by (metis ctxt.cop_add ctxt_compose.simps(2) ta_res_ctxt)
next
  case (rule f qs q i)
  have "∀ i < length qs. ∃ t. qs ! i ∈ ta_res 𝒜 t ∧ ground t"
    using rule(1, 2) set_mp[OF rule(3), of "qs ! i" for i]
    by (auto simp: r_lhs_states) (meson r_lhs_states ta_reachableE)
  then obtain ts where wit: "length ts = length qs"
    "∀ i < length qs. qs ! i ∈ ta_res 𝒜 (ts ! i) ∧ ground (ts ! i)"
    using Ex_list_of_length_P[of "length qs" "λ x i. qs ! i ∈ ta_res 𝒜 x ∧ ground x"] by blast
  {fix j assume "j < length qs"
    then have "qs ! j ∈ ta_res 𝒜 ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)"
      using wit by (cases "j < i") (auto simp: nth_append_Cons)}
  then have "∀ i < length qs. qs ! i ∈ (map (ta_res 𝒜) (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_res 𝒜 (Fun (None, Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))"
    using rule(1, 2) wit by (auto simp: 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_res.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_res_eps)
qed

lemma rule_target_eps_Q_inf:
  assumes "(None, Some f) qs → q' ∈ ta_rules 𝒜" "(q', q) ∈ (ta_eps 𝒜)⇧*"
     and "i < length qs"
   shows "(qs ! i, q) ∈ Q_inf 𝒜"
  using assms(2, 1, 3) by (induct) (auto intro: rule eps) 

lemma step_in_Q_inf:
  assumes "q ∈ ta_res_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]
  by auto (metis length_map less_add_Suc1 nth_append_length singleton_iff)

lemma ta_res_Q_inf:
  assumes "q ∈ ta_res_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_res_strict 𝒜 (map_funs_term (λf. (None, Some f)) C⟨Var p⟩)"
     "q ∈ ta_res_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 less_not_refl nth_map singletonI)
    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_states 𝒜 ⊆ ta_reachable 𝒜"
  shows "infinite {t. q ∈ ta_res 𝒜 (term_of_gterm t) ∧ fst (groot t) = None}"
proof -
  let ?P ="λ u. ground u ∧ q ∈ ta_res 𝒜 u ∧ fst (fst (the (root u))) = None"
  have [simp]: "fst (fst (the (root (term_of_gterm t)))) = fst (groot 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_res 𝒜 C⟨Var p⟩"
    by blast
  obtain C2 where
    closing_ctxt: "C2 ≠ □" "ground_ctxt C2" "fst (root_ctxt C2) = None" and cl_reach: "q ∈ ta_res 𝒜 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_res 𝒜 t" and gr_t: "ground t"
    by (meson Q_inf_states_ta_states(1) assms(2) cycle(1) subset_eq ta_reachableE)
  let ?terms = "λ n. (C ^ Suc n)⟨t⟩" let ?S = "{?terms n | n. p ∈ ta_res 𝒜 (?terms n) ∧ ground (?terms n)}"
  have "ground (?terms n)" for n using ctxt(2) gr_t by auto
  moreover have "p ∈ ta_res 𝒜 (?terms n)" for n using reach t(1)
    by (auto simp: ta_res_ctxt) (meson ta_res_ctxt ta_res_ctxt_n_loop)
  ultimately have "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_res_ctxt)}
  from infinite_set_restrict_to_property[OF _ inf, of ?P] this  
  have "infinite {u. ground u ∧ q ∈ ta_res 𝒜 u ∧ fst (fst (the (root u))) = None}" by meson
  then show ?thesis using inf_ground_terms_to_gterms[of ?P] by auto
qed

lemma prod_automata_from_none_root_dec:
  assumes "gta_lang 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ ℱ ∧ funas_gterm t ⊆ ℱ}"
    and "q ∈ ta_res 𝒜 (term_of_gterm t)" and "fst (groot t) = None"
    and "ta_states 𝒜 ⊆ ta_reachable 𝒜" and "q ∈ ta_productive 𝒜"
  shows "∃ u. t = gterm_to_None_Some u ∧ funas_gterm u ⊆ ℱ"
proof -
  have [simp]: "the (gfun_at t []) = groot t" for t by (cases t) auto
  from assms(4, 5) obtain C q⇩f where ctxt: "ground_ctxt C" and
    fin: "q⇩f ∈ ta_res 𝒜 C⟨Var q⟩" "q⇩f ∈ ta_final 𝒜"
    by (auto simp: ta_productive_def'[OF assms(4)])
  then obtain s v where gp: "gpair s v = gterm_of_term C⟨term_of_gterm t⟩" and
   funas: "funas_gterm v ⊆ ℱ"
    using assms(1, 2) gta_langI[OF fin(2), of "gterm_of_term C⟨term_of_gterm t⟩"]
    by (auto simp: ta_res_ctxt)
  from gp have mem: "hole_pos C ∈ gposs s ∪ gposs v"
    by auto (metis gpair_poss_args_poss ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv hole_pos_poss ctxt poss_gposs_conv) 
  from fst_groot_None_not_poss[OF this] have "hole_pos C ∉ gposs s" using gp assms(3) by auto
  from subst_at_gpair_nt_poss_None_Some[OF _ this, of v] this show ?thesis using funas mem
    unfolding gp by (metis UnE gsubt_at_ctxt_pos funas_poss_presv)
qed

lemma Q_inf_exec_impl_Q_inf:
  assumes "gta_lang 𝒜 ⊆ {gpair s t| s t. funas_gterm s ⊆ ℱ ∧ funas_gterm t ⊆ ℱ}"
   and "ta_states 𝒜 ⊆ ta_reachable 𝒜" and "ta_states 𝒜 ⊆ ta_productive 𝒜"
   and "q ∈ Q_inf_e 𝒜"
  shows "q ∈ Q_infty 𝒜 ℱ"
proof -
  let ?S = "{t. q ∈ ta_res 𝒜 (term_of_gterm t) ∧ fst (groot t) = None}"
  let ?P = "λ t. funas_gterm t ⊆ ℱ ∧ q ∈ ta_res 𝒜 (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 ⊆ ℱ"
      using prod_automata_from_none_root_dec[OF assms(1)] assms(2, 3)
      using ta_res_gterm_states by fastforce}
  then show ?thesis using infinite_set_dec_infinite[OF inf, of gterm_to_None_Some ?P]
    by (auto simp: Q_infty_def) blast
qed

lemma Q_inf_impl_Q_inf_exec:
  assumes "q ∈ Q_infty 𝒜 ℱ" and "finite ℱ" and "finite (ta_states 𝒜)"
  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 ⊆ ℱ ∧ q ∈ ta_res 𝒜 (?t_of_g (gterm_to_None_Some t))}"
  from assms(3) obtain n where card_st: "card (ta_states 𝒜) < n" by blast
  from assms(1) have "infinite {t |t. funas_gterm t ⊆ ℱ ∧ q ∈ ta_res 𝒜 (?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 ⊆ ℱ" by (auto simp: funas_term_of_gterm_conv subsetD)}
  from infinte_no_depth_limit[OF inf assms(2)] this assms(3) obtain u where
    funas: "funas_gterm u ⊆ ℱ" and card_d: "n < depth (?t_og_g2 u)" and reach: "q ∈ ta_res 𝒜 (?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))"
    by (induct u) (case_tac x2a, auto simp: comp_def)
  from this pigeonhole_tree_automata[OF _ assms(3) 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_res 𝒜 v ∧ p ∈ ta_res 𝒜 C2⟨Var p⟩ ∧ q ∈ ta_res 𝒜 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_res_to_ta_strict[OF _ gr(1)] loop obtain q' where
    to_strict: "(p, q') ∈ (ta_eps 𝒜)⇧* ∧ p ∈ ta_res_strict 𝒜 C2⟨Var q'⟩" by fastforce
  then have q_p: "(q', p) ∈ Q_inf 𝒜" using ta_res_Q_inf[of p 𝒜 _  q'] ctxt
    by auto (smt ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)
  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'') ∈ (ta_eps 𝒜)⇧* ∧ q ∈ ta_res_strict 𝒜 C⟨Var q''⟩"
      using ta_res_to_ta_strict[OF conjunct2[OF conjunct2[OF loop]] gr(2)] by auto
    then have "(q'', q) ∈  Q_inf 𝒜" using ta_res_Q_inf[of q 𝒜 _  q''] ctxt False
      by auto (smt ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)
    then show ?thesis using conjunct1[OF r] 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

end