--- a/Closures.thy	Wed Aug 17 07:43:09 2011 +0000
+++ b/Closures.thy	Wed Aug 17 17:36:19 2011 +0000
@@ -1,6 +1,6 @@
 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
 theory Closures
-imports Derivatives
+imports Derivatives "~~/src/HOL/Library/Infinite_Set"
 begin
 
 section {* Closure properties of regular languages *}
@@ -160,5 +160,129 @@
   then show "regular (Ders_lang B A)" by auto
 qed
 
+subsection {* Finite and co-finite set are regular *}
+
+lemma singleton_regular:
+  shows "regular {s}"
+proof (induct s)
+  case Nil
+  have "{[]} = lang (One)" by simp
+  then show "regular {[]}" by blast
+next
+  case (Cons c s)
+  have "regular {s}" by fact
+  then obtain r where "{s} = lang r" by blast
+  then have "{c # s} = lang (Times (Atom c) r)" 
+    by (auto simp add: conc_def)
+  then show "regular {c # s}" by blast
+qed
+
+lemma finite_regular:
+  assumes "finite A"
+  shows "regular A"
+using assms
+proof (induct)
+  case empty
+  have "{} = lang (Zero)" by simp
+  then show "regular {}" by blast
+next
+  case (insert s A)
+  have "regular {s}" by (simp add: singleton_regular)
+  moreover
+  have "regular A" by fact
+  ultimately have "regular ({s} \<union> A)" by (rule closure_union)
+  then show "regular (insert s A)" by simp
+qed
+
+lemma cofinite_regular:
+  fixes A::"('a::finite list) set"
+  assumes "finite (- A)"
+  shows "regular A"
+proof -
+  from assms have "regular (- A)" by (simp add: finite_regular)
+  then have "regular (-(- A))" by (rule closure_complement)
+  then show "regular A" by simp
+qed
+
+
+subsection {* non-regularity of particular languages *}
+
+lemma continuation_lemma:
+  fixes A B::"('a::finite list) set"
+  assumes reg: "regular A"
+  and     inf: "infinite B"
+  shows "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y"
+proof -
+  def eqfun \<equiv> "\<lambda>A x::('a::finite list). (\<approx>A) `` {x}"
+  have "finite (UNIV // \<approx>A)" using reg by (simp add: Myhill_Nerode)
+  moreover
+  have "(eqfun A) ` B \<subseteq> UNIV // (\<approx>A)"
+    unfolding eqfun_def quotient_def by auto
+  ultimately have "finite ((eqfun A) ` B)" by (rule rev_finite_subset)
+  with inf have "\<exists>a \<in> B. infinite {b \<in> B. eqfun A b = eqfun A a}"
+    by (rule pigeonhole_infinite)
+  then obtain a where in_a: "a \<in> B" and "infinite {b \<in> B. eqfun A b = eqfun A a}"
+    by blast
+  moreover 
+  have "{b \<in> B. eqfun A b = eqfun A a} = {b \<in> B. b \<approx>A a}"
+    unfolding eqfun_def Image_def str_eq_def by auto
+  ultimately have "infinite {b \<in> B. b \<approx>A a}" by simp
+  then have "infinite ({b \<in> B. b \<approx>A a} - {a})" by simp
+  moreover
+  have "{b \<in> B. b \<approx>A a} - {a} = {b \<in> B. b \<approx>A a \<and> b \<noteq> a}" by auto
+  ultimately have "infinite {b \<in> B. b \<approx>A a \<and> b \<noteq> a}" by simp
+  then have "{b \<in> B. b \<approx>A a \<and> b \<noteq> a} \<noteq> {}"
+    by (metis finite.emptyI)
+  then obtain b where "b \<in> B" "b \<noteq> a" "b \<approx>A a" by blast
+  with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y"
+    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