diff -r b794db0b79db -r b1258b7d2789 Closure.thy
--- a/Closure.thy	Fri Jun 03 13:59:21 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
-theory Closure
-imports Derivs
-begin
-
-section {* Closure properties of regular languages *}
-
-abbreviation
-  regular :: "lang \<Rightarrow> bool"
-where
-  "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_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 \<cdot> B)"
-proof -
-  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_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)"
-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]:
-  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]:
-  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 :: "rexp \<Rightarrow> rexp"
-where
-  "Rev NULL = NULL"
-| "Rev EMPTY = EMPTY"
-| "Rev (CHAR c) = CHAR c"
-| "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"
-| "Rev (SEQ r1 r2) = SEQ (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 Seq_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 (step s1 s2)
-  have inj: "inj (rev::string \<Rightarrow> string)" 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 intro: star_intro2)
-  then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1)
-  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 (step s1 s2)
-  have inj: "inj (rev::string \<Rightarrow> string)" 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 intro: star_intro2)
-  moreover
-  have "rev s2 \<in> (rev ` A)\<star>" by fact
-  ultimately show "rev (s1 @ s2) \<in>  (rev ` A)\<star>" by (auto intro: star_intro1)
-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 ` (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 "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