--- a/Paper/Paper.thy	Sat Feb 19 17:10:46 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 19:27:33 2011 +0000
@@ -34,8 +34,14 @@
   Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
   append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
   append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
-  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100)
-  
+  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100)
+
+lemma meta_eq_app:
+  shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+  by auto
+
 (*>*)
 
 
@@ -885,23 +891,24 @@
 
   Our method will rely on some
   \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.
+  be easy to prove that the range of these tagging functions is finite
+  (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
   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. 
   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.
+  We formally define 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
+  \begin{definition}[Tagging-Relation] Given a tag-function @{text tag}, then two strings @{text x}
+  and @{text y} are \emph{tag-related} provided
   \begin{center}
   @{text "x =tag= y \<equiv> tag x = tag y"}
   \end{center}
   \end{definition}
 
   \noindent
-  In order to establis finiteness of a set @{text A} we shall use the following powerful
+  In order to establish finiteness of a set @{text A} we shall use the following powerful
   principle from Isabelle/HOL's library.
   %
   \begin{equation}\label{finiteimageD}
@@ -918,7 +925,14 @@
   \end{lemma}
 
   \begin{proof}
-  
+  We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
+  @{text "range f"} to be subset of @{term "Pow (range tag)"}, which we know must be
+  finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+  and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+  assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
+  From the assumption we can obtain a @{text "x \<in> X"} and @{text "y \<in> Y"} with 
+  @{text "tag x = tag y"}. This in turn means that the equivalence classes @{text X}
+  and @{text Y} must be equal.\qed
   \end{proof}
 
   \begin{lemma}\label{fintwo} 
@@ -946,12 +960,27 @@
   \end{proof}
 
   \noindent
-  Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+  Chaining 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)"}.
+  range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+  Let us attempt the @{const ALT}-case.
+
+  \begin{proof}[@{const "ALT"}-Case] 
+  We take as tagging function 
+
+  \begin{center}
+  @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+  \end{center}
 
+  \noindent
+  where @{text "A"} and @{text "B"} are some arbitrary languages.
+  We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+  then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
+  @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown
+  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}.
 
-  @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
+  \end{proof}
+
 
   @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}