Theory PDA_To_CFG

subsection ‹PDA to CFG›

text ‹Starting from a PDA that accepts by empty stack, we construct an equivalent CFG.
The formalization is based on the Lean formalization by Leichtfried\cite{lean}.›

theory PDA_To_CFG
imports
  Pushdown_Automata
  Context_Free_Grammar.Context_Free_Grammar
begin

datatype ('q, 's) pda_nt = Start_sym | Single_sym 'q 's 'q | List_sym 'q "'s list" 'q

context pda begin

abbreviation all_pushes :: "'s list set" where 
  "all_pushes ≡ {α. ∃ p q a z. (p, α) ∈ δ M q a z} ∪ {α.∃p q z. (p, α) ∈ δε M q z}"

abbreviation max_push :: nat where 
  "max_push ≡ Suc (Max (length ` all_pushes))"

abbreviation is_allowed_nt :: "('q, 's) pda_nt set" where 
  "is_allowed_nt ≡ {List_sym p α q| p α q. length α ≤ max_push} ∪ (⋃p Z q. {Single_sym p Z q}) ∪ {Start_sym}"

abbreviation empty_rule :: "'q ⇒ (('q, 's) pda_nt, 'a) Prods" where
  "empty_rule q ≡ {(List_sym q [] q, [])}"

abbreviation trans_rule :: "'q ⇒ 'q ⇒ 'a ⇒ 's ⇒ (('q, 's) pda_nt, 'a) Prods" where
  "trans_rule q⇩0 q⇩1 a Z ≡ (λ(p, α). (Single_sym q⇩0 Z q⇩1, [Tm a, Nt (List_sym p α q⇩1)])) ` δ M q⇩0 a Z"

abbreviation eps_rule :: "'q ⇒ 'q ⇒ 's ⇒ (('q, 's) pda_nt, 'a) Prods" where
  "eps_rule q⇩0 q⇩1 Z ≡ (λ(p, α). (Single_sym q⇩0 Z q⇩1, [Nt (List_sym p α q⇩1)])) ` δε M q⇩0 Z"

fun split_rule :: "'q ⇒ ('q, 's) pda_nt ⇒ (('q, 's) pda_nt, 'a) Prods" where
  "split_rule q (List_sym p⇩0 (Z#α) p⇩1) = {(List_sym p⇩0 (Z#α) p⇩1, [Nt (Single_sym p⇩0 Z q), Nt (List_sym q α p⇩1)])}"
| "split_rule _ _ = {}"

abbreviation start_rule :: "'q ⇒ (('q, 's) pda_nt, 'a) Prods" where
  "start_rule q ≡ {(Start_sym, [Nt (List_sym (init_state M) [init_symbol M] q)])}"

abbreviation rule_set :: "(('q, 's) pda_nt, 'a) Prods" where
  "rule_set ≡ (⋃q. empty_rule q) ∪ (⋃q p a Z. trans_rule q p a Z) ∪ (⋃q p Z. eps_rule q p Z) ∪ 
                 ⋃ {split_rule q nt| q nt. nt ∈ is_allowed_nt} ∪ (⋃q. start_rule q)"

definition G :: "(('q, 's) pda_nt,'a) Cfg" where
  "G ≡ Cfg rule_set Start_sym"

lemma finite_is_allowed_nt: "finite (is_allowed_nt)"
proof (intro finite_UnI)
  show "finite {List_sym (p :: 'q) (α :: 's list) q| p α q. length α ≤ max_push}"
  proof -
    let ?A = "⋃(⋃((λs. (λf. f ` UNIV) ` s) ` ((λf. f ` {xs :: 's list. set xs ⊆ UNIV ∧ length xs ≤ max_push}) ` (List_sym ` (UNIV :: 'q set)))))"

    have "{List_sym p α q| p α q. length α ≤ max_push} = ?A"
      by auto

    moreover have "finite ?A" (is "finite (⋃?B)")
    proof (rule finite_Union)
      show "finite ?B" (is "finite (⋃?C)")
      proof (rule finite_Union)
        show "finite ?C" by simp
      next
        show "⋀M. M ∈ ?C ⟹ finite M" 
          using finite_lists_length_le[of UNIV max_push] by force
      qed
    next
      show "⋀M. M ∈ ?B ⟹ finite M" by fastforce
    qed

    ultimately show ?thesis by simp
  qed
next
  show "finite (⋃(p :: 'q) (Z :: 's) q. {Single_sym p Z q})"
    by (rule, simp)+
qed simp

lemma finite_split_rule: "finite (split_rule q nt)"
  by (induction q nt rule: split_rule.induct) auto

lemma "finite (Prods G)"
proof -
  have "finite (⋃q. empty_rule q)" by simp

  moreover have "finite (⋃q p a Z. trans_rule q p a Z)"
    by (simp add: finite_delta)

  moreover have "finite (⋃q p Z. eps_rule q p Z)"
    by (simp add: finite_delta_eps)

  moreover have "finite (⋃ {split_rule q nt| q nt. nt ∈ is_allowed_nt})"
  proof -
    have "{split_rule q nt| q nt. nt ∈ is_allowed_nt} = ⋃ ((λf. f ` is_allowed_nt) ` (split_rule ` UNIV))"
      by fastforce

    moreover have "finite (⋃ (⋃ ((λf. f ` is_allowed_nt) ` (split_rule ` UNIV))))" (is "finite (⋃?A)")
    proof (rule finite_Union)
      show "finite ?A" (is "finite (⋃?B)")
      proof (rule finite_Union)
        show "finite ?B" by simp
      next
        show "⋀M. M ∈ ?B ⟹ finite M"
          using finite_is_allowed_nt by blast
      qed
    next
      show "⋀M. M ∈ ?A ⟹ finite M"
        by (auto simp: finite_split_rule)
    qed

    ultimately show ?thesis by simp
  qed

  moreover have "finite (⋃q. start_rule q)" by simp

  ultimately show ?thesis
    by (simp add: G_def)
qed

lemma split_rule_simp:
  "(A, w) ∈ split_rule q nt ⟷
   (∃p⇩0 Z α p⇩1. nt = (List_sym p⇩0 (Z#α) p⇩1) ∧ 
                A = List_sym p⇩0 (Z#α) p⇩1 ∧ w = [Nt (Single_sym p⇩0 Z q), Nt (List_sym q α p⇩1)])"
by (induction q nt rule: split_rule.induct) auto

lemma pda_to_cfg_derive_empty:
  "Prods G ⊢ [Nt (List_sym p⇩1 [] p⇩2)] ⇒ x ⟷ p⇩2 = p⇩1 ∧ x = []"
unfolding G_def using derive_singleton[of rule_set] split_rule_simp by auto

lemma finite_all_pushes: "finite all_pushes"
proof -
  let ?A = "(λ(p, α). α) ` (⋃q a Z. δ M q a Z ∪ (⋃q Z. δε M q Z))" 
  have "all_pushes = ?A" by fast

  moreover have "finite ?A" 
    by (rule, simp add: finite_delta finite_delta_eps)+

  ultimately show ?thesis by simp
qed

lemma push_trans_leq_max:
  "(p, α) ∈ δ M q a Z ⟹ length α ≤ max_push"
proof -
  have "(p, α) ∈ δ M q a Z ⟹ length α ≤ Max (length ` all_pushes)" 
    by (rule Max_ge) (use finite_all_pushes in blast)+ 
  thus "(p, α) ∈ δ M q a Z ⟹ length α ≤ max_push" by simp
qed

lemma push_eps_leq_max:
  "(p, α) ∈ δε M q Z ⟹ length α ≤ max_push"
proof -
  have "(p, α) ∈ δε M q Z ⟹ length α ≤ Max (length ` all_pushes)"
    by (rule Max_ge) (use finite_all_pushes in blast)+ 
  thus "(p, α) ∈ δε M q Z ⟹ length α ≤ max_push" by simp
qed

lemma pda_to_cfg_derive_split:
 "Prods G ⊢ [Nt (List_sym p⇩1 (Z#α) p⇩2)] ⇒ w ⟷
  (∃q. length (Z#α) ≤ max_push ∧ w = [Nt (Single_sym p⇩1 Z q), Nt (List_sym q α p⇩2)])"
(is "?l ⟷ ?r")
proof
  assume ?l
  hence "(List_sym p⇩1 (Z # α) p⇩2, w) ∈ rule_set"
    using derive_singleton[of "Prods G" "Nt (List_sym p⇩1 (Z # α) p⇩2)" w] by (simp add: G_def)
  thus ?r
    by (auto simp: split_rule_simp)
next
  assume ?r
  then obtain q where len_α: "length (Z#α) ≤ max_push" and w_def: "w = [Nt (Single_sym p⇩1 Z q), Nt (List_sym q α p⇩2)]" by blast
  from w_def have "(List_sym p⇩1 (Z#α) p⇩2, w) ∈ split_rule q (List_sym p⇩1 (Z # α) p⇩2)" by simp
  with len_α have "(List_sym p⇩1 (Z#α) p⇩2, w) ∈ ⋃ {split_rule q nt| q nt. nt ∈ is_allowed_nt}"
    by (subst Union_iff) fast
  hence "(List_sym p⇩1 (Z#α) p⇩2, w) ∈ rule_set" by simp
  thus ?l
    using derive_singleton[of "Prods G" "Nt (List_sym p⇩1 (Z # α) p⇩2)" w] by (simp add: G_def)
qed

lemma pda_to_cfg_derive_single:
"Prods G ⊢ [Nt (Single_sym q⇩0 Z q⇩1)] ⇒ w ⟷ 
   (∃p α a. (p, α) ∈ δ M q⇩0 a Z ∧ w = [Tm a, Nt (List_sym p α q⇩1)]) ∨ 
      (∃p α. (p, α) ∈ δε M q⇩0 Z  ∧ w = [Nt (List_sym p α q⇩1)])"
unfolding G_def using derive_singleton[of rule_set] split_rule_simp by fastforce

lemma pda_to_cfg_derive_start:
"Prods G ⊢ [Nt Start_sym] ⇒ w ⟷ (∃q. w = [Nt (List_sym (init_state M) [init_symbol M] q)])"
unfolding G_def using derive_singleton[of rule_set] split_rule_simp by auto

lemma pda_to_cfg_derives_if_stepn:
  assumes "(q, x, γ) ↝(n) (p, [], [])"
      and "length γ ≤ max_push"
    shows "Prods G ⊢ [Nt (List_sym q γ p)] ⇒* map Tm x"
using assms proof (induction n arbitrary: x p q γ rule: less_induct)
  case (less n)
  then show ?case proof (cases γ)
    case Nil
    from less(2) have "(q, x, γ) ↝* (p, [], [])"
      using stepn_steps by blast
    with Nil have "q = p ∧ x = []"
      using steps_empty_stack by simp
    with Nil show ?thesis
      using pda_to_cfg_derive_empty by auto
  next
    case (Cons Z α)
    with less(2) obtain n' q' x' γ' where n_def: "n = Suc n'" and 
                                          step1: "(q, x, γ) ↝ (q', x', γ')" and 
                                          stepn: "(q', x', γ') ↝(n') (p, [], [])"
      using stepn_not_refl_split_first by blast
    from Cons step1 have rule: "(∃β. x' = x ∧ γ' = β@α ∧ (q', β) ∈ δε M q Z) 
                            ∨ (∃a β. x = a # x' ∧ γ' = β@α ∧ (q',β) ∈ δ M q a Z)" (is "?l ∨ ?r")
      using step⇩1_rule by simp
    show ?thesis proof (rule disjE[OF rule])
      assume ?l
      then obtain β where x_def: "x' = x" and γ'_split: "γ' = β@α" and eps: "(q', β) ∈ δε M q Z" by blast
      from stepn γ'_split obtain p' m⇩1 m⇩2 y y' where x'_def: "x' = y @ y'" and m1_m2_n': "m⇩1 + m⇩2 = n'" 
                  and stepm1: "stepn m⇩1 (q', y, β) (p', [], [])" and stepm2: "stepn m⇩2 (p', y', α) (p, [], [])"
        using split_stack[of n' q' x' β α p] by blast
      from n_def m1_m2_n' have m1_less_n: "m⇩1 < n" by simp
      from n_def m1_m2_n' have m2_less_n: "m⇩2 < n" by simp
      from eps have len_β: "length β ≤ max_push"
        using push_eps_leq_max by blast

      from Cons less(3) have "Prods G ⊢ [Nt (List_sym q γ p)] ⇒ [Nt (Single_sym q Z p'), Nt (List_sym p' α p)]"
        using pda_to_cfg_derive_split by simp

      moreover from eps have "Prods G ⊢ [Nt (Single_sym q Z p'), Nt (List_sym p' α p)] ⇒ 
                                  [Nt (List_sym q' β p'), Nt (List_sym p' α p)]"
        using pda_to_cfg_derive_single derive_append[of "Prods G" "[Nt (Single_sym q Z p')]" "[Nt (List_sym q' β p')]"
                                                            "[Nt (List_sym p' α p)]"] by simp
      
      moreover have "Prods G ⊢ [Nt (List_sym q' β p'), Nt (List_sym p' α p)] ⇒* map Tm y @ [Nt (List_sym p' α p)]"
        using derives_append[OF less(1)[OF m1_less_n stepm1 len_β]] by simp

      moreover from x_def x'_def Cons less(3) have "Prods G ⊢ map Tm y @ [Nt (List_sym p' α p)] ⇒* map Tm x"
        using derives_prepend[OF less(1)[OF m2_less_n stepm2]] by auto

      ultimately show ?thesis by simp
    next
      assume ?r
      then obtain a β where x_def: "x = a # x'" and γ'_split: "γ' = β@α" and trans: "(q', β) ∈ δ M q a Z" by blast
      from stepn γ'_split obtain p' m⇩1 m⇩2 y y' where x'_def: "x' = y @ y'" and m1_m2_n': "m⇩1 + m⇩2 = n'" 
                  and stepm1: "stepn m⇩1 (q', y, β) (p', [], [])" and stepm2: "stepn m⇩2 (p', y', α) (p, [], [])"
        using split_stack[of n' q' x' β α p] by blast
      from n_def m1_m2_n' have m1_less_n: "m⇩1 < n" by simp
      from n_def m1_m2_n' have m2_less_n: "m⇩2 < n" by simp
      from trans have len_β: "length β ≤ max_push"
        using push_trans_leq_max by blast

      from Cons less(3) have "Prods G ⊢ [Nt (List_sym q γ p)] ⇒ [Nt (Single_sym q Z p'), Nt (List_sym p' α p)]"
        using pda_to_cfg_derive_split by simp

      moreover from trans have "Prods G ⊢ [Nt (Single_sym q Z p'), Nt (List_sym p' α p)] ⇒
                                    [Tm a, Nt (List_sym q' β p'), Nt (List_sym p' α p)]"
        using pda_to_cfg_derive_single derive_append[of "Prods G" "[Nt (Single_sym q Z p')]" "[Tm a, Nt (List_sym q' β p')]"
                                                            "[Nt (List_sym p' α p)]"] by simp

      moreover have "Prods G ⊢ [Tm a, Nt (List_sym q' β p'), Nt (List_sym p' α p)] ⇒*
                                      Tm a # map Tm y @ [Nt (List_sym p' α p)]"
        using derives_append[OF less(1)[OF m1_less_n stepm1 len_β]] by (simp add: derives_Tm_Cons)

      moreover from x'_def x_def Cons less(3) have "Prods G ⊢ Tm a # map Tm y @ [Nt (List_sym p' α p)] ⇒* map Tm x"
        using derives_prepend[OF less(1)[OF m2_less_n stepm2], of "Tm a # map Tm y"] by simp

      ultimately show ?thesis by simp
    qed
  qed
qed

(* TODO: CFG? *)
lemma derivel_append_decomp:
  "P ⊢ u@v ⇒l w ⟷
  (∃u'. w = u'@v ∧ P ⊢ u ⇒l u') ∨ (∃u' v'. w = u@v' ∧ u = map Tm u' ∧ P ⊢ v ⇒l v')"
(is "?l ⟷ ?r")
proof
  assume ?l
  then obtain A r u1 u2
    where Ar: "(A,r) ∈ P"
      and uv: "u@v = map Tm u1 @ Nt A # u2"
      and w: "w = map Tm u1 @ r @ u2"
    by (auto simp: derivel_iff)
  from uv have case_dist: "(∃s. u2 = s @ v ∧ u = map Tm u1 @ Nt A # s) ∨
  (∃s. map Tm u1 = u @ s  ∧ v = s @ Nt A # u2)" (is "?h1 ∨ ?h2")
    by (auto simp: append_eq_append_conv2 append_eq_Cons_conv)
  show ?r proof (rule disjE[OF case_dist])
    assume ?h1
    with Ar w show ?thesis by (fastforce simp: derivel_iff)
  next
    assume ?h2
    then obtain s where map_u1_def: "map Tm u1 = u @ s" and v_def: "v = s @ Nt A # u2" by blast
    from map_u1_def obtain u' s' where u_def: "u = map Tm u'" and s_def: "s = map Tm s'"
      using append_eq_map_conv[of u s Tm u1] by auto

    from w map_u1_def s_def have "w = u @ (map Tm s' @ r @ u2)" by simp

    moreover from Ar v_def s_def have "P ⊢ v ⇒l map Tm s' @ r @ u2"
      using derivel_iff[of P] by blast

    ultimately show ?thesis
      using u_def by blast
  qed
next
  show "?r ⟹ ?l"
    by (auto simp add: derivel_append derivel_map_Tm_append)
qed

(* TODO: CFG? *)
lemma split_derivel':
  assumes "P ⊢ x#v ⇒l(n) u"
  shows "(∃u'. u = u' @ v ∧ P ⊢ [x] ⇒l(n) u') ∨ (∃w⇩1 u⇩2 m⇩1 m⇩2. m⇩1 + m⇩2 = n ∧ u = map Tm w⇩1 @ u⇩2 
                                                    ∧ P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1 ∧ P ⊢ v ⇒l(m⇩2) u⇩2)"
using assms proof (induction n arbitrary: u)
  case (Suc n)
  from Suc(2) obtain w where x_v_deriveln_w: "P ⊢ x # v ⇒l(n) w" and w_derivel_u: "P ⊢ w ⇒l u" by auto
  from Suc(1)[OF x_v_deriveln_w] have IH: "(∃u'. w = u' @ v ∧ P ⊢ [x] ⇒l(n) u') ∨
  (∃w⇩1 u⇩2 m⇩1 m⇩2. m⇩1 + m⇩2 = n ∧ w = map Tm w⇩1 @ u⇩2 ∧ P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1 ∧ P ⊢ v ⇒l(m⇩2) u⇩2)" (is "?l ∨ ?r") .
  show ?case proof (rule disjE[OF IH])
    assume ?l
    then obtain u' where w_def: "w = u' @ v" and x_deriveln_u': "P ⊢ [x] ⇒l(n) u'" by blast
    from w_def w_derivel_u have "P ⊢ u' @ v ⇒l u" by simp
    hence case_dist: "(∃u⇩0. u = u⇩0 @ v ∧ P ⊢ u' ⇒l u⇩0) ∨
                  (∃u⇩1 u⇩2. u = u' @ u⇩2 ∧ u' = map Tm u⇩1 ∧ P ⊢ v ⇒l u⇩2)" (is "?h1 ∨ ?h2")
      using derivel_append_decomp[of P u' v u] by simp
    show ?thesis proof (rule disjE[OF case_dist])
      assume ?h1
      then obtain u⇩0 where u_def: "u = u⇩0 @ v" and u'_derivel_u0: "P ⊢ u' ⇒l u⇩0" by blast
      from x_deriveln_u' u'_derivel_u0 have "P ⊢ [x] ⇒l(Suc n) u⇩0" by auto
      with u_def show ?thesis by blast
    next
      assume ?h2
      then obtain u⇩1 u⇩2 where u_def: "u = u' @ u⇩2" and u'_def: "u' = map Tm u⇩1" and v_derivel_u2: "P ⊢ v ⇒l u⇩2" by blast
      from x_deriveln_u' u'_def have "P ⊢ [x] ⇒l(n) map Tm u⇩1" by simp
      with u_def u'_def v_derivel_u2 show ?thesis by fastforce
    qed
  next
    assume ?r
    then obtain w⇩1 u⇩2 m⇩1 m⇩2 where m1_m2_n: "m⇩1 + m⇩2 = n" and w_def: "w = map Tm w⇩1 @ u⇩2" and 
                                      x_derivelm1_w1: "P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1" and v_derivelm2_u2: "P ⊢ v ⇒l(m⇩2) u⇩2" by blast
    from w_def w_derivel_u have "P ⊢ map Tm w⇩1 @ u⇩2 ⇒l u" by simp
    then obtain u' where u_def: "u = map Tm w⇩1 @ u'" and u2_derivel_u': "P ⊢ u⇩2 ⇒l u'"
      using derivel_map_Tm_append by blast

    from m1_m2_n have "m⇩1 + Suc m⇩2 = Suc n" by simp

    moreover from v_derivelm2_u2 u2_derivel_u' have "P ⊢ v ⇒l(Suc m⇩2) u'" by auto

    ultimately show ?thesis
      using u_def x_derivelm1_w1 by blast
  qed
qed simp

(* TODO: CFG? *)
lemma split_derivel:
  assumes "P ⊢ x#v ⇒l(n) map Tm w"
  shows "∃w⇩1 w⇩2 m⇩1 m⇩2. m⇩1 + m⇩2 = n ∧ w = w⇩1 @ w⇩2 ∧ P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1 ∧ P ⊢ v ⇒l(m⇩2) map Tm w⇩2"
proof -
  have case_dist: "(∃u'. map Tm w = u' @ v ∧ P ⊢ [x] ⇒l(n) u') ∨ (∃w⇩1 u⇩2 m⇩1 m⇩2. m⇩1 + m⇩2 = n ∧ map Tm w = map Tm w⇩1 @ u⇩2 
                                                    ∧ P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1 ∧ P ⊢ v ⇒l(m⇩2) u⇩2)" (is "?l ∨ ?r")
    using split_derivel'[OF assms] by simp
  show ?thesis proof (rule disjE[OF case_dist])
    assume ?l
    then obtain u' where map_w_def: "map Tm w = u' @ v" and x_derives_u': "P ⊢ [x] ⇒l(n) u'" by blast
    from map_w_def obtain w⇩1 w⇩2 where "w = w⇩1 @ w⇩2" and map_w⇩1_def: "map Tm w⇩1 = u'" and "map Tm w⇩2 = v"
      using map_eq_append_conv[of Tm w u' v] by blast

    moreover from x_derives_u' map_w⇩1_def have "P ⊢ [x] ⇒l(n) map Tm w⇩1" by simp

    moreover have "P ⊢ map Tm w⇩2 ⇒l(0) map Tm w⇩2" by simp

    ultimately show ?thesis by force
  next
    assume ?r
    then obtain w⇩1 u⇩2 m⇩1 m⇩2 where m1_m2_n: "m⇩1 + m⇩2 = n" and map_w_def: "map Tm w = map Tm w⇩1 @ u⇩2" 
                                               and x_derivelm1_w1: "P ⊢ [x] ⇒l(m⇩1) map Tm w⇩1" and v_derivelm2_u2: "P ⊢ v ⇒l(m⇩2) u⇩2" by blast
    from map_w_def obtain w⇩1' u⇩2' where "w = w⇩1' @ u⇩2'" and "map (Tm :: 'c ⇒ ('b, 'c) sym) w⇩1 = map Tm w⇩1'" and "u⇩2 = map (Tm :: 'c ⇒ ('b, 'c) sym) u⇩2'"
      using map_eq_append_conv[of "Tm :: 'c ⇒ ('b, 'c) sym" w "map Tm w⇩1" u⇩2] by blast
    with m1_m2_n x_derivelm1_w1 v_derivelm2_u2 show ?thesis by auto
  qed                    
qed

lemma pda_to_cfg_steps_if_derivel:
  assumes "Prods G ⊢ [Nt (List_sym q γ p)] ⇒l(n) map Tm x"
  shows "(q, x, γ) ↝* (p, [], [])"
using assms proof (induction n arbitrary: x p q γ rule: less_induct)
  case (less n)
  then show ?case proof (cases γ)
    case Nil
    have derives: "Prods G ⊢ [Nt (List_sym q γ p)] ⇒* map Tm x"
      using derivels_imp_derives[OF relpowp_imp_rtranclp[OF less(2)]] .
    have "p = q ∧ x = []"
    proof -
      from derives_start1[OF derives] obtain α where d1: "Prods G ⊢ [Nt (List_sym q γ p)] ⇒ α" and 
                                                        ds: "Prods G ⊢ α ⇒* map Tm x"
        using derive_singleton by blast
      from Nil d1 have *: "p = q" and α_def: "α = []"
        using pda_to_cfg_derive_empty by simp_all
      from α_def ds have **: "x = []" by simp
      from * ** show ?thesis by simp
    qed
    with Nil show ?thesis
      by (simp add: steps_refl)
  next
    case (Cons Z α)
    from less(2) have "n > 0"
      using gr0I by fastforce
    then obtain n' where n_def: "n = Suc n'"
      using not0_implies_Suc by blast
    with less(2) obtain γ' where l1: "Prods G ⊢ [Nt (List_sym q γ p)] ⇒l γ'" and ln': "Prods G ⊢ γ' ⇒l(n') map Tm x"
      using relpowp_Suc_E2[of n' "derivel (Prods G)" "[Nt (List_sym q γ p)]" "map Tm x"] by blast
    from Cons obtain q' where γ'_def: "γ' = [Nt (Single_sym q Z q'), Nt (List_sym q' α p)]"
      using pda_to_cfg_derive_split derivel_imp_derive[OF l1] by blast
    with ln' have "n' > 0"
      using gr0I by fastforce
    then obtain n'' where n'_def: "n' = Suc n''"
      using not0_implies_Suc by blast
    with ln' γ'_def obtain γ'' where l2: "Prods G ⊢ [Nt (Single_sym q Z q'), Nt (List_sym q' α p)] ⇒l γ''" and
                                      ln'': "Prods G ⊢ γ'' ⇒l(n'') map Tm x"
      using relpowp_Suc_E2[of n'' "derivel (Prods G)" "[Nt (Single_sym q Z q'), Nt (List_sym q' α p)]" "map Tm x"] by blast
    from l2 obtain γ''⇩2 where l2': "Prods G ⊢ [Nt (Single_sym q Z q')] ⇒l γ''⇩2" and γ''_split: "γ'' = γ''⇩2 @ [Nt (List_sym q' α p)]"
      using derivel_Nt_Cons by (metis append.right_neutral) 
    have "(∃q'' α'' a. (q'', α'') ∈ δ M q a Z ∧ γ''⇩2 = [Tm a, Nt (List_sym q'' α'' q')]) ∨ 
                    (∃q'' α''. (q'', α'') ∈ δε M q Z  ∧ γ''⇩2 = [Nt (List_sym q'' α'' q')])"
      using pda_to_cfg_derive_single derivel_imp_derive[OF l2'] by simp
    with γ''_split have rule: "(∃q'' α'' a. (q'', α'') ∈ δ M q a Z ∧ 
                                  γ'' = [Tm a, Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)]) ∨ 
                            (∃q'' α''. (q'', α'') ∈ δε M q Z  ∧ 
                                  γ'' = [Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)])" (is "?l ∨ ?r") by simp
    show ?thesis proof (rule disjE[OF rule])
      assume ?l
      then obtain q'' α'' a where trans: "(q'', α'') ∈ δ M q a Z" and 
                                     γ''_def: "γ'' = [Tm a, Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)]" by blast
      from γ''_def ln'' obtain x' where x_def: "x = a#x'" and 
                               split: "Prods G ⊢ [Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)] ⇒l(n'') map Tm x'"
        using deriveln_Tm_Cons[of n'' "Prods G" a "[Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)]" "map Tm x"] by auto
      obtain w⇩1 w⇩2 m⇩1 m⇩2 where m1_m2_n''': "m⇩1 + m⇩2 = n''" and x'_def: "x' = w⇩1 @ w⇩2" 
                                    and m1_path: "Prods G ⊢ [Nt (List_sym q'' α'' q')] ⇒l(m⇩1) map Tm w⇩1" 
                                    and m2_path: "Prods G ⊢ [Nt (List_sym q' α p)] ⇒l(m⇩2) map Tm w⇩2" 
        using split_derivel[OF split] by blast
      from m1_m2_n''' n_def n'_def have m1_lessn: "m⇩1 < n" by simp
      from m1_m2_n''' n_def n'_def have m2_lessn: "m⇩2 < n" by simp

      from trans x_def Cons have "(q, x, γ) ↝ (q'', x', α'' @ α)"
        using step⇩1_rule by simp

      moreover from x'_def have "(q'', x', α'' @ α) ↝* (q', w⇩2, α)"
        using steps_stack_app[OF less(1)[OF m1_lessn m1_path], of α] 
              steps_word_app[of q'' w⇩1 "α'' @ α" q' "[]" α w⇩2] by simp

      moreover have "(q', w⇩2, α) ↝* (p, [], [])"
        using less(1)[OF m2_lessn m2_path] .

      ultimately show ?thesis
        unfolding steps_def
        by (meson converse_rtranclp_into_rtranclp rtranclp_trans)
    next
      assume ?r
      then obtain q'' α'' where eps: "(q'', α'') ∈ δε M q Z" and  
                                  γ''_def: "γ'' = [Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)]" by blast
      from γ''_def ln'' have split: "Prods G ⊢ [Nt (List_sym q'' α'' q'), Nt (List_sym q' α p)] ⇒l(n'') map Tm x" by simp
      obtain w⇩1 w⇩2 m⇩1 m⇩2 where m1_m2_n''': "m⇩1 + m⇩2 = n''" and x_def: "x = w⇩1 @ w⇩2" 
                             and m1_path: "Prods G ⊢ [Nt (List_sym q'' α'' q')] ⇒l(m⇩1) map Tm w⇩1" 
                             and m2_path: "Prods G ⊢ [Nt (List_sym q' α p)] ⇒l(m⇩2) map Tm w⇩2"
        using split_derivel[OF split] by blast
      from m1_m2_n''' n_def n'_def have m1_lessn: "m⇩1 < n" by simp
      from m1_m2_n''' n_def n'_def have m2_lessn: "m⇩2 < n" by simp

      from eps Cons have "(q, x, γ) ↝ (q'', x, α'' @ α)"
        using step⇩1_rule by simp

      moreover from x_def have "(q'', x, α'' @ α) ↝* (q', w⇩2, α)"
        using steps_stack_app[OF less(1)[OF m1_lessn m1_path], of α] 
              steps_word_app[of q'' w⇩1 "α'' @ α" q' "[]" α w⇩2] by simp

      moreover have "(q', w⇩2, α) ↝* (p, [], [])"
        using less(1)[OF m2_lessn m2_path] .

      ultimately show ?thesis
        using step⇩1_steps steps_trans by metis
    qed
  qed
qed

lemma pda_to_cfg: "LangS G = accept_stack" (is "?L = ?P")
proof
  show "?L ⊆ ?P"
  proof
    fix x
    assume "x ∈ ?L"
    hence derives: "Prods G ⊢ [Nt Start_sym] ⇒* map Tm x"
      by (simp add: G_def Lang_def)
    then obtain γ where fs: "Prods G ⊢ [Nt Start_sym] ⇒ γ" and ls: "Prods G ⊢ γ ⇒* map Tm x"
      using converse_rtranclpE[OF derives] by blast
    from fs obtain q where "γ = [Nt (List_sym (init_state M) [init_symbol M] q)]"
      using pda_to_cfg_derive_start[of γ] by blast
    with ls obtain n where "Prods G ⊢ [Nt (List_sym (init_state M) [init_symbol M] q)] ⇒l(n) map Tm x"
      using derivels_iff_derives[of "Prods G" γ x] rtranclp_power[of "derivel (Prods G)" γ "map Tm x"] by blast
    hence "steps (init_state M, x, [init_symbol M]) (q, [], [])"
      using pda_to_cfg_steps_if_derivel by simp
    thus "x ∈ ?P"
      by (auto simp: accept_stack_def)
  qed
next
  show "?P ⊆ ?L"
  proof
    fix x
    assume "x ∈ ?P"
    then obtain q where "steps (init_state M, x, [init_symbol M]) (q, [], [])"
      by (auto simp: accept_stack_def)
    then obtain n where "(init_state M, x, [init_symbol M]) ↝(n) (q, [], [])"
      using stepn_steps by blast

    hence "Prods G ⊢ [Nt (List_sym (init_state M) [init_symbol M] q)] ⇒* map Tm x"
      using pda_to_cfg_derives_if_stepn by simp

    moreover have "Prods G ⊢ [Nt Start_sym] ⇒ [Nt (List_sym (init_state M) [init_symbol M] q)]"
      using pda_to_cfg_derive_start by simp

    ultimately have "Prods G ⊢ [Nt (Start G)] ⇒* map Tm x"
      by (simp add: G_def)

    thus "x ∈ ?L"
      by (simp add: Lang_def)
  qed
qed

end
end