diff -r 09e6f3719cbc -r 5d724fe0e096 Derivatives.thy
--- a/Derivatives.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Derivatives.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -1,67 +1,81 @@
 theory Derivatives
-imports Myhill_2
+imports Regular_Exp
 begin
 
-section {* Left-Quotients and Derivatives *}
-
-subsection {* Left-Quotients *}
+section {* Leftquotients, Derivatives and Partial Derivatives *}
 
-definition
-  Delta :: "'a lang \<Rightarrow> 'a lang"
-where
-  "Delta A = (if [] \<in> A then {[]} else {})"
+text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}
+
+subsection {* Left-Quotients of languages *}
 
-definition
-  Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
-  "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
+definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Deriv x A = { xs. x#xs \<in> A }"
 
-definition
-  Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
-  "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Derivs xs A = { ys. xs @ ys \<in> A }"
 
 abbreviation 
-  "Derss s A \<equiv> \<Union> (Ders s) ` A"
+  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"
+by (auto simp: Deriv_def)
 
-lemma Der_simps [simp]:
-  shows "Der c {} = {}"
-  and   "Der c {[]} = {}"
-  and   "Der c {[d]} = (if c = d then {[]} else {})"
-  and   "Der c (A \<union> B) = Der c A \<union> Der c B"
-unfolding Der_def by auto
+lemma Deriv_conc_subset:
+"Deriv a A @@ B \<subseteq> Deriv a (A @@ B)" (is "?L \<subseteq> ?R")
+proof 
+  fix w assume "w \<in> ?L"
+  then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"
+    by (auto simp: Deriv_def)
+  then have "a # w \<in> A @@ B"
+    by (auto intro: concI[of "a # u", simplified])
+  thus "w \<in> ?R" by (auto simp: Deriv_def)
+qed
 
 lemma Der_conc [simp]:
-  shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
-unfolding Der_def Delta_def conc_def
+  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 Der_star [simp]:
-  shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
+lemma Deriv_star [simp]:
+  shows "Deriv c (star A) = (Deriv c A) @@ star A"
 proof -
-  have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
-    unfolding Der_def Delta_def conc_def 
-    apply(auto)
+  have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
+    unfolding Deriv_def conc_def 
+    apply(auto simp add: Cons_eq_append_conv)
     apply(drule star_decom)
     apply(auto simp add: Cons_eq_append_conv)
     done
-    
-  have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
+
+  have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
     by (simp only: star_unfold_left[symmetric])
-  also have "... = Der c (A \<cdot> A\<star>)"
-    by (simp only: Der_simps) (simp)
-  also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
+  also have "... = Deriv c (A @@ star A)"
+    by (simp only: Deriv_union) (simp)
+  also have "... =  (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
     by simp
-  also have "... =  (Der c A) \<cdot> A\<star>"
+   also have "... =  (Deriv c A) @@ star A"
     using incl by auto
-  finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 
+  finally show "Deriv c (star A) = (Deriv c A) @@ star A" . 
 qed
 
-lemma Ders_simps [simp]:
-  shows "Ders [] A = A"
-  and   "Ders (c # s) A = Ders s (Der c A)"
-  and   "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
-unfolding Ders_def Der_def by auto
+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 Deriv_insert_eps[simp]: 
+"Deriv a (insert [] A) = Deriv a A"
+by (auto simp: Deriv_def)
+*)
+
+
 
 subsection {* Brozowsky's derivatives of regular expressions *}
 
@@ -76,247 +90,254 @@
 | "nullable (Star r) = True"
 
 fun
-  der :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+  deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
-  "der c (Zero) = Zero"
-| "der c (One) = Zero"
-| "der c (Atom c') = (if c = c' then One else Zero)"
-| "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
-| "der c (Times r1 r2) = 
-    (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
-| "der c (Star r) = Times (der c r) (Star r)"
+  "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)"
 
 fun 
-  ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+  derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
-  "ders [] r = r"
-| "ders (c # s) r = ders s (der c r)"
+  "derivs [] r = r"
+| "derivs (c # s) r = derivs s (deriv c r)"
 
 
-lemma Delta_nullable:
-  shows "Delta (lang r) = (if nullable r then {[]} else {})"
-unfolding Delta_def
+lemma nullable_iff:
+  shows "nullable r \<longleftrightarrow> [] \<in> lang r"
 by (induct r) (auto simp add: conc_def split: if_splits)
 
-lemma Der_der:
-  shows "Der c (lang r) = lang (der c r)"
-by (induct r) (simp_all add: Delta_nullable)
+lemma Deriv_deriv:
+  shows "Deriv c (lang r) = lang (deriv c r)"
+by (induct r) (simp_all add: nullable_iff)
 
-lemma Ders_ders:
-  shows "Ders s (lang r) = lang (ders s r)"
-by (induct s arbitrary: r) (simp_all add: Der_der)
+lemma Derivs_derivs:
+  shows "Derivs s (lang r) = lang (derivs s r)"
+by (induct s arbitrary: r) (simp_all add: Deriv_deriv)
 
 
-subsection {* Antimirov's Partial Derivatives *}
+subsection {* Antimirov's partial derivivatives *}
 
 abbreviation
   "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
 
 fun
-  pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+  pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
 where
-  "pder c Zero = {}"
-| "pder c One = {}"
-| "pder c (Atom c') = (if c = c' then {One} else {})"
-| "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
-| "pder c (Times r1 r2) = 
-    (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)"
-| "pder c (Star r) = Timess (pder c r) (Star r)"
-
-abbreviation
-  "pder_set c rs \<equiv> \<Union> pder c ` rs"
+  "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)"
 
 fun
-  pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+  pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 where
-  "pders [] r = {r}"
-| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
+  "pderivs [] r = {r}"
+| "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)"
 
 abbreviation
-  "pderss s A \<equiv> \<Union> (pders s) ` A"
+ pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
+where
+  "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs"
 
-lemma pders_append:
-  "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
+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 pders_snoc:
-  shows "pders (s @ [c]) r = pder_set c (pders s r)"
-by (simp add: pders_append)
+lemma pderivs_snoc:
+  shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"
+by (simp add: pderivs_append)
 
-lemma pders_simps [simp]:
-  shows "pders s Zero = (if s= [] then {Zero} else {})"
-  and   "pders s One = (if s = [] then {One} else {})"
-  and   "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
+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 pders_Atom [intro]:
-  shows "pders s (Atom c) \<subseteq> {Atom c, One}"
+lemma pderivs_Atom:
+  shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
 by (induct s) (simp_all)
 
-subsection {* Relating left-quotients and partial derivatives *}
+subsection {* Relating left-quotients and partial derivivatives *}
 
-lemma Der_pder:
-  shows "Der c (lang r) = \<Union> lang ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
+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 Ders_pders:
-  shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
+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. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
-  have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp
-  also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder)
-  also have "\<dots> = Derss s (lang ` (pder c r))"
-    by (auto simp add:  Ders_def)
-  also have "\<dots> = \<Union> lang ` (pderss s (pder c r))"
+  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 ` (pders (c # s) r)" by simp
-  finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
-qed (simp add: Ders_def)
+  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 {* Relating derivatives and partial derivatives *}
+subsection {* Relating derivivatives and partial derivivatives *}
 
-lemma der_pder:
-  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
+lemma deriv_pderiv:
+  shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)"
+unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp
 
-lemma ders_pders:
-  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
+lemma derivs_pderivs:
+  shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)"
+unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp
 
 
-subsection {* There are only finitely many partial derivatives for a language *}
+subsection {* Finiteness property of partial derivivatives *}
 
 definition
-  "pders_lang A r \<equiv> \<Union>x \<in> A. pders x r"
-
-lemma pders_lang_subsetI [intro]:
-  assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
-  shows "pders_lang A r \<subseteq> C"
-using assms unfolding pders_lang_def by (rule UN_least)
+  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 pders_lang_union:
-  shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
-by (simp add: pders_lang_def)
+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 pders_lang_subset:
-  shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r"
-by (auto simp add: pders_lang_def)
+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 pders_lang_Zero [simp]:
-  shows "pders_lang UNIV1 Zero = {}"
-unfolding UNIV1_def pders_lang_def by auto
+lemma pderivs_lang_Zero [simp]:
+  shows "pderivs_lang UNIV1 Zero = {}"
+unfolding UNIV1_def pderivs_lang_def by auto
 
-lemma pders_lang_One [simp]:
-  shows "pders_lang UNIV1 One = {}"
-unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
+lemma pderivs_lang_One [simp]:
+  shows "pderivs_lang UNIV1 One = {}"
+unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)
 
-lemma pders_lang_Atom [simp]:
-  shows "pders_lang UNIV1 (Atom c) = {One}"
-unfolding UNIV1_def pders_lang_def 
+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 pders_Atom)
+apply(rule pderivs_Atom)
 apply(simp)
 apply(case_tac xa)
 apply(auto split: if_splits)
 done
 
-lemma pders_lang_Plus [simp]:
-  shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
-unfolding UNIV1_def pders_lang_def by auto
+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 {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *}
 
 definition
-  "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+  "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
-lemma Suf_snoc:
-  shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
-unfolding Suf_def conc_def
+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 Suf_Union:
-  shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
+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 pders_lang_snoc:
-  shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
-unfolding pders_lang_def
-by (simp add: Suf_Union pders_snoc)
+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 pders_Times:
-  shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
+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: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)" 
+  have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)" 
     by fact
-  have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 
-    by (simp add: pders_snoc)
-  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))"
+  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 (auto) (blast)
-  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)"
+  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> = pder_set c (Timess (pders s r1) r2) \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
-    by (simp add: pders_lang_snoc)
-  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+  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 (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+  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) (blast)
-  also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
-    by (simp add: pders_snoc)
-  also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
-    unfolding pders_lang_def by (auto simp add: Suf_snoc)  
+  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 pders_lang_Times_aux1:
+lemma pderivs_lang_Times_aux1:
   assumes a: "s \<in> UNIV1"
-  shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
-using a unfolding UNIV1_def Suf_def pders_lang_def by auto
+  shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
+using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
 
-lemma pders_lang_Times_aux2:
+lemma pderivs_lang_Times_aux2:
   assumes a: "s \<in> UNIV1"
-  shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2"
-using a unfolding pders_lang_def by auto
+  shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"
+using a unfolding pderivs_lang_def by auto
 
-lemma pders_lang_Times [intro]:
-  shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
-apply(rule pders_lang_subsetI)
+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 pders_Times)
-using pders_lang_Times_aux1 pders_lang_Times_aux2
+apply(rule pderivs_Times)
+using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2
 apply(blast)
 done
 
-lemma pders_Star:
+lemma pderivs_Star:
   assumes a: "s \<noteq> []"
-  shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
+  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> pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" by fact
+  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 "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
-    also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
+    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 (auto) (blast)
-    also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
+    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) (blast)+
-    also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
-      by (simp only: Suf_snoc pders_lang_snoc pders_lang_union)
-         (auto simp add: pders_lang_def)
-    also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
-      by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def)
+    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
-      apply (auto simp add: pders_lang_def pders_snoc Suf_def)
+      apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
       apply(rule_tac x = "[c]" in exI)
       apply(auto)
       done
@@ -324,14 +345,14 @@
   ultimately show ?case by blast
 qed (simp)
 
-lemma pders_lang_Star [intro]:
-  shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
-apply(rule pders_lang_subsetI)
+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 pders_Star)
+apply(rule pderivs_Star)
 apply(simp add: UNIV1_def)
-apply(simp add: UNIV1_def Suf_def)
-apply(auto simp add: pders_lang_def)
+apply(simp add: UNIV1_def PSuf_def)
+apply(auto simp add: pderivs_lang_def)
 done
 
 lemma finite_Timess [simp]:
@@ -339,72 +360,27 @@
   shows "finite (Timess A r)"
 using a by auto
 
-lemma finite_pders_lang_UNIV1:
-  shows "finite (pders_lang UNIV1 r)"
+lemma finite_pderivs_lang_UNIV1:
+  shows "finite (pderivs_lang UNIV1 r)"
 apply(induct r)
 apply(simp_all add: 
-  finite_subset[OF pders_lang_Times]
-  finite_subset[OF pders_lang_Star])
+  finite_subset[OF pderivs_lang_Times]
+  finite_subset[OF pderivs_lang_Star])
 done
     
-lemma pders_lang_UNIV:
-  shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
-unfolding UNIV1_def pders_lang_def
+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_pders_lang_UNIV:
-  shows "finite (pders_lang UNIV r)"
-unfolding pders_lang_UNIV
-by (simp add: finite_pders_lang_UNIV1)
-
-lemma finite_pders_lang:
-  shows "finite (pders_lang A r)"
-apply(rule rev_finite_subset[OF finite_pders_lang_UNIV])
-apply(rule pders_lang_subset)
-apply(simp)
-done
-
-text {* Relating the Myhill-Nerode relation with left-quotients. *}
-
-lemma MN_Rel_Ders:
-  shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
-unfolding Ders_def str_eq_def
-by auto
-
-subsection {*
-  The second direction of the Myhill-Nerode theorem using
-  partial derivatives.
-*}
+lemma finite_pderivs_lang_UNIV:
+  shows "finite (pderivs_lang UNIV r)"
+unfolding pderivs_lang_UNIV
+by (simp add: finite_pderivs_lang_UNIV1)
 
-lemma Myhill_Nerode3:
-  fixes r::"'a rexp"
-  shows "finite (UNIV // \<approx>(lang r))"
-proof -
-  have "finite (UNIV // =(\<lambda>x. pders x r)=)"
-  proof - 
-    have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)"
-      unfolding pders_lang_def by auto
-    moreover 
-    have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang)
-    ultimately
-    have "finite (range (\<lambda>x. pders x r))"
-      by (simp add: finite_subset)
-    then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 
-      by (rule finite_eq_tag_rel)
-  qed
-  moreover 
-  have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
-    unfolding tag_eq_def
-    by (auto simp add: MN_Rel_Ders Ders_pders)
-  moreover 
-  have "equiv UNIV =(\<lambda>x. pders x r)="
-  and  "equiv UNIV (\<approx>(lang r))"
-    unfolding equiv_def refl_on_def sym_def trans_def
-    unfolding tag_eq_def str_eq_def
-    by auto
-  ultimately show "finite (UNIV // \<approx>(lang r))" 
-    by (rule refined_partition_finite)
-qed
+lemma finite_pderivs_lang:
+  shows "finite (pderivs_lang A r)"
+by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
 
 
 end
\ No newline at end of file