Theory Finiteness

(* Author: Tobias Nipkow *)

(* TODO: instead of assuming ‹∀A∈Nts P. useful P S A› restrict the pumpable check to
those Nts which can be reached from S within a Tms context, weakening ‹⊲› to ‹⊴› (to be defined).
Also needs Context_Free_Grammar.Infinite_iff_Pumpable to be modified
*)

section ‹Automating Finiteness Check of Language generated by CFG›

theory Finiteness
imports
  Context_Free_Grammar.Infinite_iff_Pumpable
  Context_Free_Grammar.Saturation_Algorithms
  Pre_Star
  LTS_Automata_Regular
begin

(* TODO mv *)
lemma finite_set_True[code]: "finite(set xs) = True"
  by simp

lemma neq_Nil_conv2: "(xs ≠ []) = (∃y ys. xs = ys @ [y])"
  by (metis snoc_eq_iff_butlast)

lemma set_subset_inj_imageD:
  "inj f ⟹ set xs ⊆ f ` A ⟹ ∃as. set as ⊆ A ∧ map f as = xs"
using ex_map_conv[of xs f] inj_image_subset_iff[of f "set _" A] by auto


subsection ‹Regularity of Pumpable›

definition "pump_lang P A = (let tms = (λt. [t]) ` Tm ` Tms P in
  star tms @@ {[Nt A]} @@ tms @@ star tms ∪ tms @@ star tms @@ {[Nt A]} @@ star tms)"

lemma pumpable_iff_in_pre_star: fixes P :: "('n,'t)Prods"
    shows "(P ⊢ A ⊲ A) ⟷ ([Nt A] ∈ pre_star P (pump_lang P A))" (is "?L = ?R")
proof
  assume ?L
  then obtain u v where *: "P ⊢ [Nt A] ⇒* map Tm u @ [Nt A] @ map Tm v" and uv: "u ≠ [] ∨ v ≠ []"
    unfolding reach_Tm_ctxt1_def by blast
  let ?u = "map Tm u" let ?v = "map Tm v"
  let ?tms = "(λs. [s]) ` Tm ` Tms P"
  have **: "?u ∈ star ?tms" "?v ∈ star ?tms"
    using derives_Tms_syms_subset[OF *] by(auto simp: star_image_single)
  have "[Nt A] ∈ pre_star P (pump_lang P A)" using uv
  proof
    assume "u ≠ []"
    hence "map Tm u ∈ ?tms @@ star ?tms" using **(1) star_decom by (metis concI list.map_disc_iff)
    with **(2) have "map Tm u @ [Nt A] @ map Tm v ∈ ?tms @@ star ?tms @@ {[Nt A]} @@ star ?tms"
      by (metis concI conc_assoc singletonI)
    with * have "[Nt A] ∈ pre_star P (?tms @@ star ?tms @@ {[Nt A]} @@ star ?tms)"
      using pre_star_iff by blast
    thus ?thesis unfolding pump_lang_def by (meson UnCI pre_star_iff)
  next
    assume "v ≠ []"
    hence "map Tm v ∈ ?tms @@ star ?tms" using **(2) star_decom concI by (metis list.map_disc_iff)
    with **(1) have "map Tm u @ [Nt A] @ map Tm v ∈ star ?tms @@ {[Nt A]} @@ ?tms @@ star ?tms"
      by (metis concI singletonI)
    with * have "[Nt A] ∈ pre_star P (star ?tms @@ {[Nt A]} @@ ?tms @@ star ?tms)"
      using pre_star_iff by blast
    thus ?thesis unfolding pump_lang_def by (meson UnCI pre_star_iff)
  qed
  thus ?R unfolding pump_lang_def Let_def .
next
  assume ?R
  then show ?L unfolding reach_Tm_ctxt1_def Let_def pre_star_def pump_lang_def
    apply (auto simp add: conc_def star_image_single dest!: set_subset_inj_imageD[OF inj_Tm])
     apply (metis list.distinct(1) list.map(2))
    by (metis append_Cons list.distinct(1) list.map(2))
qed

definition pump_auto :: "('n × ('n, 't) sym list) set ⇒ 'n ⇒ (_, ('n, 't) sym) auto"
  where "pump_auto P A = (let tms = Tm ` Tms P; one_of_auto_eps = auto_eps_of o one_of_auto;
  TA = one_of_auto_eps tms in
  elim_eps_auto (union_auto_eps
    (conc_auto_eps (star_auto_eps TA)
    (conc_auto_eps (one_of_auto_eps {Nt A})
    (conc_auto_eps TA (star_auto_eps TA))))
    (conc_auto_eps TA
    (conc_auto_eps (star_auto_eps TA)
    (conc_auto_eps (one_of_auto_eps {Nt A})
    (star_auto_eps TA))))))
"

lemma finite_star_auto_eps_lts:
  "finite(auto.finals A) ⟹ finite (auto.lts A) ⟹ finite (star_auto_lts_eps A)"
  by (auto simp add: star_auto_lts_eps_def)

lemma finite_lts_one_of_auto: "finite T ⟹ finite (auto.lts (one_of_auto T))"
by (simp add: one_of_auto_def one_of_lts_def)

lemma finite_lts_pump_auto: "finite P ⟹ finite(auto.lts (pump_auto P A))"
by(simp add: pump_auto_def finite_elim_eps_ltsI
    lts_union_auto_eps finite_union_auto_eps_lts
    lts_conc_auto_eps finite_conc_auto_eps_lts finite_finals_star_auto_eps
    finite_embed_lts lts_star_auto_eps finite_star_auto_eps_lts
    finite_lts_auto_eps_of finite_lts_one_of_auto finite_Tms)

lemma accepts_auto_elim_eps_auto: "accepts_auto(elim_eps_auto A) w = (w ∈ Lang_auto_eps A)"
  by (simp add: Lang_auto_eps_def)

theorem Lang_auto_pump_auto: "Lang_auto (pump_auto P A) = pump_lang P A"
  unfolding pump_auto_def pump_lang_def Let_def accepts_auto_elim_eps_auto
   Lang_auto_eps_union_auto_eps_lts Lang_auto_eps_conc_auto_eps Lang_auto_eps_star_auto_lts_eps
   o_def Lang_auto_eps_auto_eps_of_one_of_auto
  by blast

lemma pre_star_finite_code:
  fixes P :: "('n, 't) Prods"
  assumes "finite P" and "∀A∈Nts P. useful P S A"
  shows "finite(Lang P S) ⟷
    (∀A ∈ Nts P. [Nt A] ∉ Lang_auto (pre_star_auto P (pump_auto P A)))"
proof -
  have "⋀A. Lang_auto (pre_star_auto P (pump_auto P A)) = pre_star P (Lang_auto (pump_auto P A))"
    by (intro pre_star_auto_correct; simp add: finite_lts_pump_auto assms(1))
  then show ?thesis
    using Lang_auto_pump_auto infinite_Lang_iff_pumpable[OF assms] pumpable_iff_in_pre_star
    by (metis)
qed

text ‹Example:›

lemma fixes P_fin :: "(int,int)Prods"
  defines "P_fin ≡ {(0,[Nt 0, Nt 0]), (0,[Nt 1]), (1,[]), (1,[Nt 0])}"
  shows "finite(Lang P_fin 0)"
  unfolding P_fin_def
  apply(subst pre_star_finite_code)
  apply eval
  apply eval
  apply eval
  done

end