--- 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

--- a/Journal/Paper.thy	Wed Sep 14 13:00:44 2011 +0000
+++ b/Journal/Paper.thy	Wed Sep 14 13:39:03 2011 +0000
@@ -2440,7 +2440,7 @@
   code.  The closure properties in Section~\ref{closure} (except Theorem~\ref{subseqreg}) 
   can be established in
   190 lines of code. The Continuation Lemma and the non-regularity of @{text "a\<^sup>n b\<^sup>n"} 
-  require 80 lines of code.
+  require 70 lines of code.
   The algorithm for solving equational systems, which we
   used in the first direction, is conceptually relatively simple. Still the
   use of sets over which the algorithm operates means it is not as easy to