--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Closures.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -0,0 +1,161 @@
+(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
+theory Closures
+imports Derivatives
+begin
+
+section {* Closure properties of regular languages *}
+
+abbreviation
+  regular :: "'a lang \<Rightarrow> bool"
+where
+  "regular A \<equiv> \<exists>r. A = lang 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::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto
+  then have "A \<union> B = lang (Plus 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 \<cdot> B)"
+proof -
+  from assms obtain r1 r2::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto
+  then have "A \<cdot> B = lang (Times 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::"'a rexp" where "lang r = A" by auto
+  then have "A\<star> = lang (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]:
+  fixes A::"('a::finite) lang"
+  assumes "regular A"
+  shows "regular (- A)"
+proof -
+  from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)
+  then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)
+  then show "regular (- A)" by (simp add: Myhill_Nerode)
+qed
+
+lemma closure_difference [intro]:
+  fixes A::"('a::finite) lang"
+  assumes "regular A" "regular B" 
+  shows "regular (A - B)"
+proof -
+  have "A - B = - (- A \<union> B)" by blast
+  moreover
+  have "regular (- (- A \<union> B))" 
+    using assms by blast
+  ultimately show "regular (A - B)" by simp
+qed
+
+lemma closure_intersection [intro]:
+  fixes A::"('a::finite) lang"
+  assumes "regular A" "regular B" 
+  shows "regular (A \<inter> B)"
+proof -
+  have "A \<inter> B = - (- A \<union> - B)" by blast
+  moreover
+  have "regular (- (- A \<union> - B))" 
+    using assms by blast
+  ultimately show "regular (A \<inter> B)" by simp
+qed
+
+subsection {* Closure under string reversal *}
+
+fun
+  Rev :: "'a rexp \<Rightarrow> 'a rexp"
+where
+  "Rev Zero = Zero"
+| "Rev One = One"
+| "Rev (Atom c) = Atom c"
+| "Rev (Plus r1 r2) = Plus (Rev r1) (Rev r2)"
+| "Rev (Times r1 r2) = Times (Rev r2) (Rev r1)"
+| "Rev (Star r) = Star (Rev r)"
+
+lemma rev_seq[simp]:
+  shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)"
+unfolding conc_def image_def
+by (auto) (metis rev_append)+
+
+lemma rev_star1:
+  assumes a: "s \<in> (rev ` A)\<star>"
+  shows "s \<in> rev ` (A\<star>)"
+using a
+proof(induct rule: star_induct)
+  case (append s1 s2)
+  have inj: "inj (rev::'a list \<Rightarrow> 'a list)" unfolding inj_on_def by auto
+  have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+
+  then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto
+  then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto)
+  then have "x2 @ x1 \<in> A\<star>" by (auto)
+  then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff)
+  then show "s1 @ s2 \<in>  rev ` A\<star>" using eqs by simp
+qed (auto)
+
+lemma rev_star2:
+  assumes a: "s \<in> A\<star>"
+  shows "rev s \<in> (rev ` A)\<star>"
+using a
+proof(induct rule: star_induct)
+  case (append s1 s2)
+  have inj: "inj (rev::'a list \<Rightarrow> 'a list)" unfolding inj_on_def by auto
+  have "s1 \<in> A"by fact
+  then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff)
+  then have "rev s1 \<in> (rev ` A)\<star>" by (auto)
+  moreover
+  have "rev s2 \<in> (rev ` A)\<star>" by fact
+  ultimately show "rev (s1 @ s2) \<in>  (rev ` A)\<star>" by (auto)
+qed (auto)
+
+lemma rev_star [simp]:
+  shows " rev ` (A\<star>) = (rev ` A)\<star>"
+using rev_star1 rev_star2 by auto
+
+lemma rev_lang:
+  shows "rev ` (lang r) = lang (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::"'a rexp" where "A = lang r" by auto
+  then have "lang (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::"'a rexp" where eq: "lang r = A" by auto
+  have fin: "finite (pders_set B r)" by (rule finite_pders_set)
+  
+  have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))"
+    by (simp add: Ders_set_pders_set)
+  also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp
+  finally have "Ders_set B A = lang (\<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