regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:54aa3b6dd71c
+:2409827d8eb8
 \begin{quote}
 \it%
 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
 `` & If the reader finds the above treatment in terms of bit lists revoltingly
-concrete, I cannot disagree. A more abstract approach is clearly desirable.''\\
+concrete, I cannot disagree. A more abstract approach is clearly desirable.''\smallskip\\
 `` & All lemmas appear obvious given a picture of the composition of automata\ldots
 Yet their proofs require a painful amount of detail.''
 \end{tabular}
 \end{quote}
 Because of these problems to do with representing automata, there seems
 to be no substantial formalisation of automata theory and regular languages
 carried out in HOL-based theorem provers. Nipkow establishes in
 \cite{Nipkow98} the link between regular expressions and automata in
-the restricted context of lexing. The only larger formalisations of automata theory
+the context of lexing. The only larger formalisations of automata theory
 are carried out in Nuprl \cite{Constable00} and in Coq (for example
 \cite{Filliatre97}).
 In this paper, we will not attempt to formalise automata theory in
 Isabelle/HOL, but take a completely different approach to regular
 (iii) & @{thm seq_Union_left} \\
 \end{tabular}
 \end{proposition}
 \noindent
-In @{text "(ii)"} we use the notation @{term "length s"} for the length of a string.
+In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
-We omit the proofs for these properties, but invite the reader to consult
+string.  This property states that if @{term "[] \<notin> A"} then the lengths of
-our formalisation.\footnote{Available at ???}
+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 ???}
 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}"}.
 @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
 \end{tabular}
 \end{tabular}
 \end{center}
-Given a set of regular expressions @{text rs}, we will make use of the operation of generating
+Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
 a regular expression that matches all languages of @{text rs}. We only need to know the existence
 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
-set @{text rs} with @{const NULL} for the empty set. We can prove that for finite sets @{text rs}
+set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
 \begin{center}
 @{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}
 \end{center}
 \noindent
 holds, whereby @{text "\<calL> ` rs"} stands for the
 image of the set @{text rs} under function @{text "\<calL>"}.
 *}
-section {* Finite Partitions Imply Regularity of a Language *}
+section {* The Myhill-Nerode Theorem, First Part *}
 text {*
 The key definition in the Myhill-Nerode theorem is the
 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
 strings are related, provided there is no distinguishing extension in this
 @{thm[mode=IfThen] Myhill_Nerode1}
 \end{theorem}
 \noindent
 To prove this theorem, we first define the set @{term "finals A"} as those equivalence
-classes that contain strings of @{text A}, namely
+classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
 %
 \begin{equation}
 @{thm finals_def}
 \end{equation}
 \noindent
 In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
 It is straightforward to show that in general @{thm lang_is_union_of_finals} and
 @{thm finals_in_partitions} hold.
 Therefore if we know that there exists a regular expression for every
-equivalence class in @{term "finals A"} (which by assumption must be
+equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
 that matches every string in @{text A}.
 Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
 @{text X}. Note that we do not define an automaton here, we merely relate two sets
 (with respect to 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 equational system that
+Next we build an \emph{initial} equational system that
 contains an equation for each equivalence class. 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
 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
 \end{tabular}
 \end{center}
 \noindent
-where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions
+where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
-@{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. Our internal represeantation for the right-hand
+stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
-sides are sets of terms.
+X\<^isub>i"}.   There can only be
-There can only be finitely many such
+finitely many such terms in a right-hand side since there are only finitely many
-terms since there are only finitely many equivalence classes
+equivalence classes and only finitely many characters.  The term @{text
-and only finitely many characters.
+"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
-The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence
+containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
-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''
+the method by Brzozowski \cite{Brzozowski64}, where he marks the
-states. We are forced to set up the equational system in our way, because
+``terminal'' states. We are forced to set up the equational system in our
-the Myhill-Nerode relation determines the ``direction'' of the transitions.
+way, because the Myhill-Nerode relation determines the ``direction'' of the
-The successor ``state'' of an equivalence class @{text Y} can be reached by adding
+transitions. The successor ``state'' of an equivalence class @{text Y} can
-characters to the end of @{text Y}. This is also the reason why we have to use
+be reached by adding characters to the end of @{text Y}. This is also the
-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>"} %
 @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
 @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
 \end{center}
 \noindent
-we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
 %
 \begin{equation}\label{inv1}
 @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
 \end{equation}
 \end{equation}
 \noindent
 The reason for adding the @{text \<lambda>}-marker to our equational system is
 to obtain this equation: it only holds in this form since none of
-the other terms contain the empty string. Since we use sets for representing
+the other terms contain the empty string.
-the right-hans side we can write \eqref{inv1} and \eqref{inv2} more
-concisely for an equation of the form @{text "X = rhs"} as
+Our represeantation of the equations are pairs,
+where the first component is an equivalence class and the second component
+is a set of terms standing for the right-hand side. Given a set of equivalence
+classes @{text CS}, our initial equational system @{term "Init CS"} is thus
+defined as
+\begin{center}
+\begin{tabular}{rcl}
+@{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+@{text "if"}~@{term "[] \<in> X"}\\
+& & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
+& & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
+@{thm (lhs) Init_def}     & @{text "\<equiv>"} & @{thm (rhs) Init_def}
+\end{tabular}
+\end{center}
+\noindent
+Because we use sets of terms
+for representing the right-hand sides in the equational system we can
+prove \eqref{inv1} and \eqref{inv2} more concisely as
 %
-\begin{equation}\label{inv}
+\begin{lemma}\label{inv}
-\mbox{@{text "X = \<Union> (\<calL> ` rhs)"}}
+If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
-\end{equation}
+\end{lemma}
 \noindent
 Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
-equational system into a \emph{solved form} maintaining the invariant
+initial equational system into one in \emph{solved form} maintaining the invariant
-\eqref{inv}. From the solved form we will be able to read
+in Lemma \ref{inv}. From the solved form we will be able to read
 off the regular expressions.
-In order to transform an equational system into solved form, we have two main
+In order to transform an equational system into solved form, we have two
 operations: one that takes an equation of the form @{text "X = rhs"} and removes
 the recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
 Lemma. The other operation takes an equation @{text "X = rhs"}
 and substitutes @{text X} throughout the rest of the equational system
 adjusting the remaining regular expressions approriately. To define this adjustment
 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 occurence of @{text X}.
-We lift these two operation to work over equational systems @{text ES}: @{const Subst_all}
+With these two operation 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} completely removes such an equaution from @{text ES} by substituting
+@{const Remove} then completely removes such an equation from @{text ES} by substituting
-it to the rest of the equational system, but first removing all recursive occurences
+it to the rest of the equational system, but first eliminating all recursive occurences
 of @{text X} by applying @{const Arden} to @{text "xrhs"}.
 \begin{center}
 \begin{tabular}{rcl}
 @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
 @{thm (lhs) Remove_def}    & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
 \end{tabular}
 \end{center}
+\noindent
+Finially, we can define how an equational system should be solved. For this
+we will iterate the elimination of an equation until only one equation
+will be left in the system. However, we not just want to have any equation
+as being the last one, but the one for which we want to calculate the regular
+expression. Therefore we define the iteration step so that it chooses an
+equation with an equivalence class that is not @{text X}. This allows us to
+control, which equation will be the last. We use again Hilbert's choice operator,
+written @{text SOME}, to chose an equation in a equational system @{text ES}.
+\begin{center}
+\begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+@{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+& & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+& &  \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+\end{tabular}
+\end{center}
+\noindent
+The last definition in our
+\begin{center}
+@{thm Solve_def}
+\end{center}
+\begin{center}
+@{thm while_rule}
+\end{center}
 *}
-section {* Regular Expressions Generate Finitely Many Partitions *}
+section {* Myhill-Nerode, Second Part *}
 text {*
 \begin{theorem}
 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.

changeset 100	2409827d8eb8
parent 98	36f9d19be0e6
child 101	d3fe0597080a