
diff -r d8d1e1f53d6e -r fd39492b187c Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Apr 19 02:25:21 2011 +0000
+++ b/Paper/Paper.thy	Thu Apr 21 12:07:11 2011 +0000
@@ -265,7 +265,7 @@
 
   \noindent
   In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
-  string; this property states that if @{term "[] \<notin> A"} then the lengths of
+  string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
   the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
   the proofs for these properties, but invite the reader to consult our
   formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
@@ -273,14 +273,14 @@
   The notation in Isabelle/HOL for the quotient of a language @{text A} according to an 
   equivalence relation @{term REL} is @{term "A // REL"}. We will write 
   @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined 
-  as @{text "{y | y \<approx> x}"}.
+  as \mbox{@{text "{y | y \<approx> x}"}}.
 
 
   Central to our proof will be the solution of equational systems
-  involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64},
+  involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
   which solves equations of the form @{term "X = A ;; X \<union> B"} provided
   @{term "[] \<notin> A"}. However we will need the following `reverse' 
-  version of Arden's lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
+  version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
   \mbox{@{term "X ;; A"}}).
 
   \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
@@ -446,8 +446,9 @@
   @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any 
   other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
   
-  Next we build an \emph{initial equational system} that
-  contains an equation for each equivalence class. Suppose we have 
+  Next we construct an \emph{initial equational system} that
+  contains an equation for each equivalence class. We first give
+  an informal description of this construction. Suppose we have 
   the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
   contains the empty string @{text "[]"} (since equivalence classes are disjoint).
   Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
@@ -464,9 +465,13 @@
   \noindent
   where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
   stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
-  X\<^isub>i"}.   There can only be
-  finitely many such terms in a right-hand side since by assumption there are only finitely many
-  equivalence classes and only finitely many characters.  The term @{text
+  X\<^isub>i"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+  corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states 
+  are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these 
+  predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be
+  finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
+  since by assumption there are only finitely many
+  equivalence classes and only finitely many characters. The term @{text
   "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
   containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
   single `initial' state in the equational system, which is different from
@@ -475,7 +480,7 @@
   way, because the Myhill-Nerode relation determines the `direction' of the
   transitions---the successor `state' of an equivalence class @{text Y} can
   be reached by adding a character to the end of @{text Y}. This is also the
-  reason why we have to use our reverse version of Arden's lemma.}
+  reason why we have to use our reverse version of Arden's Lemma.}
   Overloading the function @{text \<calL>} for the two kinds of terms in the
   equational system, we have
   
@@ -571,8 +576,8 @@
   then we calculate the combined regular expressions for all @{text r} coming 
   from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
   finally we append this regular expression to @{text rhs'}. It can be easily seen 
-  that this operation mimics Arden's lemma on the level of equations. To ensure
-  the non-emptiness condition of Arden's lemma we say that a right-hand side is
+  that this operation mimics Arden's Lemma on the level of equations. To ensure
+  the non-emptiness condition of Arden's Lemma we say that a right-hand side is
   @{text ardenable} provided
 
   \begin{center}
@@ -580,7 +585,7 @@
   \end{center}
 
   \noindent
-  This allows us to prove a version of Arden's lemma on the level of equations.
+  This allows us to prove a version of Arden's Lemma on the level of equations.
 
   \begin{lemma}\label{ardenable}
   Given an equation @{text "X = rhs"}.
@@ -591,7 +596,9 @@
   \end{lemma}
   
   \noindent
-  The \emph{substitution-operation} takes an equation
+  Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
+  but we can still ensure that it holds troughout our algorithm of transforming equations
+  into solved form. 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}
@@ -710,7 +717,7 @@
   equations is preserved under our transformations. The other properties are a bit more
   technical, but are needed to get our proof through. Distinctness states that every
   equation in the system is distinct. @{text Ardenable} ensures that we can always
-  apply the arden operation. 
+  apply the @{text Arden} operation. 
   The last property states that every @{text rhs} can only contain equivalence classes
   for which there is an equation. Therefore @{text lhss} is just the set containing 
   the first components of an equational system,
@@ -742,7 +749,7 @@
   \end{lemma}
 
   \begin{proof} 
-  This boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+  The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
   and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"} 
   preserves the invariant.
   We prove this as follows:
@@ -753,7 +760,7 @@
   \end{center}
 
   \noindent
-  Finiteness is straightforward, as @{const Subst} and @{const Arden} operations 
+  Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations 
   keep the equational system finite. These operations also preserve soundness 
   and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
   The property @{text ardenable} is clearly preserved because the append-operation
@@ -829,7 +836,7 @@
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
   this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the 
   invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
-  we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
+  we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
   removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
   This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
   So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
@@ -1104,8 +1111,8 @@
   \end{center}
   %
   \noindent
-  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B},
-  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
+  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
+  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
   In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
   following tagging-function
   %
@@ -1347,19 +1354,19 @@
   choice has consequences about how the initial equational system is set up. We have
   the $\lambda$-term on our `initial state', while Brzozowski has it on the
   terminal states. This means we also need to reverse the direction of Arden's
-  lemma.
+  Lemma.
 
   We briefly considered using the method Brzozowski presented in the Appendix
   of~\cite{Brzozowski64} in order to prove the second direction of the
   Myhill-Nerode theorem. There he calculates the derivatives for regular
-  expressions and shows that there can be only finitely many of them (if regarded equal 
-  modulo ACI). We could
-  have used as the tag of a string @{text s} the derivative of a regular expression
-  generated with respect to @{text s}.  Using the fact that two strings are
+  expressions and shows that there can be only finitely many of them with 
+  respect to a language (if regarded equal modulo ACI). We could
+  have used as the tag of a string @{text s} the set of derivatives of a regular expression
+  generated by a language.  Using the fact that two strings are
   Myhill-Nerode related whenever their derivative is the same, together with
-  the fact that there are only finitely many derivatives for a regular
-  expression would give us a similar argument as ours. However it seems not so easy to
-  calculate the derivatives and then to count them. Therefore we preferred our
+  the fact that there are only finitely such derivatives
+  would give us a similar argument as ours. However it seems not so easy to
+  calculate the set of derivatives modulo ACI and then to count them. Therefore we preferred our
   direct method of using tagging-functions. This
   is also where our method shines, because we can completely side-step the
   standard argument \cite{Kozen97} where automata need to be composed, which




