Theory Infinite_iff_Pumpable

(* Author: Tobias Nipkow *)

section‹Finiteness of Language Generated by Finite CFG›

theory Infinite_iff_Pumpable
imports
  Context_Free_Grammar.Context_Free_Language
  Context_Free_Grammar.Epsilon_Elimination
  Context_Free_Grammar.Unit_Elimination
begin

text ‹This theory fills a gap in the correctness proof of the finiteness check according to
Esparza and Rossmanith. They claim that the language generated by a finite grammar is finite
if and only if there is no pumpable non-terminal. For the proof they refer to Hopcroft and Ullman.
However, Hopcroft and Ullman only prove this equivalence for grammars in CNF.
This theory proves that the claim by Esparza and Rossmanith is correct for any grammar.
There is no need for CNF.›

text ‹One ‹Nt› can reach another ‹Nt› in a non-empty ‹Tm› context:›

definition reach_Tm_ctxt1 :: "('n,'t) Prods ⇒ 'n ⇒ 'n ⇒ bool" ("(2_ ⊢/ (_ ⊲/ _))" [50, 0, 50] 50)
  where "(P ⊢ X ⊲ Y) = (∃u v. P ⊢ [Nt X] ⇒* map Tm u @ [Nt Y] @ map Tm v ∧ u@v ≠ [])"

text ‹In the special case that ‹X ⊲ X› we say that ‹X› it ❙‹pumpable›.›

lemma reach_Tm_ctxt1_trans: "⟦ P ⊢ A ⊲ B; P ⊢ B ⊲ C ⟧ ⟹ P ⊢ A ⊲ C"
  unfolding reach_Tm_ctxt1_def
  apply(elim exE conjE)
  subgoal premises assms for uB uC vB vC
    using  rtranclp_trans[OF assms(1) derives_embed[OF assms(3)]] assms(4)
    by (metis Nil_is_append_conv append_assoc map_append)
  done

lemma in_Lhss_if_reach_Tm_ctxt11:
  "P ⊢ A ⊲ B ⟹ A ∈ Lhss P"
by(auto simp: reach_Tm_ctxt1_def Cons_eq_append_conv derivep_Nt_in_Lhss dest: rtranclpD)

lemma in_Nts_if_reach_Tm_ctxt12:
  "P ⊢ A ⊲ B ⟹ B ∈ Nts P" (* Rhs_Nts? *)
apply(frule in_Lhss_if_reach_Tm_ctxt11)
unfolding reach_Tm_ctxt1_def
using derives_Nts_syms_subset Nts_Lhss_Rhs_Nts by fastforce

lemma infinite_Lang_if_pumpable:
  assumes all_productive: "Lang P X ≠ {}"
   and "P ⊢ X ⊲ X"
  shows "infinite (Lang P X)"
proof -
  obtain u v where X: "P ⊢ [Nt X] ⇒* map Tm u @ [Nt X] @ map Tm v" "u ≠ [] ∨ v ≠ []"
    using assms(2) unfolding reach_Tm_ctxt1_def by blast
  obtain w where w: "P ⊢ [Nt X] ⇒* map Tm w" using assms(1) Lang_def by fastforce
  let ?uTm = "map Tm u" let ?vTm = "map Tm v" let ?wTm = "map Tm w"
  let ?uwvTm = "λi. ?uTm ^^ i @ ?wTm @ ?vTm ^^ i"
  let ?uwv = "λi. u ^^ i @ w @ v ^^ i"
  have "P ⊢ [Nt X] ⇒* ?uwvTm n" for n
  proof(induction n)
    case 0 thus ?case using w by simp
  next
    case (Suc n)
    from X(1) Suc.IH have "P ⊢ [Nt X] ⇒* ?uTm @ ?uwvTm n @ ?vTm"
      by (meson derives_append derives_prepend rtranclp_trans)
    also have "... = ?uwvTm (Suc n)" by (simp add: pow_list_comm)  
    finally show ?case .
  qed
  hence "⋀n. P ⊢ [Nt X] ⇒* ?uwvTm n" using w
    by (meson derives_append derives_prepend rtranclp_trans)
  hence 0: "?uwv ` UNIV ⊆ Lang P X" unfolding Lang_def by (auto simp: image_def)
  have "?uTm ^^ (Suc n) ≠ [] ∨ ?vTm ^^ (Suc n) ≠ []" for n using X(2) by simp
  hence "i ≠ j ⟹ length(?uwv i) ≠ length(?uwv j)" for i j
    apply (simp add: length_pow_list)
    apply (metis add_is_0 add_mult_distrib2 length_0_conv mult_cancel2)
    done
  hence "inj ?uwv" unfolding inj_def by metis
  hence 1: "infinite(?uwv ` UNIV)" using finite_imageD by blast
  show ?thesis using finite_subset[OF 0] 1 by blast
qed

abbreviation reach_Tm_ctxt1_converse :: "('n,'t) Prods ⇒ ('n × 'n) set" where
  "reach_Tm_ctxt1_converse P ≡ {(Y, X). P ⊢ X ⊲ Y}"

lemma reach_Tm_ctxt1_converse_trans: "(B,A) ∈ (reach_Tm_ctxt1_converse P)^+ ⟹ P ⊢ A ⊲ B"
proof(induction rule: trancl_induct)
  case (step)
  then show ?case using reach_Tm_ctxt1_trans[of P] by blast
qed simp

lemma reach_Tm_ctxt1_converse_wf:
  assumes "finite P"
    and "∀X ∈ Nts P. ¬ P ⊢ X ⊲ X"
  shows "wf (reach_Tm_ctxt1_converse P)"
proof -
  have "reach_Tm_ctxt1_converse P ⊆ Nts P × Nts P"
    using in_Lhss_if_reach_Tm_ctxt11[of P] in_Nts_if_reach_Tm_ctxt12[of P]
    unfolding Nts_Lhss_Rhs_Nts
    by blast
  hence finite: "finite (reach_Tm_ctxt1_converse P)"
    by (simp add: assms(1) finite_Nts finite_subset)
  have "acyclic (reach_Tm_ctxt1_converse P)"
    unfolding acyclic_def 
    using assms(2) reach_Tm_ctxt1_converse_trans[of _ _ P] in_Nts_if_reach_Tm_ctxt12[of P]
    by blast
  from finite_acyclic_wf[OF finite this] show ?thesis .
qed

lemma finite_Lang_if_not_pumpable:
  assumes "finite P" "Eps_free P" "Unit_free P"
    and no_self_pembed: "∀X ∈ Nts P. ¬ P ⊢ X ⊲ X"
  shows "finite (Lang P A)"
proof -
  from reach_Tm_ctxt1_converse_wf[OF assms(1,4)]
  show ?thesis
  proof (induction)
    case (less A)
    have "Lang P A = (⋃α ∈ Rhss P A. inst_syms (Lang P) α)"
      by(rule Lang_unfold)
    have "finite(inst_syms (Lang P) α)" if "α ∈ Rhss P A" for α
    proof(cases "∃B ∈ Nts_syms α. Lang P B = {}")
      case True
      then obtain B where "B ∈ Nts_syms α" "Lang P B = {}" by blast
      hence "inst_syms (Lang P) α = {}"
        by (simp add: inst_syms_empty)
      then show ?thesis by simp
    next
      case False
      then obtain w where "∀B ∈ Nts_syms α. w B ∈ Lang P B"
        by (meson equals0I)
      have "(A,α) ∈ P" using Rhss_def ‹α ∈ _› by force
      have 1: "∄B. α = [Nt B]" using ‹Unit_free P› Unit_free_def ‹(A, α) ∈ P› by fastforce
      have "(B, A) ∈ reach_Tm_ctxt1_converse P" if B: "B ∈ Nts_syms α" for B
      proof -
        from B obtain α1 α2 where "α = α1 @ [Nt B] @ α2"
          by (metis append_Cons append_Nil in_Nts_syms in_set_conv_decomp)
        from False ‹α = _› obtain w1 w2 where w12: "P ⊢ α1 ⇒* map Tm w1 ∧ P ⊢ α2 ⇒* map Tm w2"
          by (meson derives_append_map_Tm productives_if_Langs_nonempty)
        have "α1@α2 ≠ []" using 1 ‹α = _› by auto
        hence "w1@w2 ≠ []" using w12 Eps_free_derives_Nil[OF ‹Eps_free P›] by fastforce
        hence "P ⊢ A ⊲ B" unfolding reach_Tm_ctxt1_def using ‹(A,α) ∈ P› ‹α = _› w12
          by (meson converse_rtranclp_into_rtranclp derive_singleton derives_append_append
              derives_prepend)
        thus ?thesis by auto
      qed
      hence "finite(Lang P B)" if "B ∈ Nts_syms α" for B
        using less.IH that by blast
      thus ?thesis using finite_inst_syms by metis
    qed
    thus ?case by (simp add: Lang_unfold finite_Rhss[OF assms(1)])
  qed
qed

lemma reach_Tm_ctxt1_if_Esp_elim:
  "Eps_elim P ⊢ X ⊲ X ⟹ P ⊢ X ⊲ X"
unfolding reach_Tm_ctxt1_def using Eps_elim_r3 by blast

lemma reach_Tm_ctxt1_if_Unit_elim: "Unit_elim P ⊢ X ⊲ X ⟹ P ⊢ X ⊲ X"
unfolding reach_Tm_ctxt1_def using Unit_elim_rel_r4 by blast

lemma reach_Tm_ctxt1_Unit_Eps_elimD: "Unit_elim (Eps_elim P) ⊢ A ⊲ A ⟹ P ⊢ A ⊲ A"
  by (metis reach_Tm_ctxt1_if_Unit_elim reach_Tm_ctxt1_if_Esp_elim)

theorem infinite_Lang_iff_pumpable:
  assumes "finite P" and "∀A∈Nts P. useful P S A"
  shows "infinite (Lang P S) ⟷ (∃A ∈ Nts P. P ⊢ A ⊲ A)" (is "?inf = ?pump")
proof
  let ?P = "Unit_elim(Eps_elim P)"
  note fin = finite_Unit_elim[OF finite_Eps_elim[OF assms(1)]]
  note eps = Unit_elim_Eps_free [OF Eps_free_Eps_elim]
  assume ?inf                                          
  hence "infinite(Lang ?P S)"
    by (simp add: Lang_Eps_elim Lang_Unit_elim)
  then show "?pump"
    using finite_Lang_if_not_pumpable[OF fin eps Unit_Free_Unit_elim]
      reach_Tm_ctxt1_Unit_Eps_elimD in_Nts_if_reach_Tm_ctxt12 
    by metis 
next
  assume ?pump
  then obtain A where "A∈Nts P" "P ⊢ A ⊲ A" ..
  with assms(2) obtain β where *: "P ⊢ [Nt S] ⇒* β" "Nt A ∈ set β" "productives P β"
    unfolding useful_def by blast
  have "infinite (Lang P A)"
    using *(2,3) infinite_Lang_if_pumpable[OF Lang_nonempty_if_derives_Tms ‹P ⊢ A ⊲ A›] by blast
  moreover have "∀A ∈ Nts_syms β. Lang P A ≠ {}"
    by (meson *(3) Lang_nonempty_if_derives_Tms in_Nts_syms)
  ultimately have "infinite(Langs P β)"
    using *(2) Langs_eq_inst_syms_Lang in_Nts_syms infinite_inst_syms by (metis)
  moreover from *(1) have "Langs P β ⊆ Lang P S" by (metis Lang_def Langs_def Langs_mono_derives)
  ultimately show ?inf
    by (metis finite_subset)
qed

end