Theory Epsilon_Elimination

(*
Author: August Martin Stimpfle
Based on HOL4 theories by Aditi Barthwal
*)

section ‹Elimination of Epsilon Productions›

theory Epsilon_Elimination
imports
  Context_Free_Grammar
  "HOL-Library.While_Combinator"
begin

inductive Nullable :: "('n,'t) Prods ⇒ ('n,'t) sym ⇒ bool"
for P where
  NullableSym:
  "⟦ (A, w) ∈ P; ∀s ∈ set w. Nullable P s⟧
  ⟹ Nullable P (Nt A)"

abbreviation "Nullables P w ≡ (∀s ∈ set w. Nullable P s)"

definition nullables_wrt :: "'n set ⇒ ('n, 't) syms ⇒ bool" where
"nullables_wrt N w = (Tms_syms w = {} ∧ Nts_syms w ⊆ N)"

definition nullable_step :: "('n,'t)Prods ⇒ 'n set ⇒ 'n set" where
"nullable_step P N = fst ` {(A,w) ∈ P. nullables_wrt N w}"

definition nullable_fun :: "('n,'t)Prods ⇒ 'n set option" where
"nullable_fun P = while_option (λN. nullable_step P N ≠ N) (nullable_step P) {}"

lemma "nullable_fun {(0::int,[Nt 1::(int,int)sym]), (1,[])} = Some{0,1}"
by eval

lemma mono_nullable_step: "mono (nullable_step P)"
unfolding mono_def nullable_step_def nullables_wrt_def by auto

(* TODO mv? *)
lemma while_option_Some_closed:
  fixes f :: "'a::complete_lattice ⇒ 'a"
  assumes "while_option (λx. f x ≠ x) f bot = Some x" shows "f x = x"
using while_option_stop2[OF assms(1)] by fastforce

lemma nullable_fun_Some_closed: "nullable_fun P = Some N ⟹ nullable_step P N = N"
unfolding nullable_fun_def using while_option_Some_closed[of "nullable_step P"] by blast

lemma Nullable_if_nullable_fun:
assumes "finite P" "nullable_fun P = Some N" shows "∀A∈N. Nullable P (Nt A)"
proof -
  let ?I = "λN. ∀A∈N. Nullable P (Nt A)"
  have 0: "?I {}" by simp
  have "?I (nullable_step P N)" if "?I N" for N
  proof -
    have "Nullable P (Nt A)" if asms: "(A, w) ∈ P" "Tms_syms w = {}" "Nts_syms w ⊆ N" for A w
    proof -
      have "Nullable P s" if "s ∈ set w" for s
      proof -
        have "s ∈ Nt ` N" using asms(2,3) ‹s ∈ set w› unfolding Nts_syms_def Tms_syms_def
          by(cases s) auto
        thus ?thesis using ‹?I N› by blast
      qed
      then show ?thesis by (metis asms(1) NullableSym)
    qed
    then show ?thesis using ‹?I N› unfolding nullable_step_def nullables_wrt_def by auto
  qed
  from while_option_rule[where P = ?I and s = "{}", OF this assms(2)[unfolded nullable_fun_def] 0]
  show ?thesis by blast
qed

lemma nullable_fun_if_Nullable: assumes "nullable_fun P = Some N"
  shows "Nullable P s ⟹ (⋀A. s = Nt A ⟹ A ∈ N)"
proof(induction rule: Nullable.induct)
  case (NullableSym B w)
  then have [simp]: "B = A" by auto
  from NullableSym have "A ∈ nullable_step P N"
   unfolding nullable_step_def nullables_wrt_def image_def Nts_syms_def Tms_syms_def
   apply auto
   using Nullable.cases by blast
  with NullableSym show ?case
    using assms nullable_fun_Some_closed by blast
qed

lemma nullable_fun_Some: assumes "finite P" shows "∃N. nullable_fun P = Some N"
proof -
  let ?M = "Nts P"
  have *: "⋀X. X ⊆ Nts P ⟹ nullable_step P X ⊆ Nts P"
    unfolding nullable_step_def nullables_wrt_def Nts_def by(auto)
  from while_option_finite_subset_Some[OF mono_nullable_step * finite_Nts[OF assms]]
  show ?thesis unfolding nullable_fun_def by blast
qed

lemma Nullable_iff_nullable_fun: "finite P ⟹ Nullable P (Nt A) = (A ∈ the(nullable_fun P))"
  by (metis Nullable_if_nullable_fun nullable_fun_Some nullable_fun_if_Nullable
      option.sel)

lemma nullable_Tm[code]: "Nullable P (Tm a) = False"
  using Nullable.cases by blast

lemma nullable_Nt[code]: "Nullable (set ps) (Nt A) = (A ∈ the(nullable_fun (set ps)))"
  by (simp add: Nullable_iff_nullable_fun)

lemma "nullable_fun {(0::int, [Nt 1, Nt 2, Nt 1]), (1, [Tm (0::int), Nt 1]), (1, []), (2, [Tm 1, Nt 2]), (2,[])}
 = Some{0,1,2}"
by eval

lemma "Nullable {(0::int,[Nt 1::(int,int)sym]), (1,[])} (Nt 0)"
by eval

lemma nullables_if: 
  assumes "P ⊢ u ⇒* v" 
    and "u=[a]" "Nullables P v"
  shows "Nullables P u"
  using assms
proof(induction arbitrary: a rule: rtranclp.induct)
  case (rtrancl_refl a)
  then show ?case by simp
next
  case (rtrancl_into_rtrancl u v w)
  from ‹P ⊢ v ⇒ w› obtain A α l r where Aα: "v = l @ [Nt A] @ r ∧ w = l @ α @ r ∧ (A, α) ∈ P"
    by (auto simp: derive.simps)
  from this ‹Nullables P w› have "Nullables P α ∧ Nullables P l ∧ Nullables P r"
    by simp
  hence "Nullables P [Nt A]"
    using Aα Nullable.simps by auto
  from this ‹Nullables P α ∧ Nullables P l ∧ Nullables P r› have "Nullables P v"
    using Aα by auto
  thus ?case
    using rtrancl_into_rtrancl.IH rtrancl_into_rtrancl.prems(1) by blast
qed

lemma nullable_if: "P ⊢ [a] ⇒* [] ⟹ Nullable P a"
  using nullables_if[of P "[a]" "[]" a] by simp

lemma nullable_aux: "∀s∈set gamma. P ⊢ [s] ⇒* [] ⟹ P ⊢ gamma ⇒* []"
proof (induction gamma)
  case (Cons a list)
  hence "P ⊢ list ⇒* []"
    by simp
  moreover have "P ⊢ [a] ⇒* []"
    using Cons by simp
  ultimately show ?case 
    using derives_Cons[of ‹P› list ‹[]› ‹a›] by simp
qed simp

lemma if_nullable: "Nullable P a ⟹ P ⊢ [a] ⇒* []"
proof (induction rule: Nullable.induct)
  case (NullableSym x gamma)
    hence "P ⊢ [Nt x] ⇒* gamma" 
      using derive_singleton by blast
    also have "P ⊢ gamma ⇒* []" 
      using NullableSym nullable_aux by blast
  finally show ?case .
qed

corollary nullable_iff: "Nullable P a ⟷ P ⊢ [a] ⇒* []"
  by (auto simp: nullable_if if_nullable)

fun eps_closure :: "('n, 't) Prods ⇒ ('n, 't) syms ⇒ ('n, 't) syms list" where
  "eps_closure ps [] = [[]]" |
  "eps_closure ps (s#sl) = (
    if Nullable ps s then (map ((#) s) (eps_closure ps sl)) @ eps_closure ps sl 
    else map ((#) s) (eps_closure ps sl))"

definition Eps_elim :: "('n, 't) Prods ⇒ ('n, 't) Prods" where
"Eps_elim P = {(l,r'). ∃r. (l,r) ∈ P ∧ r' ∈ set (eps_closure P r) ∧ (r' ≠ [])}"

lemma Eps_elim_code[code]: "Eps_elim P =
  (⋃(l,r) ∈ P. ⋃r' ∈ set (eps_closure P r). if r' = [] then {} else {(l,r')})"
unfolding Eps_elim_def by (auto split: prod.split)

definition eps_elim :: "('n, 't) prods ⇒ ('n, 't) prods" where
"eps_elim ps ≡ concat (map (λ(l,r). map (λr'. (l,r')) (filter (λr'. r' ≠ []) (eps_closure (set ps) r))) ps)"

lemma set_eps_elim: "set(eps_elim ps) = Eps_elim (set ps)"
unfolding eps_elim_def Eps_elim_def by auto

lemma "Eps_elim
  {(0::int, [Nt 1, Nt 2, Nt 1]), (1, [Tm (0::int), Nt 1]), (1, []), (2, [Tm 1, Nt 2]), (2,[])}
 = {(2, [Tm 1, Nt 2]), (2, [Tm 1]), (1, [Tm 0, Nt 1]), (1, [Tm 0]), (0, [Nt 1, Nt 2, Nt 1]),
    (0, [Nt 1, Nt 2]), (0, [Nt 1, Nt 1]), (0, [Nt 1]), (0, [Nt 2, Nt 1]), (0, [Nt 2])}"
by eval

lemma Eps_free_Eps_elim: "Eps_free (Eps_elim ps')"
unfolding Eps_elim_def Eps_free_def by blast

text ‹@{const Eps_elim} is identity on @{const Eps_free} input.›

lemma Eps_free_not_Nullable: "Eps_free P ⟹ ¬ Nullable P A"
  by (auto simp: nullable_iff Eps_free_derives_Nil)

lemma Eps_free_eps_closure: "Eps_free P ⟹ eps_closure P w = [w]"
  by (induction w, auto simp: Eps_free_not_Nullable)

lemma Eps_elim_id: "Eps_free P ⟹ Eps_elim P = P"
  by (auto simp: Eps_elim_def Eps_free_eps_closure Eps_free_Nil)

(* auxiliary function to prove finiteness *)
definition Eps_elim_fun :: "('n, 't) Prods ⇒ ('n, 't) prod ⇒ ('n, 't) Prods" where 
  "Eps_elim_fun ps p = {(l',r'). l' = fst p ∧ r' ∈ set (eps_closure ps (snd p)) ∧ (r' ≠ [])}"

lemma Eps_elim_fun_eq: "Eps_elim ps = ⋃((Eps_elim_fun ps) ` ps)"
proof 
  show "Eps_elim ps ⊆ (⋃ (Eps_elim_fun ps ` ps))" 
   unfolding Eps_elim_def Eps_elim_fun_def by auto
next
  show "⋃((Eps_elim_fun ps) ` ps) ⊆ Eps_elim ps"
  proof
    fix x
    assume "x ∈ ⋃((Eps_elim_fun ps) ` ps)"
    obtain l r' where "x = (l,r')" by fastforce
    hence "(l,r') ∈ ⋃((Eps_elim_fun ps) ` ps)" 
      using ‹x ∈ ⋃((Eps_elim_fun ps) ` ps)› by simp
    hence 1: "∃r. r' ∈ set (eps_closure ps r) ∧ (r' ≠ []) ∧ (l,r) ∈ ps" 
      using Eps_elim_fun_def by fastforce
    from this  obtain r where "r' ∈ set (eps_closure ps r) ∧ (l,r) ∈ ps" 
      by blast
    thus "x ∈ Eps_elim ps" unfolding Eps_elim_fun_def Eps_elim_def
      using 1 ‹x = (l, r')› by blast 
  qed
qed

lemma finite_Eps_elim: assumes "finite ps" shows "finite (Eps_elim ps)" 
proof -
  have "∀p ∈ ps. finite (Eps_elim_fun ps p)"
    unfolding Eps_elim_fun_def by auto
  hence "finite (⋃((Eps_elim_fun ps) ` ps))"
    using finite_UN assms by simp
  thus ?thesis using Eps_elim_fun_eq by metis
qed

lemma eps_closure_nullable:  "[] ∈ set (eps_closure ps w) ⟹ Nullables ps w"
proof (induction w)
  case Nil
  then show ?case by simp
next
  case (Cons a r)
  hence "Nullable ps a"
    using image_iff[of ‹[]› ‹eps_closure ps› ‹{a#r}›] by auto
  then show ?case 
    using Cons Un_iff by auto
qed

lemma Eps_elim_rel_1: "r' ∈ set (eps_closure ps r) ⟹ ps ⊢ r ⇒* r'"
proof (induction r arbitrary: r')
  case (Cons a r)
  then show ?case 
  proof (cases "Nullable ps a")
    case True
    obtain e where e: "e ∈ set (eps_closure ps r) ∧ (r' = (a#e) ∨ r' = e)"
      using Cons.prems True by auto
    hence 1: "ps ⊢ r ⇒* e" 
      using Cons.IH by blast
    hence 2: "ps ⊢ [a]@r ⇒* [a]@e" 
      using e derives_prepend by blast
    have "ps ⊢ [a] ⇒* []" 
      using True if_nullable by blast
    hence "ps ⊢ [a]@r ⇒* r" 
      using derives_append by fastforce
    thus ?thesis 
      using 1 2 e by force 
  next
    case False
    obtain e where e: "e ∈ set (eps_closure ps r) ∧ (r' = (a#e))"
      using Cons.prems False by auto
    hence "ps ⊢ r ⇒* e" 
      using Cons.IH by simp
    hence "ps ⊢ [a]@r ⇒* [a]@e" 
      using derives_prepend by blast
    thus ?thesis
      using e by simp
  qed
qed simp

lemma Eps_elim_rel_r2: 
  assumes "Eps_elim ps ⊢ u ⇒ v"
  shows "ps ⊢ u ⇒* v"
  using assms 
proof -
  obtain A α x y where A: "(A, α) ∈ Eps_elim ps ∧ u = x @ [Nt A] @ y ∧ v = x @ α @ y"
    using assms derive.cases by meson
  hence 1: "(A, α) ∈ {(l,r'). ∃r. (l,r) ∈ ps ∧ r' ∈ set (eps_closure ps r) ∧ (r' ≠ [])}"
    unfolding Eps_elim_def by simp
  obtain r where r: "(A, r) ∈ ps ∧ α ∈ set (eps_closure ps r)"
    using 1 by blast
  hence "ps ⊢ r ⇒* α" 
    using Eps_elim_rel_1 by blast
  hence 2: "ps ⊢ x @ r @ y ⇒* x @ α @ y"
    using r derives_prepend derives_append by blast
  hence "ps ⊢ x @ [Nt A] @ y ⇒ x @ r @ y" 
    using r derive.simps by fast
  thus ?thesis 
    using 2 by (simp add: A)
qed

lemma Eps_elim_rel_r3:
  assumes "Eps_elim ps ⊢ u ⇒* v"
  shows "ps ⊢ u ⇒* v"
    using assms by (induction v rule: rtranclp_induct) (auto simp: Eps_elim_rel_r2 rtranclp_trans)

lemma Eps_elim_rel_r5: "r ∈ set (eps_closure ps r)" 
  by (induction r) auto

lemma Eps_elim_rel_r4:
  assumes "(l,r) ∈ ps"
    and "(r' ≠ [])" 
    and "r' ∈ set (eps_closure ps r)"
  shows "(l,r') ∈ Eps_elim ps"
  using assms unfolding Eps_elim_def by blast

lemma Eps_elim_rel_r7: 
  assumes "ps ⊢ [Nt A] ⇒ v"
    and "v' ∈ set (eps_closure ps v) ∧ (v' ≠ [])"
  shows "Eps_elim ps ⊢ [Nt A] ⇒ v'"
proof -
  have "(A,v) ∈ ps" 
    using assms(1) by (simp add: derive_singleton)
  hence "(A,v') ∈ Eps_elim ps" 
    using assms Eps_elim_rel_r4 conjE by fastforce
  thus ?thesis 
    using derive_singleton by fast
qed

lemma Eps_elim_rel_r12a: 
  assumes "x' ∈ set (eps_closure ps x)"
    and "y' ∈ set (eps_closure ps y)"
  shows "(x'@y') ∈ set (eps_closure ps (x@y))"
  using assms by (induction x arbitrary: x' y y' rule: eps_closure.induct) auto

lemma Eps_elim_rel_r12b:
  assumes "x' ∈ set (eps_closure ps x)"
    and "y' ∈ set (eps_closure ps y)"
    and "z' ∈ set (eps_closure ps z)"
  shows "(x'@y'@z') ∈ set (eps_closure ps (x@y@z))"
  using assms 
  by (induction x arbitrary: x' y y' z z' rule: eps_closure.induct) (auto simp: Eps_elim_rel_r12a)

lemma Eps_elim_rel_r14:
  assumes "r' ∈ set (eps_closure ps (x@y))"
  shows "∃x' y'. (r'=x'@y') ∧ x' ∈ set (eps_closure ps x) ∧ y' ∈ set (eps_closure ps y)"
  using assms
proof (induction x arbitrary: y r' rule: eps_closure.induct)
  case (2 ps s sl)
  then show ?case
  proof -
    have "∃x' y'. s # x = x' @ y' ∧ (x' ∈ (#) s ` set (eps_closure ps sl) ∨ x' ∈ set (eps_closure ps sl)) ∧ y' ∈ set (eps_closure ps y)"
      if "⋀r' y. r' ∈ set (eps_closure ps (sl @ y)) ⟹ ∃x' y'. r' = x' @ y' ∧ x' ∈ set (eps_closure ps sl) ∧ y' ∈ set (eps_closure ps y)"
        and "Nullable ps s"
        and "x ∈ set (eps_closure ps (sl @ y))"
        and "r' = s # x"
      for x :: "('a, 'b) sym list"
      using that by (metis append_Cons imageI)
    moreover have "∃x' y'. r' = x' @ y' ∧ (x' ∈ (#) s ` set (eps_closure ps sl) ∨ x' ∈ set (eps_closure ps sl)) ∧ y' ∈ set (eps_closure ps y)"
      if "⋀r' y. r' ∈ set (eps_closure ps (sl @ y)) ⟹ ∃x' y'. r' = x' @ y' ∧ x' ∈ set (eps_closure ps sl) ∧ y' ∈ set (eps_closure ps y)"
        and "Nullable ps s"
        and "r' ∈ set (eps_closure ps (sl @ y))"
      using that by metis
    moreover have "∃x' y'. s # x = x' @ y' ∧ x' ∈ (#) s ` set (eps_closure ps sl) ∧ y' ∈ set (eps_closure ps y)"
      if "⋀r' y. r' ∈ set (eps_closure ps (sl @ y)) ⟹ ∃x' y'. r' = x' @ y' ∧ x' ∈ set (eps_closure ps sl) ∧ y' ∈ set (eps_closure ps y)"
        and "¬ Nullable ps s"
        and "x ∈ set (eps_closure ps (sl @ y))"
        and "r' = s # x"
      for x :: "('a, 'b) sym list"
      using that by (metis append_Cons imageI)
    ultimately show ?thesis
      using 2 by auto
  qed
qed simp

lemma Eps_elim_rel_r15:
  assumes "ps ⊢ [Nt S] ⇒* u"
    and "v ∈ set (eps_closure ps u) ∧ (v ≠ [])"
  shows "Eps_elim ps ⊢ [Nt S] ⇒* v"
  using assms
proof (induction u arbitrary: v rule: derives_induct)
  case base
  then show ?case
    by (cases "Nullable ps (Nt S)") auto
next
  case (step x A y w)
  then obtain x' w' y' where 
    v: "(v = (x'@w'@y')) ∧ x' ∈ set (eps_closure ps x) ∧ w' ∈ set (eps_closure ps w) ∧ y' ∈ set (eps_closure ps y)"
    using step Eps_elim_rel_r14 by metis
  then show ?case
  proof (cases "w' = []")
    case True
      hence "v = x'@y'" 
        using v by simp 
      have "[] ∈ set (eps_closure ps w)"
        using True v by simp
      hence "Nullables ps w"
        using eps_closure_nullable by blast
      hence "[] ∈ set (eps_closure ps [Nt A])" 
        using step(2) NullableSym by fastforce
      hence "(x'@y') ∈ set (eps_closure ps (x@[Nt A]@y))"
        using Eps_elim_rel_r12b[of x' ps x ‹[]› ‹[Nt A]› y' y] v by simp
      then show ?thesis 
        using ‹v = x' @ y'› step by blast
  next
    case False
      have "(x'@[Nt A]@y') ∈ set (eps_closure ps (x@[Nt A]@y)) "
        using Eps_elim_rel_r12b[of x' ps x ‹[Nt A]› ‹[Nt A]› y' y] Eps_elim_rel_r5[of ‹[Nt A]› ps] v by blast
      hence 1: "Eps_elim ps ⊢ [Nt S] ⇒* (x'@[Nt A]@y')" 
        using step by blast
      have "ps ⊢ [Nt A] ⇒ w" 
        using step(2) derive_singleton by blast
      hence "Eps_elim ps ⊢ [Nt A] ⇒ w'"
        using Eps_elim_rel_r7[of ps A w w'] False step v by blast
      hence "Eps_elim ps ⊢ (x'@[Nt A]@y') ⇒ (x'@w'@y')" 
        using derive_append derive_prepend by blast
      thus ?thesis using 1
      by (simp add: v step.prems(1))
  qed
qed

theorem Eps_elim_rel_eq_if_noe:
  assumes "[] ∉ Lang ps S"
  shows "Lang ps S = Lang (Eps_elim ps) S"
proof 
  show "Lang ps S ⊆ Lang (Eps_elim ps) S"
  proof 
    fix x
    assume "x ∈ Lang ps S"
    have "∀x. ps ⊢ [Nt S] ⇒* x ⟶ x ≠ []"
      using assms Lang_def by fastforce
    hence "(map Tm x) ∈ set (eps_closure ps (map Tm x))" 
      using Eps_elim_rel_r5 by auto
    hence "Eps_elim ps ⊢ [Nt S] ⇒* (map Tm x)"
      using assms ‹x ∈ Lang ps S› Lang_def Eps_elim_rel_r15[of ps S ‹map Tm x›] by fast
    thus "x ∈ Lang (Eps_elim ps) S"
      using Lang_def ‹x ∈ Lang ps S› by fast 
  qed
next
  show "Lang (Eps_elim ps) S ⊆ Lang ps S"
  proof
    fix x'
    assume "x' ∈ Lang (Eps_elim ps) S"
    show "x' ∈ Lang ps S" 
      using assms Lang_def ‹x' ∈ Lang (Eps_elim ps) S› Eps_elim_rel_r3[of ps ‹[Nt S]› ‹map Tm x'›] by fast
  qed
qed

(* correctness *)
lemma noe_lang_Eps_elim_rel_aux: 
  assumes "ps ⊢ [Nt S] ⇒* w" "w = []"  
  shows "∃A. ps ⊢ [Nt S] ⇒* [Nt A] ∧ (A, w) ∈ ps"
  using assms by (induction w rule: rtranclp_induct) (auto simp: derive.simps)

lemma noe_lang_Eps_elim_rel: "[] ∉ Lang (Eps_elim ps) S"
proof (rule notI)
  assume "[] ∈ Lang (Eps_elim ps) S"
  hence "Eps_elim ps ⊢ [Nt S] ⇒* map Tm []"
    using Lang_def by fast
  hence "Eps_elim ps ⊢ [Nt S] ⇒* []"
    by simp
  hence "∃A. Eps_elim ps ⊢ [Nt S] ⇒* [Nt A] ∧ (A, []) ∈ Eps_elim ps"
    using noe_lang_Eps_elim_rel_aux[of ‹Eps_elim ps›] by blast
  thus False 
    unfolding Eps_elim_def by blast
qed

theorem Lang_Eps_elim: "Lang (Eps_elim ps) S = Lang ps S - {[]}"
proof 
  show "Lang (Eps_elim ps) S ⊆ Lang ps S - {[]}"
  proof 
    fix w
    assume "w ∈ Lang (Eps_elim ps) S"
    hence "w ∈ Lang (Eps_elim ps) S - {[]}"
      by (simp add: noe_lang_Eps_elim_rel)
    thus "w ∈ Lang ps S - {[]}"
      by (auto simp: Lang_def Eps_elim_rel_r3)
  qed
next
  show "Lang ps S - {[]} ⊆ Lang (Eps_elim ps) S"
  proof 
    fix w
    assume "w ∈ Lang ps S - {[]}"
    hence 1: "(map Tm w) ≠ []" 
      by simp
    have 2: "ps ⊢ [Nt S] ⇒* (map Tm w)"
      using ‹w ∈ Lang ps S - {[]}› Lang_def by fast
    have "(map Tm w) ∈ set (eps_closure ps (map Tm w)) "
      using ‹w ∈ Lang ps S - {[]}› Eps_elim_rel_r5 by blast
    hence "Eps_elim ps ⊢ [Nt S] ⇒* (map Tm w)"
      using 1 2 Eps_elim_rel_r15[of ps] by simp
    thus "w ∈ Lang (Eps_elim ps) S"
      by (simp add: Lang_def)
  qed
qed

lemma set_eps_closure_subset: "u ∈ set(eps_closure P w) ⟹ set u ⊆ set w"
apply(induction P w arbitrary: u rule: eps_closure.induct)
 apply simp
apply (fastforce split: if_splits)
done

lemma Lhss_Eps_elim: "Lhss (Eps_elim P) ⊆ Lhss P"
by(auto simp: Lhss_def Eps_elim_def dest: set_eps_closure_subset)

lemma Tms_Eps_elim: "Tms (Eps_elim P) ⊆ Tms P"
by(auto simp: Tms_def Tms_syms_def Eps_elim_def dest: set_eps_closure_subset)

lemma Rhs_Nts_Eps_elim: "Rhs_Nts (Eps_elim P) ⊆ Rhs_Nts P"
by(auto simp: Rhs_Nts_def Nts_syms_def Eps_elim_def dest: set_eps_closure_subset)

lemma Nts_Eps_elim: "Nts (Eps_elim P) ⊆ Nts P"
  using Lhss_Eps_elim[of P] Rhs_Nts_Eps_elim[of P]
by (auto simp: Nts_Lhss_Rhs_Nts)

corollary nts_eps_elim: "Nts(set(eps_elim ps)) ⊆ Nts(set ps)"
  by (metis set_eps_elim Nts_Eps_elim)

corollary lang_eps_elim: "lang (eps_elim ps) S = lang ps S - {[]}"
  by (metis Lang_Eps_elim set_eps_elim)

corollary eps_free_eps_elim: "eps_free (eps_elim ps)"
  by (metis set_eps_elim Eps_free_Eps_elim)

end