# HG changeset patch
# User urbanc
# Date 1316007543 0
# Node ID bcef7669f55a88413ca984d25b7228221b10009c
# Parent  8e2c497d699eb2778562b5142a05c1df986112ae
polished the non-regularity proof

diff -r 8e2c497d699e -r bcef7669f55a Closures.thy
--- 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
diff -r 8e2c497d699e -r bcef7669f55a Journal/Paper.thy
--- 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