diff --git a/Regular-Sets/Derivatives.thy b/Regular-Sets/Derivatives.thy
deleted file mode 100644
index 6cfde24..0000000
--- a/Regular-Sets/Derivatives.thy
+++ /dev/null
@@ -1,375 +0,0 @@
-section "Derivatives of regular expressions"
-
-(* Author: Christian Urban *)
-
-theory Derivatives
-imports Regular_Exp
-begin
-
-text\<open>This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}.\<close>
-
-subsection \<open>Brzozowski's derivatives of regular expressions\<close>
-
-primrec
-  deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "deriv c (Zero) = Zero"
-| "deriv c (One) = Zero"
-| "deriv c (Atom c') = (if c = c' then One else Zero)"
-| "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
-| "deriv c (Times r1 r2) = 
-    (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
-| "deriv c (Star r) = Times (deriv c r) (Star r)"
-
-primrec 
-  derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "derivs [] r = r"
-| "derivs (c # s) r = derivs s (deriv c r)"
-
-
-lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
-by (induction r) (auto)
-
-lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> atoms r"
-by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD])
-
-lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
-by (induct r) (simp_all add: nullable_iff)
-
-lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)"
-by (induct s arbitrary: r) (simp_all add: lang_deriv)
-
-text \<open>A regular expression matcher:\<close>
-
-definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
-"matcher r s = nullable (derivs s r)"
-
-lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
-by (induct s arbitrary: r)
-   (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
-
-
-subsection \<open>Antimirov's partial derivatives\<close>
-
-abbreviation
-  "Timess rs r \<equiv> (\<Union>r' \<in> rs. {Times r' r})"
-
-lemma Timess_eq_image:
-  "Timess rs r = (\<lambda>r'. Times r' r) ` rs"
-  by auto
-
-primrec
-  pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
-where
-  "pderiv c Zero = {}"
-| "pderiv c One = {}"
-| "pderiv c (Atom c') = (if c = c' then {One} else {})"
-| "pderiv c (Plus r1 r2) = (pderiv c r1) \<union> (pderiv c r2)"
-| "pderiv c (Times r1 r2) = 
-    (if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)"
-| "pderiv c (Star r) = Timess (pderiv c r) (Star r)"
-
-primrec
-  pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
-where
-  "pderivs [] r = {r}"
-| "pderivs (c # s) r = \<Union> (pderivs s ` pderiv c r)"
-
-abbreviation
- pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
-where
-  "pderiv_set c rs \<equiv> \<Union> (pderiv c ` rs)"
-
-abbreviation
-  pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
-where
-  "pderivs_set s rs \<equiv> \<Union> (pderivs s ` rs)"
-
-lemma pderivs_append:
-  "pderivs (s1 @ s2) r = \<Union> (pderivs s2 ` pderivs s1 r)"
-by (induct s1 arbitrary: r) (simp_all)
-
-lemma pderivs_snoc:
-  shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"
-by (simp add: pderivs_append)
-
-lemma pderivs_simps [simp]:
-  shows "pderivs s Zero = (if s = [] then {Zero} else {})"
-  and   "pderivs s One = (if s = [] then {One} else {})"
-  and   "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \<union> (pderivs s r2))"
-by (induct s) (simp_all)
-
-lemma pderivs_Atom:
-  shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
-by (induct s) (simp_all)
-
-subsection \<open>Relating left-quotients and partial derivatives\<close>
-
-lemma Deriv_pderiv:
-  shows "Deriv c (lang r) = \<Union> (lang ` pderiv c r)"
-by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
-
-lemma Derivs_pderivs:
-  shows "Derivs s (lang r) = \<Union> (lang ` pderivs s r)"
-proof (induct s arbitrary: r)
-  case (Cons c s)
-  have ih: "\<And>r. Derivs s (lang r) = \<Union> (lang ` pderivs s r)" by fact
-  have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
-  also have "\<dots> = Derivs s (\<Union> (lang ` pderiv c r))" by (simp add: Deriv_pderiv)
-  also have "\<dots> = Derivss s (lang ` (pderiv c r))"
-    by (auto simp add:  Derivs_def)
-  also have "\<dots> = \<Union> (lang ` (pderivs_set s (pderiv c r)))"
-    using ih by auto
-  also have "\<dots> = \<Union> (lang ` (pderivs (c # s) r))" by simp
-  finally show "Derivs (c # s) (lang r) = \<Union> (lang ` pderivs (c # s) r)" .
-qed (simp add: Derivs_def)
-
-subsection \<open>Relating derivatives and partial derivatives\<close>
-
-lemma deriv_pderiv:
-  shows "\<Union> (lang ` (pderiv c r)) = lang (deriv c r)"
-unfolding lang_deriv Deriv_pderiv by simp
-
-lemma derivs_pderivs:
-  shows "\<Union> (lang ` (pderivs s r)) = lang (derivs s r)"
-unfolding lang_derivs Derivs_pderivs by simp
-
-
-subsection \<open>Finiteness property of partial derivatives\<close>
-
-definition
-  pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
-where
-  "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r"
-
-lemma pderivs_lang_subsetI:
-  assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C"
-  shows "pderivs_lang A r \<subseteq> C"
-using assms unfolding pderivs_lang_def by (rule UN_least)
-
-lemma pderivs_lang_union:
-  shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)"
-by (simp add: pderivs_lang_def)
-
-lemma pderivs_lang_subset:
-  shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r"
-by (auto simp add: pderivs_lang_def)
-
-definition
-  "UNIV1 \<equiv> UNIV - {[]}"
-
-lemma pderivs_lang_Zero [simp]:
-  shows "pderivs_lang UNIV1 Zero = {}"
-unfolding UNIV1_def pderivs_lang_def by auto
-
-lemma pderivs_lang_One [simp]:
-  shows "pderivs_lang UNIV1 One = {}"
-unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)
-
-lemma pderivs_lang_Atom [simp]:
-  shows "pderivs_lang UNIV1 (Atom c) = {One}"
-unfolding UNIV1_def pderivs_lang_def 
-apply(auto)
-apply(frule rev_subsetD)
-apply(rule pderivs_Atom)
-apply(simp)
-apply(case_tac xa)
-apply(auto split: if_splits)
-done
-
-lemma pderivs_lang_Plus [simp]:
-  shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2"
-unfolding UNIV1_def pderivs_lang_def by auto
-
-
-text \<open>Non-empty suffixes of a string (needed for the cases of @{const Times} and @{const Star} below)\<close>
-
-definition
-  "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
-
-lemma PSuf_snoc:
-  shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}"
-unfolding PSuf_def conc_def
-by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
-
-lemma PSuf_Union:
-  shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"
-by (auto simp add: conc_def)
-
-lemma pderivs_lang_snoc:
-  shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))"
-unfolding pderivs_lang_def
-by (simp add: PSuf_Union pderivs_snoc)
-
-lemma pderivs_Times:
-  shows "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
-proof (induct s rule: rev_induct)
-  case (snoc c s)
-  have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)" 
-    by fact
-  have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))" 
-    by (simp add: pderivs_snoc)
-  also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
-    using ih by fastforce
-  also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
-    by (simp)
-  also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
-    by (simp add: pderivs_lang_snoc)
-  also 
-  have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
-    by auto
-  also 
-  have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
-    by (auto simp add: if_splits)
-  also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
-    by (simp add: pderivs_snoc)
-  also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2"
-    unfolding pderivs_lang_def by (auto simp add: PSuf_snoc)  
-  finally show ?case .
-qed (simp) 
-
-lemma pderivs_lang_Times_aux1:
-  assumes a: "s \<in> UNIV1"
-  shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
-using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
-
-lemma pderivs_lang_Times_aux2:
-  assumes a: "s \<in> UNIV1"
-  shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"
-using a unfolding pderivs_lang_def by auto
-
-lemma pderivs_lang_Times:
-  shows "pderivs_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2"
-apply(rule pderivs_lang_subsetI)
-apply(rule subset_trans)
-apply(rule pderivs_Times)
-using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2
-apply auto
-apply blast
-done
-
-lemma pderivs_Star:
-  assumes a: "s \<noteq> []"
-  shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)"
-using a
-proof (induct s rule: rev_induct)
-  case (snoc c s)
-  have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact
-  { assume asm: "s \<noteq> []"
-    have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
-    also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
-      using ih[OF asm] by fast
-    also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
-      by (auto split: if_splits)
-    also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))"
-      by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union)
-         (auto simp add: pderivs_lang_def)
-    also have "\<dots> = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)"
-      by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def)
-    finally have ?case .
-  }
-  moreover
-  { assume asm: "s = []"
-    then have ?case by (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
-  }
-  ultimately show ?case by blast
-qed (simp)
-
-lemma pderivs_lang_Star:
-  shows "pderivs_lang UNIV1 (Star r) \<subseteq> Timess (pderivs_lang UNIV1 r) (Star r)"
-apply(rule pderivs_lang_subsetI)
-apply(rule subset_trans)
-apply(rule pderivs_Star)
-apply(simp add: UNIV1_def)
-apply(simp add: UNIV1_def PSuf_def)
-apply(auto simp add: pderivs_lang_def)
-done
-
-lemma finite_Timess [simp]:
-  assumes a: "finite A"
-  shows "finite (Timess A r)"
-using a by auto
-
-lemma finite_pderivs_lang_UNIV1:
-  shows "finite (pderivs_lang UNIV1 r)"
-apply(induct r)
-apply(simp_all add: 
-  finite_subset[OF pderivs_lang_Times]
-  finite_subset[OF pderivs_lang_Star])
-done
-    
-lemma pderivs_lang_UNIV:
-  shows "pderivs_lang UNIV r = pderivs [] r \<union> pderivs_lang UNIV1 r"
-unfolding UNIV1_def pderivs_lang_def
-by blast
-
-lemma finite_pderivs_lang_UNIV:
-  shows "finite (pderivs_lang UNIV r)"
-unfolding pderivs_lang_UNIV
-by (simp add: finite_pderivs_lang_UNIV1)
-
-lemma finite_pderivs_lang:
-  shows "finite (pderivs_lang A r)"
-by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
-
-
-text\<open>The following relationship between the alphabetic width of regular expressions
-(called @{text awidth} below) and the number of partial derivatives was proved
-by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
-
-fun awidth :: "'a rexp \<Rightarrow> nat" where
-"awidth Zero = 0" |
-"awidth One = 0" |
-"awidth (Atom a) = 1" |
-"awidth (Plus r1 r2) = awidth r1 + awidth r2" |
-"awidth (Times r1 r2) = awidth r1 + awidth r2" |
-"awidth (Star r1) = awidth r1"
-
-lemma card_Timess_pderivs_lang_le:
-  "card (Timess (pderivs_lang A r) s) \<le> card (pderivs_lang A r)"
-  using finite_pderivs_lang unfolding Timess_eq_image by (rule card_image_le)
-
-lemma card_pderivs_lang_UNIV1_le_awidth: "card (pderivs_lang UNIV1 r) \<le> awidth r"
-proof (induction r)
-  case (Plus r1 r2)
-  have "card (pderivs_lang UNIV1 (Plus r1 r2)) = card (pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2)" by simp
-  also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
-    by(simp add: card_Un_le)
-  also have "\<dots> \<le> awidth (Plus r1 r2)" using Plus.IH by simp
-  finally show ?case .
-next
-  case (Times r1 r2)
-  have "card (pderivs_lang UNIV1 (Times r1 r2)) \<le> card (Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2)"
-    by (simp add: card_mono finite_pderivs_lang pderivs_lang_Times)
-  also have "\<dots> \<le> card (Timess (pderivs_lang UNIV1 r1) r2) + card (pderivs_lang UNIV1 r2)"
-    by (simp add: card_Un_le)
-  also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
-    by (simp add: card_Timess_pderivs_lang_le)
-  also have "\<dots> \<le> awidth (Times r1 r2)" using Times.IH by simp
-  finally show ?case .
-next
-  case (Star r)
-  have "card (pderivs_lang UNIV1 (Star r)) \<le> card (Timess (pderivs_lang UNIV1 r) (Star r))"
-    by (simp add: card_mono finite_pderivs_lang pderivs_lang_Star)
-  also have "\<dots> \<le> card (pderivs_lang UNIV1 r)" by (rule card_Timess_pderivs_lang_le)
-  also have "\<dots> \<le> awidth (Star r)" by (simp add: Star.IH)
-  finally show ?case .
-qed (auto)
-
-text\<open>Antimirov's Theorem 3.4:\<close>
-theorem card_pderivs_lang_UNIV_le_awidth: "card (pderivs_lang UNIV r) \<le> awidth r + 1"
-proof -
-  have "card (insert r (pderivs_lang UNIV1 r)) \<le> Suc (card (pderivs_lang UNIV1 r))"
-    by(auto simp: card_insert_if[OF finite_pderivs_lang_UNIV1])
-  also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pderivs_lang_UNIV1_le_awidth)
-  finally show ?thesis by(simp add: pderivs_lang_UNIV)
-qed 
-
-text\<open>Antimirov's Corollary 3.5:\<close>
-corollary card_pderivs_lang_le_awidth: "card (pderivs_lang A r) \<le> awidth r + 1"
-by(rule order_trans[OF
-  card_mono[OF finite_pderivs_lang_UNIV pderivs_lang_subset[OF subset_UNIV]]
-  card_pderivs_lang_UNIV_le_awidth])
-
-end
diff --git a/Regular-Sets/Equivalence_Checking.thy b/Regular-Sets/Equivalence_Checking.thy
deleted file mode 100644
index 1abcc85..0000000
--- a/Regular-Sets/Equivalence_Checking.thy
+++ /dev/null
@@ -1,230 +0,0 @@
-section \<open>Deciding Regular Expression Equivalence\<close>
-
-theory Equivalence_Checking
-imports
-  NDerivative
-  "HOL-Library.While_Combinator"
-begin
-
-
-subsection \<open>Bisimulation between languages and regular expressions\<close>
-
-coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
-"([] \<in> K \<longleftrightarrow> [] \<in> L) 
- \<Longrightarrow> (\<And>x. bisimilar (Deriv x K) (Deriv x L))
- \<Longrightarrow> bisimilar K L"
-
-lemma equal_if_bisimilar:
-assumes "bisimilar K L" shows "K = L"
-proof (rule set_eqI)
-  fix w
-  from \<open>bisimilar K L\<close> show "w \<in> K \<longleftrightarrow> w \<in> L"
-  proof (induct w arbitrary: K L)
-    case Nil thus ?case by (auto elim: bisimilar.cases)
-  next
-    case (Cons a w K L)
-    from \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
-      by (auto elim: bisimilar.cases)
-    then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L" by (rule Cons(1))
-    thus ?case by (auto simp: Deriv_def)
-  qed
-qed
-
-lemma language_coinduct:
-fixes R (infixl "\<sim>" 50)
-assumes "K \<sim> L"
-assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
-assumes "\<And>K L x. K \<sim> L \<Longrightarrow> Deriv x K \<sim> Deriv x L"
-shows "K = L"
-apply (rule equal_if_bisimilar)
-apply (rule bisimilar.coinduct[of R, OF \<open>K \<sim> L\<close>])
-apply (auto simp: assms)
-done
-
-type_synonym 'a rexp_pair = "'a rexp * 'a rexp"
-type_synonym 'a rexp_pairs = "'a rexp_pair list"
-
-definition is_bisimulation ::  "'a::order list \<Rightarrow> 'a rexp_pair set \<Rightarrow> bool"
-where
-"is_bisimulation as R =
-  (\<forall>(r,s)\<in> R. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
-    (\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R))"
-
-lemma bisim_lang_eq:
-assumes bisim: "is_bisimulation as ps"
-assumes "(r, s) \<in> ps"
-shows "lang r = lang s"
-proof -
-  define ps' where "ps' = insert (Zero, Zero) ps"
-  from bisim have bisim': "is_bisimulation as ps'"
-    by (auto simp: ps'_def is_bisimulation_def)
-  let ?R = "\<lambda>K L. (\<exists>(r,s)\<in>ps'. K = lang r \<and> L = lang s)"
-  show ?thesis
-  proof (rule language_coinduct[where R="?R"])
-    from \<open>(r, s) \<in> ps\<close> 
-    have "(r, s) \<in> ps'" by (auto simp: ps'_def)
-    thus "?R (lang r) (lang s)" by auto
-  next
-    fix K L assume "?R K L"
-    then obtain r s where rs: "(r, s) \<in> ps'"
-      and KL: "K = lang r" "L = lang s" by auto
-    with bisim' have "nullable r \<longleftrightarrow> nullable s"
-      by (auto simp: is_bisimulation_def)
-    thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff KL)
-    fix a
-    show "?R (Deriv a K) (Deriv a L)"
-    proof cases
-      assume "a \<in> set as"
-      with rs bisim'
-      have "(nderiv a r, nderiv a s) \<in> ps'"
-        by (auto simp: is_bisimulation_def)
-      thus ?thesis by (force simp: KL lang_nderiv)
-    next
-      assume "a \<notin> set as"
-      with bisim' rs
-      have "a \<notin> atoms r" "a \<notin> atoms s" by (auto simp: is_bisimulation_def)
-      then have "nderiv a r = Zero" "nderiv a s = Zero"
-        by (auto intro: deriv_no_occurrence)
-      then have "Deriv a K = lang Zero" 
-        "Deriv a L = lang Zero" 
-        unfolding KL lang_nderiv[symmetric] by auto
-      thus ?thesis by (auto simp: ps'_def)
-    qed
-  qed  
-qed
-
-subsection \<open>Closure computation\<close>
-
-definition closure ::
-  "'a::order list \<Rightarrow> 'a rexp_pair \<Rightarrow> ('a rexp_pairs * 'a rexp_pair set) option"
-where
-"closure as = rtrancl_while (%(r,s). nullable r = nullable s)
-  (%(r,s). map (\<lambda>a. (nderiv a r, nderiv a s)) as)"
-
-definition pre_bisim :: "'a::order list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp \<Rightarrow>
- 'a rexp_pairs * 'a rexp_pair set \<Rightarrow> bool"
-where
-"pre_bisim as r s = (\<lambda>(ws,R).
- (r,s) \<in> R \<and> set ws \<subseteq> R \<and>
- (\<forall>(r,s)\<in> R. atoms r \<union> atoms s \<subseteq> set as) \<and>
- (\<forall>(r,s)\<in> R - set ws. (nullable r \<longleftrightarrow> nullable s) \<and>
-   (\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R)))"
-
-theorem closure_sound:
-assumes result: "closure as (r,s) = Some([],R)"
-and atoms: "atoms r \<union> atoms s \<subseteq> set as"
-shows "lang r = lang s"
-proof-
-  let ?test = "While_Combinator.rtrancl_while_test (%(r,s). nullable r = nullable s)"
-  let ?step = "While_Combinator.rtrancl_while_step (%(r,s). map (\<lambda>a. (nderiv a r, nderiv a s)) as)"
-  { fix st assume inv: "pre_bisim as r s st" and test: "?test st"
-    have "pre_bisim as r s (?step st)"
-    proof (cases st)
-      fix ws R assume "st = (ws, R)"
-      with test obtain r s t where st: "st = ((r, s) # t, R)" and "nullable r = nullable s"
-        by (cases ws) auto
-      with inv show ?thesis using atoms_nderiv[of _ r] atoms_nderiv[of _ s]
-        unfolding st rtrancl_while_test.simps rtrancl_while_step.simps pre_bisim_def Ball_def
-        by simp_all blast+
-    qed
- }
-  moreover
-  from atoms
-  have "pre_bisim as r s ([(r,s)],{(r,s)})" by (simp add: pre_bisim_def)
-  ultimately have pre_bisim_ps: "pre_bisim as r s ([],R)"
-    by (rule while_option_rule[OF _ result[unfolded closure_def rtrancl_while_def]])
-  then have "is_bisimulation as R" "(r, s) \<in> R"
-    by (auto simp: pre_bisim_def is_bisimulation_def)
-  thus "lang r = lang s" by (rule bisim_lang_eq)
-qed
-
-subsection \<open>Bisimulation-free proof of closure computation\<close>
-
-text\<open>The equivalence check can be viewed as the product construction
-of two automata. The state space is the reflexive transitive closure of
-the pair of next-state functions, i.e. derivatives.\<close>
-
-lemma rtrancl_nderiv_nderivs: defines "nderivs == foldl (%r a. nderiv a r)"
-shows "{((r,s),(nderiv a r,nderiv a s))| r s a. a : A}^* =
-       {((r,s),(nderivs r w,nderivs s w))| r s w. w : lists A}" (is "?L = ?R")
-proof-
-  note [simp] = nderivs_def
-  { fix r s r' s'
-    have "((r,s),(r',s')) : ?L \<Longrightarrow> ((r,s),(r',s')) : ?R"
-    proof(induction rule: converse_rtrancl_induct2)
-      case refl show ?case by (force intro!: foldl.simps(1)[symmetric])
-    next
-      case step thus ?case by(force intro!: foldl.simps(2)[symmetric])
-    qed
-  } moreover
-  { fix r s r' s'
-    { fix w have "\<forall>x\<in>set w. x \<in> A \<Longrightarrow> ((r, s), nderivs r w, nderivs s w) :?L"
-      proof(induction w rule: rev_induct)
-        case Nil show ?case by simp
-      next
-        case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
-      qed
-    } 
-    hence "((r,s),(r',s')) : ?R \<Longrightarrow> ((r,s),(r',s')) : ?L" by auto
-  } ultimately show ?thesis by (auto simp: in_lists_conv_set) blast
-qed
-
-lemma nullable_nderivs:
-  "nullable (foldl (%r a. nderiv a r) r w) = (w : lang r)"
-by (induct w arbitrary: r) (simp_all add: nullable_iff lang_nderiv Deriv_def)
-
-theorem closure_sound_complete:
-assumes result: "closure as (r,s) = Some(ws,R)"
-and atoms: "set as = atoms r \<union> atoms s"
-shows "ws = [] \<longleftrightarrow> lang r = lang s"
-proof -
-  have leq: "(lang r = lang s) =
-  (\<forall>(r',s') \<in> {((r0,s0),(nderiv a r0,nderiv a s0))| r0 s0 a. a : set as}^* `` {(r,s)}.
-    nullable r' = nullable s')"
-    by(simp add: atoms rtrancl_nderiv_nderivs Ball_def lang_eq_ext imp_ex nullable_nderivs
-         del:Un_iff)
-  have "{(x,y). y \<in> set ((\<lambda>(p,q). map (\<lambda>a. (nderiv a p, nderiv a q)) as) x)} =
-    {((r,s), nderiv a r, nderiv a s) |r s a. a \<in> set as}"
-    by auto
-  with atoms rtrancl_while_Some[OF result[unfolded closure_def]]
-  show ?thesis by (auto simp add: leq Ball_def split: if_splits)
-qed
-
-subsection \<open>The overall procedure\<close>
-
-primrec add_atoms :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "add_atoms Zero = id"
-| "add_atoms One = id"
-| "add_atoms (Atom a) = List.insert a"
-| "add_atoms (Plus r s) = add_atoms s o add_atoms r"
-| "add_atoms (Times r s) = add_atoms s o add_atoms r"
-| "add_atoms (Star r) = add_atoms r"
-
-lemma set_add_atoms: "set (add_atoms r as) = atoms r \<union> set as"
-by (induct r arbitrary: as) auto
-
-
-definition check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool" where
-"check_eqv r s =
-  (let nr = norm r; ns = norm s; as = add_atoms nr (add_atoms ns [])
-   in case closure as (nr, ns) of
-     Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
-
-lemma soundness: 
-assumes "check_eqv r s" shows "lang r = lang s"
-proof -
-  let ?nr = "norm r" let ?ns = "norm s"
-  let ?as = "add_atoms ?nr (add_atoms ?ns [])"
-  obtain R where 1: "closure ?as (?nr,?ns) = Some([],R)"
-    using assms by (auto simp: check_eqv_def Let_def split:option.splits list.splits)
-  then have "lang (norm r) = lang (norm s)"
-    by (rule closure_sound) (auto simp: set_add_atoms dest!: subsetD[OF atoms_norm])
-  thus "lang r = lang s" by simp
-qed
-
-text\<open>Test:\<close>
-lemma "check_eqv (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))"
-by eval
-
-end
diff --git a/Regular-Sets/Equivalence_Checking2.thy b/Regular-Sets/Equivalence_Checking2.thy
deleted file mode 100644
index 724a3cb..0000000
--- a/Regular-Sets/Equivalence_Checking2.thy
+++ /dev/null
@@ -1,318 +0,0 @@
-section \<open>Deciding Equivalence of Extended Regular Expressions\<close>
-
-theory Equivalence_Checking2
-imports Regular_Exp2 "HOL-Library.While_Combinator"
-begin
-
-subsection \<open>Term ordering\<close>
-
-fun le_rexp :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool"
-where
-  "le_rexp Zero _ = True"
-| "le_rexp _ Zero = False"
-| "le_rexp One _ = True"
-| "le_rexp _ One = False"
-| "le_rexp (Atom a) (Atom b) = (a <= b)"
-| "le_rexp (Atom _) _ = True"
-| "le_rexp _ (Atom _) = False"
-| "le_rexp (Star r) (Star s) = le_rexp r s"
-| "le_rexp (Star _) _ = True"
-| "le_rexp _ (Star _) = False"
-| "le_rexp (Not r) (Not s) = le_rexp r s"
-| "le_rexp (Not _) _ = True"
-| "le_rexp _ (Not _) = False"
-| "le_rexp (Plus r r') (Plus s s') =
-    (if r = s then le_rexp r' s' else le_rexp r s)"
-| "le_rexp (Plus _ _) _ = True"
-| "le_rexp _ (Plus _ _) = False"
-| "le_rexp (Times r r') (Times s s') =
-    (if r = s then le_rexp r' s' else le_rexp r s)"
-| "le_rexp (Times _ _) _ = True"
-| "le_rexp _ (Times _ _) = False"
-| "le_rexp (Inter r r') (Inter s s') =
-    (if r = s then le_rexp r' s' else le_rexp r s)"
-
-subsection \<open>Normalizing operations\<close>
-
-text \<open>associativity, commutativity, idempotence, zero\<close>
-
-fun nPlus :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
-where
-  "nPlus Zero r = r"
-| "nPlus r Zero = r"
-| "nPlus (Plus r s) t = nPlus r (nPlus s t)"
-| "nPlus r (Plus s t) =
-     (if r = s then (Plus s t)
-     else if le_rexp r s then Plus r (Plus s t)
-     else Plus s (nPlus r t))"
-| "nPlus r s =
-     (if r = s then r
-      else if le_rexp r s then Plus r s
-      else Plus s r)"
-
-lemma lang_nPlus[simp]: "lang S (nPlus r s) = lang S (Plus r s)"
-by (induct r s rule: nPlus.induct) auto
-
-text \<open>associativity, zero, one\<close>
-
-fun nTimes :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
-where
-  "nTimes Zero _ = Zero"
-| "nTimes _ Zero = Zero"
-| "nTimes One r = r"
-| "nTimes r One = r"
-| "nTimes (Times r s) t = Times r (nTimes s t)"
-| "nTimes r s = Times r s"
-
-lemma lang_nTimes[simp]: "lang S (nTimes r s) = lang S (Times r s)"
-by (induct r s rule: nTimes.induct) (auto simp: conc_assoc)
-
-text \<open>more optimisations:\<close>
-
-fun nInter :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
-where
-  "nInter Zero _ = Zero"
-| "nInter _ Zero = Zero"
-| "nInter r s = Inter r s"
-
-lemma lang_nInter[simp]: "lang S (nInter r s) = lang S (Inter r s)"
-by (induct r s rule: nInter.induct) (auto)
-
-primrec norm :: "nat rexp \<Rightarrow> nat rexp"
-where
-  "norm Zero = Zero"
-| "norm One = One"
-| "norm (Atom a) = Atom a"
-| "norm (Plus r s) = nPlus (norm r) (norm s)"
-| "norm (Times r s) = nTimes (norm r) (norm s)"
-| "norm (Star r) = Star (norm r)"
-| "norm (Not r) = Not (norm r)"
-| "norm (Inter r1 r2) = nInter (norm r1) (norm r2)"
-
-lemma lang_norm[simp]: "lang S (norm r) = lang S r"
-by (induct r) auto
-
-
-subsection \<open>Derivative\<close>
-
-primrec nderiv :: "nat \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
-where
-  "nderiv _ Zero = Zero"
-| "nderiv _ One = Zero"
-| "nderiv a (Atom b) = (if a = b then One else Zero)"
-| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)"
-| "nderiv a (Times r s) =
-    (let r's = nTimes (nderiv a r) s
-     in if nullable r then nPlus r's (nderiv a s) else r's)"
-| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)"
-| "nderiv a (Not r) = Not (nderiv a r)"
-| "nderiv a (Inter r1 r2) = nInter (nderiv a r1) (nderiv a r2)"
-
-lemma lang_nderiv: "a:S \<Longrightarrow> lang S (nderiv a r) = Deriv a (lang S r)"
-by (induct r) (auto simp: Let_def nullable_iff[where S=S])
-
-lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \<union> atoms s"
-by (induct r s rule: nPlus.induct) auto
-
-lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
-by (induct r s rule: nTimes.induct) auto
-
-lemma atoms_nInter: "atoms (nInter r s) \<subseteq> atoms r \<union> atoms s"
-by (induct r s rule: nInter.induct) auto
-
-lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
-by (induct r) (auto dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
-
-lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
-by (induct r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
-
-
-subsection \<open>Bisimulation between languages and regular expressions\<close>
-
-context
-fixes S :: "'a set"
-begin
-
-coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
-"K \<subseteq> lists S \<Longrightarrow> L \<subseteq> lists S
- \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L) 
- \<Longrightarrow> (\<And>x. x:S \<Longrightarrow> bisimilar (Deriv x K) (Deriv x L))
- \<Longrightarrow> bisimilar K L"
-
-lemma equal_if_bisimilar:
-assumes "K \<subseteq> lists S" "L \<subseteq> lists S" "bisimilar K L" shows "K = L"
-proof (rule set_eqI)
-  fix w
-  from assms show "w \<in> K \<longleftrightarrow> w \<in> L"
-  proof (induction w arbitrary: K L)
-    case Nil thus ?case by (auto elim: bisimilar.cases)
-  next
-    case (Cons a w K L)
-    show ?case
-    proof cases
-      assume "a : S"
-      with \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
-        by (auto elim: bisimilar.cases)
-      then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L"
-        by (metis Cons.IH bisimilar.cases)
-      thus ?case by (auto simp: Deriv_def)
-    next
-      assume "a \<notin> S"
-      thus ?case using Cons.prems by auto
-    qed
-  qed
-qed
-
-lemma language_coinduct:
-fixes R (infixl "\<sim>" 50)
-assumes "\<And>K L. K \<sim> L \<Longrightarrow> K \<subseteq> lists S \<and> L \<subseteq> lists S"
-assumes "K \<sim> L"
-assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
-assumes "\<And>K L x. K \<sim> L \<Longrightarrow> x : S \<Longrightarrow> Deriv x K \<sim> Deriv x L"
-shows "K = L"
-apply (rule equal_if_bisimilar)
-apply (metis assms(1) assms(2))
-apply (metis assms(1) assms(2))
-apply (rule bisimilar.coinduct[of R, OF \<open>K \<sim> L\<close>])
-apply (auto simp: assms)
-done
-
-end
-
-type_synonym rexp_pair = "nat rexp * nat rexp"
-type_synonym rexp_pairs = "rexp_pair list"
-
-definition is_bisimulation :: "nat list \<Rightarrow> rexp_pairs \<Rightarrow> bool"
-where
-"is_bisimulation as ps =
-  (\<forall>(r,s)\<in> set ps. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
-    (\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps))"
-
-
-lemma bisim_lang_eq:
-assumes bisim: "is_bisimulation as ps"
-assumes "(r, s) \<in> set ps"
-shows "lang (set as) r = lang (set as) s"
-proof -
-  let ?R = "\<lambda>K L. (\<exists>(r,s)\<in>set ps. K = lang (set as) r \<and> L = lang (set as) s)"
-  show ?thesis
-  proof (rule language_coinduct[where R="?R" and S = "set as"])
-    from \<open>(r, s) \<in> set ps\<close> show "?R (lang (set as) r) (lang (set as) s)"
-      by auto
-  next
-    fix K L assume "?R K L"
-    then obtain r s where rs: "(r, s) \<in> set ps"
-      and KL: "K = lang (set as) r" "L = lang (set as) s" by auto
-    with bisim have "nullable r \<longleftrightarrow> nullable s"
-      by (auto simp: is_bisimulation_def)
-    thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff[where S="set as"] KL)
-  txt\<open>next case, but shared context\<close>
-    from bisim rs KL lang_subset_lists[of _ "set as"]
-    show "K \<subseteq> lists (set as) \<and> L \<subseteq> lists (set as)"
-      unfolding is_bisimulation_def by blast
-  txt\<open>next case, but shared context\<close>
-    fix a assume "a \<in> set as"
-    with rs bisim
-    have "(nderiv a r, nderiv a s) \<in> set ps"
-      by (auto simp: is_bisimulation_def)
-    thus "?R (Deriv a K) (Deriv a L)" using \<open>a \<in> set as\<close>
-      by (force simp: KL lang_nderiv)
-  qed
-qed
-
-subsection \<open>Closure computation\<close>
-
-fun test :: "rexp_pairs * rexp_pairs \<Rightarrow> bool"
-where "test (ws, ps) = (case ws of [] \<Rightarrow>  False | (p,q)#_ \<Rightarrow> nullable p = nullable q)"
-
-fun step :: "nat list \<Rightarrow> rexp_pairs * rexp_pairs \<Rightarrow> rexp_pairs * rexp_pairs"
-where "step as (ws,ps) =
-    (let 
-      (r, s) = hd ws;
-      ps' = (r, s) # ps;
-      succs = map (\<lambda>a. (nderiv a r, nderiv a s)) as;
-      new = filter (\<lambda>p. p \<notin> set ps' \<union> set ws) succs
-    in (new @ tl ws, ps'))"
-
-definition closure ::
-  "nat list \<Rightarrow> rexp_pairs * rexp_pairs
-   \<Rightarrow> (rexp_pairs * rexp_pairs) option" where
-"closure as = while_option test (step as)"
-
-definition pre_bisim :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow>
- rexp_pairs * rexp_pairs \<Rightarrow> bool"
-where
-"pre_bisim as r s = (\<lambda>(ws,ps).
- ((r, s) \<in> set ws \<union> set ps) \<and>
- (\<forall>(r,s)\<in> set ws \<union> set ps. atoms r \<union> atoms s \<subseteq> set as) \<and>
- (\<forall>(r,s)\<in> set ps. (nullable r \<longleftrightarrow> nullable s) \<and>
-   (\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps \<union> set ws)))"
-
-theorem closure_sound:
-assumes result: "closure as ([(r,s)],[]) = Some([],ps)"
-and atoms: "atoms r \<union> atoms s \<subseteq> set as"
-shows "lang (set as) r = lang (set as) s"
-proof-
-  { fix st have "pre_bisim as r s st \<Longrightarrow> test st \<Longrightarrow> pre_bisim as r s (step as st)"
-      unfolding pre_bisim_def
-      by (cases st) (auto simp: split_def split: list.splits prod.splits
-        dest!: subsetD[OF atoms_nderiv]) }
-  moreover
-  from atoms
-  have "pre_bisim as r s ([(r,s)],[])" by (simp add: pre_bisim_def)
-  ultimately have pre_bisim_ps: "pre_bisim as r s ([],ps)"
-    by (rule while_option_rule[OF _ result[unfolded closure_def]])
-  then have "is_bisimulation as ps" "(r, s) \<in> set ps"
-    by (auto simp: pre_bisim_def is_bisimulation_def)
-  thus "lang (set as) r = lang (set as) s" by (rule bisim_lang_eq)
-qed
-
-
-subsection \<open>The overall procedure\<close>
-
-primrec add_atoms :: "nat rexp \<Rightarrow> nat list \<Rightarrow> nat list"
-where
-  "add_atoms Zero = id"
-| "add_atoms One = id"
-| "add_atoms (Atom a) = List.insert a"
-| "add_atoms (Plus r s) = add_atoms s o add_atoms r"
-| "add_atoms (Times r s) = add_atoms s o add_atoms r"
-| "add_atoms (Not r) = add_atoms r"
-| "add_atoms (Inter r s) = add_atoms s o add_atoms r"
-| "add_atoms (Star r) = add_atoms r"
-
-lemma set_add_atoms: "set (add_atoms r as) = atoms r \<union> set as"
-by (induct r arbitrary: as) auto
-
-definition check_eqv :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool"
-where
-"check_eqv as r s \<longleftrightarrow> set(add_atoms r (add_atoms s [])) \<subseteq> set as \<and>
-  (case closure as ([(norm r, norm s)], []) of
-     Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
-
-lemma soundness: 
-assumes "check_eqv as r s" shows "lang (set as) r = lang (set as) s"
-proof -
-  obtain ps where cl: "closure as ([(norm r,norm s)],[]) = Some([],ps)"
-    and at: "atoms r \<union> atoms s \<subseteq> set as"
-    using assms
-    by (auto simp: check_eqv_def set_add_atoms split:option.splits list.splits)
-  hence "atoms(norm r) \<union> atoms(norm s) \<subseteq> set as"
-    using atoms_norm by blast
-  hence "lang (set as) (norm r) = lang (set as) (norm s)"
-    by (rule closure_sound[OF cl])
-  thus "lang (set as) r = lang (set as) s" by simp
-qed
-
-lemma "check_eqv [0] (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))"
-by eval
-
-lemma "check_eqv [0,1] (Not(Atom 0))
-  (Plus One (Times (Plus (Atom 1) (Times (Atom 0) (Plus (Atom 0) (Atom 1))))
-                   (Star(Plus (Atom 0) (Atom 1)))))"
-by eval
-
-lemma "check_eqv [0] (Atom 0) (Inter (Star (Atom 0)) (Atom 0))"
-by eval
-
-end
diff --git a/Regular-Sets/NDerivative.thy b/Regular-Sets/NDerivative.thy
deleted file mode 100644
index 7a9ef1a..0000000
--- a/Regular-Sets/NDerivative.thy
+++ /dev/null
@@ -1,85 +0,0 @@
-section \<open>Normalizing Derivative\<close>
-
-theory NDerivative
-imports
-  Regular_Exp
-begin
-
-subsection \<open>Normalizing operations\<close>
-
-text \<open>associativity, commutativity, idempotence, zero\<close>
-
-fun nPlus :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "nPlus Zero r = r"
-| "nPlus r Zero = r"
-| "nPlus (Plus r s) t = nPlus r (nPlus s t)"
-| "nPlus r (Plus s t) =
-     (if r = s then (Plus s t)
-     else if le_rexp r s then Plus r (Plus s t)
-     else Plus s (nPlus r t))"
-| "nPlus r s =
-     (if r = s then r
-      else if le_rexp r s then Plus r s
-      else Plus s r)"
-
-lemma lang_nPlus[simp]: "lang (nPlus r s) = lang (Plus r s)"
-by (induction r s rule: nPlus.induct) auto
-
-text \<open>associativity, zero, one\<close>
-
-fun nTimes :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "nTimes Zero _ = Zero"
-| "nTimes _ Zero = Zero"
-| "nTimes One r = r"
-| "nTimes r One = r"
-| "nTimes (Times r s) t = Times r (nTimes s t)"
-| "nTimes r s = Times r s"
-
-lemma lang_nTimes[simp]: "lang (nTimes r s) = lang (Times r s)"
-by (induction r s rule: nTimes.induct) (auto simp: conc_assoc)
-
-primrec norm :: "'a::order rexp \<Rightarrow> 'a rexp"
-where
-  "norm Zero = Zero"
-| "norm One = One"
-| "norm (Atom a) = Atom a"
-| "norm (Plus r s) = nPlus (norm r) (norm s)"
-| "norm (Times r s) = nTimes (norm r) (norm s)"
-| "norm (Star r) = Star (norm r)"
-
-lemma lang_norm[simp]: "lang (norm r) = lang r"
-by (induct r) auto
-
-primrec nderiv :: "'a::order \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "nderiv _ Zero = Zero"
-| "nderiv _ One = Zero"
-| "nderiv a (Atom b) = (if a = b then One else Zero)"
-| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)"
-| "nderiv a (Times r s) =
-    (let r's = nTimes (nderiv a r) s
-     in if nullable r then nPlus r's (nderiv a s) else r's)"
-| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)"
-
-lemma lang_nderiv: "lang (nderiv a r) = Deriv a (lang r)"
-by (induction r) (auto simp: Let_def nullable_iff)
-
-lemma deriv_no_occurrence: 
-  "x \<notin> atoms r \<Longrightarrow> nderiv x r = Zero"
-by (induction r) auto
-
-lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \<union> atoms s"
-by (induction r s rule: nPlus.induct) auto
-
-lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
-by (induction r s rule: nTimes.induct) auto
-
-lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
-by (induction r) (auto dest!:subsetD[OF atoms_nTimes])
-
-lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
-by (induction r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes])
-
-end
diff --git a/Regular-Sets/ROOT b/Regular-Sets/ROOT
deleted file mode 100644
index 423f5d3..0000000
--- a/Regular-Sets/ROOT
+++ /dev/null
@@ -1,12 +0,0 @@
-chapter AFP
-
-session "Regular-Sets" (AFP) = "HOL-Library" +
-  options [timeout = 600]
-  theories
-    Regexp_Method
-    Regexp_Constructions
-    pEquivalence_Checking
-    Equivalence_Checking2
-  document_files
-    "root.bib"
-    "root.tex"
diff --git a/Regular-Sets/Regexp_Constructions.thy b/Regular-Sets/Regexp_Constructions.thy
deleted file mode 100644
index 2e2dceb..0000000
--- a/Regular-Sets/Regexp_Constructions.thy
+++ /dev/null
@@ -1,395 +0,0 @@
-(*
-  File:     Regexp_Constructions.thy
-  Author:   Manuel Eberl <eberlm@in.tum.de>
-
-  Some simple constructions on regular expressions to illustrate closure properties of regular
-  languages: reversal, substitution, prefixes, suffixes, subwords ("fragments")
-*)
-section \<open>Basic constructions on regular expressions\<close>
-theory Regexp_Constructions
-imports
-  Main
-  "HOL-Library.Sublist"
-  Regular_Exp
-begin
-
-subsection \<open>Reverse language\<close>
-
-lemma rev_conc [simp]: "rev ` (A @@ B) = rev ` B @@ rev ` A"
-  unfolding conc_def image_def by force
-
-lemma rev_compower [simp]: "rev ` (A ^^ n) = (rev ` A) ^^ n"
-  by (induction n) (simp_all add: conc_pow_comm)
-
-lemma rev_star [simp]: "rev ` star A = star (rev ` A)"
-  by (simp add: star_def image_UN)
-
-
-subsection \<open>Substituting characters in a language\<close>    
-
-definition subst_word :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
-  "subst_word f xs = concat (map f xs)"
-  
-lemma subst_word_Nil [simp]: "subst_word f [] = []"
-  by (simp add: subst_word_def)
-    
-lemma subst_word_singleton [simp]: "subst_word f [x] = f x"
-  by (simp add: subst_word_def)
-    
-lemma subst_word_append [simp]: "subst_word f (xs @ ys) = subst_word f xs @ subst_word f ys"
-  by (simp add: subst_word_def)
-    
-lemma subst_word_Cons [simp]: "subst_word f (x # xs) = f x @ subst_word f xs"
-  by (simp add: subst_word_def)
-    
-lemma subst_word_conc [simp]: "subst_word f ` (A @@ B) = subst_word f ` A @@ subst_word f ` B"
-  unfolding conc_def image_def by force 
-
-lemma subst_word_compower [simp]: "subst_word f ` (A ^^ n) = (subst_word f ` A) ^^ n"
-  by (induction n) simp_all
-    
-lemma subst_word_star [simp]: "subst_word f ` (star A) = star (subst_word f ` A)"
-  by (simp add: star_def image_UN)
-    
-
-text \<open>Suffix language\<close>
-
-definition Suffixes :: "'a list set \<Rightarrow> 'a list set" where
-  "Suffixes A = {w. \<exists>q. q @ w \<in> A}"
-
-lemma Suffixes_altdef [code]: "Suffixes A = (\<Union>w\<in>A. set (suffixes w))"
-  unfolding Suffixes_def set_suffixes_eq suffix_def by blast
-
-lemma Nil_in_Suffixes_iff [simp]: "[] \<in> Suffixes A \<longleftrightarrow> A \<noteq> {}"
-  by (auto simp: Suffixes_def)
-
-lemma Suffixes_empty [simp]: "Suffixes {} = {}"
-  by (auto simp: Suffixes_def)
-    
-lemma Suffixes_empty_iff [simp]: "Suffixes A = {} \<longleftrightarrow> A = {}"
-  by (auto simp: Suffixes_altdef)
-    
-lemma Suffixes_singleton [simp]: "Suffixes {xs} = set (suffixes xs)"
-  by (auto simp: Suffixes_altdef)
-    
-lemma Suffixes_insert: "Suffixes (insert xs A) = set (suffixes xs) \<union> Suffixes A"
-  by (simp add: Suffixes_altdef)
-
-lemma Suffixes_conc [simp]: "A \<noteq> {} \<Longrightarrow> Suffixes (A @@ B) = Suffixes B \<union> (Suffixes A @@ B)"
-  unfolding Suffixes_altdef conc_def by (force simp: suffix_append)
-    
-lemma Suffixes_union [simp]: "Suffixes (A \<union> B) = Suffixes A \<union> Suffixes B"
-  by (auto simp: Suffixes_def)
-  
-lemma Suffixes_UNION [simp]: "Suffixes (UNION A f) = UNION A (\<lambda>x. Suffixes (f x))"
-  by (auto simp: Suffixes_def)
-
-lemma Suffixes_compower: 
-  assumes "A \<noteq> {}"
-  shows   "Suffixes (A ^^ n) = insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k))"
-proof (induction n)
-  case (Suc n)
-  from Suc have "Suffixes (A ^^ Suc n) = 
-                   insert [] (Suffixes A @@ ((\<Union>k<n. A ^^ k) \<union> A ^^ n))"
-    by (simp_all add: assms conc_Un_distrib)
-  also have "(\<Union>k<n. A ^^ k) \<union> A ^^ n = (\<Union>k\<in>insert n {..<n}. A ^^ k)"  by blast
-  also have "insert n {..<n} = {..<Suc n}" by auto
-  finally show ?case .
-qed simp_all
-
-lemma Suffixes_star [simp]: 
-  assumes "A \<noteq> {}"
-  shows   "Suffixes (star A) = Suffixes A @@ star A"
-proof -
-  have "star A = (\<Union>n. A ^^ n)" unfolding star_def ..
-  also have "Suffixes \<dots> = (\<Union>x. Suffixes (A ^^ x))" by simp
-  also have "\<dots> = (\<Union>n. insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k)))"
-    using assms by (subst Suffixes_compower) auto
-  also have "\<dots> = insert [] (Suffixes A @@ (\<Union>n. (\<Union>k<n. A ^^ k)))"
-    by (simp_all add: conc_UNION_distrib)
-  also have "(\<Union>n. (\<Union>k<n. A ^^ k)) = (\<Union>n. A ^^ n)" by auto
-  also have "\<dots> = star A" unfolding star_def ..
-  also have "insert [] (Suffixes A @@ star A) = Suffixes A @@ star A" 
-    using assms by auto
-  finally show ?thesis .
-qed
-  
-text \<open>Prefix language\<close>
-
-definition Prefixes :: "'a list set \<Rightarrow> 'a list set" where
-  "Prefixes A = {w. \<exists>q. w @ q \<in> A}"
-
-lemma Prefixes_altdef [code]: "Prefixes A = (\<Union>w\<in>A. set (prefixes w))"
-  unfolding Prefixes_def set_prefixes_eq prefix_def by blast
-
-lemma Nil_in_Prefixes_iff [simp]: "[] \<in> Prefixes A \<longleftrightarrow> A \<noteq> {}"
-  by (auto simp: Prefixes_def)
-
-lemma Prefixes_empty [simp]: "Prefixes {} = {}"
-  by (auto simp: Prefixes_def)
-    
-lemma Prefixes_empty_iff [simp]: "Prefixes A = {} \<longleftrightarrow> A = {}"
-  by (auto simp: Prefixes_altdef)
-    
-lemma Prefixes_singleton [simp]: "Prefixes {xs} = set (prefixes xs)"
-  by (auto simp: Prefixes_altdef)
-    
-lemma Prefixes_insert: "Prefixes (insert xs A) = set (prefixes xs) \<union> Prefixes A"
-  by (simp add: Prefixes_altdef)
-
-lemma Prefixes_conc [simp]: "B \<noteq> {} \<Longrightarrow> Prefixes (A @@ B) = Prefixes A \<union> (A @@ Prefixes B)"
-  unfolding Prefixes_altdef conc_def by (force simp: prefix_append)
-    
-lemma Prefixes_union [simp]: "Prefixes (A \<union> B) = Prefixes A \<union> Prefixes B"
-  by (auto simp: Prefixes_def)
-  
-lemma Prefixes_UNION [simp]: "Prefixes (UNION A f) = UNION A (\<lambda>x. Prefixes (f x))"
-  by (auto simp: Prefixes_def)
-
-
-lemma Prefixes_rev: "Prefixes (rev ` A) = rev ` Suffixes A"
-  by (auto simp: Prefixes_altdef prefixes_rev Suffixes_altdef)
-
-lemma Suffixes_rev: "Suffixes (rev ` A) = rev ` Prefixes A"
-  by (auto simp: Prefixes_altdef suffixes_rev Suffixes_altdef)    
-
-
-lemma Prefixes_compower:
-  assumes "A \<noteq> {}"
-  shows   "Prefixes (A ^^ n) = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
-proof -
-  have "A ^^ n = rev ` ((rev ` A) ^^ n)" by (simp add: image_image)
-  also have "Prefixes \<dots> = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
-    unfolding Prefixes_rev 
-    by (subst Suffixes_compower) (simp_all add: image_UN image_image Suffixes_rev assms)
-  finally show ?thesis .
-qed
-
-lemma Prefixes_star [simp]:
-  assumes "A \<noteq> {}"
-  shows   "Prefixes (star A) = star A @@ Prefixes A"
-proof -
-  have "star A = rev ` star (rev ` A)" by (simp add: image_image)
-  also have "Prefixes \<dots> = star A @@ Prefixes A"
-    unfolding Prefixes_rev
-    by (subst Suffixes_star) (simp_all add: assms image_image Suffixes_rev)
-  finally show ?thesis .
-qed
-  
-
-subsection \<open>Subword language\<close>
-
-text \<open>
-  The language of all sub-words, i.e. all words that are a contiguous sublist of a word in
-  the original language.
-\<close>
-definition Sublists :: "'a list set \<Rightarrow> 'a list set" where
-  "Sublists A = {w. \<exists>q\<in>A. sublist w q}"
-
-lemma Sublists_altdef [code]: "Sublists A = (\<Union>w\<in>A. set (sublists w))"
-  by (auto simp: Sublists_def)
-
-lemma Sublists_empty [simp]: "Sublists {} = {}"
-  by (auto simp: Sublists_def)
-    
-lemma Sublists_singleton [simp]: "Sublists {w} = set (sublists w)"
-  by (auto simp: Sublists_altdef)
-
-lemma Sublists_insert: "Sublists (insert w A) = set (sublists w) \<union> Sublists A"
-  by (auto simp: Sublists_altdef)
-    
-lemma Sublists_Un [simp]: "Sublists (A \<union> B) = Sublists A \<union> Sublists B"
-  by (auto simp: Sublists_altdef)
-
-lemma Sublists_UN [simp]: "Sublists (UNION A f) = UNION A (\<lambda>x. Sublists (f x))"
-  by (auto simp: Sublists_altdef)
-
-lemma Sublists_conv_Prefixes: "Sublists A = Prefixes (Suffixes A)"
-  by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def)
-    
-lemma Sublists_conv_Suffixes: "Sublists A = Suffixes (Prefixes A)"
-  by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def)
-
-lemma Sublists_conc [simp]: 
-  assumes "A \<noteq> {}" "B \<noteq> {}"
-  shows   "Sublists (A @@ B) = Sublists A \<union> Sublists B \<union> Suffixes A @@ Prefixes B"
-  using assms unfolding Sublists_conv_Suffixes by auto
-
-lemma star_not_empty [simp]: "star A \<noteq> {}"
-  by auto
-    
-lemma Sublists_star:
-  "A \<noteq> {} \<Longrightarrow> Sublists (star A) = Sublists A \<union> Suffixes A @@ star A @@ Prefixes A"
-  by (simp add: Sublists_conv_Prefixes)
-
-lemma Prefixes_subset_Sublists: "Prefixes A \<subseteq> Sublists A"
-  unfolding Prefixes_def Sublists_def by auto
-
-lemma Suffixes_subset_Sublists: "Suffixes A \<subseteq> Sublists A"
-  unfolding Suffixes_def Sublists_def by auto
-
-
-subsection \<open>Fragment language\<close>
-  
-text \<open>
-  The following is the fragment language of a given language, i.e. the set of all words that
-  are (not necessarily contiguous) sub-sequences of a word in the original language.
-\<close>
-definition Subseqs where "Subseqs A = (\<Union>w\<in>A. set (subseqs w))"
-
-lemma Subseqs_empty [simp]: "Subseqs {} = {}"
-  by (simp add: Subseqs_def)
-
-lemma Subseqs_insert [simp]: "Subseqs (insert xs A) = set (subseqs xs) \<union> Subseqs A"
-  by (simp add: Subseqs_def)
-    
-lemma Subseqs_singleton [simp]: "Subseqs {xs} = set (subseqs xs)"
-  by simp
-    
-lemma Subseqs_Un [simp]: "Subseqs (A \<union> B) = Subseqs A \<union> Subseqs B"
-  by (simp add: Subseqs_def)
-    
-lemma Subseqs_UNION [simp]: "Subseqs (UNION A f) = UNION A (\<lambda>x. Subseqs (f x))"
-  by (simp add: Subseqs_def)
-  
-lemma Subseqs_conc [simp]: "Subseqs (A @@ B) = Subseqs A @@ Subseqs B"
-proof safe
-  fix xs assume "xs \<in> Subseqs (A @@ B)"
-  then obtain ys zs where *: "ys \<in> A" "zs \<in> B" "subseq xs (ys @ zs)" 
-    by (auto simp: Subseqs_def conc_def)
-  from *(3) obtain xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs"
-    by (rule subseq_appendE)
-  with *(1,2) show "xs \<in> Subseqs A @@ Subseqs B" by (auto simp: Subseqs_def set_subseqs_eq)
-next
-  fix xs assume "xs \<in> Subseqs A @@ Subseqs B"
-  then obtain xs1 xs2 ys zs 
-    where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" "ys \<in> A" "zs \<in> B"
-    by (auto simp: conc_def Subseqs_def)
-  thus "xs \<in> Subseqs (A @@ B)" by (force simp: Subseqs_def conc_def intro: list_emb_append_mono)
-qed
-
-lemma Subseqs_compower [simp]: "Subseqs (A ^^ n) = Subseqs A ^^ n"
-  by (induction n) simp_all
-    
-lemma Subseqs_star [simp]: "Subseqs (star A) = star (Subseqs A)"
-  by (simp add: star_def)
-    
-lemma Sublists_subset_Subseqs: "Sublists A \<subseteq> Subseqs A"
-  by (auto simp: Sublists_def Subseqs_def dest!: sublist_imp_subseq)
-
-
-subsection \<open>Various regular expression constructions\<close>
-
-text \<open>A construction for language reversal of a regular expression:\<close>
-
-primrec rexp_rev where
-  "rexp_rev Zero = Zero"
-| "rexp_rev One = One"
-| "rexp_rev (Atom x) = Atom x"
-| "rexp_rev (Plus r s) = Plus (rexp_rev r) (rexp_rev s)"
-| "rexp_rev (Times r s) = Times (rexp_rev s) (rexp_rev r)"
-| "rexp_rev (Star r) = Star (rexp_rev r)"
-
-lemma lang_rexp_rev [simp]: "lang (rexp_rev r) = rev ` lang r"
-  by (induction r) (simp_all add: image_Un)  
-    
-
-text \<open>The obvious construction for a singleton-language regular expression:\<close>
-
-fun rexp_of_word where
-  "rexp_of_word [] = One"
-| "rexp_of_word [x] = Atom x"
-| "rexp_of_word (x#xs) = Times (Atom x) (rexp_of_word xs)"
-  
-lemma lang_rexp_of_word [simp]: "lang (rexp_of_word xs) = {xs}"
-  by (induction xs rule: rexp_of_word.induct) (simp_all add: conc_def)
-
-lemma size_rexp_of_word [simp]: "size (rexp_of_word xs) = Suc (2 * (length xs - 1))"
-  by (induction xs rule: rexp_of_word.induct) auto
-
-
-text \<open>Character substitution in a regular expression:\<close>
-
-primrec rexp_subst where
-  "rexp_subst f Zero = Zero"
-| "rexp_subst f One = One"
-| "rexp_subst f (Atom x) = rexp_of_word (f x)"
-| "rexp_subst f (Plus r s) = Plus (rexp_subst f r) (rexp_subst f s)"
-| "rexp_subst f (Times r s) = Times (rexp_subst f r) (rexp_subst f s)"
-| "rexp_subst f (Star r) = Star (rexp_subst f r)"
-
-lemma lang_rexp_subst: "lang (rexp_subst f r) = subst_word f ` lang r"
-  by (induction r) (simp_all add: image_Un)
-
-
-text \<open>Suffix language of a regular expression:\<close>
-
-primrec suffix_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
-  "suffix_rexp Zero = Zero"
-| "suffix_rexp One = One"
-| "suffix_rexp (Atom a) = Plus (Atom a) One"
-| "suffix_rexp (Plus r s) = Plus (suffix_rexp r) (suffix_rexp s)"
-| "suffix_rexp (Times r s) =
-    (if rexp_empty r then Zero else Plus (Times (suffix_rexp r) s) (suffix_rexp s))"
-| "suffix_rexp (Star r) =
-    (if rexp_empty r then One else Times (suffix_rexp r) (Star r))"
-
-theorem lang_suffix_rexp [simp]:
-  "lang (suffix_rexp r) = Suffixes (lang r)"
-  by (induction r) (auto simp: rexp_empty_iff)
-
-
-text \<open>Prefix language of a regular expression:\<close>
-
-primrec prefix_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
-  "prefix_rexp Zero = Zero"
-| "prefix_rexp One = One"
-| "prefix_rexp (Atom a) = Plus (Atom a) One"
-| "prefix_rexp (Plus r s) = Plus (prefix_rexp r) (prefix_rexp s)"
-| "prefix_rexp (Times r s) =
-    (if rexp_empty s then Zero else Plus (Times r (prefix_rexp s)) (prefix_rexp r))"
-| "prefix_rexp (Star r) =
-    (if rexp_empty r then One else Times (Star r) (prefix_rexp r))"
-
-theorem lang_prefix_rexp [simp]:
-  "lang (prefix_rexp r) = Prefixes (lang r)"
-  by (induction r) (auto simp: rexp_empty_iff)
-
-
-text \<open>Sub-word language of a regular expression\<close>    
-
-primrec sublist_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
-  "sublist_rexp Zero = Zero"
-| "sublist_rexp One = One"
-| "sublist_rexp (Atom a) = Plus (Atom a) One"
-| "sublist_rexp (Plus r s) = Plus (sublist_rexp r) (sublist_rexp s)"
-| "sublist_rexp (Times r s) =
-    (if rexp_empty r \<or> rexp_empty s then Zero else 
-       Plus (sublist_rexp r) (Plus (sublist_rexp s) (Times (suffix_rexp r) (prefix_rexp s))))"
-| "sublist_rexp (Star r) =
-    (if rexp_empty r then One else 
-       Plus (sublist_rexp r) (Times (suffix_rexp r) (Times (Star r) (prefix_rexp r))))"
-
-theorem lang_sublist_rexp [simp]:
-  "lang (sublist_rexp r) = Sublists (lang r)"
-  by (induction r) (auto simp: rexp_empty_iff Sublists_star)
-
-
-text \<open>Fragment language of a regular expression:\<close>
-  
-primrec subseqs_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
-  "subseqs_rexp Zero = Zero"
-| "subseqs_rexp One = One"
-| "subseqs_rexp (Atom x) = Plus (Atom x) One"
-| "subseqs_rexp (Plus r s) = Plus (subseqs_rexp r) (subseqs_rexp s)"
-| "subseqs_rexp (Times r s) = Times (subseqs_rexp r) (subseqs_rexp s)"
-| "subseqs_rexp (Star r) = Star (subseqs_rexp r)"
-
-lemma lang_subseqs_rexp [simp]: "lang (subseqs_rexp r) = Subseqs (lang r)"
-  by (induction r) auto
-
-
-text \<open>Subword language of a regular expression\<close>
-
-
-end
diff --git a/Regular-Sets/Regexp_Method.thy b/Regular-Sets/Regexp_Method.thy
deleted file mode 100644
index c0ef10c..0000000
--- a/Regular-Sets/Regexp_Method.thy
+++ /dev/null
@@ -1,67 +0,0 @@
-section \<open>Proving Relation (In)equalities via Regular Expressions\<close>
-
-theory Regexp_Method
-imports Equivalence_Checking Relation_Interpretation
-begin
-
-primrec rel_of_regexp :: "('a * 'a) set list \<Rightarrow> nat rexp \<Rightarrow> ('a * 'a) set" where
-"rel_of_regexp vs Zero  = {}" |
-"rel_of_regexp vs One  = Id" |
-"rel_of_regexp vs (Atom i)  = vs ! i" |
-"rel_of_regexp vs (Plus r s)  = rel_of_regexp vs r  \<union> rel_of_regexp vs s " |
-"rel_of_regexp vs (Times r s)  = rel_of_regexp vs r O rel_of_regexp vs s" |
-"rel_of_regexp vs (Star r)  = (rel_of_regexp vs r)^*"
-
-lemma rel_of_regexp_rel: "rel_of_regexp vs r = rel (\<lambda>i. vs ! i) r"
-by (induct r) auto
-
-primrec rel_eq where
-"rel_eq (r, s) vs = (rel_of_regexp vs r = rel_of_regexp vs s)"
-
-lemma rel_eqI: "check_eqv r s \<Longrightarrow> rel_eq (r, s) vs"
-unfolding rel_eq.simps rel_of_regexp_rel
-by (rule Relation_Interpretation.soundness)
- (rule Equivalence_Checking.soundness)
-
-lemmas regexp_reify = rel_of_regexp.simps rel_eq.simps
-lemmas regexp_unfold = trancl_unfold_left subset_Un_eq
-
-ML \<open>
-local
-
-fun check_eqv (ct, b) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop"}
-  ct (if b then @{cterm True} else @{cterm False});
-
-val (_, check_eqv_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (@{binding check_eqv}, check_eqv)));
-
-in
-
-val regexp_conv =
-  @{computation_conv bool terms: check_eqv datatypes: "nat rexp"}
-  (fn _ => fn b => fn ct => check_eqv_oracle (ct, b))
-
-end
-\<close>
-  
-method_setup regexp = \<open>
-  Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (
-      (TRY o eresolve_tac ctxt @{thms rev_subsetD})
-      THEN' (Subgoal.FOCUS_PARAMS (fn {context = ctxt', ...} =>
-        TRY (Local_Defs.unfold_tac ctxt' @{thms regexp_unfold})
-        THEN Reification.tac ctxt' @{thms regexp_reify} NONE 1
-        THEN resolve_tac ctxt' @{thms rel_eqI} 1
-        THEN CONVERSION (HOLogic.Trueprop_conv (regexp_conv ctxt')) 1
-        THEN resolve_tac ctxt' [TrueI] 1) ctxt)))
-\<close> \<open>decide relation equalities via regular expressions\<close>
-
-hide_const (open) le_rexp nPlus nTimes norm nullable bisimilar is_bisimulation closure
-  pre_bisim add_atoms check_eqv rel word_rel rel_eq
-
-text \<open>Example:\<close>
-
-lemma "(r \<union> s^+)^* = (r \<union> s)^*"
-  by regexp
-
-end
diff --git a/Regular-Sets/Regular_Exp.thy b/Regular-Sets/Regular_Exp.thy
deleted file mode 100644
index 497ebe0..0000000
--- a/Regular-Sets/Regular_Exp.thy
+++ /dev/null
@@ -1,176 +0,0 @@
-(*  Author: Tobias Nipkow *)
-
-section "Regular expressions"
-
-theory Regular_Exp
-imports Regular_Set
-begin
-
-datatype (atoms: 'a) rexp =
-  is_Zero: Zero |
-  is_One: One |
-  Atom 'a |
-  Plus "('a rexp)" "('a rexp)" |
-  Times "('a rexp)" "('a rexp)" |
-  Star "('a rexp)"
-
-primrec lang :: "'a rexp => 'a lang" where
-"lang Zero = {}" |
-"lang One = {[]}" |
-"lang (Atom a) = {[a]}" |
-"lang (Plus r s) = (lang r) Un (lang s)" |
-"lang (Times r s) = conc (lang r) (lang s)" |
-"lang (Star r) = star(lang r)"
-
-abbreviation (input) regular_lang where "regular_lang A \<equiv> (\<exists>r. lang r = A)"
-
-primrec nullable :: "'a rexp \<Rightarrow> bool" where
-"nullable Zero = False" |
-"nullable One = True" |
-"nullable (Atom c) = False" |
-"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
-"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
-"nullable (Star r) = True"
-
-lemma nullable_iff [code_abbrev]: "nullable r \<longleftrightarrow> [] \<in> lang r"
-  by (induct r) (auto simp add: conc_def split: if_splits)
-
-primrec rexp_empty where
-  "rexp_empty Zero \<longleftrightarrow> True"
-| "rexp_empty One \<longleftrightarrow> False"
-| "rexp_empty (Atom a) \<longleftrightarrow> False"
-| "rexp_empty (Plus r s) \<longleftrightarrow> rexp_empty r \<and> rexp_empty s"
-| "rexp_empty (Times r s) \<longleftrightarrow> rexp_empty r \<or> rexp_empty s"
-| "rexp_empty (Star r) \<longleftrightarrow> False"
-
-(* TODO Fixme: This code_abbrev rule does not work. Why? *)
-lemma rexp_empty_iff [code_abbrev]: "rexp_empty r \<longleftrightarrow> lang r = {}"
-  by (induction r) auto
-
-
-
-text\<open>Composition on rhs usually complicates matters:\<close>
-lemma map_map_rexp:
-  "map_rexp f (map_rexp g r) = map_rexp (\<lambda>r. f (g r)) r"
-  unfolding rexp.map_comp o_def ..
-
-lemma map_rexp_ident[simp]: "map_rexp (\<lambda>x. x) = (\<lambda>r. r)"
-  unfolding id_def[symmetric] fun_eq_iff rexp.map_id id_apply by (intro allI refl)
-
-lemma atoms_lang: "w : lang r \<Longrightarrow> set w \<subseteq> atoms r"
-proof(induction r arbitrary: w)
-  case Times thus ?case by fastforce
-next
-  case Star thus ?case by (fastforce simp add: star_conv_concat)
-qed auto
-
-lemma lang_eq_ext: "(lang r = lang s) =
-  (\<forall>w \<in> lists(atoms r \<union> atoms s). w \<in> lang r \<longleftrightarrow> w \<in> lang s)"
-  by (auto simp: atoms_lang[unfolded subset_iff])
-
-lemma lang_eq_ext_Nil_fold_Deriv:
-  fixes r s
-  defines "\<BB> \<equiv> {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w\<in>lists (atoms r \<union> atoms s)}"
-  shows "lang r = lang s \<longleftrightarrow> (\<forall>(K, L) \<in> \<BB>. [] \<in> K \<longleftrightarrow> [] \<in> L)"
-  unfolding lang_eq_ext \<BB>_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto
-
-
-subsection \<open>Term ordering\<close>
-
-instantiation rexp :: (order) "{order}"
-begin
-
-fun le_rexp :: "('a::order) rexp \<Rightarrow> ('a::order) rexp \<Rightarrow> bool"
-where
-  "le_rexp Zero _ = True"
-| "le_rexp _ Zero = False"
-| "le_rexp One _ = True"
-| "le_rexp _ One = False"
-| "le_rexp (Atom a) (Atom b) = (a <= b)"
-| "le_rexp (Atom _) _ = True"
-| "le_rexp _ (Atom _) = False"
-| "le_rexp (Star r) (Star s) = le_rexp r s"
-| "le_rexp (Star _) _ = True"
-| "le_rexp _ (Star _) = False"
-| "le_rexp (Plus r r') (Plus s s') =
-    (if r = s then le_rexp r' s' else le_rexp r s)"
-| "le_rexp (Plus _ _) _ = True"
-| "le_rexp _ (Plus _ _) = False"
-| "le_rexp (Times r r') (Times s s') =
-    (if r = s then le_rexp r' s' else le_rexp r s)"
-
-(* The class instance stuff is by Dmitriy Traytel *)
-
-definition less_eq_rexp where "r \<le> s \<equiv> le_rexp r s"
-definition less_rexp where "r < s \<equiv> le_rexp r s \<and> r \<noteq> s"
-
-lemma le_rexp_Zero: "le_rexp r Zero \<Longrightarrow> r = Zero"
-by (induction r) auto
-
-lemma le_rexp_refl: "le_rexp r r"
-by (induction r) auto
-
-lemma le_rexp_antisym: "\<lbrakk>le_rexp r s; le_rexp s r\<rbrakk> \<Longrightarrow> r = s"
-by (induction r s rule: le_rexp.induct) (auto dest: le_rexp_Zero)
-
-lemma le_rexp_trans: "\<lbrakk>le_rexp r s; le_rexp s t\<rbrakk> \<Longrightarrow> le_rexp r t"
-proof (induction r s arbitrary: t rule: le_rexp.induct)
-  fix v t assume "le_rexp (Atom v) t" thus "le_rexp One t" by (cases t) auto
-next
-  fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto
-next
-  fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto
-next
-  fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto
-next
-  fix v u t assume "le_rexp (Atom v) (Atom u)" "le_rexp (Atom u) t"
-  thus "le_rexp (Atom v) t" by (cases t) auto
-next
-  fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto
-next
-  fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto
-next
-  fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Atom v) t" by (cases t) auto
-next
-  fix r s t
-  assume IH: "\<And>t. le_rexp r s \<Longrightarrow> le_rexp s t \<Longrightarrow> le_rexp r t"
-    and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t"
-  thus "le_rexp (Star r) t" by (cases t) auto
-next
-  fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
-next
-  fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
-next
-  fix r1 r2 s1 s2 t
-  assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
-         "\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t"
-         "le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t"
-  thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
-next
-  fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto
-next
-  fix r1 r2 s1 s2 t
-  assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
-         "\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t"
-         "le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t"
-  thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
-qed auto
-
-instance proof
-qed (auto simp add: less_eq_rexp_def less_rexp_def
-       intro: le_rexp_refl le_rexp_antisym le_rexp_trans)
-
-end
-
-instantiation rexp :: (linorder) "{linorder}"
-begin
-
-lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s \<or> le_rexp s r"
-by (induction r s rule: le_rexp.induct) auto
-
-instance proof
-qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total)
-
-end
-
-end
diff --git a/Regular-Sets/Regular_Exp2.thy b/Regular-Sets/Regular_Exp2.thy
deleted file mode 100644
index 940138f..0000000
--- a/Regular-Sets/Regular_Exp2.thy
+++ /dev/null
@@ -1,51 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section "Extended Regular Expressions"
-
-theory Regular_Exp2
-imports Regular_Set
-begin
-
-datatype (atoms: 'a) rexp =
-  is_Zero: Zero |
-  is_One: One |
-  Atom 'a |
-  Plus "('a rexp)" "('a rexp)" |
-  Times "('a rexp)" "('a rexp)" |
-  Star "('a rexp)" |
-  Not "('a rexp)" |
-  Inter "('a rexp)" "('a rexp)"
-
-context
-fixes S :: "'a set"
-begin
-
-primrec lang :: "'a rexp => 'a lang" where
-"lang Zero = {}" |
-"lang One = {[]}" |
-"lang (Atom a) = {[a]}" |
-"lang (Plus r s) = (lang r) Un (lang s)" |
-"lang (Times r s) = conc (lang r) (lang s)" |
-"lang (Star r) = star(lang r)" |
-"lang (Not r) = lists S - lang r" |
-"lang (Inter r s) = (lang r Int lang s)"
-
-end
-
-lemma lang_subset_lists: "atoms r \<subseteq> S \<Longrightarrow> lang S r \<subseteq> lists S"
-by(induction r)(auto simp: conc_subset_lists star_subset_lists)
-
-primrec nullable :: "'a rexp \<Rightarrow> bool" where
-"nullable Zero = False" |
-"nullable One = True" |
-"nullable (Atom c) = False" |
-"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
-"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
-"nullable (Star r) = True" |
-"nullable (Not r) = (\<not> (nullable r))" |
-"nullable (Inter r s) = (nullable r \<and> nullable s)"
-
-lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang S r"
-by (induct r) (auto simp add: conc_def split: if_splits)
-
-end
diff --git a/Regular-Sets/Regular_Set.thy b/Regular-Sets/Regular_Set.thy
deleted file mode 100644
index 317e699..0000000
--- a/Regular-Sets/Regular_Set.thy
+++ /dev/null
@@ -1,456 +0,0 @@
-(*  Author: Tobias Nipkow, Alex Krauss, Christian Urban  *)
-
-section "Regular sets"
-
-theory Regular_Set
-imports Main
-begin
-
-type_synonym 'a lang = "'a list set"
-
-definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
-"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
-
-text \<open>checks the code preprocessor for set comprehensions\<close>
-export_code conc checking SML
-
-overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-begin
-  primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
-  "lang_pow 0 A = {[]}" |
-  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
-end
-
-text \<open>for code generation\<close>
-
-definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
-  lang_pow_code_def [code_abbrev]: "lang_pow = compow"
-
-lemma [code]:
-  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
-  "lang_pow 0 A = {[]}"
-  by (simp_all add: lang_pow_code_def)
-
-hide_const (open) lang_pow
-
-definition star :: "'a lang \<Rightarrow> 'a lang" where
-"star A = (\<Union>n. A ^^ n)"
-
-
-subsection\<open>@{term "(@@)"}\<close>
-
-lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"
-by (auto simp add: conc_def)
-
-lemma concE[elim]: 
-assumes "w \<in> A @@ B"
-obtains u v where "u \<in> A" "v \<in> B" "w = u@v"
-using assms by (auto simp: conc_def)
-
-lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> C @@ D"
-by (auto simp: conc_def) 
-
-lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"
-by auto
-
-lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"
-by (simp_all add:conc_def)
-
-lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"
-by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)
-
-lemma conc_Un_distrib:
-shows "A @@ (B \<union> C) = A @@ B \<union> A @@ C"
-and   "(A \<union> B) @@ C = A @@ C \<union> B @@ C"
-by auto
-
-lemma conc_UNION_distrib:
-shows "A @@ UNION I M = UNION I (%i. A @@ M i)"
-and   "UNION I M @@ A = UNION I (%i. M i @@ A)"
-by auto
-
-lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
-by(fastforce simp: conc_def in_lists_conv_set)
-
-lemma Nil_in_conc[simp]: "[] \<in> A @@ B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
-by (metis append_is_Nil_conv concE concI)
-
-lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A @@ B"
-by (metis append_Nil concI)
-
-lemma conc_Diff_if_Nil1: "[] \<in> A \<Longrightarrow> A @@ B = (A - {[]}) @@ B \<union> B"
-by (fastforce elim: concI_if_Nil1)
-
-lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A @@ B"
-by (metis append_Nil2 concI)
-
-lemma conc_Diff_if_Nil2: "[] \<in> B \<Longrightarrow> A @@ B = A @@ (B - {[]}) \<union> A"
-by (fastforce elim: concI_if_Nil2)
-
-lemma singleton_in_conc:
-  "[x] : A @@ B \<longleftrightarrow> [x] : A \<and> [] : B \<or> [] : A \<and> [x] : B"
-by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv
-       conc_Diff_if_Nil1 conc_Diff_if_Nil2)
-
-
-subsection\<open>@{term "A ^^ n"}\<close>
-
-lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"
-by (induct n) (auto simp: conc_assoc)
-
-lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"
-by (induct n) auto
-
-lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"
-by (simp add: lang_pow_empty)
-
-lemma conc_pow_comm:
-  shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
-by (induct n) (simp_all add: conc_assoc[symmetric])
-
-lemma length_lang_pow_ub:
-  "\<forall>w \<in> A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
-by(induct n arbitrary: w) (fastforce simp: conc_def)+
-
-lemma length_lang_pow_lb:
-  "\<forall>w \<in> A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
-by(induct n arbitrary: w) (fastforce simp: conc_def)+
-
-lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
-by(induct n)(auto simp: conc_subset_lists)
-
-
-subsection\<open>@{const star}\<close>
-
-lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
-unfolding star_def by(blast dest: lang_pow_subset_lists)
-
-lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"
-by (auto simp: star_def)
-
-lemma Nil_in_star[iff]: "[] : star A"
-proof (rule star_if_lang_pow)
-  show "[] : A ^^ 0" by simp
-qed
-
-lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"
-proof (rule star_if_lang_pow)
-  show "w : A ^^ 1" using \<open>w : A\<close> by simp
-qed
-
-lemma append_in_starI[simp]:
-assumes "u : star A" and "v : star A" shows "u@v : star A"
-proof -
-  from \<open>u : star A\<close> obtain m where "u : A ^^ m" by (auto simp: star_def)
-  moreover
-  from \<open>v : star A\<close> obtain n where "v : A ^^ n" by (auto simp: star_def)
-  ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)
-  thus ?thesis by simp
-qed
-
-lemma conc_star_star: "star A @@ star A = star A"
-by (auto simp: conc_def)
-
-lemma conc_star_comm:
-  shows "A @@ star A = star A @@ A"
-unfolding star_def conc_pow_comm conc_UNION_distrib
-by simp
-
-lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
-assumes "w : star A"
-  and "P []"
-  and step: "!!u v. u : A \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)"
-shows "P w"
-proof -
-  { fix n have "w : A ^^ n \<Longrightarrow> P w"
-    by (induct n arbitrary: w) (auto intro: \<open>P []\<close> step star_if_lang_pow) }
-  with \<open>w : star A\<close> show "P w" by (auto simp: star_def)
-qed
-
-lemma star_empty[simp]: "star {} = {[]}"
-by (auto elim: star_induct)
-
-lemma star_epsilon[simp]: "star {[]} = {[]}"
-by (auto elim: star_induct)
-
-lemma star_idemp[simp]: "star (star A) = star A"
-by (auto elim: star_induct)
-
-lemma star_unfold_left: "star A = A @@ star A \<union> {[]}" (is "?L = ?R")
-proof
-  show "?L \<subseteq> ?R" by (rule, erule star_induct) auto
-qed auto
-
-lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A"
-by (induct ws) simp_all
-
-lemma in_star_iff_concat:
-  "w \<in> star A = (\<exists>ws. set ws \<subseteq> A \<and> w = concat ws)"
-  (is "_ = (\<exists>ws. ?R w ws)")
-proof
-  assume "w : star A" thus "\<exists>ws. ?R w ws"
-  proof induct
-    case Nil have "?R [] []" by simp
-    thus ?case ..
-  next
-    case (append u v)
-    then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast
-    with append have "?R (u@v) (u#ws)" by auto
-    thus ?case ..
-  qed
-next
-  assume "\<exists>us. ?R w us" thus "w : star A"
-  by (auto simp: concat_in_star)
-qed
-
-lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"
-by (fastforce simp: in_star_iff_concat)
-
-lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
-proof-
-  { fix us
-    have "set us \<subseteq> insert [] A \<Longrightarrow> \<exists>vs. concat us = concat vs \<and> set vs \<subseteq> A"
-      (is "?P \<Longrightarrow> \<exists>vs. ?Q vs")
-    proof
-      let ?vs = "filter (%u. u \<noteq> []) us"
-      show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto
-    qed
-  } thus ?thesis by (auto simp: star_conv_concat)
-qed
-
-lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) \<union> {[]}"
-by (metis insert_Diff_single star_insert_eps star_unfold_left)
-
-lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}"
-proof -
-  have "[] \<notin> (A - {[]}) @@ star A" by simp
-  thus ?thesis using star_unfold_left_Nil by blast
-qed
-
-lemma star_decom: 
-  assumes a: "x \<in> star A" "x \<noteq> []"
-  shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
-using a by (induct rule: star_induct) (blast)+
-
-
-subsection \<open>Left-Quotients of languages\<close>
-
-definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-  where "Deriv x A = { xs. x#xs \<in> A }"
-    
-definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where "Derivs xs A = { ys. xs @ ys \<in> A }"
-
-abbreviation 
-  Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
-where
-  "Derivss s As \<equiv> \<Union> (Derivs s ` As)"
-
-
-lemma Deriv_empty[simp]:   "Deriv a {} = {}"
-  and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
-  and Deriv_char[simp]:    "Deriv a {[b]} = (if a = b then {[]} else {})"
-  and Deriv_union[simp]:   "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
-  and Deriv_inter[simp]:   "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B"
-  and Deriv_compl[simp]:   "Deriv a (-A) = - Deriv a A"
-  and Deriv_Union[simp]:   "Deriv a (Union M) = Union(Deriv a ` M)"
-  and Deriv_UN[simp]:      "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
-by (auto simp: Deriv_def)
-
-lemma Der_conc [simp]: 
-  shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
-unfolding Deriv_def conc_def
-by (auto simp add: Cons_eq_append_conv)
-
-lemma Deriv_star [simp]: 
-  shows "Deriv c (star A) = (Deriv c A) @@ star A"
-proof -
-  have "Deriv c (star A) = Deriv c ({[]} \<union> A @@ star A)"
-    by (metis star_unfold_left sup.commute)
-  also have "... = Deriv c (A @@ star A)"
-    unfolding Deriv_union by (simp)
-  also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
-    by simp
-  also have "... =  (Deriv c A) @@ star A"
-    unfolding conc_def Deriv_def
-    using star_decom by (force simp add: Cons_eq_append_conv)
-  finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
-qed
-
-lemma Deriv_diff[simp]:   
-  shows "Deriv c (A - B) = Deriv c A - Deriv c B"
-by(auto simp add: Deriv_def)
-
-lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S"
-by(auto simp add: Deriv_def)
-
-lemma Derivs_simps [simp]:
-  shows "Derivs [] A = A"
-  and   "Derivs (c # s) A = Derivs s (Deriv c A)"
-  and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
-unfolding Derivs_def Deriv_def by auto
-
-lemma in_fold_Deriv: "v \<in> fold Deriv w L \<longleftrightarrow> w @ v \<in> L"
-  by (induct w arbitrary: L) (simp_all add: Deriv_def)
-
-lemma Derivs_alt_def [code]: "Derivs w L = fold Deriv w L"
-  by (induct w arbitrary: L) simp_all
-
-lemma Deriv_code [code]: 
-  "Deriv x A = tl ` Set.filter (\<lambda>xs. case xs of x' # _ \<Rightarrow> x = x' | _ \<Rightarrow> False) A"
-  by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits)
-
-subsection \<open>Shuffle product\<close>
-
-definition Shuffle (infixr "\<parallel>" 80) where
-  "Shuffle A B = \<Union>{shuffle xs ys | xs ys. xs \<in> A \<and> ys \<in> B}"
-
-lemma Deriv_Shuffle[simp]:
-  "Deriv a (A \<parallel> B) = Deriv a A \<parallel> B \<union> A \<parallel> Deriv a B"
-  unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffle_iff neq_Nil_conv)
-
-lemma shuffle_subset_lists:
-  assumes "A \<subseteq> lists S" "B \<subseteq> lists S"
-  shows "A \<parallel> B \<subseteq> lists S"
-unfolding Shuffle_def proof safe
-  fix x and zs xs ys :: "'a list"
-  assume zs: "zs \<in> shuffle xs ys" "x \<in> set zs" and "xs \<in> A" "ys \<in> B"
-  with assms have "xs \<in> lists S" "ys \<in> lists S" by auto
-  with zs show "x \<in> S" by (induct xs ys arbitrary: zs rule: shuffle.induct) auto
-qed
-
-lemma Nil_in_Shuffle[simp]: "[] \<in> A \<parallel> B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
-  unfolding Shuffle_def by force
-
-lemma shuffle_Un_distrib:
-shows "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
-and   "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
-unfolding Shuffle_def by fast+
-
-lemma shuffle_UNION_distrib:
-shows "A \<parallel> UNION I M = UNION I (%i. A \<parallel> M i)"
-and   "UNION I M \<parallel> A = UNION I (%i. M i \<parallel> A)"
-unfolding Shuffle_def by fast+
-
-lemma Shuffle_empty[simp]:
-  "A \<parallel> {} = {}"
-  "{} \<parallel> B = {}"
-  unfolding Shuffle_def by auto
-
-lemma Shuffle_eps[simp]:
-  "A \<parallel> {[]} = A"
-  "{[]} \<parallel> B = B"
-  unfolding Shuffle_def by auto
-
-
-subsection \<open>Arden's Lemma\<close>
-
-lemma arden_helper:
-  assumes eq: "X = A @@ X \<union> B"
-  shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
-proof (induct n)
-  case 0 
-  show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)"
-    using eq by simp
-next
-  case (Suc n)
-  have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact
-  also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp
-  also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
-    by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
-  also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)"
-    by (auto simp add: atMost_Suc)
-  finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" .
-qed
-
-lemma Arden:
-  assumes "[] \<notin> A" 
-  shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B"
-proof
-  assume eq: "X = A @@ X \<union> B"
-  { fix w assume "w : X"
-    let ?n = "size w"
-    from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
-      by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
-    hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
-      by (metis length_lang_pow_lb nat_mult_1)
-    hence "\<forall>u \<in> A^^(?n+1)@@X. length u \<ge> ?n+1"
-      by(auto simp only: conc_def length_append)
-    hence "w \<notin> A^^(?n+1)@@X" by auto
-    hence "w : star A @@ B" using \<open>w : X\<close> using arden_helper[OF eq, where n="?n"]
-      by (auto simp add: star_def conc_UNION_distrib)
-  } moreover
-  { fix w assume "w : star A @@ B"
-    hence "\<exists>n. w \<in> A^^n @@ B" by(auto simp: conc_def star_def)
-    hence "w : X" using arden_helper[OF eq] by blast
-  } ultimately show "X = star A @@ B" by blast 
-next
-  assume eq: "X = star A @@ B"
-  have "star A = A @@ star A \<union> {[]}"
-    by (rule star_unfold_left)
-  then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B"
-    by metis
-  also have "\<dots> = (A @@ star A) @@ B \<union> B"
-    unfolding conc_Un_distrib by simp
-  also have "\<dots> = A @@ (star A @@ B) \<union> B" 
-    by (simp only: conc_assoc)
-  finally show "X = A @@ X \<union> B" 
-    using eq by blast 
-qed
-
-
-lemma reversed_arden_helper:
-  assumes eq: "X = X @@ A \<union> B"
-  shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
-proof (induct n)
-  case 0 
-  show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))"
-    using eq by simp
-next
-  case (Suc n)
-  have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact
-  also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp
-  also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
-    by (simp add: conc_Un_distrib conc_assoc)
-  also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))"
-    by (auto simp add: atMost_Suc)
-  finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" .
-qed
-
-theorem reversed_Arden:
-  assumes nemp: "[] \<notin> A"
-  shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A"
-proof
- assume eq: "X = X @@ A \<union> B"
-  { fix w assume "w : X"
-    let ?n = "size w"
-    from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
-      by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
-    hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
-      by (metis length_lang_pow_lb nat_mult_1)
-    hence "\<forall>u \<in> X @@ A^^(?n+1). length u \<ge> ?n+1"
-      by(auto simp only: conc_def length_append)
-    hence "w \<notin> X @@ A^^(?n+1)" by auto
-    hence "w : B @@ star A" using \<open>w : X\<close> using reversed_arden_helper[OF eq, where n="?n"]
-      by (auto simp add: star_def conc_UNION_distrib)
-  } moreover
-  { fix w assume "w : B @@ star A"
-    hence "\<exists>n. w \<in> B @@ A^^n" by (auto simp: conc_def star_def)
-    hence "w : X" using reversed_arden_helper[OF eq] by blast
-  } ultimately show "X = B @@ star A" by blast 
-next 
-  assume eq: "X = B @@ star A"
-  have "star A = {[]} \<union> star A @@ A" 
-    unfolding conc_star_comm[symmetric]
-    by(metis Un_commute star_unfold_left)
-  then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)"
-    by metis
-  also have "\<dots> = B \<union> B @@ (star A @@ A)"
-    unfolding conc_Un_distrib by simp
-  also have "\<dots> = B \<union> (B @@ star A) @@ A" 
-    by (simp only: conc_assoc)
-  finally show "X = X @@ A \<union> B" 
-    using eq by blast 
-qed
-
-end
diff --git a/Regular-Sets/Relation_Interpretation.thy b/Regular-Sets/Relation_Interpretation.thy
deleted file mode 100644
index 41e71ce..0000000
--- a/Regular-Sets/Relation_Interpretation.thy
+++ /dev/null
@@ -1,53 +0,0 @@
-section \<open>Regular Expressions as Homogeneous Binary Relations\<close>
-
-theory Relation_Interpretation
-imports Regular_Exp
-begin
-
-primrec rel :: "('a \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a rexp \<Rightarrow> ('b * 'b) set"
-where
-  "rel v Zero = {}" |
-  "rel v One = Id" |
-  "rel v (Atom a) = v a" |
-  "rel v (Plus r s) = rel v r \<union> rel v s" |
-  "rel v (Times r s) = rel v r O rel v s" |
-  "rel v (Star r) = (rel v r)^*"
-
-primrec word_rel :: "('a \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a list \<Rightarrow> ('b * 'b) set"
-where
-  "word_rel v [] = Id"
-| "word_rel v (a#as) = v a O word_rel v as"
-
-lemma word_rel_append: 
-  "word_rel v w O word_rel v w' = word_rel v (w @ w')"
-by (rule sym) (induct w, auto)
-
-lemma rel_word_rel: "rel v r = (\<Union>w\<in>lang r. word_rel v w)"
-proof (induct r)
-  case Times thus ?case 
-    by (auto simp: rel_def word_rel_append conc_def relcomp_UNION_distrib relcomp_UNION_distrib2)
-next
-  case (Star r)
-  { fix n
-    have "(rel v r) ^^ n = (\<Union>w \<in> lang r ^^ n. word_rel v w)"
-    proof (induct n)
-      case 0 show ?case by simp
-    next
-      case (Suc n) thus ?case
-        unfolding relpow.simps relpow_commute[symmetric]
-        by (auto simp add: Star conc_def word_rel_append
-          relcomp_UNION_distrib relcomp_UNION_distrib2)
-    qed }
-
-  thus ?case unfolding rel.simps
-    by (force simp: rtrancl_power star_def)
-qed auto
-
-
-text \<open>Soundness:\<close>
-
-lemma soundness:
- "lang r = lang s \<Longrightarrow> rel v r = rel v s"
-unfolding rel_word_rel by auto
-
-end
diff --git a/Regular-Sets/document/root.bib b/Regular-Sets/document/root.bib
deleted file mode 100644
index c92c210..0000000
--- a/Regular-Sets/document/root.bib
+++ /dev/null
@@ -1,36 +0,0 @@
-@article{KraussN-JAR,author={Alexander Krauss and Tobias Nipkow},
-title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},
-journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}
-
-@inproceedings{Rutten98,
-  author    = {Jan J. M. M. Rutten},
-  title     = {Automata and Coinduction (An Exercise in Coalgebra)},
-  editor    = {Davide Sangiorgi and Robert de Simone},
-  booktitle = {Concurrency Theory (CONCUR'98)},
-  pages     = {194--218},
-  publisher = {Springer},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {1466},
-  year      = {1998},
-}
-
-@article{Brzozowski64,
- author = {J.~A.~Brzozowski},
- title = {{D}erivatives of {R}egular {E}xpressions},
- journal = {Journal of the ACM},
- volume = {11},
- issue = {4},
- year = {1964},
- pages = {481--494},
- publisher = {ACM}
-} 
-
-@ARTICLE{Antimirov95,
-    author = {V.~Antimirov},
-    title = {{P}artial {D}erivatives of {R}egular {E}xpressions and 
-     {F}inite {A}utomata {C}onstructions},
-    journal = {Theoretical Computer Science},
-    year = {1995},
-    volume = {155},
-    pages = {291--319}
-}
\ No newline at end of file
diff --git a/Regular-Sets/document/root.tex b/Regular-Sets/document/root.tex
deleted file mode 100644
index cc5e5bd..0000000
--- a/Regular-Sets/document/root.tex
+++ /dev/null
@@ -1,47 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-\usepackage{eufrak}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-
-\begin{document}
-
-\title{Regular Sets, Expressions, Derivatives and Relation Algebra}
-\author{Alexander Krauss, Tobias Nipkow,\\
-  Chunhan Wu, Xingyuan Zhang and Christian Urban}
-\maketitle
-
-\begin{abstract}
-This is a library of constructions on regular expressions and languages.  It
-provides the operations of concatenation, Kleene star and left-quotients of
-languages. A theory of derivatives and partial derivatives is
-provided. Arden's lemma and finiteness of partial derivatives is
-established. A simple regular expression matcher based on Brozowski's
-derivatives is proved to be correct.  An executable equivalence checker for
-regular expressions is verified; it does not need automata but works directly
-on regular expressions. By mapping regular expressions to binary relations, an
-automatic and complete proof method for (in)equalities of binary relations
-over union, concatenation and (reflexive) transitive closure is obtained.
-
-For an exposition of the equivalence checker for regular and relation
-algebraic expressions see the paper by Krauss and Nipkow~\cite{KraussN-JAR}.
-
-Extended regular expressions with complement and intersection
-are also defined and an equivalence checker is provided.
-\end{abstract}
-
-\tableofcontents
-
-% include generated text of all theories
-\input{session}
-
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
diff --git a/Regular-Sets/pEquivalence_Checking.thy b/Regular-Sets/pEquivalence_Checking.thy
deleted file mode 100644
index 92aa66a..0000000
--- a/Regular-Sets/pEquivalence_Checking.thy
+++ /dev/null
@@ -1,306 +0,0 @@
-section \<open>Deciding Regular Expression Equivalence (2)\<close>
-
-theory pEquivalence_Checking
-imports Equivalence_Checking Derivatives
-begin
-
-text\<open>\noindent Similar to theory @{theory "Regular-Sets.Equivalence_Checking"}, but
-with partial derivatives instead of derivatives.\<close>
-
-text\<open>Lifting many notions to sets:\<close>
-
-definition "Lang R == UN r:R. lang r"
-definition "Nullable R == EX r:R. nullable r"
-definition "Pderiv a R == UN r:R. pderiv a r"
-definition "Atoms R == UN r:R. atoms r"
-
-(* FIXME: rename pderiv_set in Derivatives to Pderiv and drop the one above *)
-
-lemma Atoms_pderiv: "Atoms(pderiv a r) \<subseteq> atoms r"
-apply (induct r)
-apply (auto simp: Atoms_def UN_subset_iff)
-apply (fastforce)+
-done
-
-lemma Atoms_Pderiv: "Atoms(Pderiv a R) \<subseteq> Atoms R"
-using Atoms_pderiv by (fastforce simp: Atoms_def Pderiv_def)
-
-lemma pderiv_no_occurrence: 
-  "x \<notin> atoms r \<Longrightarrow> pderiv x r = {}"
-by (induct r) auto
-
-lemma Pderiv_no_occurrence: 
-  "x \<notin> Atoms R \<Longrightarrow> Pderiv x R = {}"
-by(auto simp:pderiv_no_occurrence Atoms_def Pderiv_def)
-
-lemma Deriv_Lang: "Deriv c (Lang R) = Lang (Pderiv c R)"
-by(auto simp: Deriv_pderiv Pderiv_def Lang_def)
-
-lemma Nullable_pderiv[simp]: "Nullable(pderivs w r) = (w : lang r)"
-apply(induction w arbitrary: r)
-apply (simp add: Nullable_def nullable_iff singleton_iff)
-using eqset_imp_iff[OF Deriv_pderiv[where 'a = 'a]]
-apply (simp add: Nullable_def Deriv_def)
-done
-
-
-type_synonym 'a Rexp_pair = "'a rexp set * 'a rexp set"
-type_synonym 'a Rexp_pairs = "'a Rexp_pair list"
-
-definition is_Bisimulation :: "'a list \<Rightarrow> 'a Rexp_pairs \<Rightarrow> bool"
-where
-"is_Bisimulation as ps =
-  (\<forall>(R,S)\<in> set ps. Atoms R \<union> Atoms S \<subseteq> set as \<and>
-    (Nullable R \<longleftrightarrow> Nullable S) \<and>
-    (\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps))"
-
-lemma Bisim_Lang_eq:
-assumes Bisim: "is_Bisimulation as ps"
-assumes "(R, S) \<in> set ps"
-shows "Lang R = Lang S"
-proof -
-  define ps' where "ps' = ({}, {}) # ps"
-  from Bisim have Bisim': "is_Bisimulation as ps'"
-    by (fastforce simp: ps'_def is_Bisimulation_def UN_subset_iff Pderiv_def Atoms_def)
-  let ?R = "\<lambda>K L. (\<exists>(R,S)\<in>set ps'. K = Lang R \<and> L = Lang S)"
-  show ?thesis
-  proof (rule language_coinduct[where R="?R"])
-    from \<open>(R,S) \<in> set ps\<close>
-    have "(R,S) \<in> set ps'" by (auto simp: ps'_def)
-    thus "?R (Lang R) (Lang S)" by auto
-  next
-    fix K L assume "?R K L"
-    then obtain R S where rs: "(R, S) \<in> set ps'"
-      and KL: "K = Lang R" "L = Lang S" by auto
-    with Bisim' have "Nullable R \<longleftrightarrow> Nullable S"
-      by (auto simp: is_Bisimulation_def)
-    thus "[] \<in> K \<longleftrightarrow> [] \<in> L"
-      by (auto simp: nullable_iff KL Nullable_def Lang_def)
-    fix a
-    show "?R (Deriv a K) (Deriv a L)"
-    proof cases
-      assume "a \<in> set as"
-      with rs Bisim'
-      have "(Pderiv a R, Pderiv a S) \<in> set ps'"
-        by (auto simp: is_Bisimulation_def)
-      thus ?thesis by (fastforce simp: KL Deriv_Lang)
-    next
-      assume "a \<notin> set as"
-      with Bisim' rs
-      have "a \<notin> Atoms R \<union> Atoms S"
-        by (fastforce simp: is_Bisimulation_def UN_subset_iff)
-      then have "Pderiv a R = {}" "Pderiv a S = {}"
-        by (metis Pderiv_no_occurrence Un_iff)+
-      then have "Deriv a K = Lang {}" "Deriv a L = Lang {}" 
-        unfolding KL Deriv_Lang by auto
-      thus ?thesis by (auto simp: ps'_def)
-    qed
-  qed
-qed
-
-
-subsection \<open>Closure computation\<close>
-
-fun test :: "'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool" where
-"test (ws, ps) = (case ws of [] \<Rightarrow>  False | (R,S)#_ \<Rightarrow> Nullable R = Nullable S)"
-
-fun step :: "'a list \<Rightarrow>
-  'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs"
-where "step as (ws,ps) =
-    (let
-      (R,S) = hd ws;
-      ps' = (R,S) # ps;
-      succs = map (\<lambda>a. (Pderiv a R, Pderiv a S)) as;
-      new = filter (\<lambda>p. p \<notin> set ps \<union> set ws) succs
-    in (remdups new @ tl ws, ps'))"
-
-definition closure ::
-  "'a list \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs
-   \<Rightarrow> ('a Rexp_pairs * 'a Rexp_pairs) option" where
-"closure as = while_option test (step as)"
-
-definition pre_Bisim :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set \<Rightarrow>
- 'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool"
-where
-"pre_Bisim as R S = (\<lambda>(ws,ps).
- ((R,S) \<in> set ws \<union> set ps) \<and>
- (\<forall>(R,S)\<in> set ws \<union> set ps. Atoms R \<union> Atoms S \<subseteq> set as) \<and>
- (\<forall>(R,S)\<in> set ps. (Nullable R \<longleftrightarrow> Nullable S) \<and>
-   (\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps \<union> set ws)))"
-
-lemma step_set_eq: "\<lbrakk> test (ws,ps); step as (ws,ps) = (ws',ps') \<rbrakk>
-  \<Longrightarrow> set ws' \<union> set ps' =
-     set ws \<union> set ps
-     \<union> (\<Union>a\<in>set as. {(Pderiv a (fst(hd ws)), Pderiv a (snd(hd ws)))})"
-by(auto split: list.splits)
-
-theorem closure_sound:
-assumes result: "closure as ([(R,S)],[]) = Some([],ps)"
-and atoms: "Atoms R \<union> Atoms S \<subseteq> set as"
-shows "Lang R = Lang S"
-proof-
-  { fix st
-    have "pre_Bisim as R S st \<Longrightarrow> test st \<Longrightarrow> pre_Bisim as R S (step as st)"
-    unfolding pre_Bisim_def
-    proof(split prod.splits, elim case_prodE conjE, intro allI impI conjI, goal_cases)
-      case 1 thus ?case by(auto split: list.splits)
-    next
-      case prems: (2 ws ps ws' ps')
-      note prems(2)[simp]
-      from \<open>test st\<close> obtain wstl R S where [simp]: "ws = (R,S)#wstl"
-        by (auto split: list.splits)
-      from \<open>step as st = (ws',ps')\<close> obtain P where [simp]: "ps' = (R,S) # ps"
-        and [simp]: "ws' = remdups(filter P (map (\<lambda>a. (Pderiv a R, Pderiv a S)) as)) @ wstl"
-        by auto
-      have "\<forall>(R',S')\<in>set wstl \<union> set ps'. Atoms R' \<union> Atoms S' \<subseteq> set as"
-        using prems(4) by auto
-      moreover
-      have "\<forall>a\<in>set as. Atoms(Pderiv a R) \<union> Atoms(Pderiv a S) \<subseteq> set as"
-        using prems(4) by simp (metis (lifting) Atoms_Pderiv order_trans)
-      ultimately show ?case by simp blast
-    next
-      case 3 thus ?case
-        apply (clarsimp simp: image_iff split: prod.splits list.splits)
-        by hypsubst_thin metis
-    qed
-  }
-  moreover
-  from atoms
-  have "pre_Bisim as R S ([(R,S)],[])" by (simp add: pre_Bisim_def)
-  ultimately have pre_Bisim_ps: "pre_Bisim as R S ([],ps)"
-    by (rule while_option_rule[OF _ result[unfolded closure_def]])
-  then have "is_Bisimulation as ps" "(R,S) \<in> set ps"
-    by (auto simp: pre_Bisim_def is_Bisimulation_def)
-  thus "Lang R = Lang S" by (rule Bisim_Lang_eq)
-qed
-
-
-subsection \<open>The overall procedure\<close>
-
-definition check_eqv :: "'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool"
-where
-"check_eqv r s =
-  (case closure (add_atoms r (add_atoms s [])) ([({r}, {s})], []) of
-     Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
-
-lemma soundness: assumes "check_eqv r s" shows "lang r = lang s"
-proof -
-  let ?as = "add_atoms r (add_atoms s [])"
-  obtain ps where 1: "closure ?as ([({r},{s})],[]) = Some([],ps)"
-    using assms by (auto simp: check_eqv_def split:option.splits list.splits)
-  then have "lang r = lang s"
-    by(rule closure_sound[of _ "{r}" "{s}", simplified Lang_def, simplified])
-      (auto simp: set_add_atoms Atoms_def)
-  thus "lang r = lang s" by simp
-qed
-
-text\<open>Test:\<close>
-lemma "check_eqv
-  (Plus One (Times (Atom 0) (Star(Atom 0))))
-  (Star(Atom(0::nat)))"
-by eval
-
-
-subsection "Termination and Completeness"
-
-definition PDERIVS :: "'a rexp set => 'a rexp set" where
-"PDERIVS R = (UN r:R. pderivs_lang UNIV r)"
-
-lemma PDERIVS_incr[simp]: "R \<subseteq> PDERIVS R"
-apply(auto simp add: PDERIVS_def pderivs_lang_def)
-by (metis pderivs.simps(1) insertI1)
-
-lemma Pderiv_PDERIVS: assumes "R' \<subseteq> PDERIVS R" shows "Pderiv a R' \<subseteq> PDERIVS R"
-proof
-  fix r assume "r : Pderiv a R'"
-  then obtain r' where "r' : R'" "r : pderiv a r'" by(auto simp: Pderiv_def)
-  from \<open>r' : R'\<close> \<open>R' \<subseteq> PDERIVS R\<close> obtain s w where "s : R" "r' : pderivs w s"
-    by(auto simp: PDERIVS_def pderivs_lang_def)
-  hence "r \<in> pderivs (w @ [a]) s" using \<open>r : pderiv a r'\<close> by(auto simp add:pderivs_snoc)
-  thus "r : PDERIVS R" using \<open>s : R\<close> by(auto simp: PDERIVS_def pderivs_lang_def)
-qed
-
-lemma finite_PDERIVS: "finite R \<Longrightarrow> finite(PDERIVS R)"
-by(simp add: PDERIVS_def finite_pderivs_lang_UNIV)
-
-lemma closure_Some: assumes "finite R0" "finite S0" shows "\<exists>p. closure as ([(R0,S0)],[]) = Some p"
-proof(unfold closure_def)
-  let ?Inv = "%(ws,bs).  distinct ws \<and> (ALL (R,S) : set ws. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set bs)"
-  let ?m1 = "%bs. Pow(PDERIVS R0) \<times> Pow(PDERIVS S0) - set bs"
-  let ?m2 = "%(ws,bs). card(?m1 bs)"
-  have Inv0: "?Inv ([(R0, S0)], [])" by simp
-  { fix s assume "test s" "?Inv s"
-    obtain ws bs where [simp]: "s = (ws,bs)" by fastforce
-    from \<open>test s\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
-      by(auto split: prod.splits list.splits)
-    let ?bs' = "(R,S) # bs"
-    let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
-    let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
-    let ?ws' = "remdups ?new @ ws'"
-    have *: "?Inv (step as s)"
-    proof -
-      from \<open>?Inv s\<close> have "distinct ?ws'" by auto
-      have "ALL (R,S) : set ?ws'. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set ?bs'" using \<open>?Inv s\<close>
-        by(simp add: Ball_def image_iff) (metis Pderiv_PDERIVS)
-      with \<open>distinct ?ws'\<close> show ?thesis by(simp)
-    qed
-    have "?m2(step as s) < ?m2 s"
-    proof -
-      have "finite(?m1 bs)"
-        by(metis assms finite_Diff finite_PDERIVS finite_cartesian_product finite_Pow_iff)
-      moreover have "?m2(step as s) < ?m2 s" using \<open>?Inv s\<close>
-        by(auto intro: psubset_card_mono[OF \<open>finite(?m1 bs)\<close>])
-      then show ?thesis using \<open>?Inv s\<close> by simp
-    qed
-    note * and this
-  } note step = this
-  show "\<exists>p. while_option test (step as) ([(R0, S0)], []) = Some p" 
-    by(rule measure_while_option_Some [where P = ?Inv and f = ?m2, OF _ Inv0])(simp add: step)
-qed
-
-theorem closure_Some_Inv: assumes "closure as ([({r},{s})],[]) = Some p"
-shows "\<forall>(R,S)\<in>set(fst p). \<exists>w. R = pderivs w r \<and> S = pderivs w s" (is "?Inv p")
-proof-
-  from assms have 1: "while_option test (step as) ([({r},{s})],[]) = Some p"
-    by(simp add: closure_def)
-  have Inv0: "?Inv ([({r},{s})],[])" by simp (metis pderivs.simps(1))
-  { fix p assume "?Inv p" "test p"
-    obtain ws bs where [simp]: "p = (ws,bs)" by fastforce
-    from \<open>test p\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
-      by(auto split: prod.splits list.splits)
-    let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
-    let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
-    let ?ws' = "remdups ?new @ ws'"
-    from \<open>?Inv p\<close> obtain w where [simp]: "R = pderivs w r" "S = pderivs w s"
-      by auto
-    { fix x assume "x : set as"
-      have "EX w. Pderiv x R = pderivs w r \<and> Pderiv x S = pderivs w s"
-        by(rule_tac x="w@[x]" in exI)(simp add: pderivs_append Pderiv_def)
-    }
-    with \<open>?Inv p\<close> have "?Inv (step as p)" by auto
-  } note Inv_step = this
-  show ?thesis
-    apply(rule while_option_rule[OF _ 1])
-    apply(erule (1) Inv_step)
-    apply(rule Inv0)
-    done
-qed
-
-lemma closure_complete: assumes "lang r = lang s"
- shows "EX bs. closure as ([({r},{s})],[]) = Some([],bs)" (is ?C)
-proof(rule ccontr)
-  assume "\<not> ?C"
-  then obtain R S ws bs
-    where cl: "closure as ([({r},{s})],[]) = Some((R,S)#ws,bs)"
-    using closure_Some[of "{r}" "{s}", simplified]
-    by (metis (hide_lams, no_types) list.exhaust prod.exhaust)
-  from assms closure_Some_Inv[OF this]
-    while_option_stop[OF cl[unfolded closure_def]]
-  show "False" by auto
-qed
-
-corollary completeness: "lang r = lang s \<Longrightarrow> check_eqv r s"
-by(auto simp add: check_eqv_def dest!: closure_complete
-      split: option.split list.split)
-
-end