--- a/Derivatives.thy	Tue Aug 09 22:14:41 2011 +0000
+++ b/Derivatives.thy	Tue Aug 09 22:15:11 2011 +0000
@@ -173,11 +173,11 @@
 
 subsection {* Relating derivatives and partial derivatives *}
 
-lemma
+lemma der_pder:
   shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
 unfolding Der_der[symmetric] Der_pder by simp
 
-lemma
+lemma ders_pders:
   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
 unfolding Ders_ders[symmetric] Ders_pders by simp
 
@@ -185,7 +185,7 @@
 subsection {* There are only finitely many partial derivatives for a language *}
 
 abbreviation
-  "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
+  "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r"
 
 text {* Non-empty suffixes of a string *}
 
@@ -201,61 +201,61 @@
   shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
 by (auto simp add: conc_def)
 
-lemma pders_set_snoc:
-  shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))"
+lemma pders_lang_snoc:
+  shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
 by (simp add: Suf_Union pders_snoc)
 
 lemma pders_Times:
-  shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)"
+  shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf 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_set (Suf s) r2)" 
+  have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf 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_set (Suf s) r2))"
+  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))"
     using ih by (auto) (blast)
-  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)"
+  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)"
     by (simp)
-  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2"
-    by (simp add: pders_set_snoc)
-  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+  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"
     by auto
-  also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
-    by (auto simp add: if_splits pders_snoc) (blast)
-  also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2"
+  also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[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> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
     by (auto simp add: Suf_snoc)  
   finally show ?case .
 qed (simp) 
 
-
 lemma pders_Star:
   assumes a: "s \<noteq> []"
-  shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))"
+  shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf 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> (\<Union>v\<in>Suf s. Timess (pders v r) (Star r))" by fact
+  have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> Timess (pders_lang (Suf 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 (\<Union>v\<in>Suf s. Timess (pders v r) (Star r)))"
+    also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
       using ih[OF asm] by (auto) (blast)
-    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))"
-      by simp
-    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
-      by (auto split: if_splits) 
-    also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
-      using asm by (auto simp add: Suf_def)
-    also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))"
-      by (simp add: pders_snoc)
-    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))"
+    also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder 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 (auto simp add: Suf_snoc pders_lang_snoc)
+    also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
       by (auto simp add: Suf_snoc Suf_Union pders_snoc)
     finally have ?case .
   }
   moreover
   { assume asm: "s = []"
     then have ?case
-      by (auto simp add: pders_snoc Suf_def)
+      apply (auto simp add: pders_snoc Suf_def)
+      apply(rule_tac x = "[c]" in exI)
+      apply(auto)
+      done
   }
   ultimately show ?case by blast
 qed (simp)
@@ -263,29 +263,29 @@
 definition
   "UNIV1 \<equiv> UNIV - {[]}"
 
-lemma pders_set_Zero:
-  shows "pders_set UNIV1 Zero = {Zero}"
+lemma pders_lang_Zero [simp]:
+  shows "pders_lang UNIV1 Zero = {Zero}"
 unfolding UNIV1_def by auto
 
-lemma pders_set_One:
-  shows "pders_set UNIV1 One = {Zero}"
+lemma pders_lang_One [simp]:
+  shows "pders_lang UNIV1 One = {Zero}"
 unfolding UNIV1_def by (auto split: if_splits)
 
-lemma pders_set_Atom:
-  shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
+lemma pders_lang_Atom:
+  shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
 unfolding UNIV1_def by (auto split: if_splits)
 
-lemma pders_set_Plus:
-  shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
+lemma pders_lang_Plus:
+  shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
 unfolding UNIV1_def by auto
 
-lemma pders_set_Times_aux:
+lemma pders_lang_Times_aux:
   assumes a: "s \<in> UNIV1"
-  shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
-using a unfolding UNIV1_def Suf_def by (auto)
+  shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
+using a unfolding UNIV1_def Suf_def by auto
 
-lemma pders_set_Times:
-  shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Timess (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+lemma pders_lang_Times [intro]:
+  shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
 unfolding UNIV1_def
 apply(rule UN_least)
 apply(rule subset_trans)
@@ -294,12 +294,12 @@
 apply(rule conjI) 
 apply(auto)[1]
 apply(rule subset_trans)
-apply(rule pders_set_Times_aux)
+apply(rule pders_lang_Times_aux)
 apply(auto simp add: UNIV1_def)
 done
 
-lemma pders_set_Star:
-  shows "pders_set UNIV1 (Star r) \<subseteq> Timess (pders_set UNIV1 r) (Star r)"
+lemma pders_lang_Star [intro]:
+  shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
 unfolding UNIV1_def
 apply(rule UN_least)
 apply(rule subset_trans)
@@ -312,60 +312,60 @@
 lemma finite_Timess:
   assumes a: "finite A"
   shows "finite (Timess A r)"
-using a by (auto)
+using a by auto
 
-lemma finite_pders_set_UNIV1:
-  shows "finite (pders_set UNIV1 r)"
+lemma finite_pders_lang_UNIV1:
+  shows "finite (pders_lang UNIV1 r)"
 apply(induct r)
 apply(simp)
-apply(simp only: pders_set_One)
+apply(simp only: pders_lang_One)
 apply(simp)
 apply(rule finite_subset)
-apply(rule pders_set_Atom)
+apply(rule pders_lang_Atom)
 apply(simp)
-apply(simp only: pders_set_Plus)
+apply(simp only: pders_lang_Plus)
 apply(simp)
 apply(rule finite_subset)
-apply(rule pders_set_Times)
+apply(rule pders_lang_Times)
 apply(simp only: finite_Timess finite_Un)
 apply(simp)
 apply(rule finite_subset)
-apply(rule pders_set_Star)
+apply(rule pders_lang_Star)
 apply(simp only: finite_Timess)
 done
     
-lemma pders_set_UNIV_UNIV1:
-  shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
+lemma pders_lang_UNIV_UNIV1:
+  shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
 unfolding UNIV1_def
 apply(auto)
 apply(rule_tac x="[]" in exI)
 apply(simp)
 done
 
-lemma finite_pders_set_UNIV:
-  shows "finite (pders_set UNIV r)"
-unfolding pders_set_UNIV_UNIV1
-by (simp add: finite_pders_set_UNIV1)
+lemma finite_pders_lang_UNIV:
+  shows "finite (pders_lang UNIV r)"
+unfolding pders_lang_UNIV_UNIV1
+by (simp add: finite_pders_lang_UNIV1)
 
-lemma finite_pders_set:
-  shows "finite (pders_set A r)"
+lemma finite_pders_lang:
+  shows "finite (pders_lang A r)"
 apply(rule rev_finite_subset)
-apply(rule_tac r="r" in finite_pders_set_UNIV)
+apply(rule_tac r="r" in finite_pders_lang_UNIV)
 apply(auto)
 done
 
 lemma finite_pders:
   shows "finite (pders s r)"
-using finite_pders_set[where A="{s}" and r="r"]
+using finite_pders_lang[where A="{s}" and r="r"]
 by simp
 
 lemma finite_pders2:
   shows "finite {pders s r | s. s \<in> A}"
 proof -
-  have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto
+  have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_lang A r)" by auto
   moreover
-  have "finite (Pow (pders_set A r))"
-    using finite_pders_set by simp
+  have "finite (Pow (pders_lang A r))"
+    using finite_pders_lang by simp
   ultimately 
   show "finite {pders s r | s. s \<in> A}"
     by(rule finite_subset)
@@ -405,13 +405,9 @@
     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
-    by auto
-  moreover
-  have "equiv UNIV (\<approx>(lang r))"
-    unfolding equiv_def refl_on_def sym_def trans_def
-    unfolding str_eq_def
+    unfolding tag_eq_def str_eq_def
     by auto
   ultimately show "finite (UNIV // \<approx>(lang r))" 
     by (rule refined_partition_finite)