--- a/Paper/Paper.thy	Sat Feb 19 12:01:16 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 17:10:46 2011 +0000
@@ -884,13 +884,14 @@
   directly. The reader is invited to try. 
 
   Our method will rely on some
-  \emph{tagging} functions of strings. Given the inductive hypothesis, it will 
+  \emph{tagging functions} defined over 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).
+  implies that @{term "UNIV // \<approx>(L r)"} must also be finite. 
+  A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+  We also define formally the notion of a \emph{tag-relation} as follows.
 
   \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x}
   and @{text y} are tag-related provided
@@ -899,26 +900,49 @@
   \end{center}
   \end{definition}
 
+  \noindent
+  In order to establis finiteness of a set @{text A} we shall use the following powerful
+  principle from Isabelle/HOL's library.
+  %
+  \begin{equation}\label{finiteimageD}
+  @{thm[mode=IfThen] finite_imageD}
+  \end{equation}
+
+  \noindent
+  It states that if an image of a set under an injective function @{text f} (over this set) 
+  is finite, then @{text A} itself must be finite. We can use it to establish the following 
+  two lemmas.
+
   \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"]}.
+  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where
+  @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+  If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
   \end{lemma}
 
   \begin{proof}
-
+  We prove this lemma again using \eqref{finiteimageD}. For this we set @{text f} to
+  be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that 
+  @{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"},
+  which is finite by assumption. What remains to be shown is that @{text f} is injective
+  on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence 
+  classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+  @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+  @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+  We know there exists a @{text x} with @{term "X = R\<^isub>2 `` {x}"}
+  and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+  and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. From this we can obtain a @{text y}
+  such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. This means @{text x} and @{text y}
+  are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+  they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
   \end{proof}
 
   \noindent