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

--- a/Paper/Paper.thy	Sat Feb 19 10:23:51 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 12:01:16 2011 +0000
@@ -365,10 +365,13 @@
   The key definition in the Myhill-Nerode theorem is the
   \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 
   strings are related, provided there is no distinguishing extension in this
-  language. This can be defined as tertiary relation:
+  language. This can be defined as tertiary relation.
 
-  \begin{definition}[Myhill-Nerode Relation]\mbox{}\\
+  \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+  @{text y} are related provided
+  \begin{center}
   @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
+  \end{center}
   \end{definition}
 
   \noindent
@@ -877,10 +880,52 @@
   \end{proof}
 
   \noindent
-  Much more interesting are the inductive cases, which seem hard to be solved 
-  directly. The reader is invited to try. Our method will rely on some
+  Much more interesting, however, are the inductive cases. They seem hard to be solved 
+  directly. The reader is invited to try. 
+
+  Our method will rely on some
   \emph{tagging} functions of strings. Given the inductive hypothesis, it will 
   be easy to prove that the range of these tagging functions is finite.
+  With this we will be able to infer that the tagging functions, seen as a relation,
+  give rise to finitely many equivalence classes of @{const UNIV}. Finally we 
+  will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which
+  implies that @{term "UNIV // \<approx>(L r)"} must also be finite. For this we define the 
+  notion of a \emph{tag-relation} (which is often also called a kernel relation).
+
+  \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x}
+  and @{text y} are tag-related provided
+  \begin{center}
+  @{text "x =tag= y \<equiv> tag x = tag y"}
+  \end{center}
+  \end{definition}
+
+  \begin{lemma}\label{finone}
+  @{thm[mode=IfThen] finite_eq_tag_rel}
+  \end{lemma}
+
+  \begin{proof}
+
+  \end{proof}
+
+  \noindent
+  
+
+  \begin{lemma}\label{fintwo} 
+  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, then
+  if @{thm (prem 1) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  and @{thm (prem 2) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  then @{thm (concl) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+  \end{lemma}
+
+  \begin{proof}
+
+  \end{proof}
+
+  \noindent
+  Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+  that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose
+  range is finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+
 
   @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
 
@@ -890,6 +935,7 @@
 *}
 
 
+
 section {* Conclusion and Related Work *}
 
 text {*