Theory Stack_To_Final_PDA

section ‹Equivalence of Final and Stack Acceptance›

subsection ‹Stack Acceptance to Final Acceptance›

text ‹Starting from a PDA that accepts by empty stack
we construct an equivalent PDA that accepts by final state,
following Kozen \cite{kozen2007automata}.›

theory Stack_To_Final_PDA
imports Pushdown_Automata 
begin

datatype 'q st_extended = Old_st 'q | New_init | New_final 
datatype 's sym_extended = Old_sym 's | New_sym

lemma inj_Old_sym: "inj Old_sym"
by (meson injI sym_extended.inject)

instance st_extended :: (finite) finite
proof
  have *: "UNIV = {t. ∃q. t = Old_st q} ∪ {New_init, New_final}"
    by auto (metis st_extended.exhaust)
  show "finite (UNIV :: 'a st_extended set)"
    by (simp add: * full_SetCompr_eq)
qed

instance sym_extended :: (finite) finite
proof
  have *: "UNIV = {t. ∃s. t = Old_sym s} ∪ {New_sym}"
    by auto (metis sym_extended.exhaust)
  show "finite (UNIV :: 'a sym_extended set)"
    by (simp add: * full_SetCompr_eq)
qed

context pda begin

fun final_of_stack_delta :: "'q st_extended ⇒ 'a ⇒ 's sym_extended ⇒ ('q st_extended × 's sym_extended list) set" where
  "final_of_stack_delta (Old_st q) a (Old_sym Z) = (λ(p, α). (Old_st p, map Old_sym α)) ` (δ M q a Z)"
| "final_of_stack_delta _ _ _ = {}"

text ‹We slight modify the transition function from Kozen's proof to simplify the formalization (see \isa{stack\_to\_final\_pda\_last\_step}):›

fun final_of_stack_delta_eps :: "'q st_extended ⇒ 's sym_extended ⇒ ('q st_extended × 's sym_extended list) set" where
  "final_of_stack_delta_eps (Old_st q) (Old_sym Z) = (λ(p, α). (Old_st p, map Old_sym α)) ` (δε M q Z)"
| "final_of_stack_delta_eps New_init New_sym = {(Old_st (init_state M), [Old_sym (init_symbol M), New_sym])}"
| "final_of_stack_delta_eps (Old_st q) New_sym = {(New_final, [])}"
| "final_of_stack_delta_eps _ _ = {}"

definition final_of_stack_pda :: "('q st_extended, 'a, 's sym_extended) pda" where
  "final_of_stack_pda ≡ ⦇ init_state = New_init, init_symbol = New_sym, final_states = {New_final}, 
                    delta = final_of_stack_delta, delta_eps = final_of_stack_delta_eps ⦈"

lemma pda_final_of_stack: "pda final_of_stack_pda"
proof (standard, goal_cases)
  case (1 p x z)
  have "finite (final_of_stack_delta p x z)"
    by (induction p x z rule: final_of_stack_delta.induct) (auto simp: finite_delta)
  then show ?case
    by (simp add: final_of_stack_pda_def)
next
  case (2 p z)
  have "finite (final_of_stack_delta_eps p z)"
    by (induction p z rule: final_of_stack_delta_eps.induct) (auto simp: finite_delta_eps)
  then show ?case
    by (simp add: final_of_stack_pda_def)
qed

lemma final_of_stack_pda_trans:
  "(p, β) ∈ δ M q a Z ⟷ 
          (Old_st p, map Old_sym β) ∈ δ final_of_stack_pda (Old_st q) a (Old_sym Z)"
by (auto simp: final_of_stack_pda_def inj_map_eq_map[OF inj_Old_sym])

lemma final_of_stack_pda_eps:
  "(p, β) ∈ δε M q Z ⟷ (Old_st p, map Old_sym β) ∈ δε final_of_stack_pda (Old_st q) (Old_sym Z)"
by (auto simp: final_of_stack_pda_def inj_map_eq_map[OF inj_Old_sym])

lemma final_of_stack_pda_step: 
  "(p1, w1, α1) ↝ (p2, w2, α2) ⟷
      pda.step1 final_of_stack_pda (Old_st p1, w1, map Old_sym α1) (Old_st p2, w2, map Old_sym α2)" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain Z α where α1_def: "α1 = Z # α" and rule: "(∃β. w2 = w1 ∧ α2 = β@α ∧ (p2, β) ∈ δε M p1 Z) 
                            ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α ∧ (p2,β) ∈ δ M p1 a Z)"
    using step1_rule_ext by auto
  from rule have "(∃β. w2 = w1 ∧ map Old_sym α2 = map Old_sym β @ map Old_sym α ∧ (Old_st p2, map Old_sym β) ∈ δε final_of_stack_pda (Old_st p1) (Old_sym Z)) 
            ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = map Old_sym β @ map Old_sym α ∧ 
                 (Old_st p2, map Old_sym β) ∈ δ final_of_stack_pda (Old_st p1) a (Old_sym Z))"
    using final_of_stack_pda_trans final_of_stack_pda_eps by auto
  hence "(∃β. w2 = w1 ∧ map Old_sym α2 = β @ map Old_sym α ∧ (Old_st p2, β) ∈ δε final_of_stack_pda (Old_st p1) (Old_sym Z)) 
            ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = β @ map Old_sym α ∧ (Old_st p2, β) ∈ δ final_of_stack_pda (Old_st p1) a (Old_sym Z))" 
    by blast
  with α1_def show ?r
    using pda.step1_rule[OF pda_final_of_stack] by simp
next
  assume ?r
  then obtain Z α where map_α1_def: "map Old_sym α1 = Old_sym Z # map Old_sym α" and 
     rule: "(∃β. w2 = w1 ∧ map Old_sym α2 = β @ map Old_sym α ∧ (Old_st p2, β) ∈ δε final_of_stack_pda (Old_st p1) (Old_sym Z)) 
         ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = β@ map Old_sym α ∧ (Old_st p2,β) ∈ δ final_of_stack_pda (Old_st p1) a (Old_sym Z))"
    using pda.step1_rule_ext[OF pda_final_of_stack] by auto
  from map_α1_def have α1_def: "α1 = Z # α"
    by (metis list.inj_map_strong list.simps(9) sym_extended.inject)
  from rule have "(∃β. w2 = w1 ∧ map Old_sym α2 = map Old_sym β@ map Old_sym α ∧ (Old_st p2, map Old_sym β) ∈ δε final_of_stack_pda (Old_st p1) (Old_sym Z)) 
     ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = map Old_sym β@ map Old_sym α ∧ (Old_st p2, map Old_sym β) ∈ δ final_of_stack_pda (Old_st p1) a (Old_sym Z))"
    using append_eq_map_conv[where ?f = Old_sym] by metis
  hence "(∃β. w2 = w1 ∧ α2 = β@α ∧ (p2, β) ∈ δε M p1 Z)
    ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α ∧ (p2,β) ∈ δ M p1 a Z)"
    using final_of_stack_pda_trans final_of_stack_pda_eps by (metis list.inj_map_strong sym_extended.inject map_append)
  with α1_def show ?l
    using step1_rule by simp
qed

abbreviation α_with_new :: "'s list ⇒ 's sym_extended list" where
  "α_with_new α ≡ map Old_sym α @ [New_sym]"

lemma final_of_stack_pda_step1_drop:
  assumes "pda.step1 final_of_stack_pda (Old_st p1, w1, α_with_new α1) 
                                            (Old_st p2, w2, α_with_new α2)"
    shows "(p1, w1, α1) ↝ (p2, w2, α2)"
proof -
  from assms obtain Z α where α1_with_new_def: "α_with_new α1 = Z # α" and
    rule: "(∃β. w2 = w1 ∧ α_with_new α2 = β@α ∧ (Old_st p2, β) ∈ final_of_stack_delta_eps (Old_st p1) Z) 
         ∨ (∃a β. w1 = a # w2 ∧ α_with_new α2 = β@α ∧ (Old_st p2,β) ∈ final_of_stack_delta (Old_st p1) a Z)"
    using pda.step1_rule_ext[OF pda_final_of_stack] by (auto simp: final_of_stack_pda_def)
  from rule have "Z ≠ New_sym"
    by (induction "Old_st p1" Z rule: final_of_stack_delta_eps.induct) auto
  with α1_with_new_def have "map Old_sym α1 ≠ []" by auto
  with assms have "pda.step1 final_of_stack_pda (Old_st p1, w1, map Old_sym α1) 
                                                (Old_st p2, w2, map Old_sym α2)"
    using pda.step1_stack_drop[OF pda_final_of_stack] by blast
  thus ?thesis
    using final_of_stack_pda_step by simp
qed

lemma final_of_stack_pda_from_old:
  assumes "pda.step1 final_of_stack_pda (Old_st p1, w1, α1) (p2, w2, α2)"
    shows "(∃p2'. p2 = Old_st p2') ∨ p2 = New_final"
proof -
  from assms obtain Z α where 
            "(∃β. w2 = w1 ∧ α2 = β@α ∧ (p2, β) ∈ final_of_stack_delta_eps (Old_st p1) Z) 
              ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α ∧ (p2,β) ∈ final_of_stack_delta (Old_st p1) a Z)"
    using pda.step1_rule_ext[OF pda_final_of_stack] by (auto simp: final_of_stack_pda_def)+
  thus ?thesis 
    by (induction "Old_st p1" Z rule: final_of_stack_delta_eps.induct) auto
qed

lemma final_of_stack_pda_no_step_final:
  "¬pda.step1 final_of_stack_pda (New_final, w1, α1) (p, w2, α2)"
  apply (cases α1)
   apply (simp add: pda.step1_empty_stack[OF pda_final_of_stack])
  apply (use pda.step1_rule[OF pda_final_of_stack] final_of_stack_pda_def in simp)
  done

lemma final_of_stack_pda_from_oldn:
  assumes "pda.steps final_of_stack_pda (Old_st p1, w1, α1) (p2, w2, α2)"
  shows "∃q'. p2 = Old_st q' ∨ p2 = New_final"
by (induction "(Old_st p1, w1, α1)" "(p2, w2, α2)" arbitrary: p2 w2 α2 rule: pda.steps_induct2_bw[OF pda_final_of_stack])
  (use assms final_of_stack_pda_from_old final_of_stack_pda_no_step_final in blast)+

lemma final_of_stack_pda_to_old:
  assumes "pda.step1 final_of_stack_pda (p1, w1, α1) (Old_st p2, w2, α2)"
    shows "(∃q'. p1 = Old_st q') ∨ p1 = New_init"
using assms final_of_stack_pda_no_step_final by (metis st_extended.exhaust)

lemma final_of_stack_pda_bottom_elem:
  assumes "pda.steps final_of_stack_pda (Old_st p1, w1, α_with_new α1)
                                         (Old_st p2, w2, γ)"
  shows "∃α. γ = α_with_new α"
using assms proof (induction "(Old_st p1, w1, α_with_new α1)" "(Old_st p2, w2, γ)" arbitrary: p2 w2 γ
                          rule: pda.steps_induct2_bw[OF pda_final_of_stack])
  case (3 p2 w2 α2 w3 α3 p3)
  obtain p2' where p2_def: "p2 = Old_st p2'"
    using final_of_stack_pda_from_oldn[OF 3(1)] final_of_stack_pda_to_old[OF 3(2)] by blast
  with 3(1,3) have α2_def: "∃α. α2 = α_with_new α" by simp
  from 3(2)[unfolded p2_def] obtain Z α where α2_split: "α2 = Z # α" and rule:
    "(∃β. w3 = w2 ∧ α3 = β @ α ∧ (Old_st p3, β) ∈ final_of_stack_delta_eps (Old_st p2') Z) 
     ∨ (∃a β. w2 = a # w3 ∧ α3 = β @ α ∧ (Old_st p3, β) ∈ final_of_stack_delta (Old_st p2') a Z)"
      using pda.step1_rule_ext[OF pda_final_of_stack] by (auto simp: final_of_stack_pda_def)
    from rule have "∃Z'. Z = Old_sym Z'"
      by (induction "Old_st p2'" Z rule: final_of_stack_delta_eps.induct) auto
    with α2_def α2_split have "∃γ. α = α_with_new γ"
      by (metis hd_append list.sel(1,3) map_tl sym_extended.simps(3) tl_append_if)
    with rule show ?case
      by (induction "Old_st p2'" Z rule: final_of_stack_delta_eps.induct, auto) (metis map_append)+
qed (rule assms, blast)

lemma final_of_stack_pda_stepn:
  "(p1, w1, α1) ↝(n) (p2, w2, α2) ⟷ 
            pda.stepn final_of_stack_pda n (Old_st p1, w1, α_with_new α1) (Old_st p2, w2, α_with_new α2)" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
  proof (induction n "(p1, w1, α1)" "(p2, w2, α2)" arbitrary: p2 w2 α2 rule: stepn.induct)
    case (stepn n p2 w2 α2 p3 w3 α3)
    from stepn(3) have "pda.step1 final_of_stack_pda (Old_st p2, w2, map Old_sym α2) (Old_st p3, w3, map Old_sym α3)"
      using final_of_stack_pda_step by simp
    hence "pda.step1 final_of_stack_pda (Old_st p2, w2, α_with_new α2) (Old_st p3, w3, α_with_new α3)"
      using pda.step1_stack_app[OF pda_final_of_stack] by simp
    with stepn(2) show ?case
      by (simp add: pda.stepn[OF pda_final_of_stack])
  qed (simp add: pda.refln[OF pda_final_of_stack])
next
  assume r: ?r thus ?l
  proof (induction n "(Old_st p1, w1, α_with_new α1)" "(Old_st p2, w2, α_with_new α2)" 
                 arbitrary: p2 w2 α2 rule: pda.stepn.induct[OF pda_final_of_stack])
    case (3 n p2 w2 α2 w3 p3 α3)
    from 3(1) have steps_3_1: "pda.steps final_of_stack_pda (Old_st p1, w1, α_with_new α1) (p2, w2, α2)"
      using pda.stepn_steps[OF pda_final_of_stack] by blast
    obtain p2' where p2_def: "p2 = Old_st p2'"
      using final_of_stack_pda_from_oldn[OF steps_3_1] final_of_stack_pda_to_old[OF 3(3)] by blast
    with steps_3_1 obtain γ where α2_def: "α2 = map Old_sym γ @ [New_sym]"
      using final_of_stack_pda_bottom_elem by blast

    with p2_def 3(1,2) have "pda.stepn M n (p1, w1, α1) (p2', w2, γ)" by simp

    moreover from p2_def α2_def 3(3) have "pda.step1 M (p2', w2, γ) (p3, w3, α3)"
      using final_of_stack_pda_step1_drop by simp

    ultimately show ?case by simp
  qed (rule r, metis refln list.inj_map_strong sym_extended.inject)
qed

lemma final_of_stack_pda_steps:
  "(p1, w1, α1) ↝* (p2, w2, α2) ⟷ 
            pda.steps final_of_stack_pda (Old_st p1, w1, α_with_new α1) (Old_st p2, w2, α_with_new α2)"
using final_of_stack_pda_stepn pda.stepn_steps[OF pda_final_of_stack] stepn_steps by simp

lemma final_of_stack_pda_first_step:
  assumes "pda.step1 final_of_stack_pda (New_init, w1, [New_sym]) (p2, w2, α)"
  shows "p2 = Old_st (init_state M) ∧ w2 = w1 ∧ α = [Old_sym (init_symbol M), New_sym]"
using assms pda.step1_rule[OF pda_final_of_stack] by (simp add: final_of_stack_pda_def)

text ‹By not allowing any moves from the new final state, we obtain a distinct last step, which simplifies 
the argument about splitting the path that the constructed automaton takes upon accepting a word:›

lemma final_of_stack_pda_last_step:
  assumes "pda.step1 final_of_stack_pda (p1, w1, α1) (New_final, w2, α2)"
    shows "∃q. p1 = Old_st q ∧ w1 = w2 ∧ α1 = New_sym # α2"
proof -
  from assms obtain Z α where α1_def: "α1 = Z # α" and rule: 
        "(∃β. w2 = w1 ∧ α2 = β @ α ∧ (New_final, β) ∈ final_of_stack_delta_eps p1 Z) 
            ∨ (∃a β. w1 = a # w2 ∧ α2 = β @ α ∧ (New_final, β) ∈ final_of_stack_delta p1 a Z)"
    using pda.step1_rule_ext[OF pda_final_of_stack] by (auto simp: final_of_stack_pda_def)
  from rule have "w2 = w1" and "α2 = α" and "∃q. p1 = Old_st q ∧ Z = New_sym"
    by (induction p1 Z rule: final_of_stack_delta_eps.induct) auto
  with α1_def show ?thesis by simp
qed

lemma final_of_stack_pda_split_path:
  assumes "pda.stepn final_of_stack_pda (Suc (Suc n)) (New_init, w1, [New_sym]) (New_final, w2, γ)"
    shows "∃q. pda.step1 final_of_stack_pda (New_init, w1, [New_sym]) 
                                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym]) ∧
           pda.stepn final_of_stack_pda n (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                                               (Old_st q, w2, [New_sym]) ∧
           pda.step1 final_of_stack_pda (Old_st q, w2, [New_sym]) 
                                               (New_final, w2, γ) ∧ γ = []"
proof -
  from assms have fstep: "pda.step1 final_of_stack_pda (New_init, w1, [New_sym]) 
                                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])"
                 and stepn: "pda.stepn final_of_stack_pda (Suc n) 
                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                              (New_final, w2, γ)"
    using pda.stepn_split_first[OF pda_final_of_stack] final_of_stack_pda_first_step by blast+
  from stepn obtain q where lstep: "pda.step1 final_of_stack_pda (Old_st q, w2, New_sym # γ) (New_final, w2, γ)"
                        and stepn': "pda.stepn final_of_stack_pda n 
                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                              (Old_st q, w2, New_sym # γ)"
    using pda.stepn_split_last[OF pda_final_of_stack] final_of_stack_pda_last_step by blast
  from stepn' have "∃α. New_sym # γ = α_with_new α"
    using final_of_stack_pda_bottom_elem pda.stepn_steps[OF pda_final_of_stack]
    by (metis (no_types, opaque_lifting) Cons_eq_appendI append_Nil list.map_disc_iff list.simps(9))
  hence "γ = []"
    by (metis Nil_is_map_conv hd_append2 hd_map list.sel(1,3) sym_extended.simps(3) tl_append_if)
  with fstep lstep stepn' show ?thesis by auto
qed

lemma final_of_stack_pda_path_length:
  assumes "pda.stepn final_of_stack_pda n (New_init, w1, [New_sym]) (New_final, w2, γ)"
  shows "∃n'. n = Suc (Suc (Suc n'))"
proof -
  from assms obtain n' where n_def: "n = Suc n'" and fstep: "pda.step1 final_of_stack_pda (New_init, w1, [New_sym]) 
                                                          (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])"
                                                  and stepn: "pda.stepn final_of_stack_pda n' 
                                                          (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                                                              (New_final, w2, γ)"
    using pda.stepn_not_refl_split_first[OF pda_final_of_stack] final_of_stack_pda_first_step by blast
  from stepn obtain n'' where n'_def: "n' = Suc n''"
    using pda.stepn_not_refl_split_last[OF pda_final_of_stack] by blast
  with n_def assms have "∃q. pda.stepn final_of_stack_pda n'' 
                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym]) (Old_st q, w2, [New_sym])"
    using final_of_stack_pda_split_path by blast
  then obtain n''' where "n'' = Suc n'''"
    using pda.stepn_not_refl_split_last[OF pda_final_of_stack] by blast
  with n_def n'_def show ?thesis by simp
qed

lemma accepted_final_of_stack:  
"(∃q. (init_state M, w, [init_symbol M]) ↝* (q, [], [])) ⟷ (∃q γ. q ∈ final_states final_of_stack_pda ∧ 
  pda.steps final_of_stack_pda (init_state final_of_stack_pda, w, [init_symbol final_of_stack_pda]) (q, [], γ))" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain q where "(init_state M, w, [init_symbol M]) ↝* (q, [], [])" by blast
  hence "pda.steps final_of_stack_pda (Old_st (init_state M), w, [Old_sym (init_symbol M), New_sym]) (Old_st q, [], [New_sym])"
    using final_of_stack_pda_steps by simp

  moreover have "pda.step1 final_of_stack_pda (init_state final_of_stack_pda, w, [init_symbol final_of_stack_pda]) 
                                         (Old_st (init_state M), w, [Old_sym (init_symbol M), New_sym])"
    using pda.step1_rule[OF pda_final_of_stack] by (simp add: final_of_stack_pda_def)

  moreover have "pda.step1 final_of_stack_pda (Old_st q, [], [New_sym]) (New_final, [], [])"
    using pda.step1_rule[OF pda_final_of_stack] by (simp add: final_of_stack_pda_def)

  ultimately have a1:
    "pda.steps final_of_stack_pda (init_state final_of_stack_pda, w, [init_symbol final_of_stack_pda ]) (New_final, [], [])"
    using pda.step1_steps[OF pda_final_of_stack] pda.steps_trans[OF pda_final_of_stack] by metis

  moreover have "New_final ∈ final_states final_of_stack_pda"
    by (simp add: final_of_stack_pda_def)

  ultimately show ?r by blast
next
  assume ?r
  then obtain q γ where q_final: "q ∈ final_states final_of_stack_pda" and
                steps: "pda.steps final_of_stack_pda (init_state final_of_stack_pda, w, [init_symbol final_of_stack_pda]) (q, [], γ)" by blast
  from q_final have q_def: "q = New_final"
    by (simp add: final_of_stack_pda_def)
  with steps obtain n where stepn: "pda.stepn final_of_stack_pda n (New_init, w, [New_sym]) (New_final, [], γ)"
    using pda.stepn_steps[OF pda_final_of_stack] by (fastforce simp add: final_of_stack_pda_def)
  then obtain n' where "n = Suc (Suc n')"
    using final_of_stack_pda_path_length by blast
  with stepn obtain p where "pda.stepn final_of_stack_pda n' (Old_st (init_state M), w, [Old_sym (init_symbol M), New_sym])
                                                                (Old_st p, [], [New_sym])"
    using final_of_stack_pda_split_path by blast
  hence "(init_state M, w, [(init_symbol M)]) ↝(n') (p, [], [])"
    using final_of_stack_pda_stepn by simp
  thus ?l
    using stepn_steps by blast
qed

lemma final_of_stack: "pda.accept_stack M = pda.accept_final final_of_stack_pda"
  unfolding accept_stack_def pda.accept_final_def[OF pda_final_of_stack] using accepted_final_of_stack by blast

end
end