Theory Context_Free_Grammar

(*
Authors: Tobias Nipkow, Akihisa Yamada
*)

section "Context-Free Grammars"

theory Context_Free_Grammar
imports
  "Fresh_Identifiers.Fresh_Nat"
  "Regular-Sets.Regular_Set"
begin

lemma append_Cons_eq_append_Cons:
  "y' ∉ set xs ⟹ y ∉ set xs' ⟹
   xs @ y # zs = xs' @ y' # zs' ⟷ xs = xs' ∧ y = y' ∧ zs = zs'"
  by (induction xs arbitrary: xs'; force simp: Cons_eq_append_conv)

lemma insert_conc: "insert w W @@ V = {w @ v | v. v ∈ V} ∪ W @@ V"
  by auto

lemma conc_insert: "W @@ insert v V = {w @ v | w. w ∈ W} ∪ W @@ V"
  by auto

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 isNt_simps[simp,code]:
  ‹isNt (Nt A) = True›
  ‹isNt (Tm a) = False› 
by (simp_all add: isNt_def)

lemma isTm_simps[simp,code]:
  ‹isTm (Nt A) = False›
  ‹isTm (Tm a) = True› 
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)"

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

lemma Tms_mono: "P ⊆ P' ⟹ Tms P ⊆ Tms P'"
unfolding Tms_def Tms_syms_def by blast

definition nts_syms_acc :: "('n,'t)syms ⇒ 'n list ⇒ 'n list" where
"nts_syms_acc = foldr (λsy ns. case sy of Nt A ⇒ List.insert A ns | Tm _ ⇒ ns)"

definition nts_syms :: "('n,'t)syms ⇒ 'n list" where
"nts_syms sys = nts_syms_acc sys []"

definition nts :: "('n,'t)prods ⇒ 'n list" where
"nts ps = foldr (λ(A,sys) ns. List.insert A (nts_syms_acc sys ns)) ps []"

definition tms_syms_acc :: "('n,'t)syms ⇒ 't list ⇒ 't list" where
"tms_syms_acc = foldr (λsy ts. case sy of Tm a ⇒ List.insert a ts | Nt _ ⇒ ts)"

definition tms_syms :: "('n,'t)syms ⇒ 't list" where
"tms_syms sys = tms_syms_acc sys []"

definition tms :: "('n,'t)prods ⇒ 't list" where
"tms ps = foldr (λ(_,sys). tms_syms_acc sys) ps []"

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 Rhss_code[code]: "Rhss P A = snd ` {Aw ∈ P. fst Aw = A}"
by(auto simp add: Rhss_def image_iff)

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,code]: "Nts_syms [] = {}"
unfolding Nts_syms_def by auto

lemma Nts_syms_Cons[simp,code]: "Nts_syms (s#ss) = (case s of Nt A ⇒ {A} | _ ⇒ {}) ∪ Nts_syms ss"
by (auto simp: Nts_syms_def split: sym.split)

lemma Tms_syms_Nil[simp,code]: "Tms_syms [] = {}"
unfolding Tms_syms_def by auto

lemma Tms_syms_Cons[simp,code]: "Tms_syms (s#ss) = (case s of Tm a ⇒ {a} | _ ⇒ {}) ∪ Tms_syms ss"
by (auto simp: Tms_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 Tms_syms_append[simp]: "Tms_syms (u @ v) = Tms_syms u ∪ Tms_syms v"
by (auto simp: Tms_syms_def)

lemma Nts_syms_map_Nt[simp]: "Nts_syms (map Nt w) = set w"
unfolding Nts_syms_def by auto

lemma Tms_syms_map_Tm[simp]: "Tms_syms (map Tm w) = set w"
unfolding Tms_syms_def by auto

lemma Nts_syms_map_Tm[simp]: "Nts_syms (map Tm w) = {}"
unfolding Nts_syms_def by auto

lemma Tms_syms_map_Nt[simp]: "Tms_syms (map Nt w) = {}"
unfolding Tms_syms_def by auto

lemma Nts_syms_rev: "Nts_syms (rev w) = Nts_syms w"
by(auto simp: Nts_syms_def)

lemma Tms_syms_rev: "Tms_syms (rev w) = Tms_syms w"
by(auto simp: Tms_syms_def)

lemma Nts_syms_empty_iff: "Nts_syms w = {} ⟷ (∃u. w = map Tm u)"
by(induction w) (auto simp: ex_map_conv split: sym.split)

lemma Tms_syms_empty_iff: "Tms_syms w = {} ⟷ (∃u. w = map Nt u)"
by(induction w) (auto simp: ex_map_conv split: sym.split)

text ‹If a sentential form contains a ‹Nt›, it must have a last and a first ‹Nt›:›

lemma non_word_has_last_Nt: "Nts_syms w ≠ {} ⟹ ∃u A v. w = u @ [Nt A] @ map Tm v"
proof (induction w)
  case Nil
  then show ?case by simp
next
  case (Cons a list)
  then show ?case using Nts_syms_empty_iff[of list]
    by(auto simp: Cons_eq_append_conv split: sym.splits)
qed

lemma non_word_has_first_Nt: "Nts_syms w ≠ {} ⟹ ∃u A v. w = map Tm u @ Nt A # v"
  using Nts_syms_rev non_word_has_last_Nt[of "rev w"]
  by (metis append.assoc append_Cons append_Nil rev.simps(2) rev_eq_append_conv rev_map)

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_mono: "G ⊆ H ⟹ Nts G ⊆ Nts H"
by (auto simp add: Nts_def)

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

lemma Rhs_Nts_Un: "Rhs_Nts (P ∪ Q) = Rhs_Nts P ∪ Rhs_Nts Q"
  by (simp add: Rhs_Nts_def)

lemma Rhss_Un: "Rhss (P ∪ Q) A = Rhss P A ∪ Rhss Q A"
  by (auto simp: Rhss_def)

lemma Rhss_UN: "Rhss (⋃PP) A = ⋃{Rhss P A | P. P ∈ PP}"
  by (auto simp: Rhss_def)

lemma Rhss_empty[simp]: "Rhss {} A = {}"
  by (auto simp: Rhss_def)

lemma Rhss_insert: "Rhss (insert (A,α) P) B = (if A = B then insert α (Rhss P B) else Rhss P B)"
  by (auto simp: Rhss_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)

lemma in_LhssI: "(A,α) ∈ P ⟹ A ∈ Lhss P"
by (auto simp: Lhss_def)

lemma Lhss_Collect: "Lhss {p. X p} = {A. ∃α. X (A,α)}"
  by (auto simp: Lhss_def)

lemma in_Rhs_NtsI: "(A,α) ∈ P ⟹ B ∈ Nts_syms α ⟹ B ∈ Rhs_Nts P"
by (auto simp: Rhs_Nts_def)

lemma set_nts_syms: "set(nts_syms_acc sys ns) = Nts_syms sys ∪ set ns"
unfolding nts_syms_acc_def
by(induction sys arbitrary: ns) (auto split: sym.split)

lemma set_nts: "set(nts ps) = Nts (set ps)"
by(induction ps) (auto simp: nts_def Nts_def set_nts_syms split: prod.splits)

lemma distinct_nts_syms_acc: "distinct(nts_syms_acc sys ns) = distinct ns"
unfolding nts_syms_acc_def
by(induction sys arbitrary: ns) (auto split: sym.split)

lemma distinct_nts_syms: "distinct(nts_syms sys)"
unfolding nts_syms_def by(simp add: distinct_nts_syms_acc)

lemma distinct_nts: "distinct(nts ps)"
by(induction ps) (auto simp: nts_def distinct_nts_syms_acc distinct_nts_syms)

lemma set_tms_syms_acc: "set(tms_syms_acc sys ts) = Tms_syms sys ∪ set ts"
unfolding tms_syms_acc_def
by(induction sys arbitrary: ts) (auto split: sym.split)

corollary set_tms_syms: "set(tms_syms sys) = Tms_syms sys"
unfolding tms_syms_def Tms_syms_def set_tms_syms_acc Tms_syms_def by (auto)

lemma set_tms: "set(tms ps) = Tms (set ps)"
by(induction ps) (auto simp: tms_def Tms_def set_tms_syms_acc split: prod.splits)

lemma distinct_tms_syms_acc: "distinct(tms_syms_acc sys ts) = distinct ts"
unfolding tms_syms_acc_def
by(induction sys arbitrary: ts) (auto split: sym.split)

lemma distinct_tms_syms: "distinct(tms_syms sys)"
unfolding tms_syms_def by(simp add: distinct_tms_syms_acc)

lemma distinct_tms: "distinct(tms ps)"
by(induction ps) (auto simp: tms_def distinct_tms_syms_acc split: sym.split)


subsubsection ‹Finiteness Lemmas›

lemma finite_Nts_syms: "finite (Nts_syms w)"
by (induction w) (auto split: sym.split)

lemma finite_Tms_syms: "finite (Tms_syms w)"
by (induction w) (auto split: sym.split)

lemma finite_nts: "finite(Nts (set ps))"
unfolding Nts_def by (simp add: finite_Nts_syms split_def)

lemma finite_tms: "finite(Tms (set ps))"
unfolding Tms_def by (simp add: finite_Tms_syms split_def)

lemma fresh0_nts: "fresh0(Nts (set ps)) ∉ Nts (set ps)"
by(fact fresh0_notIn[OF finite_nts])

lemma finite_nts_prods_start: "finite(Nts(set(prods g)) ∪ {start g})"
unfolding Nts_def by (simp add: finite_Nts_syms split_def)

lemma fresh_nts_prods_start: "fresh0(Nts(set(prods g)) ∪ {start g}) ∉ Nts(set(prods g)) ∪ {start g}"
by(fact fresh0_notIn[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_Tms: "finite P ⟹ finite (Tms P)"
unfolding Tms_def by (simp add: case_prod_beta finite_Tms_syms)

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


subsection "Derivations and Languages"

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

inductive derive :: "('n,'t) Prods ⇒ ('n,'t) syms ⇒ ('n,'t)syms ⇒ bool"
  ("(2_ ⊢/ (_ ⇒/ _))" [50, 0, 50] 50) for P 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]

text ‹The \emph{language} of a nonterminal is the set of the terminal words it derives.›

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)"

text ‹Language is extended over mixed words.›

definition Lang_of :: "('n,'t) Prods ⇒ ('n,'t) syms ⇒ 't list set" where
"Lang_of P α = {w. P ⊢ α ⇒* map Tm w}"

abbreviation Lang_of_set :: "('n,'t) Prods ⇒ ('n,'t) syms set ⇒ 't list set" where
"Lang_of_set P X ≡ ⋃(Lang_of P ` X)"

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

lemma Lang_subset_if_Ders_subset: "Ders R A ⊆ Ders R' A ⟹ Lang R A ⊆ Lang R' A"
by (auto simp add: Lang_def Ders_def)

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)

lemma Lang_of_mono: "P ⊆ P' ⟹ Lang_of P w ⊆ Lang_of P' w"
  using derives_mono by (auto simp: Lang_of_def)

lemma derive_set_subset:
  "P ⊢ u ⇒ v ⟹ set v ⊆ set u ∪ Syms P"
by (auto simp: derive_iff Syms_def)

lemma deriven_set_subset:
  "P ⊢ u ⇒(n) v ⟹ set v ⊆ set u ∪ Syms P"
  by (induction n arbitrary: u)
    (auto simp: relpowp_Suc_left dest!: derive_set_subset)

lemma derives_set_subset:
  "P ⊢ u ⇒* v ⟹ set v ⊆ set u ∪ Syms P"
  by (auto simp: rtranclp_power dest!: deriven_set_subset)

lemma derive_Nts_syms_subset:
  "P ⊢ u ⇒ v ⟹ Nts_syms v ⊆ Nts_syms u ∪ Rhs_Nts P"
by(auto simp: Rhs_Nts_def derive_iff)

lemma deriven_Nts_syms_subset:
  "P ⊢ u ⇒(n) v ⟹ Nts_syms v ⊆ Nts_syms u ∪ Rhs_Nts P"
  by (induction n arbitrary: u)
    (auto simp: relpowp_Suc_left dest!: derive_Nts_syms_subset)

lemma derives_Nts_syms_subset:
  "P ⊢ u ⇒* v ⟹ Nts_syms v ⊆ Nts_syms u ∪ Rhs_Nts P"
  by (auto simp: rtranclp_power dest!: deriven_Nts_syms_subset)

lemma derive_Tms_syms_subset:
  "P ⊢ u ⇒ v ⟹ Tms_syms v ⊆ Tms_syms u ∪ Tms P"
by(auto simp: Tms_def derive_iff)

lemma deriven_Tms_syms_subset:
  "P ⊢ u ⇒(n) v ⟹ Tms_syms v ⊆ Tms_syms u ∪ Tms P"
  by (induction n arbitrary: u)
    (auto simp: relpowp_Suc_left dest!: derive_Tms_syms_subset)

lemma derives_Tms_syms_subset:
  "P ⊢ u ⇒* v ⟹ Tms_syms v ⊆ Tms_syms u ∪ Tms P"
  by (auto simp: rtranclp_power dest!: deriven_Tms_syms_subset)


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 notin_Lhss_iff_Rhss: "A ∉ Lhss P ⟷ Rhss P A = {}"
  by (auto simp: Lhss_def Rhss_def)

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 deriven_Tms_prepend: "R ⊢ map Tm t @ u ⇒(n) v ⟹ ∃v1. v = map Tm t @ v1 ∧ R ⊢ u ⇒(n) v1"
  by (induction t arbitrary: v) (auto simp add: deriven_Tm_Cons)  

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 derives_append_append:
  "P ⊢ α ⇒* α' ⟹ P ⊢ β ⇒* β' ⟹ P ⊢ α @ β ⇒* α' @ β'"
  using derives_append_decomp by blast

lemma derives_append_Nt_Cons:
"(B,β) ∈ P ⟹
  P ⊢ α ⇒* α' ⟹ P ⊢ β ⇒* β' ⟹ P ⊢ γ ⇒* γ' ⟹
  P ⊢ α @ Nt B # γ ⇒* α' @ β' @ γ'"
  by (metis derives_Cons_decomp derives_append_decomp)

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

subsubsection ‹Derivations leading to terminal words›

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 word_decomp1: 
  "R ⊢ p @ [Nt A] @ map Tm ts ⇒(n) map Tm q 
  ⟹ ∃pt At w k m. R ⊢ p ⇒(k) map Tm pt ∧ R ⊢ w ⇒(m) map Tm At ∧ (A, w) ∈ R 
      ∧ q = pt @ At @ ts ∧ n = Suc(k + m)"
proof -
  assume assm: "R ⊢ p @ [Nt A] @ map Tm ts ⇒(n) map Tm q"
  then obtain q1 where P: "R ⊢ p@[Nt A] ⇒(n) q1 ∧ map Tm q = q1 @ map Tm ts"
    unfolding deriven_append_decomp
    by (metis add.commute add_0 append.assoc not_derive_from_Tms relpowp_E2)
  then obtain q1t where "q1 = map Tm q1t" "q = q1t @ ts"
    by (metis map_Tm_inject_iff map_eq_append_conv)
  with P obtain pt At w k m where P2: "R ⊢ p ⇒(k) map Tm pt ∧ R ⊢ w ⇒(m) map Tm At ∧ (A, w) ∈ R 
     ∧ q1t = pt @ At ∧ n = Suc(k + m)" 
    by(fastforce simp: deriven_append_decomp map_eq_append_conv dest: deriven_start1)
  then have "q = pt @ At @ ts" using ‹q = _› by simp
  then show ?thesis using P2 by blast
qed

lemma deriven_start_sent: 
  "R ⊢ u @ Nt V # w ⇒(Suc n) map Tm x ⟹ ∃v. (V, v) ∈ R ∧ R ⊢ u @ v @ w ⇒(n) map Tm x"
proof -
  assume assm: "R ⊢ u @ Nt V # w ⇒(Suc n) map Tm x"
  then obtain n1 n2 xu xvw 
    where P1: "Suc n = n1 + n2 ∧ map Tm x = xu @ xvw ∧ R ⊢ u ⇒(n1) xu ∧ R ⊢ Nt V # w ⇒(n2) xvw"
    by (auto simp add: deriven_append_decomp)
  then have t: "∄t. xvw = Nt V # t"
    by (metis append_eq_map_conv map_eq_Cons_D sym.distinct(1))
  then obtain n3 n4 v xv xw 
    where P2: "n2 = Suc (n3 + n4) ∧ xvw = xv @ xw ∧ (V,v) ∈ R ∧ R ⊢ v ⇒(n3) xv ∧ R ⊢ w ⇒(n4) xw"
    using P1 t by (auto simp add: deriven_Cons_decomp)
  then have "R ⊢ v @ w ⇒(n3 + n4) xvw" using P2
    using deriven_append_decomp diff_Suc_1 by blast
  then have "R ⊢ u @ v @ w ⇒(n1 + n3 + n4) map Tm x" using P1 P2 deriven_append_decomp
    using ab_semigroup_add_class.add_ac(1) by blast
  then have "R ⊢ u @ v @ w ⇒(n) map Tm x" using P1 P2
    by (simp add: add.assoc)
  then show ?thesis using P2 by blast
qed

lemma deriven_Nt_Cons_map_Tm: "P ⊢ Nt A # β ⇒(n) map Tm w ⟷
(∃α m l v u. (A,α) ∈ P ∧ P ⊢ α ⇒(m) map Tm v ∧ P ⊢ β ⇒(l) map Tm u ∧
  n = Suc (m + l) ∧ w = v @ u)"
  by (force simp: deriven_Cons_decomp map_eq_append_conv)

lemma deriven_Tm_Cons_map_Tm: "P ⊢ Tm a # β ⇒(n) map Tm w ⟷
(∃v. P ⊢ β ⇒(n) map Tm v ∧ w = a # v)"
  by (auto simp: deriven_Tm_Cons)

lemma deriven_Cons_map_Tm:
  "P ⊢ x # u ⇒(n) map Tm w ⟷
  (∃a v2. x = Tm a ∧ w = a # v2 ∧ P ⊢ u ⇒(n) map Tm v2) ∨
  (∃n1 n2 A α v1 v2. n = Suc (n1 + n2) ∧ w = v1 @ v2 ∧ x = Nt A ∧
   (A,α) ∈ P ∧ P ⊢ α ⇒(n1) map Tm v1 ∧ P ⊢ u ⇒(n2) map Tm v2)"
  apply (cases x)
   apply (force simp: deriven_Nt_Cons_map_Tm)
  by (force simp: deriven_Tm_Cons_map_Tm)

lemma deriven_append_map_Tm: "P ⊢ α @ β ⇒(n) map Tm w ⟷
  (∃m l v u. P ⊢ α ⇒(m) map Tm v ∧ P ⊢ β ⇒(l) map Tm u ∧ n = m + l ∧ w = v @ u)"
proof (induction α arbitrary: β n w)
  case Nil
  show ?case by simp
next
  case (Cons x α)
  show ?case
  proof (cases x)
    case x: (Tm a)
    show ?thesis by (force simp: x deriven_Tm_Cons_map_Tm Cons)
  next
    case x: (Nt A)
    show ?thesis
    proof safe
      assume "P ⊢ (x # α) @ β ⇒(n) map Tm w"
      from this[unfolded x append.simps deriven_Nt_Cons_map_Tm]
      obtain γ m l v u where
        n: "n = Suc (m + l)" and A: "(A,γ) ∈ P" and w: "w = v @ u"
        and γv: "P ⊢ γ ⇒(m) map Tm v" and αβ: "P ⊢ α @ β ⇒(l) map Tm u"
        by auto
      from A γv have Av: "P ⊢ [Nt A] ⇒(Suc m) map Tm v"
        by (simp add: derive_singleton relpowp_Suc_I2)
      from αβ[unfolded Cons]
      obtain k j t s where l: "l = k + j" and u: "u = t @ s"
        and α: "P ⊢ α ⇒(k) map Tm t" and β: "P ⊢ β ⇒(j) map Tm s" by auto
      from Av α have xα: "P ⊢ x # α ⇒(Suc m + k) map Tm (v @ t)"
        by (force simp: x deriven_Nt_Cons_map_Tm simp del: map_append)
      show "∃m l v u.
       P ⊢ x # α ⇒(m) map Tm v ∧
       P ⊢ β ⇒(l) map Tm u ∧ n = m + l ∧
       w = v @ u"
        apply (intro exI conjI)
           apply (fact xα)
          apply (fact β)
        by (auto simp: n l w u)
    next
      fix m l v u
      assume n: "n = m + l" and w: "w = v @ u"
        and xα: "P ⊢ x # α ⇒(m) map Tm v"
        and β: "P ⊢ β ⇒(l) map Tm u"
      from xα[unfolded x deriven_Nt_Cons_map_Tm]
      obtain γ k j t s where
        m: "m = Suc (k + j)" and A: "(A,γ) ∈ P" and v: "v = t @ s"
        and γ: "P ⊢ γ ⇒(k) map Tm t" and α: "P ⊢ α ⇒(j) map Tm s"
        by auto
      show "P ⊢ (x # α) @ β ⇒(m + l) map Tm (v @ u)"
        apply (unfold x append.simps deriven_Nt_Cons_map_Tm)
      proof (intro exI conjI)
        show "m + l = Suc (k + (j + l))" by (simp add: m)
        show "(A,γ) ∈ P" using A.
        show "v @ u = t @ s @ u" by (simp add: v)
        show  "P ⊢ γ ⇒(k) map Tm t" using γ.
        from α β show αβ: "P ⊢ α @ β ⇒(j+l) map Tm (s @ u)"
          by (unfold Cons, auto)
      qed
    qed
  qed
qed

lemma deriven_Nt_map_Tm: "P ⊢ α @ Nt B # γ ⇒(n) map Tm w ⟷
(∃β m l k v u t. (B,β) ∈ P ∧
  P ⊢ α ⇒(m) map Tm v ∧ P ⊢ β ⇒(l) map Tm u ∧ P ⊢ γ ⇒(k) map Tm t ∧
  n = Suc (m + l + k) ∧ w = v @ u @ t)"
  by (force simp: deriven_append_map_Tm deriven_Nt_Cons_map_Tm)

lemma map_Tm_Nt_eq_map_Tm_Nt:
  "map Tm xs @ Nt y # zs = map Tm xs' @ Nt y' # zs' ⟷ xs = xs' ∧ y = y' ∧ zs = zs'"
  apply (subst append_Cons_eq_append_Cons)
  by auto

lemma deriven_Suc_map_Tm_decomp: "P ⊢ α ⇒(Suc n) map Tm w ⟷
(∃v B β γ u t m l. (B,β) ∈ P ∧ P ⊢ β ⇒(m) map Tm u ∧ P ⊢ γ ⇒(l) map Tm t ∧
  n = m + l ∧ α = map Tm v @ Nt B # γ ∧ w = v @ u @ t)"
  by (fastforce simp: deriven_Suc_decomp_left map_eq_append_conv map_Tm_Nt_eq_map_Tm_Nt append_eq_map_conv)

lemma derives_append_map_Tm:
  "P ⊢ α @ β ⇒* map Tm w ⟷
  (∃v u. P ⊢ α ⇒* map Tm v ∧ P ⊢ β ⇒* map Tm u ∧ w = v @ u)"
  by (force simp: rtranclp_power deriven_append_map_Tm)

lemma derives_Nt_map_Tm:
 "P ⊢ α @ Nt B # γ ⇒* map Tm w ⟷
  (∃β v u t. (B,β) ∈ P ∧
    P ⊢ α ⇒* map Tm v ∧ P ⊢ β ⇒* map Tm u ∧ P ⊢ γ ⇒* map Tm t ∧
    w = v @ u @ t)"
  by (force simp: rtranclp_power deriven_Nt_map_Tm)

lemma derives_Nt_Cons_map_Tm:
 "P ⊢ Nt A # β ⇒* map Tm w ⟷
  (∃α v u. (A,α) ∈ P ∧ P ⊢ α ⇒* map Tm v ∧ P ⊢ β ⇒* map Tm u ∧ w = v @ u)"
  using derives_Nt_map_Tm[where α = "[]"] by simp

lemma derives_Nt_Cons_Lang:
"P ⊢ Nt A # α ⇒* map Tm w ⟷ (∃v u. v ∈ Lang P A ∧ P ⊢ α ⇒* map Tm u ∧ w = v @ u)"
  by (force simp: derives_Cons_decomp Lang_def map_eq_Cons_conv map_eq_append_conv)

lemma Lang_of_Nil[simp]: "Lang_of P [] = {[]}"
  by (auto simp: Lang_of_def)

lemma Lang_of_iff_derives: "w ∈ Lang_of P α ⟷ P ⊢ α ⇒* map Tm w"
  by (auto simp: Lang_of_def)

lemma Lang_ofE_deriven:
  assumes "w ∈ Lang_of P α" and "⋀n. P ⊢ α ⇒(n) map Tm w ⟹ thesis"
  shows thesis
  using assms by (auto simp: Lang_of_iff_derives rtranclp_power)

lemma Lang_of_Tm_Cons: "Lang_of P (Tm a # α) = {[a]} @@ Lang_of P α"
  by (auto simp: Lang_of_def derives_Tm_Cons conc_def)

lemma Lang_of_map_Tm: "Lang_of P (map Tm w) = {w}"
  by (induction w, simp_all add: Lang_of_Tm_Cons insert_conc)

lemma Lang_of_Nt_Cons: "Lang_of P (Nt A # α) = Lang P A @@ Lang_of P α"
  by (force simp add: Lang_of_def Lang_def derives_Cons_decomp map_eq_append_conv conc_def)

lemma Lang_of_Cons: "Lang_of P (x # α) = (case x of Tm a ⇒ {[a]} | Nt A ⇒ Lang P A) @@ Lang_of P α"
  by (simp add: Lang_of_Tm_Cons Lang_of_Nt_Cons split: sym.splits)

lemma Lang_of_append: "Lang_of P (α @ β) = Lang_of P α @@ Lang_of P β"
  by (induction α arbitrary: β, simp_all add: Lang_of_Cons conc_assoc split: sym.splits)

lemma Lang_of_set_conc: "Lang_of_set P (X @@ Y) = Lang_of_set P X @@ Lang_of_set P Y"
  by (force simp: Lang_of_append elim!: concE)

lemma Lang_of_set_Rhss: "Lang_of_set P (Rhss P A) = Lang P A"
  by (auto simp: Lang_def Lang_of_def Rhss_def converse_rtranclp_into_rtranclp derive_singleton
      dest: derives_start1)

lemma Lang_of_prod_subset: "(A,α) ∈ P ⟹ Lang_of P α ⊆ Lang P A"
  apply (fold Lang_of_set_Rhss) by (auto simp: Rhss_def)

lemma Lang_le_iff_Lang_of_le: "Lang P ≤ Lang P' ⟷ Lang_of P ≤ Lang_of P'"
proof (safe intro!: le_funI)
  fix α w
  assume le: "Lang P ≤ Lang P'" and w: "w ∈ Lang_of P α"
  from w show "w ∈ Lang_of P' α"
    apply (induction α arbitrary: w)
    using le[THEN le_funD, THEN subsetD]
    by (auto simp: Lang_of_Cons insert_conc split: sym.splits)
next
  fix A w
  assume le: "Lang_of P ≤ Lang_of P'" and w: "w ∈ Lang P A"
  from le[THEN le_funD, of "[Nt A]"] w
  show "w ∈ Lang P' A" by (auto simp: Lang_of_Cons)
qed

lemma Lang_eq_iff_Lang_of_eq: "Lang P = Lang P' ⟷ Lang_of P = Lang_of P'"
  apply (subst eq_iff) by (auto simp: Lang_le_iff_Lang_of_le)

lemma Lang_of_le_iff_derives:
  "Lang_of P ≤ Lang_of P' ⟷ (∀α w. P ⊢ α ⇒* map Tm w ⟶ P' ⊢ α ⇒* map Tm w)"
  by (auto simp: Lang_of_def le_fun_def)

lemma Lang_le_iff_derives:
  "Lang P ≤ Lang P' ⟷ (∀α w. P ⊢ α ⇒* map Tm w ⟶ P' ⊢ α ⇒* map Tm w)"
  by (simp only: Lang_le_iff_Lang_of_le Lang_of_le_iff_derives)

lemma Lang_eq_iff_derives:
  "Lang P = Lang P' ⟷ (∀α w. P ⊢ α ⇒* map Tm w ⟷ P' ⊢ α ⇒* map Tm w)"
  apply (subst eq_iff) by (auto simp: Lang_le_iff_derives)

lemma Rhss_le_Ders: "Rhss P ≤ Ders P"
  by (auto simp: le_fun_def Rhss_def Ders_def derive_singleton)

lemma Lang_of_set_pow: "Lang_of_set P (X ^^ n) = Lang_of_set P X ^^ n"
  by (induction n, simp_all add: Lang_of_set_conc)

lemma Lang_of_set_star: "Lang_of_set P (star X) = star (Lang_of_set P X)"
  by (auto simp: star_def Lang_of_set_pow)

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_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_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_Cons:
  "P ⊢ x # u ⇒l v ⟷
  (case x of Nt A ⇒ ∃w. (A,w) ∈ P ∧ v = w @ u | Tm a ⇒ ∃w. v = Tm a # w ∧ P ⊢ u ⇒l w)"
  by (auto simp: derivel_Nt_Cons derivel_Tm_Cons split: sym.splits)

lemma deriveln_Cons:
"P ⊢ x # u ⇒l(n) v ⟷ (
  case n of 0 ⇒ v = x # u
  | Suc m ⇒ (
    case x of Nt A ⇒ ∃w. (A,w) ∈ P ∧ P ⊢ w @ u ⇒l(m) v
    | Tm a ⇒ ∃w. v = Tm a # w ∧ P ⊢ u ⇒l(n) w))"
  by (auto simp: deriveln_Nt_Cons deriveln_Tm_Cons split: nat.splits sym.splits)

lemma derivel_not_elim_Tm:
  "P ⊢ xs ⇒l map Nt w ⟹ ∃v. xs = map Nt v"
  by (cases xs)
    (auto simp: derivel_Cons Cons_eq_map_conv map_eq_append_conv split: sym.splits)

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

(* TODO: CFG? *)
lemma derivel_append_iff:
  "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

lemma deriveln_ConsD:
  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 (metis relpowp_Suc_E)
  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_iff[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 (simp add: relpowp_Suc_I)
      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 (simp add: relpowp_Suc_I)

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

lemma deriveln_Cons_TmsD:
  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 deriveln_ConsD[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) w⇩1 = map Tm w⇩1'" and "u⇩2 = map (Tm) u⇩2'"
      using map_eq_append_conv[of "Tm" w "map Tm w⇩1" u⇩2] by auto
    with m1_m2_n x_derivelm1_w1 v_derivelm2_u2 show ?thesis by auto
  qed                    
qed

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 derivern_prepend: "R ⊢ u ⇒r(n) v ⟹ R ⊢ p @ u ⇒r(n) p @ v"
  by (fastforce simp: derivern_iff_rev_deriveln rev_map deriveln_append rev_eq_append_conv)

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)

lemma derivern_snoc_Nt_Tms_decomp1: 
  "R ⊢ p @ [Nt A] ⇒r(n) map Tm q 
   ⟹ ∃pt At w k m. R ⊢ p ⇒(k) map Tm pt ∧ R ⊢ w ⇒(m) map Tm At ∧ (A, w) ∈ R 
        ∧ q = pt @ At ∧ n = Suc(k + m)"
proof-
  assume assm: "R ⊢ p @ [Nt A] ⇒r(n) map Tm q"
  then have "R ⊢ p @ [Nt A] ⇒(n) map Tm q" by (simp add: derivern_iff_deriven)
  then have "∃n1 n2 q1 q2. n = n1 + n2 ∧ map Tm q = q1@q2 ∧ R ⊢ p ⇒(n1) q1 ∧ R ⊢ [Nt A] ⇒(n2) q2"
    using deriven_append_decomp by blast
  then obtain n1 n2 q1 q2 
    where decomp1: "n = n1 + n2 ∧ map Tm q = q1 @ q2 ∧ R ⊢ p ⇒(n1) q1 ∧ R ⊢ [Nt A] ⇒(n2) q2"
    by blast
  then have "∃pt At. q1 = map Tm pt ∧ q2 = map Tm At ∧ q = pt @ At"
    by (meson map_eq_append_conv)
  then obtain pt At where decomp_tms: "q1 = map Tm pt ∧ q2 = map Tm At ∧ q = pt @ At" by blast
  then have "∃w m. n2 = Suc m ∧ R ⊢ w ⇒(m) (map Tm At) ∧ (A,w) ∈ R" 
    using decomp1 
    by (auto simp add: deriven_start1)
  then obtain w m where "n2 = Suc m ∧ R ⊢ w ⇒(m) (map Tm At) ∧ (A,w) ∈ R" by blast
  then have "R ⊢ p ⇒(n1) map Tm pt ∧ R ⊢ w ⇒(m) map Tm At ∧ (A, w) ∈ R 
     ∧ q = pt @ At ∧ n = Suc(n1 + m)" 
    using decomp1 decomp_tms by auto
  then show ?thesis by blast
qed

subsection ‹Redundant Productions›

text ‹Productions of the form ‹A → A› are redundant.›

lemma no_self_loops_derive:
  "reflclp (derive {(A,α) ∈ P. α ≠ [Nt A]}) = reflclp (derive P)"
  by (force simp: fun_eq_iff derive_iff)

lemma no_self_loops_derives:
  "{(A,α) ∈ P. α ≠ [Nt A]} ⊢ u ⇒* v ⟷ P ⊢ u ⇒* v"
  apply (subst rtranclp_reflclp[symmetric])
  by (simp add: no_self_loops_derive)

lemma Lang_of_no_self_loops:
  "Lang_of {(A,α) ∈ P. α ≠ [Nt A]} = Lang_of P"
  by (simp add: fun_eq_iff Lang_of_def no_self_loops_derives)

lemma Lang_no_self_loops:
  "Lang {(A,α) ∈ P. α ≠ [Nt A]} = Lang P"
  by (simp add: Lang_eq_iff_Lang_of_eq Lang_of_no_self_loops)

lemma Lang_eq_Rhss_no_self_loop:
  "Lang P A = Lang_of_set P (Rhss P A - {[Nt A]})"
proof-
  have "Lang P A = Lang {(A,α) ∈ P. α ≠ [Nt A]} A"
    by (simp add: Lang_no_self_loops)
  also have "… = Lang_of_set {(A,α) ∈ P. α ≠ [Nt A]} (Rhss P A - {[Nt A]})"
    by (auto simp: Lang_of_set_Rhss[symmetric] Rhss_def)
  finally show ?thesis by (simp add: Lang_of_no_self_loops)
qed

lemma no_self_loops_derivel:
  "reflclp (derivel {(A,α) ∈ P. α ≠ [Nt A]}) = reflclp (derivel P)"
  by (force simp: fun_eq_iff derivel_iff)

lemma no_self_loops_derivels:
  "{(A,α) ∈ P. α ≠ [Nt A]} ⊢ u ⇒l* v ⟷ P ⊢ u ⇒l* v"
  apply (subst rtranclp_reflclp[symmetric])
  by (simp add: no_self_loops_derivel)

text ‹Rules that can be simulated by other rules are redundant.›

lemma Rhss_le_Ders_imp_Lang_le: assumes "Rhss P ≤ Ders P'" shows "Lang P ≤ Lang P'"
  apply (unfold Lang_le_iff_derives)
proof (intro allI impI)
  fix α w
  assume "P ⊢ α ⇒* map Tm w"
  then obtain n where "P ⊢ α ⇒(n) map Tm w" by (auto simp: rtranclp_power)
  then show "P' ⊢ α ⇒* map Tm w"
  proof (induction n arbitrary: α w rule: less_induct)
    case (less n')
    show ?case
    proof (cases n')
      case 0
      with less.prems show ?thesis by simp
    next
      case [simp]: (Suc n)
      from less.prems[unfolded this deriven_Suc_map_Tm_decomp]
      obtain B β γ v u t m l where B: "(B,β) ∈ P"
        and lb: "P ⊢ β ⇒(m) map Tm u" and lc: "P ⊢ γ ⇒(l) map Tm t"
        and [simp]: "α = map Tm v @ Nt B # γ" "w = v @ u @ t" "n = m+l"
        by blast
      from less.IH[OF _ lc] have c: "P' ⊢ γ ⇒* map Tm t" by simp
      from assms[THEN le_funD, of B] B
      have "β ∈ Ders P' B" by (auto simp: Rhss_def)
      then have "P' ⊢ [Nt B] ⇒* β" by (auto simp: Ders_def)
      from derives_prepend[OF derives_append[OF this]]
      have "P' ⊢ α ⇒* map Tm v @ β @ γ" by simp
      also from less.IH[OF _ lb] c have "P' ⊢ … ⇒* map Tm w"
        by (auto intro!: derives_append_append)
      finally show ?thesis.
    qed
  qed
qed

lemma Lang_Un_redundant: assumes "Rhss R ≤ Ders P" shows "Lang (P ∪ R) = Lang P"
proof (rule antisym)
  show "Lang (P ∪ R) ≤ Lang P"
    apply (rule Rhss_le_Ders_imp_Lang_le)
    using assms Rhss_le_Ders[of P] by (simp add: le_fun_def Rhss_Un)
next
  show "Lang P ≤ Lang (P ∪ R)"
    apply (rule le_funI)
    apply (rule Lang_mono) by simp
qed

lemmas Lang_of_Un_redundant = Lang_Un_redundant[unfolded Lang_eq_iff_Lang_of_eq]

text ‹Productions whose lhss do not appear in other rules are redundant.›

lemma derive_Un_disj_Lhss:
  assumes α: "Nts_syms α ∩ Lhss Q = {}"
  shows "P ∪ Q ⊢ α ⇒ β ⟷ P ⊢ α ⇒ β"
  using α by (auto simp: Lhss_def derive_iff)

lemma deriven_Un_disj_Lhss:
  assumes PQ: "Rhs_Nts P ∩ Lhss Q = {}" and α: "Nts_syms α ∩ Lhss Q = {}"
  shows "P ∪ Q ⊢ α ⇒(n) β ⟷ P ⊢ α ⇒(n) β" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
  proof (induction n arbitrary: β)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    from Suc.prems obtain β' where 1: "P ∪ Q ⊢ α ⇒(n) β'" and 2: "P ∪ Q ⊢ β' ⇒ β"
      by (auto simp: relpowp_Suc_right)
    from Suc.IH[OF 1] have P1: "P ⊢ α ⇒(n) β'".
    from deriven_Nts_syms_subset[OF P1] α PQ
    have "Nts_syms β' ∩ Lhss Q = {}" by auto
    from P1 2[unfolded derive_Un_disj_Lhss[OF this]]
    show ?case by (auto simp: relpowp_Suc_right)
  qed
next
  assume ?r
  from deriven_mono[OF _ this]
  show ?l by auto
qed

lemma derives_Un_disj_Lhss:
  assumes "Rhs_Nts P ∩ Lhss Q = {}" and "Nts_syms α ∩ Lhss Q = {}"
  shows "P ∪ Q ⊢ α ⇒* β ⟷ P ⊢ α ⇒* β"
  using deriven_Un_disj_Lhss[OF assms] by (simp add: rtranclp_power)

lemma Lang_Un_disj_Lhss:
  assumes disj: "Rhs_Nts P ∩ Lhss Q = {}" and A: "A ∉ Lhss Q"
  shows "Lang (P ∪ Q) A = Lang P A"
  apply (rule Lang_eqI_derives)
  apply (rule derives_Un_disj_Lhss)
  using assms by auto

lemma Lang_disj_Lhss_Un:
  assumes disj: "Lhss P ∩ Rhs_Nts Q = {}" and A: "A ∉ Lhss P"
  shows "Lang (P ∪ Q) A = Lang Q A"
  using Lang_Un_disj_Lhss[of Q P A] assms by (simp add: ac_simps)

lemma Lang_of_Un_disj_Lhss:
  assumes "Rhs_Nts P ∩ Lhss Q = {}" and "Nts_syms α ∩ Lhss Q = {}"
  shows "Lang_of (P ∪ Q) α = Lang_of P α"
  using derives_Un_disj_Lhss[OF assms] by (simp add: Lang_of_def)

lemma Lang_of_disj_Lhss_Un:
  assumes disj: "Lhss P ∩ Rhs_Nts Q = {}" "Nts_syms α ∩ Lhss P = {}"
  shows "Lang_of (P ∪ Q) α = Lang_of Q α"
  using Lang_of_Un_disj_Lhss[of Q P α] assms by (simp add: ac_simps)

lemma Lang_of_set_Un_disj_Lhss:
  assumes PQ: "Rhs_Nts P ∩ Lhss Q = {}" and VQ: "⋃(Nts_syms ` V) ∩ Lhss Q = {}"
  shows "Lang_of_set (P ∪ Q) V = Lang_of_set P V"
proof-
  { fix v assume "v ∈ V"
    with VQ have "Nts_syms v ∩ Lhss Q = {}" by auto
    note Lang_of_Un_disj_Lhss[OF PQ this]
  }
  then show ?thesis by auto
qed

lemma Lang_of_set_disj_Lhss_Un:
  assumes disj: "Lhss P ∩ Rhs_Nts Q = {}" "⋃(Nts_syms ` V) ∩ Lhss P = {}"
  shows "Lang_of_set (P ∪ Q) V = Lang_of_set Q V"
  using Lang_of_set_Un_disj_Lhss[of Q P V] assms by (simp add: ac_simps)

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›

text ‹Some facts about ‹ε›-derivations:›

lemma deriven_Cons_Nil: "P ⊢ x # xs ⇒(n) [] ⟷
  (∃A α l m. P ⊢ α ⇒(l) [] ∧ P ⊢ xs ⇒(m) [] ∧ x = Nt A ∧ (A,α) ∈ P ∧ n = Suc (l+m))"
  using deriven_Nt_Cons_map_Tm[where w=Nil,simplified]
  by (cases x, auto simp add: deriven_Nt_Cons_map_Tm[where w=Nil,simplified]
      deriven_Tm_Cons)

lemma derives_Cons_Nil: "P ⊢ x # xs ⇒* [] ⟷
  (∃A α. P ⊢ α ⇒* [] ∧ P ⊢ xs ⇒* [] ∧ x = Nt A ∧ (A,α) ∈ P)"
  by (auto simp: derives_Cons_decomp)

text ‹Adding production whose rhs does not derive ‹ε› by other rules
does not change the ‹ε›-derivations.›

lemma insert_derives_Nil:
  assumes α0: "¬ P ⊢ α ⇒* []"
  shows "insert (A,α) P ⊢ α' ⇒* [] ⟷ P ⊢ α' ⇒* []" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain n where "insert (A,α) P ⊢ α' ⇒(n) []" by (auto simp: rtranclp_power)
  then show "P ⊢ α' ⇒* []"
  proof (induction n arbitrary: α' rule: less_induct)
    case (less n)
    show ?case
    proof (cases α')
      case Nil
      then show ?thesis by simp
    next
      case α': (Cons x xs)
      from less.prems[unfolded α' deriven_Cons_Nil]
      obtain B β l m where β: "insert (A,α) P ⊢ β ⇒(l) []"
        and xs: "insert (A,α) P ⊢ xs ⇒(m) []"
        and x: "x = Nt B"
        and B: "(B,β) ∈ insert (A,α) P"
        and n: "n = Suc (l + m)"
        by auto
      from less.IH[OF _ β] have Pβ: "P ⊢ β ⇒* []" by (simp add: n)
      from less.IH[OF _ xs] have Pxs: "P ⊢ xs ⇒* []" by (simp add: n)
      show ?thesis
      proof (cases "(B,β) ∈ P")
        case True
        with Pβ Pxs show ?thesis by (auto simp: α' x derives_Cons_Nil)
      next
        case False
        with B have "B = A" "β = α" by auto
        with Pβ α0 show ?thesis by simp
      qed
    qed
  qed
next
  assume r: ?r show "?l" by (rule derives_mono[OF _ r], auto) 
qed

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_deriven_Nil:
  "⟦ Eps_free R; R ⊢ l ⇒(n) [] ⟧ ⟹ l = []"
by (metis Eps_free_derives_Nil relpowp_imp_rtranclp)

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