diff -r 08afbed1c8c7 -r 604518f0127f Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Feb 21 02:33:05 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 21 03:30:38 2011 +0000
@@ -143,7 +143,7 @@
 
   \noindent
   changes the type---the disjoint union is not a set, but a set of pairs. 
-  Using this definition for disjoint unions means we do not have a single type for automata
+  Using this definition for disjoint union means we do not have a single type for automata
   and hence will not be able to state certain properties about \emph{all}
   automata, since there is no type quantification available in HOL. An
   alternative, which provides us with a single type for automata, is to give every 
@@ -228,7 +228,7 @@
   To our knowledge, our proof of the Myhill-Nerode theorem is the
   first that is based on regular expressions, only. We prove the part of this theorem 
   stating that a regular expression has only finitely many partitions using certain 
-  tagging-functions. Again to our best knowledge, these tagging functions have
+  tagging-functions. Again to our best knowledge, these tagging-functions have
   not been used before to establish the Myhill-Nerode theorem.
 *}
 
@@ -587,7 +587,7 @@
   If @{text "X = \<Union>\<calL> ` rhs"},
   @{thm (prem 2) Arden_keeps_eq}, and
   @{thm (prem 3) Arden_keeps_eq}, then
-  @{text "X = \<Union>\<calL> ` (Arden X rhs)"}
+  @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
   \end{lemma}
   
   \noindent
@@ -868,7 +868,7 @@
   theorem. It can be formulated in our setting as follows.
 
   \begin{theorem}
-  Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}.
+  Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
   \end{theorem}  
 
   \noindent
@@ -896,13 +896,13 @@
   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} defined over strings. Given the inductive hypothesis, it will 
-  be easy to prove that the range of these tagging functions is finite
+  Our proof will rely on some
+  \emph{taggingfunctions} 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 @{text "range f \<equiv> f ` UNIV"}).
-  With this we will be able to infer that the tagging functions, seen as relations,
+  With this we will be able to infer that the tagging-functions, seen as relations,
   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
+  will show that the tagging-relations are 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 formally define the notion of a \emph{tagging-relation} as follows.
@@ -953,14 +953,14 @@
   \begin{proof}
   We prove this lemma again using \eqref{finiteimageD}. This time 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)"},
+  @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "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"}
+  We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {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"}. This means we can obtain a @{text y}
   such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
   are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
@@ -969,12 +969,12 @@
 
   \noindent
   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
+  that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose
   range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
   Let us attempt the @{const ALT}-case first.
 
   \begin{proof}[@{const "ALT"}-Case] 
-  We take as tagging function 
+  We take as tagging-function 
   %
   \begin{center}
   @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
@@ -1016,13 +1016,13 @@
   to be able to infer that 
   %
   \begin{center}
-  @{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  @{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
   \end{center}
   %
   \noindent
-  using the information given by the appropriate tagging function. The complication 
+  using the information given by the appropriate tagging-function. The complication 
   is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
-  (this was easy in case of @{term "A \<union> B"}). For this we define the
+  (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
   notions of \emph{string prefixes} 
   %
   \begin{center}
@@ -1160,7 +1160,7 @@
   \end{proof}
   
   \noindent
-  The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When
+  The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
   we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the 
   empty string, we 
   have the following picture:
@@ -1204,23 +1204,23 @@
   \end{center}
   %
   \noindent
-  We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
-  @{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string 
+  We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
+  @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string 
   @{text "[]"} would do.
-  There are many such prefixes, but there can only be finitely many of them (the 
+  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'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
-  know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate
-  this string into two parts, say @{text "a"} and @{text "b"}, such @{text "a \<in> A"}
-  and @{text "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
+  know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, 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 - x'\<^isub>m\<^isub>a\<^isub>x"},
   otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
   `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
    @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
-  @{text "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{text "x @ z \<in> A\<star>"}
+  @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
   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 - x') @ z\<^isub>a"}.
 
-  In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use
+  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}
@@ -1240,9 +1240,9 @@
   \noindent
   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 @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+  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 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>})"}
@@ -1256,11 +1256,11 @@
   \end{center}
   %
   \noindent 
-  and we know that we have a @{text "y' \<in> A\<star>"} and @{text "y' < y"}
+  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 @{text "z\<^isub>b \<in> A\<star>"}.
-  Therefore, finally, @{text "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 @{text "L r"} and
+  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 "L r"} and
   complete the proof.\qed
   \end{proof}
 *}