--- a/Closures.thy	Fri Sep 02 09:53:56 2011 +0000
+++ b/Closures.thy	Fri Sep 02 12:19:00 2011 +0000
@@ -164,7 +164,6 @@
   then show "regular (Deriv_lang B A)" by auto
 qed
 
-
 subsection {* Finite and co-finite sets are regular *}
 
 lemma singleton_regular:
@@ -213,7 +212,7 @@
 subsection {* Non-regularity for languages *}
 
 lemma continuation_lemma:
-  fixes A B::"('a::finite list) set"
+  fixes A B::"'a::finite lang"
   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"
@@ -244,31 +243,57 @@
 qed
 
 
+subsubsection {* The language @{text "a ^ n b ^ n"} is not regular *}
 
-(* tests *)
-definition
-  "quot A B \<equiv> {x. \<exists>y \<in> B. x @ y \<in> A}"
+abbreviation
+  replicate_rev ("_ ^^^ _" [100, 100] 100)
+where
+  "a ^^^ n \<equiv> replicate n a"
 
 definition
-  "quot1 A B \<equiv> {x. \<exists>y \<in> B. y @ x \<in> A}"
+  "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)"
+
+lemma [simp]:
+  assumes "i \<noteq> j" "a \<noteq> b"
+  shows "length_test ((a ^^^ i) @ (b ^^^ j)) a b \<noteq> length_test ((a ^^^ n) @ (b ^^^ n)) a b"
+using assms unfolding length_test_def by auto
 
-lemma
-  "quot1 A B \<subseteq> Deriv_lang B A"
-unfolding quot1_def Derivs_def
-apply(auto)
-done
+lemma [simp]:
+  assumes "a \<noteq> b"
+  shows "filter (op= a) ((a ^^^ i) @ (b ^^^ j)) = a ^^^ i"
+  and   "filter (op= b) ((a ^^^ i) @ (b ^^^ j)) = b ^^^ j"
+using assms by simp_all
+
+lemma length_test:
+  "x = y \<Longrightarrow> length_test x a b = length_test y a b"
+by simp
 
-lemma  
-  "rev ` quot1 A B \<subseteq> quot (rev ` A) (rev ` B)"
-unfolding quot_def quot1_def
-apply(auto)
-unfolding image_def
-apply(auto)
-apply(rule_tac x="y" in bexI)
-apply(rule_tac x="y @ xa" in bexI)
-apply(auto)
-done
+lemma an_bn_not_regular:
+  shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})"
+proof
+  def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}"
+  def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
 
+  assume as: "regular A"
+  def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
+  have b: "infinite B"
+    unfolding infinite_iff_countable_subset
+    apply(rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI)
+    apply(auto simp add: inj_on_def B_def)
+    done
+  moreover
+  have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 
+    apply(auto simp add: B_def A_def)
+    apply(auto simp add: str_eq_def)
+    apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)
+    (*apply(auto simp add: f_def dest: l3)*)
+    apply(auto)
+    apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)
+    apply(simp add: length_test_def)
+    done
+  ultimately 
+  show "False" using continuation_lemma[OF as] by blast
+qed
 
 
 end
\ No newline at end of file