--- a/Journal/Paper.thy	Wed Aug 03 12:36:23 2011 +0000
+++ b/Journal/Paper.thy	Wed Aug 03 13:56:01 2011 +0000
@@ -1346,15 +1346,15 @@
   we will only go through if we know that  @{term "x \<approx>A y"} holds @{text "(*)"}. Because then 
   we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
   In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition
-  of the string @{text x}. So we have to know that @{text "x\<^isub>p"} is `@{text A}-related' to the
-  corresponding partition @{text "y\<^isub>p"}, repsectively that @{text "x\<^isub>s"} is `@{text B}-related' 
+  of the string @{text x}. So we have to know that both @{text "x\<^isub>p"} and the
+  corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related' 
   to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
-  Taking the two requirements @{text "(*)"} and @{text "(**)"}, we define the
-  tagging-function:
+  Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the
+  tagging-function as:
 
   \begin{center}
   @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
-  @{text ""}
+  @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
   \end{center}
 
   \noindent
@@ -1374,40 +1374,39 @@
   \noindent
   and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown
   above, there are two cases to be considered (see pictures above). First, 
-  there exists a @{text "z\<^isub>p"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}.
+  there exists a @{text "z\<^isub>p"} and @{text "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}.
   By the assumption about @{term "tag_Times A B"} we have
   @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
   relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude in this case
   with @{term "y @ z \<in> A \<cdot> B"}.
 
-  Second there exists a @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{term "x\<^isub>p @ x\<^isub>s = x"},
+  Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with 
   @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
   
   \begin{center}
-  @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) | x\<^isub>p x\<^isub>s. (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
+  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
   \end{center}
   
   \noindent
   and by the assumption about @{term "tag_Times A B"} also 
   
   \begin{center}
-  @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {y\<^isub>p}, \<approx>B `` {y\<^isub>s}) | y\<^isub>p y\<^isub>s. (y\<^isub>p, y\<^isub>s) \<in> Partitions y})"}
+  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^isub>p \<in> A \<and> (y\<^isub>p, y\<^isub>s) \<in> Partitions y}"}
   \end{center}
   
   \noindent
-  That means there must be a @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
-  such that @{text "y\<^isub>p @ y\<^isub>s = y"}. Moreover @{term "\<approx>A ``
-  {x\<^isub>p} = \<approx>A `` {y\<^isub>p}"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
+  This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
+  such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
   {y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the
   facts that @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}, we
-  @{term "y\<^isub>p \<in> A"} and have @{text "y\<^isub>s @ z \<in> B"}, as needed in
+  obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
   this case.  We again can complete the @{const TIMES}-case by setting @{text
   A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
   \end{proof}
 
   \noindent
   The case for @{const Star} is similar to @{const TIMES}, but poses a few
-  extra challenges.  To deal with them we define first the notions of a \emph{string
+  extra challenges.  To deal with them we define first the notion of a \emph{string
   prefix} and a \emph{strict string prefix}:
 
   \begin{center}
@@ -1418,7 +1417,7 @@
   \end{center}
 
   \noindent
-  When we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"}
+  When we analyse the case of @{text "x @ z"} being an element in @{term "A\<star>"}
   and @{text x} is not the empty string, we have the following picture:
 
   \begin{center}
@@ -1443,11 +1442,11 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "x\<^isub>s @ z\<^isub>a \<in> A"}};
+               node[midway, below=0.5em]{@{term "x\<^isub>s @ z\<^isub>a \<in> A"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
@@ -1466,7 +1465,8 @@
   There are potentially many such prefixes, but there can only be finitely many of them (the 
   string @{text x} is finite). Let us therefore choose the longest one and call it 
   @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
-  know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
+  know it is in @{term "A\<star>"} and it is not the empty string. By Lemma~\ref{langprops}@{text "(i)"}, 
+  we can separate
   this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
   and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
   otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a}
@@ -1476,50 +1476,47 @@
   such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
   `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}.
 
-  HERE
-
   In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
   the following tagging-function:
   %
   \begin{center}
-  @{thm tag_Star_def[where ?A="A", THEN meta_eq_app]}\smallskip
+  @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
+  @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>s, x\<^isub>p) \<in> Partitions x}"}
   \end{center}
 
   \begin{proof}[@{const Star}-Case]
   If @{term "finite (UNIV // \<approx>A)"} 
   then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
   @{term "tag_Star A"} is a subset of this set, and therefore finite.
-  Again we have to show injectivity of this tagging-function as  
-  %
-  \begin{center}
-  @{term "\<forall>z. tag_Star A x = tag_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
-  \end{center}  
-  %
-  \noindent
+  Again we have to show under the assumption @{term "x"}~@{term "=(tag_Star A)="}~@{term y}
+  that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}.
+
   We first need to consider the case that @{text x} is the empty string.
   From the assumption we can infer @{text y} is the empty string and
   clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
   string, we can divide the string @{text "x @ z"} as shown in the picture 
-  above. By the tagging-function we have
-  %
+  above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"}, 
+  we have
+
   \begin{center}
-  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
+  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^isub>s) \<in> Partitions x}"}
   \end{center}
-  %
+  
   \noindent
   which by assumption is equal to
-  %
+  
   \begin{center}
-  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
+  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^isup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^isub>s) \<in> Partitions y}"}
   \end{center}
-  %
+  
   \noindent 
-  and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
-  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
-  relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
-  Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
-  @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "lang r"} and
-  complete the proof.
+  and we know there exist partitions @{text "y\<^isub>p"} and @{text
+  "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
+  y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term
+  "y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
+  Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
+  A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. As the last step we have to set
+  @{text "A"} to @{term "lang r"} and complete the proof.
   \end{proof}
 *}