--- a/Closure.thy	Tue May 31 20:32:49 2011 +0000
+++ b/Closure.thy	Thu Jun 02 16:44:35 2011 +0000
@@ -1,5 +1,6 @@
+(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
 theory Closure
-imports Myhill_2
+imports Derivs
 begin
 
 section {* Closure properties of regular languages *}
@@ -7,36 +8,40 @@
 abbreviation
   regular :: "lang \<Rightarrow> bool"
 where
-  "regular A \<equiv> \<exists>r::rexp. A = L r"
+  "regular A \<equiv> \<exists>r. A = L_rexp r"
 
+subsection {* Closure under set operations *}
 
 lemma closure_union[intro]:
   assumes "regular A" "regular B" 
   shows "regular (A \<union> B)"
 proof -
-  from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
-  then have "A \<union> B = L (ALT r1 r2)" by simp
+  from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto
+  then have "A \<union> B = L_rexp (ALT r1 r2)" by simp
   then show "regular (A \<union> B)" by blast
 qed
 
 lemma closure_seq[intro]:
   assumes "regular A" "regular B" 
-  shows "regular (A ;; B)"
+  shows "regular (A \<cdot> B)"
 proof -
-  from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
-  then have "A ;; B = L (SEQ r1 r2)" by simp
-  then show "regular (A ;; B)" by blast
+  from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto
+  then have "A \<cdot> B = L_rexp (SEQ r1 r2)" by simp
+  then show "regular (A \<cdot> B)" by blast
 qed
 
 lemma closure_star[intro]:
   assumes "regular A"
   shows "regular (A\<star>)"
 proof -
-  from assms obtain r::rexp where "L r = A" by auto
-  then have "A\<star> = L (STAR r)" by simp
+  from assms obtain r::rexp where "L_rexp r = A" by auto
+  then have "A\<star> = L_rexp (STAR r)" by simp
   then show "regular (A\<star>)" by blast
 qed
 
+text {* Closure under complementation is proved via the 
+  Myhill-Nerode theorem *}
+
 lemma closure_complement[intro]:
   assumes "regular A"
   shows "regular (- A)"
@@ -68,8 +73,7 @@
   ultimately show "regular (A \<inter> B)" by simp
 qed
 
-
-text {* closure under string reversal *}
+subsection {* Closure under string reversal *}
 
 fun
   Rev :: "rexp \<Rightarrow> rexp"
@@ -81,15 +85,12 @@
 | "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"
 | "Rev (STAR r) = STAR (Rev r)"
 
-lemma rev_Seq:
-  "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"
+lemma rev_seq[simp]:
+  shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)"
 unfolding Seq_def image_def
-apply(auto)
-apply(rule_tac x="xb @ xa" in exI)
-apply(auto)
-done
+by (auto) (metis rev_append)+
 
-lemma rev_Star1:
+lemma rev_star1:
   assumes a: "s \<in> (rev ` A)\<star>"
   shows "s \<in> rev ` (A\<star>)"
 using a
@@ -104,7 +105,7 @@
   then show "s1 @ s2 \<in>  rev ` A\<star>" using eqs by simp
 qed (auto)
 
-lemma rev_Star2:
+lemma rev_star2:
   assumes a: "s \<in> A\<star>"
   shows "rev s \<in> (rev ` A)\<star>"
 using a
@@ -119,22 +120,39 @@
   ultimately show "rev (s1 @ s2) \<in>  (rev ` A)\<star>" by (auto intro: star_intro1)
 qed (auto)
 
-lemma rev_Star:
-  "(rev ` A)\<star> = rev ` (A\<star>)"
-using rev_Star1 rev_Star2 by auto
+lemma rev_star[simp]:
+  shows " rev ` (A\<star>) = (rev ` A)\<star>"
+using rev_star1 rev_star2 by auto
 
 lemma rev_lang:
-  "L (Rev r) = rev ` (L r)"
-by (induct r) (simp_all add: rev_Star rev_Seq image_Un)
+  shows "rev ` (L_rexp r) = L_rexp (Rev r)"
+by (induct r) (simp_all add: image_Un)
 
 lemma closure_reversal[intro]:
   assumes "regular A"
   shows "regular (rev ` A)"
 proof -
-  from assms obtain r::rexp where "L r = A" by auto
-  then have "L (Rev r) = rev ` A" by (simp add: rev_lang)
+  from assms obtain r::rexp where "A = L_rexp r" by auto
+  then have "L_rexp (Rev r) = rev ` A" by (simp add: rev_lang)
   then show "regular (rev` A)" by blast
 qed
   
+subsection {* 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_rexp r = A" by auto
+  have fin: "finite (pders_set B r)" by (rule finite_pders_set)
+  
+  have "Ders_set B (L_rexp r) = (\<Union> L_rexp ` (pders_set B r))"
+    by (simp add: Ders_set_pders_set)
+  also have "\<dots> = L_rexp (\<Uplus>(pders_set B r))" using fin by simp
+  finally have "Ders_set B A = L_rexp (\<Uplus>(pders_set B r))" using eq
+    by simp
+  then show "regular (Ders_set B A)" by auto
+qed
+
 
 end
\ No newline at end of file