Theory Right_Linear_Automata

(*
Authors: Kaan Taskin, Tobias Nipkow
*)

section ‹Relating Strongly Right-Linear Grammars and Automata›

theory Right_Linear_Automata
imports
  NDA_rlin2
  "Finite_Automata_HF.Finite_Automata_HF"
  HereditarilyFinite.Finitary
begin

subsection ‹From Strongly Right-Linear Grammar to NFA›

definition nfa_rlin2 :: "('n,'t)Prods ⇒ ('n::finitary) ⇒ 't nfa" where
"nfa_rlin2 P S =
  ⦇ states = hf_of  ` ({S} ∪ Nts P),
    init = {hf_of S},
    final = hf_of ` {A ∈ Nts P. (A,[]) ∈ P},
    nxt = λq a. hf_of ` nxt_rlin2 P (inv hf_of q) a,
    eps = Id ⦈"               

context
  fixes P :: "('n::finitary,'t)Prods"
  assumes "finite P"
begin

interpretation NFA_rlin2: nfa "nfa_rlin2 P S"
unfolding nfa_rlin2_def proof (standard, goal_cases)
  case 1
  then show ?case by(simp)
next
  case 2
  then show ?case by auto
next
  case (3 q x)
  then show ?case by(auto simp add: nxt_rlin2_nts)
next
  case 4
  then show ?case using ‹finite P› by (simp add: Nts_def finite_nts_syms split_def)
qed
print_theorems

lemma nfa_init_nfa_rlin2: "nfa.init (nfa_rlin2 P S) = hf_of ` {S}"
by (simp add: nfa_rlin2_def)

lemma nfa_final_nfa_rlin2: "nfa.final (nfa_rlin2 P S) = hf_of ` {A ∈ Nts P. (A,[]) ∈ P}"
by (simp add: nfa_rlin2_def)

lemma nfa_nxt_nfa_rlin2: "nfa.nxt (nfa_rlin2 P S) (hf_of A) a = hf_of ` nxt_rlin2 P A a"
by (simp add: nfa_rlin2_def inj)

lemma nfa_epsclo_nfa_rlin2: "M ⊆ {hf_of S} ∪ hf_of ` Nts P ⟹ nfa.epsclo (nfa_rlin2 P S) M = M"
unfolding NFA_rlin2.epsclo_def unfolding nfa_rlin2_def by(auto)

lemma nfa_nextl_nfa_rlin2: "M ⊆ {S} ∪ Nts P
  ⟹ nfa.nextl (nfa_rlin2 P S) (hf_of ` M) xs = hf_of ` nxts_rlin2_set P M xs"
proof(induction xs arbitrary: M)
  case Nil
  then show ?case
    by (simp add: nxts_rlin2_set_def)(fastforce intro!: nfa_epsclo_nfa_rlin2)
next
  case (Cons a xs)
  let ?epsclo = "nfa.epsclo (nfa_rlin2 P S)"
  let ?nxt = "nfa.nxt (nfa_rlin2 P S)"
  let ?nxts = "nfa.nextl (nfa_rlin2 P S)"
  have "?nxts (hf_of ` M) (a # xs) = ?nxts (⋃x∈?epsclo (hf_of ` M). ?nxt x a) xs"
    by simp
  also have "… = ?nxts (⋃x∈hf_of ` M. ?nxt x a) xs"
    using Cons.prems by(subst nfa_epsclo_nfa_rlin2) auto
  also have "… = ?nxts (⋃m∈M. ?nxt (hf_of m) a) xs" by simp
  also have "… = ?nxts (⋃m∈M. hf_of ` nxt_rlin2 P m a) xs"
    by (simp add: nfa_nxt_nfa_rlin2)
  also have "… = ?nxts (hf_of ` (⋃m∈M. nxt_rlin2 P m a)) xs"
    by (metis image_UN)
  also have "… = hf_of ` nxts_rlin2_set P (⋃m∈M. nxt_rlin2 P m a) xs"
    using Cons.prems by(subst Cons.IH)(auto simp add: nxt_rlin2_nts)
  also have "… = hf_of ` nxts_rlin2_set P M (a # xs)"
    by (simp add: nxt_rlin2_set_def nxts_rlin2_set_def)
  finally show ?case .
qed

lemma lang_pres_nfa_rlin2: assumes "rlin2 P"
shows "nfa.language (nfa_rlin2 P S) = Lang P S"
proof -
  have 1: "⋀A xs. ⟦ A ∈ nxts_rlin2_set P {S} xs; A ∈ Nts P; (A, []) ∈ P⟧ ⟹
    P ⊢ [Nt S] ⇒* map Tm xs"
    using nxts_to_mult_derive by (metis (no_types, opaque_lifting) append.right_neutral derive.intros
      r_into_rtranclp rtranclp_trans singletonD)
  have "⋀A B. Nt B ∉ Syms P ⟹ (A, []) ∈ P ⟹ A ≠ B" by(auto simp: Syms_def)
  hence 2: "⋀xs. rlin2 P ⟹ P ⊢ [Nt S] ⇒* map Tm xs ⟹
          nxts_rlin2_set P {S} xs ∩ {A ∈ Nts P. (A, []) ∈ P} ≠ {}"
   using in_Nts_iff_in_Syms mult_derive_to_nxts rlin2_tms_eps
   by (metis (no_types, lifting) Int_Collect empty_iff singletonI)
  show ?thesis
    unfolding NFA_rlin2.language_def Lang_def nfa_init_nfa_rlin2 nfa_final_nfa_rlin2
      nfa_nextl_nfa_rlin2[OF Un_upper1]
    using 2[OF assms] by (auto simp: 1)
qed

lemma regular_if_rlin2: assumes "rlin2 P"
  shows "regular (Lang P S)"
using lang_pres_nfa_rlin2[OF assms] NFA_rlin2.imp_regular[of S]
by metis

end


subsection ‹From DFA to Strongly Right-Linear Grammar›

context dfa
begin

text
‹We define ‹Prods_dfa› that collects the production set from the deterministic finite automata ‹M››

definition Prods_dfa :: "(hf, 'a) Prods" where
"Prods_dfa =
  (⋃q ∈ dfa.states M. ⋃x. {(q,[Tm x, Nt(dfa.nxt M q x)])}) ∪ (⋃q ∈ dfa.final M. {(q,[])})"

lemma rlin2_prods_dfa: "rlin2 (Prods_dfa)"
  unfolding rlin2_def Prods_dfa_def by blast

text
‹We show that a word can be derived from the production set ‹Prods_dfa› if and only if traversing the word in the deterministic finite 
 automata ‹M› ends in a final state. The proofs are very similar to those in ‹DFA_rlin2.thy››

lemma mult_derive_to_nxtl:
  "Prods_dfa ⊢ [Nt A] ⇒* map Tm w @ [Nt B] ⟹ nextl A w = B"
proof (induction w arbitrary: B rule: rev_induct)
  case Nil
  thus ?case
    using rlin2_nts_derive_eq[OF rlin2_prods_dfa, of A B] by simp
next
  case (snoc x xs)
  from snoc.prems have "Prods_dfa ⊢ [Nt A] ⇒* map Tm xs @ [Tm x,Nt B]" by simp
  then obtain C where C_der: "Prods_dfa ⊢ [Nt A] ⇒* map Tm xs @ [Nt C]"
               and C_prods: "(C,[Tm x, Nt B]) ∈ Prods_dfa" using rlin2_introduce_tm[OF rlin2_prods_dfa, of A xs x B] by auto 
  have 1: "nextl A xs = C"
    using snoc.IH[OF C_der] .
  from C_prods have 2: "B = dfa.nxt M C x"
    unfolding Prods_dfa_def by blast
  from 1 2 show ?case by simp
qed

lemma nxtl_to_mult_derive:
  assumes "A ∈ dfa.states M"
    shows "Prods_dfa ⊢ [Nt A] ⇒* map Tm w @ [Nt (nextl A w)]"
proof (induction w rule: rev_induct)
  case (snoc x xs)
  let ?B = "nextl A xs"
  have "?B ∈ dfa.states M" 
    using nextl_state[OF assms, of xs] .
  hence "(?B, [Tm x, Nt (dfa.nxt M ?B x)]) ∈ Prods_dfa"
    unfolding Prods_dfa_def by blast
  hence "Prods_dfa ⊢ [Nt ?B] ⇒ [Tm x] @ [Nt (dfa.nxt M ?B x)]"
    by (simp add: derive_singleton)
  hence "Prods_dfa ⊢ [Nt A] ⇒* map Tm xs @ ([Tm x] @ [Nt (dfa.nxt M ?B x)])"
    using snoc.IH by (meson derive_prepend rtranclp.simps)
  thus ?case by auto
qed simp

theorem Prods_dfa_iff_dfa:
  "q ∈ dfa.states M ⟹ Prods_dfa ⊢ [Nt q] ⇒* map Tm w ⟷ nextl q w ∈ dfa.final M"
proof
  show "Prods_dfa ⊢ [Nt q] ⇒* map Tm w ⟹ nextl q w ∈ dfa.final M"
  proof -
    assume asm: "Prods_dfa ⊢ [Nt q] ⇒* map Tm w"
    obtain B where q_der: "Prods_dfa ⊢ [Nt q] ⇒* map Tm w @ [Nt B]" and B_in: "(B,[]) ∈ Prods_dfa" 
      unfolding Lang_def using rlin2_tms_eps[OF rlin2_prods_dfa asm] by auto
    have 1: "nextl q w = B"
      using mult_derive_to_nxtl[OF q_der] .
    from B_in have 2: "B ∈ dfa.final M"
      unfolding Prods_dfa_def by blast
    from 1 2 show ?thesis by simp
  qed
next
  assume asm1: "q ∈ dfa.states M"
  show "nextl q w ∈ dfa.final M ⟹ Prods_dfa ⊢ [Nt q] ⇒* map Tm w"
  proof -
    assume asm2: "nextl q w ∈ dfa.final M"
    let ?Z = "nextl q w"
    from asm2 have Z_eps: "(?Z,[]) ∈ Prods_dfa"
      unfolding Prods_dfa_def by blast
    have "Prods_dfa ⊢ [Nt q] ⇒* map Tm w @ [Nt ?Z]"
      using nxtl_to_mult_derive[OF asm1, of w] .
    with Z_eps show ?thesis
      by (metis derives_rule rtranclp.rtrancl_refl self_append_conv)
  qed
qed

corollary dfa_language_eq_Lang: "dfa.language M = Lang Prods_dfa (dfa.init M)"
unfolding language_def Lang_def by (simp add: Prods_dfa_iff_dfa)

end

corollary rlin2_if_regular:
  "regular L ⟹ ∃P S::hf. rlin2 P ∧ L = Lang P S"
by (metis dfa.dfa_language_eq_Lang dfa.rlin2_prods_dfa regular_def)

end