regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:d8d1e1f53d6e
+:fd39492b187c
 \end{tabular}
 \end{proposition}
 \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}}
 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{}\\
 If @{thm (prem 1) arden} then
 @{thm (lhs) arden} if and only if
 @{text X}. Note that we do not define an automaton here, we merely relate two sets
 (with the help of a character). In our concrete example we have
 @{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
+Next we construct an \emph{initial equational system} that
-contains an equation for each equivalence class. Suppose we have
+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
 \begin{center}
 \end{center}
 \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
+X\<^isub>i"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
-finitely many such terms in a right-hand side since by assumption there are only finitely many
+corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states
-equivalence classes and only finitely many characters.  The term @{text
+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
 the method by Brzozowski \cite{Brzozowski64}, where he marks the
 `terminal' states. We are forced to set up the equational system in our
 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
 \begin{center}
 @{text "\<calL>(Y, r) \<equiv>"} %
 \noindent
 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
 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
+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
+the non-emptiness condition of Arden's Lemma we say that a right-hand side is
 @{text ardenable} provided
 \begin{center}
 @{thm ardenable_def}
 \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"}.
 If @{text "X = \<Union>\<calL> ` rhs"},
 @{thm (prem 2) Arden_keeps_eq}, and
 @{thm (prem 3) Arden_keeps_eq}, then
 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
 \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}
 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
 The first two ensure that the equational system is always finite (number of equations
 and number of terms in each equation); the second makes sure the `meaning' of the
 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,
 while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
 form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
 \begin{lemma}\label{iterone}
 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
 \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:
 \begin{center}
 @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
 @{thm (concl) Subst_all_satisfies_invariant}
 \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
 cannot make a regular expression to match the empty string. Validity is
 given because @{const Arden} removes an equivalence class from @{text yrhs}
 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
 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)"}.
 With this we can conclude the proof.\qed
 \end{proof}
 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
 \end{tikzpicture}}
 \end{center}
 %
 \noindent
-Either there is a prefix of @{text x} in @{text A} and the rest is 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}.
+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
 %
 \begin{center}
 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
 state leading up to that state. Usually, however, the states are characterised as the
 strings starting from that state leading to the terminal states.  The first
 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
+expressions and shows that there can be only finitely many of them with
-modulo ACI). We could
+respect to a language (if regarded equal modulo ACI). We could
-have used as the tag of a string @{text s} the derivative of a regular expression
+have used as the tag of a string @{text s} the set of derivatives of a regular expression
-generated with respect to @{text s}.  Using the fact that two strings are
+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
+the fact that there are only finitely such derivatives
-expression would give us a similar argument as ours. However it seems not so easy to
+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
+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
 as stated in the Introduction is not so convenient to formalise in a
 HOL-based theorem prover. However, it is also the direction where we had to

changeset 156	fd39492b187c
parent 154	7c68b9ad4486
child 157	10d2d0cbe381