
diff -r 3ab755a96cef -r 08afbed1c8c7 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 18:58:34 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 21 02:33:05 2011 +0000
@@ -186,7 +186,7 @@
   upon functions in order to represent \emph{finite} automata. The best is
   probably to resort to more advanced reasoning frameworks, such as \emph{locales}
   or \emph{type classes},
-  which are \emph{not} avaiable in all HOL-based theorem provers.
+  which are \emph{not} available in all HOL-based theorem provers.
 
   Because of these problems to do with representing automata, there seems
   to be no substantial formalisation of automata theory and regular languages 
@@ -309,12 +309,12 @@
   all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
   of @{text "\<star>"}.
   For the inclusion in the other direction we assume a string @{text s}
-  with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden}
+  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
   we know by Prop.~\ref{langprops}@{text "(ii)"} that 
   @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
   From @{text "(*)"} it follows then that
-  @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
+  @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
   this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
   \end{proof}
@@ -591,7 +591,7 @@
   \end{lemma}
   
   \noindent
-  The \emph{substituion-operation} takes an equation
+  The \emph{substitution-operation} takes an equation
   of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 
   \begin{center}
@@ -604,13 +604,13 @@
   \end{center}
 
   \noindent
-  We again delete first all occurrence of @{text "(X, r)"} in @{text rhs}; we then calculate
+  We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
   the regular expression corresponding to the deleted terms; finally we append this
   regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
   the substitution operation we will arrange it so that @{text "xrhs"} does not contain
   any occurrence of @{text X}.
 
-  With these two operation in place, we can define the operation that removes one equation
+  With these two operations in place, we can define the operation that removes one equation
   from an equational systems @{text ES}. The operation @{const Subst_all}
   substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; 
   @{const Remove} then completely removes such an equation from @{text ES} by substituting 
@@ -783,7 +783,7 @@
   \end{proof}
 
   \noindent
-  This brings us to our property we want establish for @{text Solve}.
+  This brings us to our property we want to establish for @{text Solve}.
 
 
   \begin{lemma}
@@ -823,7 +823,7 @@
   \end{lemma}
 
   \begin{proof}
-  By the preceeding Lemma, we know that there exists a @{text "rhs"} such
+  By the preceding Lemma, we know that there exists a @{text "rhs"} such
   that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
   and that the invariant holds for this equation. That means we 
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
@@ -1154,7 +1154,7 @@
   Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
   By the assumption about @{term "tag_str_SEQ 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' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude aslo in this case
+  relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
   with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
   by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
   \end{proof}
@@ -1241,7 +1241,7 @@
   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
-  string, we can devide the string @{text "x @ z"} as shown in the picture 
+  string, we can divide the string @{text "x @ z"} as shown in the picture 
   above. By the tagging function we have
   %
   \begin{center}
@@ -1274,7 +1274,7 @@
   exists a regular expression that matches all of its strings. Regular
   expressions can conveniently be defined as a datatype in a HOL-based theorem
   prover. For us it was therefore interesting to find out how far we can push
-  this point of view. We have establised both directions of the Myhill-Nerode
+  this point of view. We have established both directions of the Myhill-Nerode
   theorem.
   %
   \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
@@ -1323,7 +1323,7 @@
   concise proof pearl, this should be seen in the context of the work done by
   Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
   in Nuprl using automata. They write that their four-member team needed
-  something on the magnitute of 18 months for their formalisation. The
+  something on the magnitude of 18 months for their formalisation. The
   estimate for our formalisation is that we needed approximately 3 months and
   this included the time to find our proof arguments. Unlike Constable et al,
   who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
@@ -1336,7 +1336,7 @@
 
 
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
-  algebraic mehod} used to convert a finite automaton to a regular
+  algebraic method} used to convert a finite automaton to a regular
   expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
   classes as the states of the minimal automaton for the regular language.
   However there are some subtle differences. Since we identify equivalence




