Theory NDA_rlin2

(*
Authors: Kaan Taskin, Tobias Nipkow
*)

section ‹Strongly Right-Linear Grammars as a Nondeterministic Automaton›

theory NDA_rlin2
imports Right_Linear
begin

text
‹We define what is essentially the extended transition function of a nondeterministic automaton
but is driven by a set of strongly right-linear productions ‹P›, which are of course
just another representation of the transitions of a nondeterministic automaton.
Function ‹nxts_rlin2_set P M w› traverses the terminals list ‹w›
starting from the set of non-terminals ‹M› according to the productions of ‹P›.
At the end it returns the reachable non-terminals.›

definition nxt_rlin2 :: "('n,'t)Prods ⇒ 'n ⇒ 't ⇒ 'n set" where
"nxt_rlin2 P A a = {B. (A, [Tm a, Nt B]) ∈ P}"

definition nxt_rlin2_set :: "('n,'t)Prods ⇒ 'n set ⇒ 't ⇒ 'n set" where
"nxt_rlin2_set P M a = (⋃A∈M. nxt_rlin2 P A a)"

definition nxts_rlin2_set :: "('n,'t)Prods ⇒ 'n set ⇒ 't list ⇒ 'n set" where
"nxts_rlin2_set P = foldl (nxt_rlin2_set P)"

lemma nxt_rlin2_nts:
  assumes "B∈nxt_rlin2 P A a"
  shows "B∈Nts P"
  using assms nxt_rlin2_def Nts_def nts_syms_def by fastforce

lemma nxts_rlin2_set_app: 
  "nxts_rlin2_set P M (x @ y) = nxts_rlin2_set P (nxts_rlin2_set P M x) y"
  unfolding nxts_rlin2_set_def by simp

lemma nxt_rlin2_set_pick:
  assumes "B ∈ nxt_rlin2_set P M a"
  shows   "∃C∈M. B ∈ nxt_rlin2_set P {C} a"
  using assms by (simp add:nxt_rlin2_def nxt_rlin2_set_def)

lemma nxts_rlin2_set_pick:
  assumes "B ∈ nxts_rlin2_set P M w"
  shows "∃C∈M. B ∈ nxts_rlin2_set P {C} w"
using assms proof (induction w arbitrary: B rule: rev_induct)
  case Nil
  then show ?case
    by (simp add: nxts_rlin2_set_def)
next
  case (snoc x xs)
  from snoc(2) have B_in: "B ∈ nxts_rlin2_set P (nxts_rlin2_set P M xs) [x]"
    using nxts_rlin2_set_app[of P M xs "[x]"] by simp
  hence "B ∈ nxt_rlin2_set P (nxts_rlin2_set P M xs) x"
    by (simp add: nxts_rlin2_set_def)
  hence "∃C∈(nxts_rlin2_set P M xs). B ∈ nxt_rlin2_set P {C} x"
    using nxt_rlin2_set_pick[of B P "nxts_rlin2_set P M xs" x] by simp
  then obtain C where C_def: "C ∈ nxts_rlin2_set P M xs" and C_path: "B ∈ nxt_rlin2_set P {C} x"
    by blast
  have "∃Ca∈M. C ∈ nxts_rlin2_set P {Ca} xs"
    using snoc.IH[of C, OF C_def] .
  then obtain D where *: "D ∈ M" and D_path: "C ∈ nxts_rlin2_set P {D} xs"
    by blast
  from C_path D_path have **: "B ∈ nxts_rlin2_set P {D} (xs @ [x])"
    unfolding nxts_rlin2_set_def nxt_rlin2_set_def by auto
  from * ** show ?case by blast
qed

lemma nxts_rlin2_set_first_step:
  assumes "B ∈ nxts_rlin2_set P {A} (a # w)"
  shows "∃C ∈ nxt_rlin2 P A a. B ∈ nxts_rlin2_set P {C} w"
proof -
  from assms have "B ∈ nxts_rlin2_set P {A} ([a]@w)" by simp
  hence "B ∈ nxts_rlin2_set P (nxts_rlin2_set P {A} [a]) w" 
    using nxts_rlin2_set_app[of P "{A}" "[a]" w] by simp
  hence "B ∈ nxts_rlin2_set P (nxt_rlin2 P A a) w"
    by (simp add: nxt_rlin2_set_def nxts_rlin2_set_def)
  thus "∃C ∈ nxt_rlin2 P A a. B ∈ nxts_rlin2_set P {C} w"
    using nxts_rlin2_set_pick[of B P "nxt_rlin2 P A a" w] by simp
qed

lemma nxts_trans0:
  assumes "B ∈ nxts_rlin2_set P (nxts_rlin2_set P {A} x) z"
  shows "B ∈ nxts_rlin2_set P {A} (x@z)"
  by (metis assms foldl_append nxts_rlin2_set_def)

lemma nxt_mono:
  assumes "A ⊆ B"
  shows "nxt_rlin2_set P A a ⊆ nxt_rlin2_set P B a"
  unfolding nxt_rlin2_set_def using assms by blast

lemma nxts_mono:
  assumes "A ⊆ B"
  shows "nxts_rlin2_set P A w ⊆ nxts_rlin2_set P B w"
  unfolding nxts_rlin2_set_def proof (induction w rule:rev_induct)
  case Nil
  thus ?case by (simp add: assms)
next
  case (snoc x xs)
  thus  ?case 
    using nxt_mono[of "foldl (nxt_rlin2_set P) A xs" "foldl (nxt_rlin2_set P) B xs" P x] by simp
qed

lemma nxts_trans1:
  assumes "M ⊆ nxts_rlin2_set P {A} x"
      and "B ∈ nxts_rlin2_set P M z"
  shows "B ∈ nxts_rlin2_set P {A} (x@z)"
  using assms nxts_trans0[of B P A x z] nxts_mono[of M "nxts_rlin2_set P {A} x" P z, OF assms(1)] by auto

lemma nxts_trans2:
  assumes "C ∈ nxts_rlin2_set P {A} x"
      and "B ∈ nxts_rlin2_set P {C} z"
    shows "B ∈ nxts_rlin2_set P {A} (x@z)"
  using assms nxts_trans1[of "{C}" P A x B z] by auto

lemma nxts_to_mult_derive:
  "B ∈ nxts_rlin2_set P M w ⟹ (∃A∈M. P ⊢ [Nt A] ⇒* map Tm w @ [Nt B])"
unfolding nxts_rlin2_set_def proof (induction w arbitrary: B rule: rev_induct)
  case Nil
  hence 1: "B ∈ M" by simp
  have 2: "P ⊢ [Nt B] ⇒* map Tm [] @ [Nt B]" by simp
  from 1 2 show ?case by blast
next
  case (snoc x xs)
  from snoc.prems have "∃C. C ∈ foldl (nxt_rlin2_set P) M xs ∧ (C, [Tm x, Nt B]) ∈ P"
    unfolding nxt_rlin2_set_def nxt_rlin2_def by auto
  then obtain C where C_xs: "C ∈ foldl (nxt_rlin2_set P) M xs" and C_prod: "(C, [Tm x, Nt B]) ∈ P" by blast
  from C_xs obtain A where A_der: "P ⊢ [Nt A] ⇒* map Tm xs @ [Nt C]" and A_in: "A ∈ M" 
    using snoc.IH[of C] by auto
  from C_prod have "P ⊢ [Nt C] ⇒ [Tm x, Nt B]"
    using derive_singleton[of P "Nt C" "[Tm x, Nt B]"] by blast
  hence "P ⊢ map Tm xs @ [Nt C] ⇒ map Tm xs @ [Tm x, Nt B]"
    using derive_prepend[of P "[Nt C]" "[Tm x, Nt B]" "map Tm xs"] by simp
  hence C_der: "P ⊢ map Tm xs @ [Nt C] ⇒ map Tm (xs @ [x]) @ [Nt B]" by simp
  from A_der C_der have "P ⊢ [Nt A] ⇒* map Tm (xs @ [x]) @ [Nt B]" by simp
  with A_in show ?case by blast
qed

lemma mult_derive_to_nxts:
  assumes "rlin2 P"
  shows "A∈M ⟹ P ⊢ [Nt A] ⇒* map Tm w @ [Nt B] ⟹ B ∈ nxts_rlin2_set P M w"
unfolding nxts_rlin2_set_def proof (induction w arbitrary: B rule: rev_induct)
  case Nil
  with assms have "A = B"
    using rlin2_nts_derive_eq[of P A B] by simp
  with Nil.prems(1) show ?case by simp
next
  case (snoc x xs)
  from snoc.prems(2) have "P ⊢ [Nt A] ⇒* map Tm xs @ [Tm x,Nt B]" by simp
  with assms obtain C where C_der: "P ⊢ [Nt A] ⇒* map Tm xs @ [Nt C]"
                        and C_prods: "(C,[Tm x, Nt B]) ∈ P" using rlin2_introduce_tm[of P A xs x B] by fast
  from ‹A ∈ M› C_der have "C ∈ foldl (nxt_rlin2_set P) M xs"
    using snoc.IH[of C] by auto
  with C_prods show ?case
    unfolding nxt_rlin2_set_def nxt_rlin2_def by auto
qed

text
‹Acceptance of a word ‹w› w.r.t. ‹P› (starting from ‹A›), ‹accepted P A w›, means that we can reach
an ``accepting'' nonterminal ‹Z›, i.e. one with a production ‹(Z,[])›.
On the automaton level ‹Z› reachable final state.
We show that ‹accepted P A w› iff ‹w› is in the language of ‹A› w.r.t. ‹P›.›

definition "accepted P A w = (∃Z ∈ nxts_rlin2_set P {A} w. (Z,[]) ∈ P)"

theorem accepted_if_Lang:
  assumes "rlin2 P"
      and "w ∈ Lang P A"
    shows "accepted P A w"
proof -
  from assms obtain B where A_der: "P ⊢ [Nt A] ⇒* map Tm w @ [Nt B]" and B_in: "(B,[]) ∈ P" 
    unfolding Lang_def using rlin2_tms_eps[of P A w] by auto
  from A_der have "B ∈ nxts_rlin2_set P {A} w" 
    using mult_derive_to_nxts[OF assms(1)] by auto
  with B_in show ?thesis 
    unfolding accepted_def by blast
qed

theorem Lang_if_accepted: 
  assumes "accepted P A w"
    shows "w ∈ Lang P A"
proof -
  from assms obtain Z where Z_nxts: "Z ∈ nxts_rlin2_set P {A} w" and Z_eps: "(Z,[]) ∈ P"
    unfolding accepted_def by blast
  from Z_nxts obtain B where B_der: "P ⊢ [Nt B] ⇒* map Tm w @ [Nt Z]" and B_in: "B ∈ {A}"
    using nxts_to_mult_derive by fast
  from B_in have A_eq_B: "A = B" by simp
  from Z_eps have "P ⊢ [Nt Z] ⇒ []" 
    using derive_singleton[of P "Nt Z" "[]"] by simp
  hence "P ⊢ map Tm w @ [Nt Z] ⇒ map Tm w"
    using derive_prepend[of P "[Nt Z]" "[]" "map Tm w"] by simp
  with B_der A_eq_B have "P ⊢ [Nt A] ⇒* map Tm w" by simp
  thus ?thesis 
    unfolding Lang_def by blast
qed

theorem Lang_iff_accepted_if_rlin2:
assumes "rlin2 P"
shows "w ∈ Lang P A ⟷ accepted P A w"
  using accepted_if_Lang[OF assms] Lang_if_accepted by fast

end