--- a/Derivatives.thy	Thu Aug 11 16:55:41 2011 +0000
+++ b/Derivatives.thy	Thu Aug 11 23:11:39 2011 +0000
@@ -115,12 +115,12 @@
 fun
   pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 where
-  "pder c Zero = {Zero}"
-| "pder c One = {Zero}"
-| "pder c (Atom c') = (if c = c' then {One} else {Zero})"
+  "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)"
+    (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
@@ -144,11 +144,14 @@
 by (simp add: pders_append)
 
 lemma pders_simps [simp]:
-  shows "pders s Zero = {Zero}"
-  and   "pders s One = (if s = [] then {One} else {Zero})"
-  and   "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
+  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))"
-by (induct s) (auto)
+by (induct s) (simp_all)
+
+lemma pders_Atom [intro]:
+  shows "pders s (Atom c) \<subseteq> {Atom c, One}"
+by (induct s) (simp_all)
 
 subsection {* Relating left-quotients and partial derivatives *}
 
@@ -185,7 +188,7 @@
 subsection {* There are only finitely many partial derivatives for a language *}
 
 definition
-  "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r"
+  "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"
@@ -196,20 +199,31 @@
   shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
 by (simp add: pders_lang_def)
 
+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)
+
 definition
   "UNIV1 \<equiv> UNIV - {[]}"
 
 lemma pders_lang_Zero [simp]:
-  shows "pders_lang UNIV1 Zero = {Zero}"
+  shows "pders_lang UNIV1 Zero = {}"
 unfolding UNIV1_def pders_lang_def by auto
 
 lemma pders_lang_One [simp]:
-  shows "pders_lang UNIV1 One = {Zero}"
+  shows "pders_lang UNIV1 One = {}"
 unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
 
-lemma pders_lang_Atom:
-  shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
-unfolding UNIV1_def pders_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 
+apply(auto)
+apply(frule rev_subsetD)
+apply(rule pders_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"
@@ -328,15 +342,9 @@
 lemma finite_pders_lang_UNIV1:
   shows "finite (pders_lang UNIV1 r)"
 apply(induct r)
-apply(simp)
-apply(simp)
-apply(rule finite_subset[OF pders_lang_Atom])
-apply(simp)
-apply(simp)
-apply(rule finite_subset[OF pders_lang_Times])
-apply(simp)
-apply(rule finite_subset[OF pders_lang_Star])
-apply(simp)
+apply(simp_all add: 
+  finite_subset[OF pders_lang_Times]
+  finite_subset[OF pders_lang_Star])
 done
     
 lemma pders_lang_UNIV:
@@ -351,9 +359,9 @@
 
 lemma finite_pders_lang:
   shows "finite (pders_lang A r)"
-apply(rule rev_finite_subset)
-apply(rule_tac r="r" in finite_pders_lang_UNIV)
-apply(auto simp add: pders_lang_def)
+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. *}