
diff -r b300f2c5d51d -r 11c3c302fa2e Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Aug 16 10:21:14 2011 +0000
+++ b/Journal/Paper.thy	Wed Aug 17 07:43:09 2011 +0000
@@ -1562,7 +1562,7 @@
 text {*
   \noindent
   As we have seen in the previous section, in order to establish
-  the second direction of the Myhill-Nerode theorem, we need to find 
+  the second direction of the Myhill-Nerode theorem, it is sufficient to find 
   a more refined relation than @{term "\<approx>(lang r)"} for which we can
   show that there are only finitely many equivalence classes. So far we 
   showed this directly by induction on @{text "r"} using tagging-functions. 
@@ -1617,8 +1617,8 @@
   \noindent
   where @{text "\<Delta>"} in the fifth line is a function that tests whether the
   empty string is in the language and returns @{term "{[]}"} or @{term "{}"},
-  accordingly.  In the last equation we use the list-cons operator written
-  \mbox{@{text "_ :: _"}}.  The only interesting case is the @{text "A\<star>"}-case
+  accordingly.  Note also that in the last equation we use the list-cons operator written
+  \mbox{@{text "_ :: _"}}.  The only interesting case is the case of @{term "A\<star>"}
   where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
   @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by
   using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der
@@ -1694,7 +1694,7 @@
 
 
   \noindent
-  which means the right-hand side (seen as relation) refines the Myhill-Nerode
+  which means the right-hand side (seen as a relation) refines the Myhill-Nerode
   relation.  Consequently, we can use @{text
   "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a
   tagging-relation. However, in order to be useful for the second part of the
@@ -1708,7 +1708,7 @@
 
 
   What Brzozowski \cite{Brzozowski64} established is that for every language there
-  \emph{are} only finitely `dissimilar' derivatives of a regular
+  \emph{are} only finitely `dissimilar' derivatives for a regular
   expression. Two regular expressions are said to be \emph{similar} provided
   they can be identified using the using the @{text "ACI"}-identities:
 
@@ -1723,7 +1723,7 @@
 
   \noindent
   Carrying this idea through, we must not consider the set of all derivatives,
-  but the ones modulo @{text "ACI"}.  In principle, this can be done formally, 
+  but the one modulo @{text "ACI"}.  In principle, this can be done formally, 
   but it is very painful in a theorem prover (since there is no
   direct characterisation of the set of dissimilar derivatives).
 
@@ -1853,7 +1853,7 @@
   \end{thrm}
 
   \noindent
-  Antimirov's argument first shows this theorem for the language @{term UNIV1}, 
+  Antimirov's proof first shows this theorem for the language @{term UNIV1}, 
   which is the set of all non-empty strings. For this he proves:
 
   \begin{equation}\label{pdersunivone}
@@ -1882,11 +1882,11 @@
   \end{center}
 
   \noindent
-  and for all languages @{text "A"}, @{thm pders_lang_subset[where B="UNIV",
-  simplified]} holds.  Since we follow Antimirov's proof quite closely in our
-  formalisation (only the last two cases of \eqref{pdersunivone} involve some
-  non-routine induction argument), we omit the details.
-
+  and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of
+  @{term "pders_lang UNIV r"}.  Since we follow Antimirov's proof quite
+  closely in our formalisation (only the last two cases of
+  \eqref{pdersunivone} involve some non-routine induction argument), we omit
+  the details.
 
   Let us now return to our proof about the second direction in the Myhill-Nerode
   theorem. The point of the above calculations is to use 
@@ -2053,33 +2053,34 @@
   Our insistence on regular expressions for proving the Myhill-Nerode theorem
   arose from the limitations of HOL, on which the popular theorem provers HOL4,
   HOLlight and Isabelle/HOL are based. In order to guarantee consistency,
-  formalisations can only extend HOL by definitions that introduce a new concept in
-  terms of already existing notions. A convenient definition for automata
+  formalisations can extend HOL with definitions that introduce a new concept in
+  only terms of already existing notions. A convenient definition for automata
   (based on graphs) uses a polymorphic type for the state nodes. This allows
-  us to use the standard operation of disjoint union in order to compose two
+  us to use the standard operation for disjoint union whenever we need to compose two
   automata. Unfortunately, we cannot use such a polymorphic definition
-  in HOL as part of the definition for regularity of a language (a
-  set of strings).  Consider the following attempt
+  in HOL as part of the definition for regularity of a language (a predicate
+  over set of strings).  Consider the following attempt:
 
   \begin{center}
   @{text "is_regular A \<equiv> \<exists>M(\<alpha>). is_finite_automata (M) \<and> \<calL>(M) = A"}
   \end{center}
 
   \noindent
-  which means the definiens is polymorphic in the type of the automata @{text
-  "M"}, but the definiendum @{text "is_regular"} is not. Such definitions are
-  excluded in HOL, because they can lead easily to inconsistencies (see
-  \cite{PittsHOL4} for a simple example). Also HOL does not contain
-  type-quantifiers which would allow us to get rid of the polymorphism by
-  quantifying over the type-variable @{text "\<alpha>"}. Therefore when defining
-  regularity in terms of automata, the only natural way out in HOL is to use
-  state nodes with an identity, for example a natural number. Unfortunatly,
-  the consequence is that we have to be careful when combining two automata so
-  that there is no clash between two such states. This makes formalisations
-  quite fiddly and rather unpleasant. Regular expressions proved much more
-  convenient for reasoning in HOL and we showed they can be used for
-  establishing the central result in regular language theory: the Myhill-Nerode 
-  theorem.
+  In this definifion, the definiens is polymorphic in the type of the automata
+  @{text "M"} (indicated by the @{text "\<alpha>"}), but the definiendum @{text
+  "is_regular"} is not. Such definitions are excluded in HOL, because they can
+  lead easily to inconsistencies (see \cite{PittsHOL4} for a simple
+  example). Also HOL does not contain type-quantifiers which would allow us to
+  get rid of the polymorphism by quantifying over the type-variable @{text
+  "\<alpha>"}. Therefore when defining regularity in terms of automata, the only
+  natural way out in HOL is to resort to state nodes with an identity, for
+  example a natural number. Unfortunatly, the consequence is that we have to
+  be careful when combining two automata so that there is no clash between two
+  such states. This makes formalisations quite fiddly and rather
+  unpleasant. Regular expressions proved much more convenient for reasoning in
+  HOL since they can be defined as inductive datatype and a reasoning
+  infrastructure comes for free. We showed they can be used for establishing
+  the central result in regular language theory---the Myhill-Nerode theorem.
 
   While regular expressions are convenient, they have some limitations. One is
   that there seems to be no method of calculating a minimal regular expression
@@ -2124,24 +2125,27 @@
   in \cite{Harper99} and \cite{Yi06}. While Brzozowski's derivatives lead to a
   simple regular expression matcher and he established that there are only
   finitely many dissimilar derivatives for every regular expression, this
-  result is not as straightforward to formalise in a theorem prover. The
-  reason is that the set of dissimilar derivatives is not defined inductively,
-  but in terms of an ACI-equivalence relation. This difficulty prevented for
-  example Krauss and Nipkow to prove termination of their equivalence checker
-  for regular expressions \cite{KraussNipkow11}. Their checker is based on
-  derivatives and for their argument the lack of a formal proof of termination
-  is not crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}).
-  We expect that their development simplifies by using partial derivatives,
+  result is not as straightforward to formalise in a theorem prover as one
+  might wish. The reason is that the set of dissimilar derivatives is not
+  defined inductively, but in terms of an ACI-equivalence relation. This
+  difficulty prevented for example Krauss and Nipkow to prove termination of
+  their equivalence checker for regular expressions
+  \cite{KraussNipkow11}. Their checker is based on Brzozowski's derivatives
+  and for their argument the lack of a formal proof of termination is not
+  crucial (it merely lets them ``sleep better'' \cite{KraussNipkow11}).  We
+  expect that their development simplifies by using partial derivatives,
   instead of derivatives, and that termination of the algorithm can be
-  formally established. However, since partial derivatives use sets of regular
-  expressions, one needs to carefully analyse whether the resulting algorithm
-  is still executable. Given the existing infrastructure for executable sets
-  in Isabelle/HOL, it should.
+  formally established (the main incredience is
+  Theorem~\ref{antimirov}). However, since partial derivatives use sets of
+  regular expressions, one needs to carefully analyse whether the resulting
+  algorithm is still executable. Given the existing infrastructure for
+  executable sets in Isabelle/HOL, it should.
+
 
   Our formalisation of the Myhill-Nerode theorem consists of 780 lines of
   Isabelle/Isar code for the first direction and 460 for the second (the one
   based on tagging functions), plus around 300 lines of standard material
-  about regular languages. The formalisation about derivatives and partial
+  about regular languages. The formalisation of derivatives and partial
   derivatives shown in Section~\ref{derivatives} consists of 390 lines of
   code.  The algorithm for solving equational systems, which we used in the
   first direction, is conceptually relatively simple. Still the use of sets
@@ -2149,10 +2153,10 @@
   one might hope. However, it seems sets cannot be avoided since the `input'
   of the algorithm consists of equivalence classes and we cannot see how to
   reformulate the theory so that we can use lists. Lists would be much easier
-  to reason about, since we can define function over them by recursion. For
-  sets we have to use set-comprehensions.
+  to reason about, since we can define functions over them by recursion. For
+  sets we have to use set-comprehensions, which is slightly unwieldy.
 
-  While our formalisation might be seen large, it should be seen
+  While our formalisation might appear large, it 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 magnitude of 18 months




