diff -r 54aa3b6dd71c -r 2409827d8eb8 Paper/Paper.thy --- a/Paper/Paper.thy Sun Feb 13 10:36:53 2011 +0000 +++ b/Paper/Paper.thy Mon Feb 14 07:42:16 2011 +0000 @@ -154,7 +154,7 @@ \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} @@ -171,7 +171,7 @@ 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}). @@ -239,10 +239,11 @@ \end{proposition} \noindent - In @{text "(ii)"} we use the notation @{term "length s"} for the length of a string. - We omit the proofs for these properties, but invite the reader to consult - our formalisation.\footnote{Available at ???} - + In @{text "(ii)"} we use the notation @{term "length s"} for the length of a + string. This property states that if @{term "[] \ A"} then the lengths of + the strings in @{term "A \ (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 @@ -327,11 +328,11 @@ \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 "\"} to define @{term "\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 "= \ (\ ` rs)"} @@ -342,7 +343,7 @@ image of the set @{text rs} under function @{text "\"}. *} -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 @@ -378,7 +379,7 @@ \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 // \A"} that contain strings of @{text A}, namely % \begin{equation} @{thm finals_def} @@ -389,7 +390,7 @@ 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 "\"} to obtain a regular expression that matches every string in @{text A}. @@ -412,7 +413,7 @@ @{term "X\<^isub>1 \c\ X\<^isub>2"}, @{term "X\<^isub>1 \d\ X\<^isub>3"} with @{text d} being any other character than @{text c}, and @{term "X\<^isub>3 \d\ 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,\,X\<^isub>n"}, there must be one and only one that contains the empty string @{text "[]"} (since equivalence classes are disjoint). @@ -428,22 +429,21 @@ \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 \c\<^isub>i\<^isub>j\ X\<^isub>i"}. Our internal represeantation for the right-hand - sides are sets of terms. - There can only be finitely many such - terms since there are only finitely many equivalence classes - and only finitely many characters. - The term @{text "\(EMPTY)"} in the first equation acts as a marker for the equivalence - class containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the + 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 \c\<^isub>i\<^isub>j\ + X\<^isub>i"}. There can only be + finitely many such terms in a right-hand side since there are only finitely many + equivalence classes and only finitely many characters. The term @{text + "\(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 - characters to the end of @{text Y}. This is also the reason why we have to use - our reverse version of Arden's lemma.} - Overloading the function @{text \} for the two kinds of terms in the + 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 characters to the end of @{text Y}. This is also the + reason why we have to use our reverse version of Arden's lemma.} + Overloading the function @{text \} for the two kinds of terms in the equational system, we have \begin{center} @@ -453,7 +453,7 @@ \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 = \(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \ \ \ \(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}. @@ -469,21 +469,42 @@ \noindent The reason for adding the @{text \}-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 right-hans side we can write \eqref{inv1} and \eqref{inv2} more - concisely for an equation of the form @{text "X = rhs"} as + the other terms contain the empty string. + + 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 "\"} & + @{text "if"}~@{term "[] \ X"}\\ + & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \ CS \ Y \c\ X} \ {Lam EMPTY}"}\\ + & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \ CS \ Y \c\ X}"}\\ + @{thm (lhs) Init_def} & @{text "\"} & @{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} - \mbox{@{text "X = \ (\ ` rhs)"}} - \end{equation} + \begin{lemma}\label{inv} + If @{thm (prem 1) test} then @{text "X = \ \ ` rhs"}. + \end{lemma} \noindent Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the - equational system into a \emph{solved form} maintaining the invariant - \eqref{inv}. From the solved form we will be able to read + initial equational system into one in \emph{solved form} maintaining the invariant + 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"} @@ -535,10 +556,11 @@ 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 - it to the rest of the equational system, but first removing all recursive occurences + @{const Remove} then completely removes such an equation from @{text ES} by substituting + 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} @@ -547,9 +569,42 @@ @{thm (lhs) Remove_def} & @{text "\"} & @{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 "\"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ + & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \ ES \ X \ 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 {*