--- a/Closures.thy	Wed Sep 14 11:46:50 2011 +0000
+++ b/Closures.thy	Wed Sep 14 13:00:44 2011 +0000
@@ -253,29 +253,34 @@
 definition
   "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)"
 
-lemma length_test:
-  "x = y \<Longrightarrow> length_test x a b = length_test y a b"
-by simp
-
 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 length_test: "\<And>s. s \<in> A \<Longrightarrow> length_test s (CHR ''a'') (CHR ''b'')"
+    unfolding A_def length_test_def by auto
+
   have b: "infinite B"
     unfolding infinite_iff_countable_subset
     unfolding inj_on_def B_def
     by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto)
   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)
+  have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)"
+    apply(auto)
+    unfolding B_def
     apply(auto)
-    apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)
+    apply(simp add: str_eq_def)
+    apply(drule_tac x="CHR ''b'' ^^^ n" in spec)
+    apply(subgoal_tac "CHR ''a'' ^^^ na @ CHR ''b'' ^^^ n \<notin> A")
+    apply(subgoal_tac "CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n \<in> A")
+    apply(blast)
+    apply(auto simp add: A_def)[1]
+    apply(rule notI)
+    apply(drule length_test)
     apply(simp add: length_test_def)
     done
   ultimately