diff -r 560712a29a36 -r c4893e84c88e Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Aug 02 15:27:37 2011 +0000
+++ b/Journal/Paper.thy	Wed Aug 03 00:52:41 2011 +0000
@@ -59,8 +59,8 @@
   Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
   
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
-  tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
-  tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
+  tag_Plus ("+tag _ _" [100, 100] 100) and
+  tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
   tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
   tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
   tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
@@ -261,8 +261,8 @@
   problems as with graphs.  Composing, for example, two non-deterministic automata in parallel
   requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} 
   dismisses for this the option of using identities, because it leads according to 
-  him to ``messy proofs''. He
-  opts for a variant of \eqref{disjointunion} using bit lists, but writes 
+  him to ``messy proofs''. Since he does not need to define what a regular
+  language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes 
 
   \begin{quote}
   \it%
@@ -768,8 +768,8 @@
   right-hand side.  Note we used the abbreviation 
   @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}"} 
   to stand for a regular expression that matches with every character. In 
-  our algorithm we are only interested in the existence of such a regular expresion
-  and not specify it any further. 
+  our algorithm we are only interested in the existence of such a regular expression
+  and do not specify it any further. 
 
   It can be easily seen that the @{text "Arden"}-operation mimics Arden's
   Lemma on the level of equations. To ensure the non-emptiness condition of
@@ -1101,7 +1101,7 @@
   \end{proof}
 
   \noindent
-  Much more interesting, however, are the inductive cases. They seem hard to solve 
+  Much more interesting, however, are the inductive cases. They seem hard to be solved 
   directly. The reader is invited to try. 
 
   In order to see how our proof proceeds consider the following suggestive picture 
@@ -1139,16 +1139,16 @@
 
   \noindent
   The relation @{term "\<approx>(lang r)"} partitions the set of all strings into some
-  equivalence classes. To show that there are only finitely many of
-  them, it suffices to show in each induction step the existence of another
-  relation, say @{text R}, for which we can show that there are finitely many
-  equivalence classes and which refines @{term "\<approx>(lang r)"}. A relation @{text
-  "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text
-  "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will rely on some
-  \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 
-  be easy to prove that the \emph{range} of these tagging-functions is finite. 
-  The range of a function @{text f} is defined as 
-  
+  equivalence classes. To show that there are only finitely many of them, it
+  suffices to show in each induction step that another relation, say @{text
+  R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. A
+  relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}
+  provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will
+  rely on some \emph{tagging-functions} defined over strings. Given the
+  inductive hypothesis, it will be easy to prove that the \emph{range} of
+  these tagging-functions is finite. The range of a function @{text f} is
+  defined as
+
   \begin{center}
   @{text "range f \<equiv> f ` UNIV"}
   \end{center}
@@ -1227,42 +1227,27 @@
   Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
   that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
   range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
-  Let us attempt the @{const PLUS}-case first.
-
-  \begin{proof}[@{const "PLUS"}-Case] 
-  We take as tagging-function 
-  %
+  Let us attempt the @{const PLUS}-case first. We take as tagging-function 
+ 
   \begin{center}
   @{thm tag_Plus_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_Plus A B"} is a subset of this product set---so finite. It remains to be shown
-  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
-  showing
-  %
-  \begin{center}
-  @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
-  \end{center}
-  %
-  \noindent
-  which by unfolding the Myhill-Nerode relation is identical to
-  %
-  \begin{equation}\label{pattern}
-  @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
-  \end{equation}
-  %
-  \noindent
-  since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
-  \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse 
-  in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. 
-  The definition of the tagging-function will give us in each case the
-  information to infer that @{text "y @ z \<in> A \<union> B"}.
-  Finally we
-  can discharge this case by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
+  where @{text "A"} and @{text "B"} are some arbitrary languages. The reason for this choice 
+  is that we need to that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. This amounts
+  to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
+  @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. The definition will allow to infer this.
+
+ \begin{proof}[@{const "PLUS"}-Case]
+  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_Plus A B"} is a subset of this product
+  set---so finite. For the refinement proof-obligation, we know that @{term
+  "(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
+  clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"} hold, as we needed to
+  show. Finally we can discharge this case by setting @{text A} to @{term
+  "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
   \end{proof}