--- a/Closures.thy	Wed Sep 14 13:00:44 2011 +0000
+++ b/Closures.thy	Wed Sep 14 13:39:03 2011 +0000
@@ -250,9 +250,6 @@
 where
   "a ^^^ n \<equiv> replicate n a"
 
-definition
-  "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)"
-
 lemma an_bn_not_regular:
   shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})"
 proof
@@ -261,8 +258,13 @@
   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 sameness: "\<And>i j. CHR ''a'' ^^^ i @ CHR ''b'' ^^^ j \<in> A \<longleftrightarrow> i = j"
+    unfolding A_def 
+    apply auto
+    apply(drule_tac f="\<lambda>s. length (filter (op= (CHR ''a'')) s) = length (filter (op= (CHR ''b'')) s)" 
+      in arg_cong)
+    apply(simp)
+    done
 
   have b: "infinite B"
     unfolding infinite_iff_countable_subset
@@ -275,13 +277,7 @@
     apply(auto)
     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)
+    apply(simp add: sameness)
     done
   ultimately 
   show "False" using continuation_lemma[OF as] by blast