--- a/Myhill_2.thy	Sat Feb 19 10:23:51 2011 +0000
+++ b/Myhill_2.thy	Sat Feb 19 12:01:16 2011 +0000
@@ -58,12 +58,13 @@
 *}
 
 definition 
-   f_eq_rel ("=_=")
+   tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
 where
-   "=f= \<equiv> {(x, y) | x y. f x = f y}"
+   "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
+
 
-lemma equiv_f_eq_rel:"equiv UNIV (=f=)"
-  by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
+lemma equiv_tag_eq_rel:"equiv UNIV (=f=)"
+  by (auto simp:equiv_def tag_eq_rel_def refl_on_def sym_def trans_def)
 
 lemma finite_range_image: 
   assumes "finite (range f)"
@@ -71,7 +72,9 @@
   using assms unfolding image_def
   by (rule_tac finite_subset) (auto)
 
-lemma finite_eq_f_rel:
+thm finite_imageD
+
+lemma finite_eq_tag_rel:
   assumes rng_fnt: "finite (range tag)"
   shows "finite (UNIV // =tag=)"
 proof -
@@ -83,7 +86,7 @@
       *}
     show "finite (?f ` ?A)" 
     proof -
-      have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def)
+      have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def)
       moreover from rng_fnt have "finite (Pow (range tag))" by simp
       ultimately have "finite (range ?f)"
         by (auto simp only:image_def intro:finite_subset)
@@ -94,7 +97,7 @@
       The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}:
       *}
     show "inj_on ?f ?A" 
-    proof-
+    proof -
       { fix X Y
         assume X_in: "X \<in> ?A"
           and  Y_in: "Y \<in> ?A"
@@ -105,10 +108,11 @@
           obtain x y 
             where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
             unfolding quotient_def Image_def str_eq_rel_def 
-                                   str_eq_def image_def f_eq_rel_def
+                                   str_eq_def image_def tag_eq_rel_def
             apply simp by blast
-          with X_in Y_in show ?thesis 
-            by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) 
+          with X_in Y_in show "X = Y"
+	    unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def
+	    by auto
         qed
       } thus ?thesis unfolding inj_on_def by auto
     qed
@@ -188,14 +192,14 @@
   let ?R1 = "(=tag=)"
   show ?thesis
   proof(rule_tac refined_partition_finite [of _ ?R1])
-    from finite_eq_f_rel [OF rng_fnt]
+    from finite_eq_tag_rel [OF rng_fnt]
      show "finite (UNIV // =tag=)" . 
    next
      from same_tag_eqvt
      show "(=tag=) \<subseteq> (\<approx>Lang)"
-       by (auto simp:f_eq_rel_def str_eq_def)
+       by (auto simp:tag_eq_rel_def str_eq_def)
    next
-     from equiv_f_eq_rel
+     from equiv_tag_eq_rel
      show "equiv UNIV (=tag=)" by blast
    next
      from equiv_lang_eq