--- 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