diff -r 09e6f3719cbc -r 5d724fe0e096 Closures.thy
--- a/Closures.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Closures.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -1,6 +1,6 @@
 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
 theory Closures
-imports Derivatives "~~/src/HOL/Library/Infinite_Set"
+imports Myhill "~~/src/HOL/Library/Infinite_Set"
 begin
 
 section {* Closure properties of regular languages *}
@@ -10,7 +10,7 @@
 where
   "regular A \<equiv> \<exists>r. A = lang r"
 
-subsection {* Closure under set operations *}
+subsection {* Closure under @{text "\<union>"}, @{text "\<cdot>"} and @{text "\<star>"} *}
 
 lemma closure_union [intro]:
   assumes "regular A" "regular B" 
@@ -39,6 +39,8 @@
   then show "regular (A\<star>)" by blast
 qed
 
+subsection {* Closure under complementation *}
+
 text {* Closure under complementation is proved via the 
   Myhill-Nerode theorem *}
 
@@ -52,6 +54,8 @@
   then show "regular (- A)" by (simp add: Myhill_Nerode)
 qed
 
+subsection {* Closure under @{text "-"} and @{text "\<inter>"} *}
+
 lemma closure_difference [intro]:
   fixes A::"('a::finite) lang"
   assumes "regular A" "regular B" 
@@ -143,24 +147,24 @@
 subsection {* Closure under left-quotients *}
 
 abbreviation
-  "Ders_lang A B \<equiv> \<Union>x \<in> A. Ders x B"
+  "Deriv_lang A B \<equiv> \<Union>x \<in> A. Derivs x B"
 
 lemma closure_left_quotient:
   assumes "regular A"
-  shows "regular (Ders_lang B A)"
+  shows "regular (Deriv_lang B A)"
 proof -
   from assms obtain r::"'a rexp" where eq: "lang r = A" by auto
-  have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
+  have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang)
   
-  have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
-    by (simp add: Ders_pders pders_lang_def)
-  also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
-  finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
+  have "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"
+    by (simp add: Derivs_pderivs pderivs_lang_def)
+  also have "\<dots> = lang (\<Uplus>(pderivs_lang B r))" using fin by simp
+  finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq
     by simp
-  then show "regular (Ders_lang B A)" by auto
+  then show "regular (Deriv_lang B A)" by auto
 qed
 
-subsection {* Finite and co-finite set are regular *}
+subsection {* Finite and co-finite sets are regular *}
 
 lemma singleton_regular:
   shows "regular {s}"
@@ -205,7 +209,7 @@
 qed
 
 
-subsection {* non-regularity of particular languages *}
+subsection {* Non-regularity for languages *}
 
 lemma continuation_lemma:
   fixes A B::"('a::finite list) set"
@@ -238,51 +242,5 @@
     by blast
 qed
 
-definition
-  "ex1 a b \<equiv> {replicate n a @ replicate n b | n. True}"
-
-(*
-lemma
-  fixes a b::"'a::finite"
-  assumes "a \<noteq> b"
-  shows "\<not> regular (ex1 a b)"
-proof -
-  { assume a: "regular (ex1 a b)"
-    def fool \<equiv> "{replicate i a | i. True}"
-    have b: "infinite fool"
-      unfolding fool_def
-      unfolding infinite_iff_countable_subset
-      apply(rule_tac x="\<lambda>i. replicate i a" in exI)
-      apply(auto simp add: inj_on_def)
-      done
-    from a b have "\<exists>x \<in> fool. \<exists>y \<in> fool. x \<noteq> y \<and> x \<approx>(ex1 a b) y"
-      using continuation_lemma by blast
-    moreover
-    have c: "\<forall>x \<in> fool. \<forall>y \<in> fool. x \<noteq> y \<longrightarrow> \<not>(x \<approx>(ex1 a b) y)"
-      apply(rule ballI)
-      apply(rule ballI)
-      apply(rule impI)
-      unfolding fool_def
-      apply(simp)
-      apply(erule exE)+
-      unfolding str_eq_def
-      apply(simp)
-      apply(rule_tac x="replicate i b" in exI)
-      apply(simp add: ex1_def)
-      apply(rule iffI)
-      prefer 2
-      apply(rule_tac x="i" in exI)
-      apply(simp)
-      apply(rule allI)
-      apply(rotate_tac 3)
-      apply(thin_tac "?X")
-      apply(auto)
-      sorry
-    ultimately have "False" by auto
-  }
-  then show "\<not> regular (ex1 a b)" by auto
-qed
-*)    
-  
 
 end
\ No newline at end of file