Theory Final_To_Stack_PDA

subsection ‹Final Acceptance to Stack Acceptance›

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

theory Final_To_Stack_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 stack_of_final_delta :: "'q st_extended ⇒ 'a ⇒ 's sym_extended ⇒ ('q st_extended × 's sym_extended list) set" where
  "stack_of_final_delta (Old_st q) a (Old_sym Z) = (λ(p, α). (Old_st p, map Old_sym α)) ` (δ M q a Z)"
| "stack_of_final_delta  _ _ _ = {}"

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

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

lemma pda_final_to_stack:
  "pda stack_of_final_pda"
proof (standard, goal_cases)
  case (1 p x z)
  have "finite (stack_of_final_delta p x z)"
    by (induction p x z rule: stack_of_final_delta.induct) (auto simp: finite_delta)
  then show ?case
    by (simp add: stack_of_final_pda_def)
next
  case (2 p z)
  have "finite (stack_of_final_delta_eps p z)"
    by (induction p z rule: stack_of_final_delta_eps.induct) (auto simp: finite_delta_eps)
  then show ?case
    by (simp add: stack_of_final_pda_def)
qed

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

lemma stack_of_final_pda_eps:
  "(p, β) ∈ δε M q Z ⟷ (Old_st p, map Old_sym β) ∈ δε stack_of_final_pda (Old_st q) (Old_sym Z)"
by (auto simp: stack_of_final_pda_def inj_map_eq_map[OF inj_Old_sym] split: if_splits)

lemma stack_of_final_pda_step:
  "(p1, w1, α1) ↝ (p2, w2, α2) ⟷
             pda.step1 stack_of_final_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 β) ∈ δε stack_of_final_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 β) ∈ δ stack_of_final_pda (Old_st p1) a (Old_sym Z))"
    using stack_of_final_pda_trans stack_of_final_pda_eps by fastforce
  hence "(∃β. w2 = w1 ∧ map Old_sym α2 = β @ map Old_sym α ∧ (Old_st p2, β) ∈ δε stack_of_final_pda (Old_st p1) (Old_sym Z)) 
            ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = β @ map Old_sym α ∧ (Old_st p2, β) ∈ δ stack_of_final_pda (Old_st p1) a (Old_sym Z))"  by blast
  with α1_def show ?r
    using pda.step1_rule[OF pda_final_to_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, β) ∈ δε stack_of_final_pda (Old_st p1) (Old_sym Z)) 
       ∨ (∃a β. w1 = a # w2 ∧ map Old_sym α2 = β@ map Old_sym α ∧ 
            (Old_st p2,β) ∈ δ stack_of_final_pda (Old_st p1) a (Old_sym Z))"
    using pda.step1_rule_ext[OF pda_final_to_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 β) ∈ δε stack_of_final_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 β) ∈ δ stack_of_final_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 stack_of_final_pda_trans stack_of_final_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 stack_of_final_pda_step1_drop:
  assumes "pda.step1 stack_of_final_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, β) ∈ stack_of_final_delta_eps (Old_st p1) Z) 
          ∨ (∃a β. w1 = a # w2 ∧ α_with_new α2 = β@α ∧ (Old_st p2,β) ∈ stack_of_final_delta (Old_st p1) a Z)"
    using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
  from rule have "Z ≠ New_sym"
    by (induction "Old_st p1" Z rule: stack_of_final_delta_eps.induct) (auto, metis empty_iff fst_conv singletonD st_extended.simps(5))
  with α1_with_new_def have "map Old_sym α1 ≠ []" by auto
  with assms have "pda.step1 stack_of_final_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_to_stack] by blast
  thus ?thesis
    using stack_of_final_pda_step by simp
qed

lemma stack_of_final_pda_from_old:
  assumes "pda.step1 stack_of_final_pda (Old_st p1, w1, α1) (p2, w2, α2)"
    shows "(∃p2'. p2 = Old_st p2') ∨ p2 = New_final"
proof -
  from assms obtain Z α where rule: 
        "(∃β. w2 = w1 ∧ α2 = β@α ∧ (p2, β) ∈ stack_of_final_delta_eps (Old_st p1) Z) 
            ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α ∧ (p2,β) ∈ stack_of_final_delta (Old_st p1) a Z)"
    using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)+
  thus ?thesis 
    by (induction "Old_st p1" Z rule: stack_of_final_delta_eps.induct, auto) (metis empty_iff fst_conv singletonD)+
qed

lemma stack_of_final_pda_from_final:
  assumes "pda.step1 stack_of_final_pda (New_final, w1, α1) (p2, w2, α2)"
    shows "∃Z'. p2 = New_final ∧ w2 = w1 ∧ α1 = Z'#α2"
proof -
  from assms obtain Z α where α1_def: "α1 = Z#α" and rule: 
        "(∃β. w2 = w1 ∧ α2 = β@α ∧ (p2,β) ∈ stack_of_final_delta_eps New_final Z) 
          ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α ∧ (p2,β) ∈ stack_of_final_delta New_final a Z)"
    using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
  thus ?thesis 
    by (induction "New_final:: 'q st_extended" Z rule: stack_of_final_delta_eps.induct) auto
qed

lemma stack_of_final_pda_from_oldn:
  assumes "pda.steps stack_of_final_pda (Old_st p1, w1, α1) (p2, w2, α2)"
  shows "∃q'. p2 = Old_st q' ∨ p2 = New_final"
proof (induction "(Old_st p1, w1, α1)" "(p2, w2, α2)" arbitrary: p2 w2 α2 rule: pda.steps_induct2_bw[OF pda_final_to_stack])
  case (3 p2 w2 α2 p3 w3 α3)
  then show ?case
    using stack_of_final_pda_from_final stack_of_final_pda_from_old by blast
qed (auto simp: assms)

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

lemma stack_of_final_pda_bottom_elem:
  assumes "pda.steps stack_of_final_pda (Old_st p1, w1, α_with_new α1) (Old_st p2, w2, γ)"
  shows "∃α. γ = α_with_new α"
proof (induction "(Old_st p1, w1, α_with_new α1)" "(Old_st p2, w2, γ)" arbitrary: p2 w2 γ rule: pda.steps_induct2_bw[OF pda_final_to_stack])
  case (3 p2 w2 α2 w3 α3 p3)
  obtain p2' where p2_def: "p2 = Old_st p2'"
    using stack_of_final_pda_from_oldn[OF 3(1)] stack_of_final_pda_to_old[OF 3(2)] by blast
  with 3(3) have α2_def: "∃α. α2 = α_with_new α" by simp
  from p2_def 3(2) obtain Z α where α2_split: "α2 = Z # α" and rule:
    "(∃β. w3 = w2 ∧ α3 = β @ α ∧ (Old_st p3, β) ∈ stack_of_final_delta_eps (Old_st p2') Z) 
     ∨ (∃a β. w2 = a # w3 ∧ α3 = β @ α ∧ (Old_st p3, β) ∈ stack_of_final_delta (Old_st p2') a Z)"
    using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
  hence "∃Z'. Z = Old_sym Z'"
    by (induction "Old_st p2'" Z rule: stack_of_final_delta_eps.induct) 
          (auto, meson empty_iff insert_iff prod.inject st_extended.distinct(3))
  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: stack_of_final_delta_eps.induct, auto)
        (metis empty_iff fst_conv singleton_iff st_extended.distinct(3), metis map_append,
           metis map_append, metis empty_iff fst_conv singleton_iff st_extended.distinct(3))
qed (auto simp: assms)

lemma stack_of_final_pda_stepn:
  "(p1, w1, α1) ↝(n) (p2, w2, α2) ⟷ 
      pda.stepn stack_of_final_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 stack_of_final_pda (Old_st p2, w2, map Old_sym α2) (Old_st p3, w3, map Old_sym α3)"
      using stack_of_final_pda_step by simp
    hence "pda.step1 stack_of_final_pda (Old_st p2, w2, α_with_new α2) (Old_st p3, w3, α_with_new α3)"
      using pda.step1_stack_app[OF pda_final_to_stack] by simp
    with stepn(2) show ?case
      by (simp add: pda.stepn[OF pda_final_to_stack])
  qed (simp add: pda.refln[OF pda_final_to_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_to_stack])
    case (3 n p2 w2 α2 w3 p3 α3)
    from 3(1) have steps_3_1: "pda.steps stack_of_final_pda (Old_st p1, w1, α_with_new α1) (p2, w2, α2)"
      using pda.stepn_steps[OF pda_final_to_stack] by blast
    obtain p2' where p2_def: "p2 = Old_st p2'"
      using stack_of_final_pda_from_oldn[OF steps_3_1] stack_of_final_pda_to_old[OF 3(3)] by blast
    with steps_3_1 obtain γ where α2_def: "α2 = α_with_new γ"
      using stack_of_final_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 stack_of_final_pda_step1_drop by simp

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

lemma stack_of_final_pda_steps:
  "(p1, w1, α1) ↝* (p2, w2, α2) ⟷
      pda.steps stack_of_final_pda (Old_st p1, w1, α_with_new α1) (Old_st p2, w2, α_with_new α2)"
using stack_of_final_pda_stepn pda.stepn_steps[OF pda_final_to_stack] stepn_steps by simp

lemma stack_of_final_pda_final_dump:
  "pda.steps stack_of_final_pda (New_final, w, γ) (New_final, w, [])"
proof (induction γ)
  case (Cons Z γ)
  have "(New_final, []) ∈ stack_of_final_delta_eps New_final Z" by simp
  hence "pda.step1 stack_of_final_pda (New_final, w, Z # γ) (New_final, w, γ)"
    using pda.step1_rule[OF pda_final_to_stack] by (simp add: stack_of_final_pda_def)
  with Cons.IH show ?case
    using pda.step1_steps[OF pda_final_to_stack] pda.steps_trans[OF pda_final_to_stack] by blast
qed (simp add: pda.steps_refl[OF pda_final_to_stack])

lemma stack_of_final_pda_first_step:
  assumes "pda.step1 stack_of_final_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_to_stack] by (simp add: stack_of_final_pda_def)

lemma stack_of_final_pda_empty_only_final:
  assumes "pda.steps stack_of_final_pda (New_init, w1, [New_sym]) (q, w2, [])"
  shows "q = New_final"
proof -
  from assms have "pda.steps stack_of_final_pda (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym]) (q, w2, [])"
    using pda.steps_not_refl_split_first[OF pda_final_to_stack] stack_of_final_pda_first_step by blast
  thus ?thesis
    using stack_of_final_pda_bottom_elem[of "init_state M" w1 "[init_symbol M]" _ w2 "[]"]  stack_of_final_pda_from_oldn by fastforce
qed

lemma stack_of_final_pda_split_old_final:
  assumes "pda.stepn stack_of_final_pda (Suc n) (Old_st p1, w1, α1) (New_final :: 'q st_extended, w2, α2)"
    shows "∃q k γ. k ≤ n ∧ q ∈ final_states M ∧
            pda.stepn stack_of_final_pda k (Old_st p1, w1, α1) (Old_st q, w2, γ) ∧
            pda.step1 stack_of_final_pda (Old_st q, w2, γ) (New_final, w2, γ) ∧
            pda.stepn stack_of_final_pda (n-k) (New_final, w2, γ) (New_final, w2, α2)"
using assms proof (induction "Suc n" "(Old_st p1, w1, α1)" "(New_final :: 'q st_extended, w2, α2)" 
                          arbitrary: n w2 α2 rule: pda.stepn.induct[OF pda_final_to_stack])
  case (3 n p2 w2 α2 w3 α3)
  then show ?case proof (cases n)
    case 0
    with 3(1) have p2_def: "Old_st p1 = p2" and w12: "w1 = w2" and a12: "α1 = α2"
      using pda.stepn_zeroE[OF pda_final_to_stack] by blast+
    from p2_def 3(3) obtain Z α where α2_def: "α2 = Z # α" and rule: 
            "(∃β. w3 = w2 ∧ α3 = β@α ∧ (New_final,β) ∈ stack_of_final_delta_eps (Old_st p1) Z) 
               ∨ (∃a β. w2 = a # w3 ∧ α3 = β@α ∧ (New_final,β) ∈ stack_of_final_delta (Old_st p1) a Z)"
      using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
    from α2_def rule have p1_final: "p1 ∈ final_states M" and w23: "w3 = w2" and a23: "α3 = α2"
      by (induction "Old_st p1" Z rule: stack_of_final_delta_eps.induct, auto)
         (meson empty_iff, meson empty_iff prod.inject singletonD, meson empty_iff, meson empty_iff prod.inject singletonD)

    from w12 w23 a12 a23 have "pda.stepn stack_of_final_pda 0 (Old_st p1, w1, α1) (Old_st p1, w3, α3)"
      using pda.refln[OF pda_final_to_stack] by simp

    moreover from 3(3) p2_def w23 a23 have "pda.step1 stack_of_final_pda (Old_st p1, w3, α3) (New_final, w3, α3)" by simp

    moreover from 0 have "pda.stepn stack_of_final_pda (n - 0) (New_final, w3, α3) (New_final, w3, α3)"
      using pda.refln[OF pda_final_to_stack] by simp

    ultimately show ?thesis 
      using p1_final by blast
  next
    case (Suc n')
    then show ?thesis proof (cases "p2 = New_final")
      case True
      with Suc 3(1,2) obtain q k γ where k_less: "k ≤ n'" and q_final: "q ∈ final_states M" and
       stepn: "pda.stepn stack_of_final_pda k (Old_st p1, w1, α1) (Old_st q, w2, γ)" and
       step1: "pda.step1 stack_of_final_pda (Old_st q, w2, γ) (New_final, w2, γ)" and
       stepn': "pda.stepn stack_of_final_pda (n' - k) (New_final, w2, γ) (New_final, w2, α2)" by blast
      from True 3(3) obtain Z' α' where "α2 = Z' # α'" and rule: 
          "(∃β. w3 = w2 ∧ α3 = β@α' ∧ (New_final,β) ∈ stack_of_final_delta_eps New_final Z') 
             ∨ (∃a β. w2 = a # w3 ∧ α3 = β@α' ∧ (New_final,β) ∈ stack_of_final_delta New_final a Z')"
        using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
      from rule have w23: "w3 = w2"
        by (induction "New_final :: 'q st_extended" Z' rule: stack_of_final_delta_eps.induct) auto

      moreover from k_less Suc have "k ≤ n" by simp

      moreover from stepn w23 have "pda.stepn stack_of_final_pda k (Old_st p1, w1, α1) (Old_st q, w3, γ)" by simp

      moreover from step1 w23 have "pda.step1 stack_of_final_pda (Old_st q, w3, γ) (New_final, w3, γ)" by simp

      moreover from stepn' 3(3) True w23 Suc k_less have "pda.stepn stack_of_final_pda (n - k) (New_final, w3, γ) (New_final, w3, α3)"
        using pda.stepn[OF pda_final_to_stack] by (simp add: Suc_diff_le)

      ultimately show ?thesis 
        using q_final by blast
    next
      case False
      with 3(1) obtain p2' where p2_def: "p2 = Old_st p2'"
        using stack_of_final_pda_from_oldn pda.stepn_steps[OF pda_final_to_stack] by blast
      from p2_def 3(3) obtain Z' α' where "α2 = Z' # α'" and 
            "(∃β. w3 = w2 ∧ α3 = β@α' ∧ (New_final,β) ∈ stack_of_final_delta_eps (Old_st p2') Z') 
               ∨ (∃a β. w2 = a # w3 ∧ α3 = β@α' ∧ (New_final,β) ∈ stack_of_final_delta (Old_st p2') a Z')"
        using pda.step1_rule_ext[OF pda_final_to_stack] by (auto simp: stack_of_final_pda_def)
      hence p2_final: "p2' ∈ final_states M" and w23: "w3 = w2" and a23: "α3 = α2"
        by (induction "Old_st p2'" Z' rule: stack_of_final_delta_eps.induct, auto)
          (meson empty_iff, meson empty_iff prod.inject singletonD, meson empty_iff, meson empty_iff prod.inject singletonD)

      from 3(1) p2_def w23 a23 have "pda.stepn stack_of_final_pda n (Old_st p1, w1, α1) (Old_st p2', w3, α3)" by simp

      moreover from 3(3) p2_def w23 a23 have "pda.step1 stack_of_final_pda (Old_st p2', w3, α3) (New_final, w3, α3)" by simp

      moreover have "pda.stepn stack_of_final_pda 0 (New_final, w3, α3) (New_final, w3, α3)"
        using pda.refln[OF pda_final_to_stack] by simp

      ultimately show ?thesis 
        using p2_final by force
    qed
  qed
qed (simp add: assms)

lemma stack_of_final_pda_split_path:
  assumes "pda.stepn stack_of_final_pda (Suc (Suc n)) (New_init, w1, [New_sym]) (New_final, w2, γ)"
    shows "∃q k α. k ≤ n ∧ q ∈ final_states M ∧ pda.step1 stack_of_final_pda (New_init, w1, [New_sym]) 
                                              (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym]) ∧
           pda.stepn stack_of_final_pda k (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                                               (Old_st q, w2, α) ∧
           pda.step1 stack_of_final_pda (Old_st q, w2, α) (New_final, w2, α) ∧
           pda.stepn stack_of_final_pda (n-k) (New_final, w2, α) (New_final, w2, γ)"
proof -
  from assms have fstep: "pda.step1 stack_of_final_pda (New_init, w1, [New_sym]) 
                                      (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])"
                 and stepn: "pda.stepn stack_of_final_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_to_stack] stack_of_final_pda_first_step by blast+
  from stepn have "∃q k α. k ≤ n ∧ q ∈ final_states M ∧
           pda.stepn stack_of_final_pda k (Old_st (init_state M), w1, [Old_sym (init_symbol M), New_sym])
                                               (Old_st q, w2, α) ∧
           pda.step1 stack_of_final_pda (Old_st q, w2, α) (New_final, w2, α) ∧
           pda.stepn stack_of_final_pda (n-k) (New_final, w2, α) (New_final, w2, γ)"
    using stack_of_final_pda_split_old_final by blast
  with fstep show ?thesis by blast
qed

lemma stack_of_final_pda_path_length:
  assumes "pda.stepn stack_of_final_pda n (New_init, w1, [New_sym]) (New_final, w2, γ)"
    shows "∃n'. n = Suc (Suc n')"
proof -
  from assms obtain n' where n_def: "n = Suc n'" and 
            stepn': "pda.stepn stack_of_final_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_to_stack] stack_of_final_pda_first_step by blast
  from stepn' obtain n'' where "n' = Suc n''"
    using pda.stepn_not_refl_split_first[OF pda_final_to_stack] by blast
  with n_def show ?thesis by simp
qed

lemma accepted_final_to_stack:
"(∃q γ. q ∈ final_states M ∧ (init_state M, w, [init_symbol M]) ↝* (q, [], γ)) ⟷
  (∃q. pda.steps stack_of_final_pda (init_state stack_of_final_pda, w, [init_symbol stack_of_final_pda]) (q, [], []))" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain q γ where q_final: "q ∈ final_states M" and steps: "(init_state M, w, [init_symbol M]) ↝* (q, [], γ)" by blast
  obtain Z α where map_γ_def: "α_with_new γ = Z#α"
    by (auto intro: list.exhaust_sel)
  from q_final have "(New_final, [Z]) ∈ stack_of_final_delta_eps (Old_st q) Z"
    by (induction "Old_st q" Z rule: stack_of_final_delta_eps.induct) auto

  with map_γ_def have "pda.step1 stack_of_final_pda (Old_st q, [], α_with_new γ) (New_final, [], Z#α)"
    using pda.step1_rule[OF pda_final_to_stack] by (simp add: stack_of_final_pda_def)

  moreover from steps have "pda.steps stack_of_final_pda (Old_st (init_state M), w, [Old_sym (init_symbol M), New_sym]) 
                                                    (Old_st q, [], α_with_new γ)"
    using stack_of_final_pda_steps by simp

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

  moreover have "pda.steps stack_of_final_pda (New_final, [], Z#α) (New_final, [], [])"
    using stack_of_final_pda_final_dump by simp

  ultimately show ?r 
    using pda.step1_steps[OF pda_final_to_stack] pda.steps_trans[OF pda_final_to_stack] by metis
next
  assume ?r
  then obtain q where steps: "pda.steps stack_of_final_pda (New_init, w, [New_sym]) (q, [], [])"
    by (auto simp: stack_of_final_pda_def)
  hence q_def: "q = New_final"
    using stack_of_final_pda_empty_only_final by simp
  with steps obtain n where stepn: "pda.stepn stack_of_final_pda n (New_init, w, [New_sym]) (New_final, [], [])"
    using pda.stepn_steps[OF pda_final_to_stack] by blast
  then obtain n' where "n = Suc (Suc n')"
    using stack_of_final_pda_path_length by blast
  with stepn obtain p k α where p_final: "p ∈ final_states M" and stepn': "pda.stepn stack_of_final_pda k 
                  (Old_st (init_state M), w, [Old_sym (init_symbol M), New_sym]) (Old_st p, [], α)"
    using stack_of_final_pda_split_path by blast
  from stepn' obtain α' where "α = α_with_new α'"
    using stack_of_final_pda_bottom_elem pda.stepn_steps[OF pda_final_to_stack]
    by (metis (no_types, opaque_lifting) append_Cons append_Nil list.simps(8,9))
  with stepn' have "pda.stepn M k (init_state M, w, [init_symbol M]) (p, [], α')"
    using stack_of_final_pda_stepn by simp
  with p_final show ?l
    using stepn_steps by blast
qed

lemma final_to_stack:
  "pda.accept_final M = pda.accept_stack stack_of_final_pda"
  unfolding accept_final_def pda.accept_stack_def[OF pda_final_to_stack] using accepted_final_to_stack by blast

end
end