--- a/Myhill_2.thy	Tue May 31 20:32:49 2011 +0000
+++ b/Myhill_2.thy	Thu Jun 02 16:44:35 2011 +0000
@@ -3,17 +3,22 @@
           "~~/src/HOL/Library/List_Prefix"
 begin
 
-section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
+section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
 
 definition
   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
 where
   "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
+lemma str_eq_def2:
+  shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"
+unfolding str_eq_def
+by simp
+
 definition 
    tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
 where
-   "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
+   "=tag= \<equiv> {(x, y). tag x = tag y}"
 
 lemma finite_eq_tag_rel:
   assumes rng_fnt: "finite (range tag)"
@@ -216,7 +221,7 @@
      (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
 lemma Seq_in_cases:
-  assumes "x @ z \<in> A ;; B"
+  assumes "x @ z \<in> A \<cdot> B"
   shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> 
          (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
 using assms
@@ -225,12 +230,12 @@
 
 lemma tag_str_SEQ_injI:
   assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" 
-  shows "x \<approx>(A ;; B) y"
+  shows "x \<approx>(A \<cdot> B) y"
 proof -
   { fix x y z
-    assume xz_in_seq: "x @ z \<in> A ;; B"
+    assume xz_in_seq: "x @ z \<in> A \<cdot> B"
     and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
-    have"y @ z \<in> A ;; B" 
+    have"y @ z \<in> A \<cdot> B" 
     proof -
       { (* first case with x' in A and (x - x') @ z in B *)
         fix x'
@@ -259,7 +264,7 @@
           with pref_y' y'_in 
           show ?thesis using that by blast
         qed
-	then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def)
+	then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def)
       } 
       moreover 
       { (* second case with x @ z' in A and z - z' in B *)
@@ -269,25 +274,25 @@
            using tag_xy unfolding tag_str_SEQ_def by simp
          with h2 have "y @ z' \<in> A"
             unfolding Image_def str_eq_rel_def str_eq_def by auto
-        with h1 h3 have "y @ z \<in> A ;; B"
+        with h1 h3 have "y @ z \<in> A \<cdot> B"
 	  unfolding prefix_def Seq_def
 	  by (auto) (metis append_assoc)
       }
-      ultimately show "y @ z \<in> A ;; B" 
+      ultimately show "y @ z \<in> A \<cdot> B" 
 	using Seq_in_cases [OF xz_in_seq] by blast
     qed
   }
   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-    show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast
+    show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast
 qed 
 
 lemma quot_seq_finiteI [intro]:
   fixes L1 L2::"lang"
   assumes fin1: "finite (UNIV // \<approx>L1)" 
   and     fin2: "finite (UNIV // \<approx>L2)" 
-  shows "finite (UNIV // \<approx>(L1 ;; L2))"
+  shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"
 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
-  show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
+  show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
     by (rule tag_str_SEQ_injI)
 next
   have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 
@@ -431,7 +436,7 @@
         with eq_zab show ?thesis by simp
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim: prefixE)
     qed
   } 
   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
@@ -439,15 +444,15 @@
 qed
 
 lemma quot_star_finiteI [intro]:
-  assumes finite1: "finite (UNIV // \<approx>L1)"
-  shows "finite (UNIV // \<approx>(L1\<star>))"
-proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
-  show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"
+  assumes finite1: "finite (UNIV // \<approx>A)"
+  shows "finite (UNIV // \<approx>(A\<star>))"
+proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD)
+  show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y"
     by (rule tag_str_STAR_injI)
 next
-  have *: "finite (Pow (UNIV // \<approx>L1))" 
+  have *: "finite (Pow (UNIV // \<approx>A))" 
     using finite1 by auto
-  show "finite (range (tag_str_STAR L1))"
+  show "finite (range (tag_str_STAR A))"
     unfolding tag_str_STAR_def
     apply(rule finite_subset[OF _ *])
     unfolding quotient_def
@@ -457,13 +462,12 @@
 subsubsection{* The conclusion *}
 
 lemma Myhill_Nerode2:
-  fixes r::"rexp"
-  shows "finite (UNIV // \<approx>(L r))"
+  shows "finite (UNIV // \<approx>(L_rexp r))"
 by (induct r) (auto)
 
 
 theorem Myhill_Nerode:
-  shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+  shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
 using Myhill_Nerode1 Myhill_Nerode2 by auto
 
 end