--- 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 "[] \<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 ???}
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 "\<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)"}
@@ -342,7 +343,7 @@
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
@@ -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 // \<approx>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 "\<bigplus>"} to obtain a regular expression
that matches every string in @{text A}.
@@ -412,7 +413,7 @@
@{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).
@@ -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 \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> 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 "\<lambda>(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 \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
+ 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
+ "\<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
- 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 \<calL>} 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 \<calL>} 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 = \<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)"}.
@@ -469,21 +469,42 @@
\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 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 "\<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}
- \mbox{@{text "X = \<Union> (\<calL> ` rhs)"}}
- \end{equation}
+ \begin{lemma}\label{inv}
+ If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` 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 "\<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 {*