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\ \ X"} using the definition of @{text "\"}. 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 \ X ;; (A \ Suc k)"} since its length is only @{text k} (the strings in @{term "X ;; (A \ Suc k)"} are all longer). From @{text "(*)"} it follows then that - @{term s} must be element in @{term "(\m\{0..k}. B ;; (A \ m))"}. This in turn + @{term s} must be an element in @{term "(\m\{0..k}. B ;; (A \ m))"}. This in turn implies that @{term s} is in @{term "(\n. B ;; (A \ n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} this is equal to @{term "B ;; A\"}, 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 // \A))"} returns the equation @{text "X = rhs"}, and that the invariant holds for this equation. That means we know @{text "X = \\ ` rhs"}. We further know that @@ -1154,7 +1154,7 @@ Second, there exists a @{text "z'"} such that @{term "x @ z' \ A"} and @{text "z - z' \ B"}. By the assumption about @{term "tag_str_SEQ A B"} we have @{term "\A `` {x} = \A `` {y}"} and thus @{term "x \A y"}. Which means by the Myhill-Nerode - relation that @{term "y @ z' \ A"} holds. Using @{text "z - z' \ B"}, we can conclude aslo in this case + relation that @{term "y @ z' \ A"} holds. Using @{text "z - z' \ B"}, we can conclude also in this case with @{term "y @ z \ 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 \ A\"}. 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