Theory Context_Free_Grammar

(*
Authors: Tobias Nipkow, Akihisa Yamada
*)

section "Context-Free Grammars"

theory Context_Free_Grammar
imports "HOL-Library.Infinite_Typeclass"
begin

(* TODO: make function fresh executable *)
definition fresh :: "('n::infinite) set ⇒ 'n" where
"fresh A = (SOME x. x ∉ A)"

lemma fresh_finite: "finite A ⟹ fresh A ∉ A"
unfolding fresh_def by (metis arb_element someI)

declare relpowp.simps(2)[simp del]

lemma bex_pair_conv: "(∃(x,y) ∈ R. P x y) ⟷ (∃x y. (x,y) ∈ R ∧ P x y)"
  by auto

lemma in_image_map_prod: "fgp ∈ map_prod f g ` R ⟷ (∃(x,y)∈R. fgp = (f x,g y))"
  by auto


subsection "Symbols and Context-Free Grammars"

text ‹Most of the theory is based on arbitrary sets of productions.
Finiteness of the set of productions is only required where necessary.
Finiteness of the type of terminal symbols is only required where necessary.
Whenever fresh nonterminals need to be invented, the type of nonterminals is assumed to be infinite.›

datatype ('n,'t) sym = Nt 'n | Tm 't

type_synonym ('n,'t) syms = "('n,'t) sym list"

type_synonym ('n,'t) prod = "'n × ('n,'t) syms"

type_synonym ('n,'t) prods = "('n,'t) prod list"
type_synonym ('n,'t) Prods = "('n,'t) prod set"

datatype ('n,'t) cfg = cfg (prods : "('n,'t) prods") (start : "'n")
datatype ('n,'t) Cfg = Cfg (Prods : "('n,'t) Prods") (Start : "'n")

definition isTm :: "('n, 't) sym ⇒ bool" where 
"isTm S = (∃a. S = Tm a)"

definition isNt :: "('n, 't) sym ⇒ bool" where 
"isNt S = (∃A. S = Nt A)"

fun destTm :: "('n, 't) sym  ⇒ 't" where 
‹destTm (Tm a) = a›

lemma isTm_simps[simp]:
  ‹isTm (Nt A) = False›
  ‹isTm (Tm a)› 
by (simp_all add: isTm_def)

lemma filter_isTm_map_Tm[simp]: ‹filter isTm (map Tm xs) = map Tm xs›
by(induction xs) auto

lemma destTm_o_Tm[simp]: ‹destTm ∘ Tm = id›
by auto

definition nts_syms :: "('n,'t)syms ⇒ 'n set" where
"nts_syms w = {A. Nt A ∈ set w}"

definition tms_syms :: "('n,'t)syms ⇒ 't set" where
"tms_syms w = {a. Tm a ∈ set w}"

definition Nts :: "('n,'t)Prods ⇒ 'n set" where
  "Nts P = (⋃(A,w)∈P. {A} ∪ nts_syms w)"

definition Tms :: "('n,'t)Prods ⇒ 't set" where 
  "Tms P = (⋃(A,w)∈P. tms_syms w)"

abbreviation nts :: "('n,'t) prods ⇒ 'n set" where
  "nts P ≡ Nts (set P)"

definition Syms :: "('n,'t)Prods ⇒ ('n,'t) sym set" where 
  "Syms P = (⋃(A,w)∈P. {Nt A} ∪ set w)"

abbreviation tms :: "('n,'t) prods ⇒ 't set" where
  "tms P ≡ Tms (set P)"

abbreviation syms :: "('n,'t) prods ⇒ ('n,'t) sym set" where
  "syms P ≡ Syms (set P)"

definition Lhss :: "('n, 't) Prods ⇒ 'n set" where
"Lhss P = (⋃(A,w) ∈ P. {A})"

abbreviation lhss :: "('n, 't) prods ⇒ 'n set" where
"lhss ps ≡ Lhss(set ps)"

definition Rhs_Nts :: "('n, 't) Prods ⇒ 'n set" where
"Rhs_Nts P = (⋃(_,w)∈P. nts_syms w)"

definition Rhss :: "('n × 'a) set ⇒ 'n ⇒ 'a set" where
"Rhss P A = {w. (A,w) ∈ P}"

lemma inj_Nt: "inj Nt"
by (simp add: inj_def)

lemma map_Tm_inject_iff[simp]: "map Tm xs = map Tm ys ⟷ xs = ys"
by (metis sym.inject(2) list.inj_map_strong)

lemma map_Nt_eq_map_Nt_iff[simp]: "map Nt u = map Nt v ⟷ u = v"
by(rule inj_map_eq_map[OF inj_Nt])

lemma map_Nt_eq_map_Tm_iff[simp]: "map Nt u = map Tm v ⟷ u = [] ∧ v = []"
by (cases u) auto

lemmas map_Tm_eq_map_Nt_iff[simp] = eq_iff_swap[OF map_Nt_eq_map_Tm_iff]

lemma nts_syms_Nil[simp]: "nts_syms [] = {}"
unfolding nts_syms_def by auto

lemma nts_syms_Cons[simp]: "nts_syms (a#v) = (case a of Nt A ⇒ {A} | _ ⇒ {}) ∪ nts_syms v"
by (auto simp: nts_syms_def split: sym.split)

lemma nts_syms_append[simp]: "nts_syms (u @ v) = nts_syms u ∪ nts_syms v"
by (auto simp: nts_syms_def)

lemma nts_syms_map_Nt[simp]: "nts_syms (map Nt w) = set w"
unfolding nts_syms_def by auto

lemma nts_syms_map_Tm[simp]: "nts_syms (map Tm w) = {}"
unfolding nts_syms_def by auto

lemma in_Nts_iff_in_Syms: "B ∈ Nts P ⟷ Nt B ∈ Syms P"
unfolding Nts_def Syms_def nts_syms_def by (auto)

lemma Nts_Un: "Nts (P1 ∪ P2) = Nts P1 ∪ Nts P2"
by (simp add: Nts_def)

lemma Nts_Lhss_Rhs_Nts: "Nts P = Lhss P ∪ Rhs_Nts P"
unfolding Nts_def Lhss_def Rhs_Nts_def by auto

lemma Nts_nts_syms: "w ∈ Rhss P A ⟹ nts_syms w ⊆ Nts P"
unfolding Rhss_def Nts_def by blast

lemma Syms_simps[simp]:
  "Syms {} = {}"
  "Syms(insert (A,w) P) = {Nt A} ∪ set w ∪ Syms P"
  "Syms(P ∪ P') = Syms P ∪ Syms P'"
by(auto simp: Syms_def)

lemma Lhss_simps[simp]:
  "Lhss {} = {}"
  "Lhss(insert (A,w) P) = {A} ∪ Lhss P"
  "Lhss(P ∪ P') = Lhss P ∪ Lhss P'"
by(auto simp: Lhss_def)


subsubsection ‹Finiteness Lemmas›

lemma finite_nts_syms: "finite (nts_syms w)"
proof -
  have "Nt ` {A. Nt A ∈ set w} ⊆ set w" by auto
  from finite_inverse_image[OF _ inj_Nt]
  show ?thesis unfolding nts_syms_def using finite_inverse_image[OF _ inj_Nt] by auto
qed

lemma finite_nts: "finite(nts ps)"
unfolding Nts_def by (simp add: finite_nts_syms split_def)

lemma fresh_nts: "fresh(nts ps) ∉ nts ps"
by(fact fresh_finite[OF finite_nts])

lemma finite_nts_prods_start: "finite(nts(prods g) ∪ {start g})"
unfolding Nts_def by (simp add: finite_nts_syms split_def)

lemma fresh_nts_prods_start: "fresh(nts(prods g) ∪ {start g}) ∉ nts(prods g) ∪ {start g}"
by(fact fresh_finite[OF finite_nts_prods_start])

lemma finite_Nts: "finite P ⟹ finite (Nts P)"
unfolding Nts_def by (simp add: case_prod_beta finite_nts_syms)

lemma finite_Rhss: "finite P ⟹ finite (Rhss P A)"
unfolding Rhss_def by (metis Image_singleton finite_Image)


subsection "Derivations"

subsubsection ‹The standard derivations ‹⇒›, ‹⇒*›, ‹⇒(n)››

inductive derive :: "('n,'t) Prods ⇒ ('n,'t) syms ⇒ ('n,'t)syms ⇒ bool"
  ("(2_ ⊢/ (_ ⇒/ _))" [50, 0, 50] 50) where
"(A,α) ∈ P ⟹ P ⊢ u @ [Nt A] @ v ⇒ u @ α @ v"

abbreviation deriven ("(2_ ⊢/ (_ /⇒'(_')/ _))" [50, 0, 0, 50] 50) where
"P ⊢ u ⇒(n) v ≡ (derive P ^^ n) u v"

abbreviation derives ("(2_ ⊢/ (_/ ⇒*/ _))" [50, 0, 50] 50) where
"P ⊢ u ⇒* v ≡ ((derive P) ^**) u v"

definition Ders :: "('n,'t)Prods ⇒ 'n ⇒ ('n,'t)syms set" where
"Ders P A = {w. P ⊢ [Nt A] ⇒* w}"

abbreviation ders :: "('n,'t)prods ⇒ 'n ⇒ ('n,'t)syms set" where
"ders ps ≡ Ders (set ps)"

lemma DersI:
  assumes "P ⊢ [Nt A] ⇒* w" shows "w ∈ Ders P A"
  using assms by (auto simp: Ders_def)

lemma DersD:
  assumes "w ∈ Ders P A" shows "P ⊢ [Nt A] ⇒* w"
  using assms by (auto simp: Ders_def)

lemmas DersE = DersD[elim_format]

definition Lang :: "('n,'t)Prods ⇒ 'n ⇒ 't list set" where
"Lang P A = {w. P ⊢ [Nt A] ⇒* map Tm w}"

abbreviation lang :: "('n,'t)prods ⇒ 'n ⇒ 't list set" where
"lang ps A ≡ Lang (set ps) A"

abbreviation LangS :: "('n,'t) Cfg ⇒ 't list set" where
"LangS G ≡ Lang (Prods G) (Start G)"

abbreviation langS :: "('n,'t) cfg ⇒ 't list set" where
"langS g ≡ lang (prods g) (start g)"

lemma Lang_Ders: "map Tm ` (Lang P A) ⊆ Ders P A"
unfolding Lang_def Ders_def by auto

lemma Lang_eqI_derives:
  assumes "⋀v. R ⊢ [Nt A] ⇒* map Tm v ⟷ S ⊢ [Nt A] ⇒* map Tm v"
  shows "Lang R A = Lang S A"
  by (auto simp: Lang_def assms)

lemma derive_iff: "R ⊢ u ⇒ v ⟷ (∃ (A,w) ∈ R. ∃u1 u2. u = u1 @ Nt A # u2 ∧ v = u1 @ w @ u2)"
  apply (rule iffI)
   apply (induction rule: derive.induct)
   apply (fastforce)
  using derive.intros by fastforce 

lemma not_derive_from_Tms: "¬ P ⊢ map Tm as ⇒ w"
by(auto simp add: derive_iff map_eq_append_conv)

lemma deriven_from_TmsD: "P ⊢ map Tm as ⇒(n) w ⟹ w = map Tm as"
by (metis not_derive_from_Tms relpowp_E2)
 
lemma derives_from_Tms_iff: "P ⊢ map Tm as ⇒* w ⟷ w = map Tm as"
by (meson deriven_from_TmsD rtranclp.rtrancl_refl rtranclp_power)

lemma Un_derive: "R ∪ S ⊢ y ⇒ z ⟷ R ⊢ y ⇒ z ∨ S ⊢ y ⇒ z"
  by (fastforce simp: derive_iff)

lemma derives_rule:
  assumes 2: "(A,w) ∈ R" and 1: "R ⊢ x ⇒* y @ Nt A # z" and 3: "R ⊢ y@w@z ⇒* v"
  shows "R ⊢ x ⇒* v"
proof-
  note 1
  also have "R ⊢ y @ Nt A # z ⇒ y @ w @ z"
    using derive.intros[OF 2] by simp
  also note 3
  finally show ?thesis.
qed

lemma derives_Cons_rule:
  assumes 1: "(A,w) ∈ R" and 2: "R ⊢ w @ u ⇒* v" shows "R ⊢ Nt A # u ⇒* v"
  using derives_rule[OF 1, of "Nt A # u" "[]" u v] 2 by auto

lemma deriven_mono: "P ⊆ P' ⟹ P ⊢ u ⇒(n) v ⟹ P' ⊢ u ⇒(n) v"
by (metis Un_derive relpowp_mono subset_Un_eq)

lemma derives_mono: "P ⊆ P' ⟹ P ⊢ u ⇒* v ⟹ P' ⊢ u ⇒* v"
by (meson deriven_mono rtranclp_power)

lemma Lang_mono: "P ⊆ P' ⟹ Lang P A ⊆ Lang P' A"
by (auto simp: Lang_def derives_mono)


subsubsection "Customized Induction Principles"

lemma deriven_induct[consumes 1, case_names 0 Suc]:
  assumes "P ⊢ xs ⇒(n) ys"
  and "Q 0 xs"
  and "⋀n u A v w. ⟦ P ⊢ xs ⇒(n) u @ [Nt A] @ v; Q n (u @ [Nt A] @ v); (A,w) ∈ P ⟧ ⟹ Q (Suc n) (u @ w @ v)"
  shows "Q n ys"
using assms(1) proof (induction n arbitrary: ys)
  case 0
  thus ?case using assms(2) by auto
next
  case (Suc n)
  from relpowp_Suc_E[OF Suc.prems]
  obtain xs' where n: "P ⊢ xs ⇒(n) xs'" and 1: "P ⊢ xs' ⇒ ys" by auto
  from derive.cases[OF 1] obtain u A v w where "xs' = u @ [Nt A] @ v" "(A,w) ∈ P" "ys = u @ w @ v"
    by metis
  with Suc.IH[OF n] assms(3) n
  show ?case by blast
qed

lemma derives_induct[consumes 1, case_names base step]:
  assumes "P ⊢ xs ⇒* ys"
  and "Q xs"
  and "⋀u A v w. ⟦ P ⊢ xs ⇒* u @ [Nt A] @ v; Q (u @ [Nt A] @ v); (A,w) ∈ P ⟧ ⟹ Q (u @ w @ v)"
  shows "Q ys"
using assms
proof (induction rule: rtranclp_induct)
  case base
  from this(1) show ?case .
next
  case step
  from derive.cases[OF step(2)] step(1,3-) show ?case by metis
qed

lemma converse_derives_induct[consumes 1, case_names base step]:
  assumes "P ⊢ xs ⇒* ys"
  and Base: "Q ys"
  and Step: "⋀u A v w. ⟦ P ⊢ u @ [Nt A] @ v ⇒* ys; Q (u @ w @ v); (A,w) ∈ P ⟧ ⟹ Q (u @ [Nt A] @ v)"
  shows "Q xs"
  using assms(1)
  apply (induction rule: converse_rtranclp_induct)
  by (auto elim!: derive.cases intro!: Base Step intro: derives_rule)


subsubsection "(De)composing derivations"

lemma derive_append:
  "𝒢 ⊢ u ⇒ v ⟹ 𝒢 ⊢ u@w ⇒ v@w"
apply(erule derive.cases)
using derive.intros by fastforce

lemma derive_prepend:
  "𝒢 ⊢ u ⇒ v ⟹ 𝒢 ⊢ w@u ⇒ w@v"
apply(erule derive.cases)
by (metis append.assoc derive.intros)

lemma deriven_append:
  "P ⊢ u ⇒(n) v ⟹ P ⊢ u @ w ⇒(n) v @ w"
  apply (induction n arbitrary: v)
   apply simp
  using derive_append by (fastforce simp: relpowp_Suc_right)

lemma deriven_prepend:
  "P ⊢ u ⇒(n) v ⟹ P ⊢ w @ u ⇒(n) w @ v"
  apply (induction n arbitrary: v)
   apply simp
  using derive_prepend by (fastforce simp: relpowp_Suc_right)

lemma derives_append:
  "P ⊢ u ⇒* v ⟹ P ⊢ u@w ⇒* v@w"
  by (metis deriven_append rtranclp_power)

lemma derives_prepend:
  "P ⊢ u ⇒* v ⟹ P ⊢ w@u ⇒* w@v"
  by (metis deriven_prepend rtranclp_power)

lemma derive_append_decomp:
  "P ⊢ u@v ⇒ w ⟷
  (∃u'. w = u'@v ∧ P ⊢ u ⇒ u') ∨ (∃v'. w = u@v' ∧ P ⊢ v ⇒ v')"
(is "?l ⟷ ?r")
proof
  assume ?l
  then obtain A r u1 u2
    where Ar: "(A,r) ∈ P"
      and uv: "u@v = u1 @ Nt A # u2"
      and w: "w = u1 @ r @ u2"
    by (auto simp: derive_iff)
  from uv have "(∃s. u2 = s @ v ∧ u = u1 @ Nt A # s) ∨
  (∃s. u1 = u@s ∧ v = s @ Nt A # u2)"
    by (auto simp: append_eq_append_conv2 append_eq_Cons_conv)
  with Ar w show "?r" by (fastforce simp: derive_iff)
next
  show "?r ⟹ ?l"
    by (auto simp add: derive_append derive_prepend)
qed

lemma deriven_append_decomp:
  "P ⊢ u @ v ⇒(n) w ⟷
  (∃n1 n2 w1 w2. n = n1 + n2 ∧ w = w1 @ w2 ∧ P ⊢ u ⇒(n1) w1 ∧ P ⊢ v ⇒(n2) w2)"
  (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
  proof (induction n arbitrary: u v)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    from Suc.prems
    obtain u' v'
      where or: "P ⊢ u ⇒ u' ∧ v' = v ∨ u' = u ∧ P ⊢ v ⇒ v'"
        and n: "P ⊢ u'@v' ⇒(n) w"
      by (fastforce simp: relpowp_Suc_left derive_append_decomp)
    from Suc.IH[OF n] or
    show ?case
      apply (elim disjE)
       apply (metis add_Suc relpowp_Suc_I2)
      by (metis add_Suc_right relpowp_Suc_I2)
  qed
next
  assume ?r
  then obtain n1 n2 w1 w2
    where [simp]: "n = n1 + n2" "w = w1 @ w2"
      and u: "P ⊢ u ⇒(n1) w1" and v: "P ⊢ v ⇒(n2) w2"
    by auto
  from u deriven_append
  have "P ⊢ u @ v ⇒(n1) w1 @ v" by fastforce
  also from v deriven_prepend
  have "P ⊢ w1 @ v ⇒(n2) w1 @ w2" by fastforce
  finally show ?l by auto
qed

lemma derives_append_decomp:
  "P ⊢ u @ v ⇒* w ⟷ (∃u' v'. P ⊢ u ⇒* u' ∧ P ⊢ v ⇒* v' ∧ w = u' @ v')"
  by (auto simp: rtranclp_power deriven_append_decomp)

lemma derives_concat:
  "∀i ∈ set is. P ⊢ f i ⇒* g i ⟹ P ⊢ concat(map f is) ⇒* concat(map g is)"
proof(induction "is")
  case Nil
  then show ?case by auto
next
  case Cons
  thus ?case by(auto simp: derives_append_decomp less_Suc_eq)
qed

lemma derives_concat1:
  "∀i ∈ set is. P ⊢ [f i] ⇒* g i ⟹ P ⊢ map f is ⇒* concat(map g is)"
using derives_concat[where f = "λi. [f i]"] by auto

lemma derive_Cons:
"P ⊢ u ⇒ v ⟹ P ⊢ a#u ⇒ a#v"
  using derive_prepend[of P u v "[a]"] by auto

lemma derives_Cons:
"R ⊢ u ⇒* v ⟹ R ⊢ a#u ⇒* a#v"
  using derives_prepend[of _ _ _ "[a]"] by simp

lemma derive_from_empty[simp]:
  "P ⊢ [] ⇒ w ⟷ False"
  by (auto simp: derive_iff)

lemma deriven_from_empty[simp]:
  "P ⊢ [] ⇒(n) w ⟷ n = 0 ∧ w = []"
  by (induct n, auto simp: relpowp_Suc_left)

lemma derives_from_empty[simp]:
  "𝒢 ⊢ [] ⇒* w ⟷ w = []"
  by (auto elim: converse_rtranclpE)

lemma deriven_start1:
  assumes "P ⊢ [Nt A] ⇒(n) map Tm w"
  shows "∃α m. n = Suc m ∧ P ⊢ α ⇒(m) (map Tm w) ∧ (A,α) ∈ P"
proof (cases n)
  case 0
  thus ?thesis
    using assms by auto
next
  case (Suc m)
  then obtain α where *: "P ⊢ [Nt A] ⇒ α" "P ⊢ α ⇒(m) map Tm w"
    using assms by (meson relpowp_Suc_E2)
  from  derive.cases[OF *(1)] have "(A, α) ∈ P"
    by (simp add: Cons_eq_append_conv) blast
  thus ?thesis using *(2) Suc by auto
qed

lemma derives_start1: "P ⊢ [Nt A] ⇒* map Tm w  ⟹  ∃α. P ⊢ α ⇒* map Tm w ∧ (A,α) ∈ P"
using deriven_start1 by (metis rtranclp_power)

lemma Lang_empty_if_notin_Lhss: "A ∉ Lhss P ⟹ Lang P A = {}"
unfolding Lhss_def Lang_def
using derives_start1 by fastforce

lemma derive_Tm_Cons:
  "P ⊢ Tm a # u ⇒ v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒ w)"
  by (fastforce simp: derive_iff Cons_eq_append_conv)

lemma deriven_Tm_Cons:
  "P ⊢ Tm a # u ⇒(n) v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒(n) w)"
proof (induction n arbitrary: u)
  case 0
  show ?case by auto
next
  case (Suc n)
  then show ?case by (force simp: derive_Tm_Cons relpowp_Suc_left OO_def)
qed

lemma derives_Tm_Cons:
  "P ⊢ Tm a # u ⇒* v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒* w)"
  by (metis deriven_Tm_Cons rtranclp_power)

lemma derives_Tm[simp]: "P ⊢ [Tm a] ⇒* w ⟷ w = [Tm a]"
by(simp add: derives_Tm_Cons)

lemma derive_singleton: "P ⊢ [a] ⇒ u ⟷ (∃A. (A,u) ∈ P ∧ a = Nt A)"
  by (auto simp: derive_iff Cons_eq_append_conv)

lemma deriven_singleton: "P ⊢ [a] ⇒(n) u ⟷ (
  case n of 0 ⇒ u = [a]
   | Suc m ⇒ ∃(A,w) ∈ P. a = Nt A ∧ P ⊢ w ⇒(m) u)"
  (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
  proof (induction n)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    then show ?case
      by (smt (verit, ccfv_threshold) case_prod_conv derive_singleton nat.simps(5) relpowp_Suc_E2)
  qed
  show "?r ⟹ ?l"
    by (auto simp: derive_singleton relpowp_Suc_I2 split: nat.splits)
qed

lemma deriven_Cons_decomp:
  "P ⊢ a # u ⇒(n) v ⟷
  (∃v2. v = a#v2 ∧ P ⊢ u ⇒(n) v2) ∨
  (∃n1 n2 A w v1 v2. n = Suc (n1 + n2) ∧ v = v1 @ v2 ∧ a = Nt A ∧
   (A,w) ∈ P ∧ P ⊢ w ⇒(n1) v1 ∧ P ⊢ u ⇒(n2) v2)"
(is "?l = ?r")
proof
  assume ?l
  then obtain n1 n2 v1 v2
    where [simp]: "n = n1 + n2" "v = v1 @ v2"
      and 1: "P ⊢ [a] ⇒(n1) v1" and 2: "P ⊢ u ⇒(n2) v2"
    unfolding deriven_append_decomp[of n P "[a]" u v,simplified]
    by auto
  show ?r
  proof (cases "n1")
    case 0
    with 1 2 show ?thesis by auto
  next
    case [simp]: (Suc m)
    with 1 obtain A w
      where [simp]: "a = Nt A" "(A,w) ∈ P" and w: "P ⊢ w ⇒(m) v1"
      by (auto simp: deriven_singleton)
    with 2
    have "n = Suc (m + n2) ∧ v = v1 @ v2 ∧ a = Nt A ∧
   (A,w) ∈ P ∧ P ⊢ w ⇒(m) v1 ∧ P ⊢ u ⇒(n2) v2"
      by auto
    then show ?thesis
      by (auto simp: append_eq_Cons_conv)
  qed
next
  assume "?r"
  then
  show "?l"
  proof (elim disjE exE conjE)
    fix v2
    assume [simp]: "v = a # v2" and u: "P ⊢ u ⇒(n) v2"
    from deriven_prepend[OF u, of "[a]"]
    show ?thesis
      by auto
  next
    fix n1 n2 A w v1 v2
    assume [simp]: "n = Suc (n1 + n2)" "v = v1 @ v2" "a = Nt A"
      and Aw: "(A, w) ∈ P"
      and w: "P ⊢ w ⇒(n1) v1"
      and u: "P ⊢ u ⇒(n2) v2"
    have "P ⊢ [a] ⇒ w"
      by (simp add: Aw derive_singleton)
    with w have "P ⊢ [a] ⇒(Suc n1) v1"
      by (metis relpowp_Suc_I2)
    from deriven_append[OF this]
    have 1: "P ⊢ a#u ⇒(Suc n1) v1@u"
      by auto
    also have "P ⊢ … ⇒(n2) v1@v2"
      using deriven_prepend[OF u].
    finally
    show ?thesis by simp
  qed
qed

lemma derives_Cons_decomp:
  "P ⊢ s # u ⇒* v ⟷
  (∃v2. v = s#v2 ∧ P ⊢ u ⇒* v2) ∨
  (∃A w v1 v2. v = v1 @ v2 ∧ s = Nt A ∧ (A,w) ∈ P ∧ P ⊢ w ⇒* v1 ∧ P ⊢ u ⇒* v2)" (is "?L ⟷ ?R")
proof
  assume ?L thus ?R using deriven_Cons_decomp[of _ P s u v] by (metis rtranclp_power)
next
  assume ?R thus ?L by (meson derives_Cons derives_Cons_rule derives_append_decomp)
qed

lemma deriven_Suc_decomp_left:
  "P ⊢ u ⇒(Suc n) v ⟷ (∃p A u2 w v1 v2 n1 n2.
  u = p @ Nt A # u2 ∧ v = p @ v1 @ v2 ∧ n = n1 + n2 ∧
  (A,w) ∈ P ∧ P ⊢ w ⇒(n1) v1 ∧
  P ⊢ u2 ⇒(n2) v2)" (is "?l ⟷ ?r")
proof
  show "?r ⟹ ?l"
    by (auto intro!: deriven_prepend simp: deriven_Cons_decomp)
  show "?l ⟹ ?r"
  proof(induction u arbitrary: v n)
    case Nil
    then show ?case by auto
  next
    case (Cons a u)
    from Cons.prems[unfolded deriven_Cons_decomp]
    show ?case
    proof (elim disjE exE conjE, goal_cases)
      case (1 v2)
      with Cons.IH[OF this(2)] show ?thesis
        by (metis append_Cons)
    next
      case (2 n1 n2 A w v1 v2)
      then show ?thesis by (fastforce simp:Cons_eq_append_conv)
    qed
  qed
qed

lemma derives_NilD: "P ⊢ w ⇒* [] ⟹ s ∈ set w ⟹ P ⊢ [s] ⇒* []"
proof(induction arbitrary: s rule: converse_derives_induct)
  case base
  then show ?case by simp
next
  case (step u A v w)
  then show ?case using derives_append_decomp[where u="[Nt A]" and v=v]
    by (auto simp: derives_append_decomp)
qed

lemma derive_decomp_Tm: "P ⊢ α ⇒(n) map Tm β ⟹
  ∃βs ns. β = concat βs ∧ length α = length βs ∧ length α = length ns ∧ sum_list ns = n
          ∧ (∀i < length βs. P ⊢ [α ! i] ⇒(ns!i) map Tm (βs ! i))"
  (is "_ ⟹ ∃βs ns. ?G α β n βs ns")
proof (induction α arbitrary: β n)
  case (Cons s α)
  from deriven_Cons_decomp[THEN iffD1, OF Cons.prems]
  show ?case
  proof (elim disjE exE conjE)
    fix γ assume as: "map Tm β = s # γ" "P ⊢ α ⇒(n) γ"
    then obtain s' γ' where "β = s' # γ'"  "P ⊢ α ⇒(n) map Tm γ'" "s = Tm s'" by force
    from Cons.IH[OF this(2)] obtain βs ns where *: "?G α γ' n βs ns"
      by blast
    let ?βs = "[s']#βs"
    let ?ns = "0#ns"
    have "?G (s#α) β n ?βs ?ns"
      using ‹β = _› as * by (auto simp: nth_Cons')
    then show ?thesis by blast
  next
    fix n1 n2 A w β1 β2
    assume *: "n = Suc (n1 + n2)" "map Tm β = β1 @ β2" "s = Nt A" "(A, w) ∈ P" "P ⊢ w ⇒(n1) β1" "P ⊢ α ⇒(n2) β2"
    then obtain β1' β2' where **: "β = β1' @ β2'" "P ⊢ w ⇒(n1) map Tm β1'" "P ⊢ α ⇒(n2) map Tm β2'"
      by (metis (no_types, lifting) append_eq_map_conv)
    from Cons.IH[OF this(3)] obtain βs ns
      where ***: "?G α β2' n2 βs ns"
      by blast
    let ?βs = "β1'#βs"
    let ?ns = "Suc n1 # ns"
    from * ** have "P ⊢ [(s#α) ! 0] ⇒(?ns ! 0) map Tm (?βs ! 0)"
      by (metis derive_singleton nth_Cons_0 relpowp_Suc_I2)
    then have "?G (s#α) β n ?βs ?ns"
      using * ** *** by (auto simp add: nth_Cons' derives_Cons_rule fold_plus_sum_list_rev)
    then show ?thesis by blast
  qed
qed simp

lemma derives_simul_rules:
  assumes "⋀A w. (A,w) ∈ P ⟹ P' ⊢ [Nt A] ⇒* w"
  shows "P ⊢ w ⇒* w' ⟹ P' ⊢ w ⇒* w'"
proof(induction rule: derives_induct)
  case base
  then show ?case by simp
next
  case (step u A v w)
  then show ?case
    by (meson assms derives_append derives_prepend rtranclp_trans)
qed

lemma derives_set_subset:
  "P ⊢ u ⇒* v ⟹ set v ⊆ set u ∪ Syms P"
proof (induction rule: derives_induct)
  case base
  then show ?case by simp
next
  case (step u A v w)
  then show ?case unfolding Syms_def by (auto)
qed

lemma derives_nts_syms_subset:
  "P ⊢ u ⇒* v ⟹ nts_syms v ⊆ nts_syms u ∪ Nts P"
proof (induction rule: derives_induct)
  case base
  then show ?case by simp
next
  case (step u A v w)
  then show ?case unfolding Nts_def nts_syms_def by (auto)
qed


text ‹Bottom-up definition of ‹⇒*›. Single definition yields more compact inductions.
But ‹derives_induct› may already do the job.›

inductive derives_bu :: "('n, 't) Prods ⇒ ('n,'t) syms ⇒ ('n,'t) syms ⇒ bool"
  ("(2_ ⊢/ (_/ ⇒bu/ _))" [50, 0, 50] 50) for P :: "('n, 't) Prods"
  where
bu_refl: "P ⊢ α ⇒bu α" |
bu_prod: "(A,α) ∈ P ⟹ P ⊢ [Nt A] ⇒bu α" |
bu_embed: "⟦ P ⊢ α ⇒bu α⇩1 @ α⇩2 @ α⇩3; P ⊢ α⇩2 ⇒bu β ⟧ ⟹ P ⊢ α ⇒bu α⇩1 @ β @ α⇩3"

lemma derives_if_bu: "P ⊢ α ⇒bu β ⟹ P ⊢ α ⇒* β"
proof(induction rule: derives_bu.induct)
  case (bu_refl) then show ?case by simp
next
  case (bu_prod A α) then show ?case by (simp add: derives_Cons_rule)
next
  case (bu_embed α α⇩1 α⇩2 α⇩3 β) then show ?case
    by (meson derives_append derives_prepend rtranclp_trans)
qed

lemma derives_bu_if: "P ⊢ α ⇒* β ⟹ P ⊢ α ⇒bu β"
proof(induction rule: derives_induct)
  case base
  then show ?case by (simp add: bu_refl)
next
  case (step u A v w)
  then show ?case
    by (meson bu_embed bu_prod)
qed

lemma derives_bu_iff: "P ⊢ α ⇒bu β ⟷ P ⊢ α ⇒* β"
by (meson derives_bu_if derives_if_bu)


subsubsection "Leftmost/Rightmost Derivations"

inductive derivel :: "('n,'t) Prods ⇒ ('n,'t) syms ⇒ ('n,'t)syms ⇒ bool"
  ("(2_ ⊢/ (_ ⇒l/ _))" [50, 0, 50] 50) where
"(A,α) ∈ P ⟹ P ⊢ map Tm u @ Nt A # v ⇒l map Tm u @ α @ v"

abbreviation derivels ("(2_ ⊢/ (_ ⇒l*/ _))" [50, 0, 50] 50) where
"P ⊢ u ⇒l* v ≡ ((derivel P) ^**) u v"

abbreviation derivels1 ("(2_ ⊢/ (_ ⇒l+/ _))" [50, 0, 50] 50) where
"P ⊢ u ⇒l+ v ≡ ((derivel P) ^++) u v"

abbreviation deriveln ("(2_ ⊢/ (_ ⇒l'(_')/ _))" [50, 0, 0, 50] 50) where
"P ⊢ u ⇒l(n) v ≡ ((derivel P) ^^ n) u v"

inductive deriver :: "('n,'t) Prods ⇒ ('n,'t) syms ⇒ ('n,'t)syms ⇒ bool"
  ("(2_ ⊢/ (_ ⇒r/ _))" [50, 0, 50] 50) where
"(A,α) ∈ P ⟹ P ⊢ u @ Nt A # map Tm v ⇒r u @ α @ map Tm v"

abbreviation derivers ("(2_ ⊢/ (_ ⇒r*/ _))" [50, 0, 50] 50) where
"P ⊢ u ⇒r* v ≡ ((deriver P) ^**) u v"

abbreviation derivers1 ("(2_ ⊢/ (_ ⇒r+/ _))" [50, 0, 50] 50) where
"P ⊢ u ⇒r+ v ≡ ((deriver P) ^++) u v"

abbreviation derivern ("(2_ ⊢/ (_ ⇒r'(_')/ _))" [50, 0, 0, 50] 50) where
"P ⊢ u ⇒r(n) v ≡ ((deriver P) ^^ n) u v"


lemma derivel_iff: "R ⊢ u ⇒l v ⟷
 (∃ (A,w) ∈ R. ∃u1 u2. u = map Tm u1 @ Nt A # u2 ∧ v = map Tm u1 @ w @ u2)"
  by (auto simp: derivel.simps)

lemma derivel_from_empty[simp]:
  "P ⊢ [] ⇒l w ⟷ False" by (auto simp: derivel_iff)

lemma deriveln_from_empty[simp]:
  "P ⊢ [] ⇒l(n) w ⟷ n = 0 ∧ w = []"
  by (induct n, auto simp: relpowp_Suc_left)

lemma derivels_from_empty[simp]:
  "𝒢 ⊢ [] ⇒l* w ⟷ w = []"
  by (auto elim: converse_rtranclpE)

lemma Un_derivel: "R ∪ S ⊢ y ⇒l z ⟷ R ⊢ y ⇒l z ∨ S ⊢ y ⇒l z"
  by (fastforce simp: derivel_iff)

lemma derivel_append:
  "P ⊢ u ⇒l v ⟹ P ⊢ u @ w ⇒l v @ w"
  by (force simp: derivel_iff)

lemma deriveln_append:
  "P ⊢ u ⇒l(n) v ⟹ P ⊢ u @ w ⇒l(n) v @ w"
proof (induction n arbitrary: u)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then obtain y where uy: "P ⊢ u ⇒l y" and yv: "P ⊢ y ⇒l(n) v"
    by (auto simp: relpowp_Suc_left)
  have "P ⊢ u @ w ⇒l y @ w"
    using derivel_append[OF uy].
  also from Suc.IH yv have "P ⊢ … ⇒l(n) v @ w" by auto
  finally show ?case.
qed

lemma derivels_append:
  "P ⊢ u ⇒l* v ⟹ P ⊢ u @ w ⇒l* v @ w"
  by (metis deriveln_append rtranclp_power)

lemma derivels1_append:
  "P ⊢ u ⇒l+ v ⟹ P ⊢ u @ w ⇒l+ v @ w"
  by (metis deriveln_append tranclp_power)

lemma derivel_Tm_Cons:
  "P ⊢ Tm a # u ⇒l v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒l w)"
apply (cases v)
 apply (simp add: derivel_iff)
apply (fastforce simp: derivel.simps Cons_eq_append_conv Cons_eq_map_conv)
done

lemma deriveln_Tm_Cons:
  "P ⊢ Tm a # u ⇒l(n) v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒l(n) w)"
  by (induction n arbitrary: u v;
      fastforce simp: derivel_Tm_Cons relpowp_Suc_right OO_def)

lemma derivels_Tm_Cons:
  "P ⊢ Tm a # u ⇒l* v ⟷ (∃w. v = Tm a # w ∧ P ⊢ u ⇒l* w)"
  by (metis deriveln_Tm_Cons rtranclp_power)

lemma derivel_Nt_Cons:
  "P ⊢ Nt A # u ⇒l v ⟷ (∃w. (A,w) ∈ P ∧ v = w @ u)"
  by (auto simp: derivel_iff Cons_eq_append_conv Cons_eq_map_conv)

lemma derivels1_Nt_Cons:
  "P ⊢ Nt A # u ⇒l+ v ⟷ (∃w. (A,w) ∈ P ∧ P ⊢ w @ u ⇒l* v)"
  by (auto simp: tranclp_unfold_left derivel_Nt_Cons OO_def)

lemma derivels_Nt_Cons:
  "P ⊢ Nt A # u ⇒l* v ⟷ v = Nt A # u ∨ (∃w. (A,w) ∈ P ∧ P ⊢ w @ u ⇒l* v)"
  by (auto simp: Nitpick.rtranclp_unfold derivels1_Nt_Cons)

lemma deriveln_Nt_Cons:
  "P ⊢ Nt A # u ⇒l(n) v ⟷ (
  case n of 0 ⇒ v = Nt A # u
  | Suc m ⇒ ∃w. (A,w) ∈ P ∧ P ⊢ w @ u ⇒l(m) v)"
  by (cases n) (auto simp: derivel_Nt_Cons relpowp_Suc_left OO_def)

lemma derivel_map_Tm_append:
  "P ⊢ map Tm w @ u ⇒l v ⟷ (∃x. v = map Tm w @ x ∧ P ⊢ u ⇒l x)"
  apply (induction w arbitrary:v)
  by (auto simp: derivel_Tm_Cons Cons_eq_append_conv)

lemma deriveln_map_Tm_append:
  "P ⊢ map Tm w @ u ⇒l(n) v ⟷ (∃x. v = map Tm w @ x ∧ P ⊢ u ⇒l(n) x)"
  by (induction n arbitrary: u;
      force simp: derivel_map_Tm_append relpowp_Suc_left OO_def)

lemma derivels_map_Tm_append:
  "P ⊢ map Tm w @ u ⇒l* v ⟷ (∃x. v = map Tm w @ x ∧ P ⊢ u ⇒l* x)"
  by (metis deriveln_map_Tm_append rtranclp_power)

lemma derivel_not_elim_Tm:
  assumes "P ⊢ xs ⇒l map Nt w"
  shows "∃v. xs = map Nt v"
proof -
  from assms obtain A α u xs' where
         A_w: "(A, α)∈P"
      and xs: "xs = map Tm u @ Nt A # xs'"
      and ys: "map Nt w = map Tm u @ α @ xs'"
    unfolding derivel_iff by fast

  from ys have u1: "u = []"
    by (metis Nil_is_append_conv Nil_is_map_conv hd_append list.map_sel(1) sym.simps(4))
  moreover from ys obtain u' where "xs' = map Nt u'"
    by (metis append_eq_map_conv)

  ultimately have "xs = map Nt (A # u')"
    by (simp add: xs)
  then show ?thesis by blast
qed

lemma deriveln_not_elim_Tm:
  assumes "P ⊢ xs ⇒l(n) map Nt w"
  shows "∃v. xs = map Nt v"
using assms
proof (induction n arbitrary: xs)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then obtain z where "P ⊢ xs ⇒l z" and "P ⊢ z ⇒l(n) map Nt w"
    using relpowp_Suc_E2 by metis
  with Suc show ?case using derivel_not_elim_Tm
    by blast
qed

lemma decomp_derivel_map_Nts:
  assumes "P ⊢ map Nt Xs ⇒l map Nt Zs"
  shows "∃X Xs' Ys. Xs = X # Xs' ∧ P ⊢ [Nt X] ⇒l map Nt Ys ∧ Zs = Ys @ Xs'"
using assms unfolding derivel_iff
by (fastforce simp: map_eq_append_conv split: prod.splits)

lemma derivel_imp_derive: "P ⊢ u ⇒l v ⟹ P ⊢ u ⇒ v"
  using derive.simps derivel.cases self_append_conv2 by fastforce

lemma deriveln_imp_deriven:
  "P ⊢ u ⇒l(n) v ⟹ P ⊢ u ⇒(n) v"
  using relpowp_mono derivel_imp_derive by metis

lemma derivels_imp_derives:
  "P ⊢ u ⇒l* v ⟹ P ⊢ u ⇒* v"
  by (metis derivel_imp_derive mono_rtranclp)

lemma deriveln_iff_deriven:
  "P ⊢ u ⇒l(n) map Tm v ⟷ P ⊢ u ⇒(n) map Tm v"
  (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r" using deriveln_imp_deriven.
  assume ?r
  then show "?l"
  proof (induction n arbitrary: u v rule: less_induct)
    case (less n)
    from ‹P ⊢ u ⇒(n) map Tm v›
    show ?case
    proof (induction u arbitrary: v)
      case Nil
      then show ?case by simp
    next
      case (Cons a u)
      show ?case
        using Cons.prems(1) Cons.IH less.IH
        by (auto simp: deriven_Cons_decomp deriveln_Tm_Cons deriveln_Nt_Cons)
           (metis deriven_append_decomp lessI)
    qed
  qed
qed

lemma derivels_iff_derives: "P ⊢ u ⇒l* map Tm v ⟷ P ⊢ u ⇒* map Tm v"
  using deriveln_iff_deriven
  by (metis rtranclp_power)

lemma deriver_iff: "R ⊢ u ⇒r v ⟷
  (∃ (A,w) ∈ R. ∃u1 u2. u = u1 @ Nt A # map Tm u2 ∧ v = u1 @ w @ map Tm u2)"
  by (auto simp: deriver.simps)

lemma deriver_imp_derive: "R ⊢ u ⇒r v ⟹ R ⊢ u ⇒ v"
  by (auto simp: deriver_iff derive_iff)

lemma derivern_imp_deriven: "R ⊢ u ⇒r(n) v ⟹ R ⊢ u ⇒(n) v"
  by (metis (no_types, lifting) deriver_imp_derive relpowp_mono)

lemma derivers_imp_derives: "R ⊢ u ⇒r* v ⟹ R ⊢ u ⇒* v"
  by (metis deriver_imp_derive mono_rtranclp)

lemma deriver_iff_rev_derivel:
  "P ⊢ u ⇒r v ⟷ map_prod id rev ` P ⊢ rev u ⇒l rev v" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain A w u1 u2 where Aw: "(A,w) ∈ P"
    and u: "u = u1 @ Nt A # map Tm u2"
    and v: "v = u1 @ w @ map Tm u2" by (auto simp: deriver.simps)
  from bexI[OF _ Aw] have "(A, rev w) ∈ map_prod id rev ` P" by (auto simp: image_def)
  from derivel.intros[OF this, of "rev u2" "rev u1"] u v
  show ?r by (simp add: rev_map)
next
  assume ?r
  then obtain A w u1 u2 where Aw: "(A,w) ∈ P"
    and u: "u = u1 @ Nt A # map Tm u2"
    and v: "v = u1 @ w @ map Tm u2"
    by (auto simp: derivel_iff rev_eq_append_conv rev_map)
  then show ?l by (auto simp: deriver_iff)
qed

lemma rev_deriver_iff_derivel:
  "map_prod id rev ` P ⊢ u ⇒r v ⟷ P ⊢ rev u ⇒l rev v"
  by (simp add: deriver_iff_rev_derivel image_image prod.map_comp o_def)

lemma derivern_iff_rev_deriveln:
  "P ⊢ u ⇒r(n) v ⟷ map_prod id rev ` P ⊢ rev u ⇒l(n) rev v"
proof (induction n arbitrary: u)
  case 0
  show ?case by simp
next
  case (Suc n)
  show ?case
    apply (unfold relpowp_Suc_left OO_def)
    apply (unfold Suc deriver_iff_rev_derivel)
    by (metis rev_rev_ident)
qed

lemma rev_derivern_iff_deriveln:
  "map_prod id rev ` P ⊢ u ⇒r(n) v ⟷ P ⊢ rev u ⇒l(n) rev v"
  by (simp add: derivern_iff_rev_deriveln image_image prod.map_comp o_def)

lemma derivers_iff_rev_derivels:
  "P ⊢ u ⇒r* v ⟷ map_prod id rev ` P ⊢ rev u ⇒l* rev v"
  using derivern_iff_rev_deriveln
  by (metis rtranclp_power)

lemma rev_derivers_iff_derivels:
  "map_prod id rev ` P ⊢ u ⇒r* v ⟷ P ⊢ rev u ⇒l* rev v"
  by (simp add: derivers_iff_rev_derivels image_image prod.map_comp o_def)

lemma rev_derive:
  "map_prod id rev ` P ⊢ u ⇒ v ⟷ P ⊢ rev u ⇒ rev v"
  by (force simp: derive_iff rev_eq_append_conv bex_pair_conv in_image_map_prod intro: exI[of _ "rev _"])

lemma rev_deriven:
  "map_prod id rev ` P ⊢ u ⇒(n) v ⟷ P ⊢ rev u ⇒(n) rev v"
apply (induction n arbitrary: u)
 apply simp
by (auto simp: relpowp_Suc_left OO_def rev_derive intro: exI[of _ "rev _"])

lemma rev_derives:
  "map_prod id rev ` P ⊢ u ⇒* v ⟷ P ⊢ rev u ⇒* rev v"
  using rev_deriven
  by (metis rtranclp_power)

lemma derivern_iff_deriven: "P ⊢ u ⇒r(n) map Tm v ⟷ P ⊢ u ⇒(n) map Tm v"
  by (auto simp: derivern_iff_rev_deriveln rev_map deriveln_iff_deriven rev_deriven)

lemma derivers_iff_derives: "P ⊢ u ⇒r* map Tm v ⟷ P ⊢ u ⇒* map Tm v"
  by (simp add: derivern_iff_deriven rtranclp_power)

lemma deriver_append_map_Tm:
  "P ⊢ u @ map Tm w ⇒r v ⟷ (∃x. v = x @ map Tm w ∧ P ⊢ u ⇒r x)"
  by (fastforce simp: deriver_iff_rev_derivel rev_map derivel_map_Tm_append rev_eq_append_conv)

lemma derivern_append_map_Tm:
  "P ⊢ u @ map Tm w ⇒r(n) v ⟷ (∃x. v = x @ map Tm w ∧ P ⊢ u ⇒r(n) x)"
  by (fastforce simp: derivern_iff_rev_deriveln rev_map deriveln_map_Tm_append rev_eq_append_conv)

lemma deriver_snoc_Nt:
  "P ⊢ u @ [Nt A] ⇒r v ⟷ (∃w. (A,w) ∈ P ∧ v = u @ w)"
  by (force simp: deriver_iff_rev_derivel derivel_Nt_Cons rev_eq_append_conv)

lemma deriver_singleton:
  "P ⊢ [Nt A] ⇒r v ⟷ (A,v) ∈ P"
  using deriver_snoc_Nt[of P "[]"] by auto

lemma derivers1_snoc_Nt:
  "P ⊢ u @ [Nt A] ⇒r+ v ⟷ (∃w. (A,w) ∈ P ∧ P ⊢ u @ w ⇒r* v)"
  by (auto simp: tranclp_unfold_left deriver_snoc_Nt OO_def)

lemma derivers_snoc_Nt:
  "P ⊢ u @ [Nt A] ⇒r* v ⟷ v = u @ [Nt A] ∨ (∃w. (A,w) ∈ P ∧ P ⊢ u @ w ⇒r* v)"
  by (auto simp: Nitpick.rtranclp_unfold derivers1_snoc_Nt)

lemma derivern_snoc_Tm:
  "P ⊢ u @ [Tm a] ⇒r(n) v ⟷ (∃w. v = w @ [Tm a] ∧ P ⊢ u ⇒r(n) w)"
  by (force simp: derivern_iff_rev_deriveln deriveln_Tm_Cons)

lemma derivern_snoc_Nt:
  "P ⊢ u @ [Nt A] ⇒r(n) v ⟷ (
  case n of 0 ⇒ v = u @ [Nt A]
  | Suc m ⇒ ∃w. (A,w) ∈ P ∧ P ⊢ u @ w ⇒r(m) v)"
  by (cases n) (auto simp: relpowp_Suc_left deriver_snoc_Nt OO_def)

lemma derivern_singleton:
  "P ⊢ [Nt A] ⇒r(n) v ⟷ (
  case n of 0 ⇒ v = [Nt A]
  | Suc m ⇒ ∃w. (A,w) ∈ P ∧ P ⊢ w ⇒r(m) v)"
  using derivern_snoc_Nt[of n P "[]" A v] by (cases n, auto)


subsection ‹Substitution in Lists›

text ‹Function ‹substs y ys xs› replaces every occurrence of ‹y› in ‹xs› with the list ‹ys››

fun substs :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"substs y ys [] = []" |
"substs y ys (x#xs) = (if x = y then ys @ substs y ys xs else x # substs y ys xs)"

text ‹Alternative definition, but apparently no simpler to use:
@{prop "substs y ys xs = concat (map (λx. if x=y then ys else [x]) xs)"}›

abbreviation "substsNt A ≡ substs (Nt A)"

lemma substs_append[simp]: "substs y ys (xs @ xs') = substs y ys xs @ substs y ys xs'"
by (induction xs) auto

lemma substs_skip: "y ∉ set xs ⟹ substs y ys xs = xs"
by (induction xs) auto

lemma susbstsNT_map_Tm[simp]: "substsNt A α (map Tm w) = map Tm w"
by(rule substs_skip) auto

lemma substs_len: "length (substs y [y'] xs) = length xs"
by (induction xs) auto

lemma substs_rev: "y' ∉ set xs ⟹ substs y' [y] (substs y [y'] xs) = xs"
by (induction xs) auto

lemma substs_der:
  "(B,v) ∈ P ⟹ P ⊢ u ⇒* substs (Nt B) v u"
proof (induction u)
  case Nil
  then show ?case by simp
next
  case (Cons a u)
  then show ?case
    by (auto simp add: derives_Cons_rule derives_prepend derives_Cons)
qed


subsection ‹Epsilon-Freeness›

definition Eps_free where "Eps_free R = (∀(_,r) ∈ R. r ≠ [])"

abbreviation "eps_free rs == Eps_free(set rs)"

lemma Eps_freeI:
  assumes "⋀A r. (A,r) ∈ R ⟹ r ≠ []" shows "Eps_free R"
  using assms by (auto simp: Eps_free_def)

lemma Eps_free_Nil: "Eps_free R ⟹ (A,[]) ∉ R"
  by (auto simp: Eps_free_def)

lemma Eps_freeE_Cons: "Eps_free R ⟹ (A,w) ∈ R ⟹ ∃a u. w = a#u"
  by (cases w, auto simp: Eps_free_def)

lemma Eps_free_derives_Nil:
  assumes R: "Eps_free R" shows "R ⊢ l ⇒* [] ⟷ l = []" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
  proof (induction rule: converse_derives_induct)
    case base
    show ?case by simp
  next
    case (step u A v w)
    then show ?case by (auto simp: Eps_free_Nil[OF R])
  qed
qed auto

lemma Eps_free_derivels_Nil: "Eps_free R ⟹ R ⊢ l ⇒l* [] ⟷ l = []"
by (meson Eps_free_derives_Nil derivels_from_empty derivels_imp_derives)

lemma Eps_free_deriveln_Nil: "Eps_free R ⟹ R ⊢ l ⇒l(n) [] ⟹ l = []"
by (metis Eps_free_derivels_Nil relpowp_imp_rtranclp)

lemma decomp_deriveln_map_Nts:
  assumes "Eps_free P"
  shows "P ⊢ Nt X # map Nt Xs ⇒l(n) map Nt Zs ⟹
     ∃Ys'. Ys' @ Xs = Zs ∧ P ⊢ [Nt X] ⇒l(n) map Nt Ys'"
proof (induction n arbitrary: Zs)
  case 0
  then show ?case
    by (auto)
next
  case (Suc n)
  then obtain ys where n: "P ⊢ Nt X # map Nt Xs ⇒l(n) ys" and "P ⊢ ys ⇒l map Nt Zs"
    using relpowp_Suc_E by metis
  from ‹P ⊢ ys ⇒l map Nt Zs› obtain Ys where "ys = map Nt Ys"
    using derivel_not_elim_Tm by blast
  from Suc.IH[of Ys] this n
  obtain Ys' where "Ys = Ys' @ Xs ∧ P ⊢ [Nt X] ⇒l(n) map Nt Ys'" by auto
  moreover from ‹ys = _› ‹P ⊢ ys ⇒l map Nt Zs› decomp_derivel_map_Nts[of P Ys Zs]
  obtain Y Xs' Ysa where "Ys = Y # Xs' ∧ P ⊢ [Nt Y] ⇒l map Nt Ysa ∧ Zs = Ysa @ Xs'" by auto
  ultimately show ?case using Eps_free_deriveln_Nil[OF assms, of n "[Nt X]"]
    by (auto simp: Cons_eq_append_conv derivel_Nt_Cons relpowp_Suc_I)
qed

end