diff -r b04cc5e4e84c -r 7743d2ad71d1 Derivs.thy
--- a/Derivs.thy	Tue May 31 20:32:49 2011 +0000
+++ b/Derivs.thy	Thu Jun 02 16:44:35 2011 +0000
@@ -1,8 +1,8 @@
 theory Derivs
-imports Closure
+imports Myhill_2
 begin
 
-section {* Experiments with Derivatives -- independent of Myhill-Nerode *}
+section {* Left-Quotients and Derivatives *}
 
 subsection {* Left-Quotients *}
 
@@ -52,30 +52,30 @@
 by auto
 
 lemma Der_seq [simp]:
-  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (Delta A ;; Der c B)"
+  shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
 unfolding Der_def Delta_def
 unfolding Seq_def
 by (auto simp add: Cons_eq_append_conv)
 
 lemma Der_star [simp]:
-  shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+  shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
 proof -
-  have incl: "Delta A ;; Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+  have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
     unfolding Der_def Delta_def Seq_def
     apply(auto)
     apply(drule star_decom)
     apply(auto simp add: Cons_eq_append_conv)
     done
     
-  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+  have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"
     by (simp only: star_cases[symmetric])
-  also have "... = Der c (A ;; A\<star>)"
+  also have "... = Der c (A \<cdot> A\<star>)"
     by (simp only: Der_union Der_empty) (simp)
-  also have "... = (Der c A) ;; A\<star> \<union> (Delta A ;; Der c (A\<star>))"
+  also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
     by simp
-  also have "... =  (Der c A) ;; A\<star>"
+  also have "... =  (Der c A) \<cdot> A\<star>"
     using incl by auto
-  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . 
+  finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 
 qed
 
 
@@ -126,18 +126,18 @@
   by (relation "measure (length o fst)") (auto)
 
 lemma Delta_nullable:
-  shows "Delta (L r) = (if nullable r then {[]} else {})"
+  shows "Delta (L_rexp r) = (if nullable r then {[]} else {})"
 unfolding Delta_def
 by (induct r) (auto simp add: Seq_def split: if_splits)
 
 lemma Der_der:
   fixes r::rexp
-  shows "Der c (L r) = L (der c r)"
+  shows "Der c (L_rexp r) = L_rexp (der c r)"
 by (induct r) (simp_all add: Delta_nullable)
 
 lemma Ders_ders:
   fixes r::rexp
-  shows "Ders s (L r) = L (ders s r)"
+  shows "Ders s (L_rexp r) = L_rexp (ders s r)"
 apply(induct s rule: rev_induct)
 apply(simp add: Ders_def)
 apply(simp only: ders.simps)
@@ -195,44 +195,44 @@
 done
 
 lemma pder_set_lang:
-  shows "(\<Union> (L ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))"
+  shows "(\<Union> (L_rexp ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L_rexp ` (pder c r)))"
 unfolding image_def 
 by auto
 
 lemma
-  shows seq_UNION_left:  "B ;; (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B ;; A n)"
-  and   seq_UNION_right: "(\<Union>n\<in>C. A n) ;; B = (\<Union>n\<in>C. A n ;; B)"
+  shows seq_UNION_left:  "B \<cdot> (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B \<cdot> A n)"
+  and   seq_UNION_right: "(\<Union>n\<in>C. A n) \<cdot> B = (\<Union>n\<in>C. A n \<cdot> B)"
 unfolding Seq_def by auto
 
 lemma Der_pder:
   fixes r::rexp
-  shows "Der c (L r) = \<Union> L ` (pder c r)"
+  shows "Der c (L_rexp r) = \<Union> L_rexp ` (pder c r)"
 by (induct r) (auto simp add: Delta_nullable seq_UNION_right)
 
 lemma Ders_pders:
   fixes r::rexp
-  shows "Ders s (L r) = \<Union> L ` (pders s r)"
+  shows "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)"
 proof (induct s rule: rev_induct)
   case (snoc c s)
-  have ih: "Ders s (L r) = \<Union> L ` (pders s r)" by fact
-  have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"
+  have ih: "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)" by fact
+  have "Ders (s @ [c]) (L_rexp r) = Ders [c] (Ders s (L_rexp r))"
     by (simp add: Ders_append)
-  also have "\<dots> = Der c (\<Union> L ` (pders s r))" using ih
+  also have "\<dots> = Der c (\<Union> L_rexp ` (pders s r))" using ih
     by (simp add: Ders_singleton)
-  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L r))" 
+  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L_rexp r))" 
     unfolding Der_def image_def by auto
-  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L `  (pder c r)))"
+  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L_rexp `  (pder c r)))"
     by (simp add: Der_pder)
-  also have "\<dots> = (\<Union>L ` (pder_set c (pders s r)))"
+  also have "\<dots> = (\<Union>L_rexp ` (pder_set c (pders s r)))"
     by (simp add: pder_set_lang)
-  also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))"
+  also have "\<dots> = (\<Union>L_rexp ` (pders (s @ [c]) r))"
     by simp
-  finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" .
+  finally show "Ders (s @ [c]) (L_rexp r) = \<Union> L_rexp ` pders (s @ [c]) r" .
 qed (simp add: Ders_def)
 
 lemma Ders_set_pders_set:
   fixes r::rexp
-  shows "Ders_set A (L r) = (\<Union> L ` (pders_set A r))"
+  shows "Ders_set A (L_rexp r) = (\<Union> L_rexp ` (pders_set A r))"
 by (simp add: Ders_set_Ders Ders_pders)
 
 lemma pders_NULL [simp]:
@@ -255,12 +255,12 @@
   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
 lemma Suf:
-  shows "Suf (s @ [c]) = (Suf s) ;; {[c]} \<union> {[c]}"
+  shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
 unfolding Suf_def Seq_def
 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
 
 lemma Suf_Union:
-  shows "(\<Union>v \<in> Suf s ;; {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+  shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
 by (auto simp add: Seq_def)
 
 lemma inclusion1:
@@ -277,7 +277,7 @@
     by fact
   have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp
   also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
-    using ih by auto 
+    using ih by (auto) (blast)
   also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
     by (simp)
   also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
@@ -309,7 +309,7 @@
     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))"
       by simp
     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))"
-      using inclusion1 by blast
+      using inclusion1 by (auto split: if_splits) 
     also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (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. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))"
@@ -444,78 +444,49 @@
 
 lemma Myhill_Nerode3:
   fixes r::"rexp"
-  shows "finite (UNIV // \<approx>(L r))"
+  shows "finite (UNIV // \<approx>(L_rexp r))"
 proof -
   have "finite (UNIV // =(\<lambda>x. pders x r)=)"
   proof - 
-    have "range (\<lambda>x. pders x r) \<subseteq> {pders s r | s. s \<in> UNIV}" by auto
+    have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto
     moreover 
     have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)
     ultimately
     have "finite (range (\<lambda>x. pders x r))"
-      by (rule finite_subset)
+      by simp
     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>(L r)"
+  have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(L_rexp r)"
     unfolding tag_eq_rel_def
-    by (auto simp add: str_eq_def[symmetric] MN_Rel_Ders Ders_pders)
+    unfolding str_eq_def2
+    unfolding MN_Rel_Ders
+    unfolding Ders_pders
+    by auto
   moreover 
   have "equiv UNIV =(\<lambda>x. pders x r)="
     unfolding equiv_def refl_on_def sym_def trans_def
     unfolding tag_eq_rel_def
     by auto
   moreover
-  have "equiv UNIV (\<approx>(L r))"
+  have "equiv UNIV (\<approx>(L_rexp r))"
     unfolding equiv_def refl_on_def sym_def trans_def
     unfolding str_eq_rel_def
     by auto
-  ultimately show "finite (UNIV // \<approx>(L r))" 
+  ultimately show "finite (UNIV // \<approx>(L_rexp r))" 
     by (rule refined_partition_finite)
 qed
 
 
-section {* Closure under Left-Quotients *}
-
-lemma closure_left_quotient:
-  assumes "regular A"
-  shows "regular (Ders_set B A)"
-proof -
-  from assms obtain r::rexp where eq: "L r = A" by auto
-  have fin: "finite (pders_set B r)" by (rule finite_pders_set)
-  
-  have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))"
-    by (simp add: Ders_set_pders_set)
-  also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp
-  finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq
-    by simp
-  then show "regular (Ders_set B A)" by auto
-qed
-
-
-section {* Relating standard and partial derivations *}
+section {* Relating derivatives and partial derivatives *}
 
 lemma
-  shows "(\<Union> L ` (pder c r)) = L (der c r)"
+  shows "(\<Union> L_rexp ` (pder c r)) = L_rexp (der c r)"
 unfolding Der_der[symmetric] Der_pder by simp
 
 lemma
-  shows "(\<Union> L ` (pders s r)) = L (ders s r)"
+  shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)"
 unfolding Ders_ders[symmetric] Ders_pders by simp
 
-
-
-fun
-  width :: "rexp \<Rightarrow> nat"
-where
-  "width (NULL) = 0"
-| "width (EMPTY) = 0"
-| "width (CHAR c) = 1"
-| "width (ALT r1 r2) = width r1 + width r2"
-| "width (SEQ r1 r2) = width r1 + width r2"
-| "width (STAR r) = width r"
-
-
- 
 end
\ No newline at end of file