--- a/Paper/Paper.thy Wed Feb 16 12:25:53 2011 +0000
+++ b/Paper/Paper.thy Thu Feb 17 11:42:16 2011 +0000
@@ -176,7 +176,7 @@
upon functions in order to represent \emph{finite} automata. The best is
probably to resort to more advanced reasoning frameworks, such as \emph{locales}
or \emph{type classes},
- which are not avaiable in \emph{all} HOL-based theorem provers.
+ which are \emph{not} avaiable in all HOL-based theorem provers.
Because of these problems to do with representing automata, there seems
to be no substantial formalisation of automata theory and regular languages
@@ -198,7 +198,7 @@
\end{definition}
\noindent
- The reason is that regular expressions, unlike graphs, matrices and functons, can
+ The reason is that regular expressions, unlike graphs, matrices and functions, can
be easily defined as inductive datatype. Consequently a corresponding reasoning
infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
of regular expression matching based on derivatives \cite{OwensSlind08} and
@@ -346,10 +346,10 @@
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 a finite set @{text rs}
-
- \begin{center}
- @{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}
- \end{center}
+ %
+ \begin{equation}\label{uplus}
+ \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ \end{equation}
\noindent
holds, whereby @{text "\<calL> ` rs"} stands for the
@@ -423,11 +423,11 @@
which means that if we concatenate the character @{text c} to the end of all
strings in the equivalence class @{text Y}, we obtain a subset of
@{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
+ (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 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).
@@ -446,7 +446,7 @@
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
+ 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
"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
@@ -522,10 +522,10 @@
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
- any recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
+ any recursive occurrences 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
+ adjusting the remaining regular expressions appropriately. To define this adjustment
we define the \emph{append-operation} taking a term and a regular expression as argument
\begin{center}
@@ -537,22 +537,40 @@
We lift this operation to entire right-hand sides of equations, written as
@{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
-
- \begin{center}
- \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ %
+ \begin{equation}\label{arden_def}
+ \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
@{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
& & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
& & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
& & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
- then we calculate the combinded regular expressions for all @{text r} coming
+ 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.
+ 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
+ \emph{ardenable} provided
+
+ \begin{center}
+ @{thm ardenable_def}
+ \end{center}
+
+ \noindent
+ This allows us to prove
+
+ \begin{lemma}\label{ardenable}
+ 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{substituion-operation} takes an equation
of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
@@ -566,17 +584,17 @@
\end{center}
\noindent
- We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate
+ We again delete first all occurrence of @{text "(X, r)"} in @{text rhs}; we then calculate
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}.
+ any occurrence of @{text X}.
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} 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
+ it to the rest of the equational system, but first eliminating all recursive occurrences
of @{text X} by applying @{const Arden} to @{text "xrhs"}.
\begin{center}
@@ -587,7 +605,7 @@
\end{center}
\noindent
- Finially, we can define how an equational system should be solved. For this
+ Finally, we can define how an equational system should be solved. For this
we will need to iterate the process of eliminating equations 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 involving the equivalence class for
@@ -607,10 +625,10 @@
\end{center}
\noindent
- The last definition we need applies @{term Iter} over and over again until a condition
- @{text COND} is \emph{not} satisfied anymore. The condition states that there
- are more than one equation left in the equational system @{text ES}. For this
- we use Isabelle/HOL's @{text while}-operator as follows:
+ The last definition we need applies @{term Iter} over and over until a condition
+ @{text Cond} is \emph{not} satisfied anymore. The condition states that there
+ are more than one equation left in the equational system @{text ES}. To solve
+ an equational system we use Isabelle/HOL's @{text while}-operator as follows:
\begin{center}
@{thm Solve_def}
@@ -626,18 +644,17 @@
the equivalence class @{text X} and the initial equational system
@{term "Init (UNIV // \<approx>A)"} from
\eqref{initcs} using the principle:
-
-
- \begin{center}
- \begin{tabular}{l}
+ %
+ \begin{equation}\label{whileprinciple}
+ \mbox{\begin{tabular}{l}
@{term "invariant (Init (UNIV // \<approx>A))"} \\
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
@{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
\hline
\multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
This principle states that given an invariant (which we will specify below)
@@ -662,7 +679,7 @@
& @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
& @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
& & & @{text "(distinctness)"}\\
- & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\
+ & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
& @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
\end{tabular}
\end{center}
@@ -672,28 +689,20 @@
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. For this we have to make sure that in every @{text rhs},
- terms of the form @{term "Trn Y r"} cannot have a regular expresion that matches the
- empty string. Therefore @{text "rhs_nonempty"} is defined as
-
- \begin{center}
- @{thm rhs_nonempty_def}
- \end{center}
-
- \noindent
+ equation in the system is distinct. Ardenable ensures that we can always
+ apply the 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 @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
- and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}).
+ form @{term "Trn X r"}. That means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
+ and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
- It is straightforward to prove that the inital equational system satisfies the
+ It is straightforward to prove that the initial equational system satisfies the
invariant.
- \begin{lemma}
+ \begin{lemma}\label{invzero}
@{thm[mode=IfThen] Init_ES_satisfies_invariant}
\end{lemma}
@@ -701,26 +710,47 @@
Finiteness is given by the assumption and the way how we set up the
initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
follows from the fact that the equivalence classes are disjoint. The ardenable
- property also follows from the setup of the equational system as does
+ property also follows from the setup of the equational system, as does
validity.\qed
\end{proof}
- \begin{lemma}
+ \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
+ 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
+ keep the equational system finite. These operation also preserve soundness
+ distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+ The property 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}
+ and then @{const Subst_all} removes @{text Y} from the equational system.
+ Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ which matches with our proof-obligation of @{const "Subst_all"}. Since
+ \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption
+ to complete the proof.\qed
\end{proof}
- \begin{lemma}
+ \begin{lemma}\label{itertwo}
@{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
\end{lemma}
\begin{proof}
By assumption we know that @{text "ES"} is finite and has more than one element.
Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
- @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distictness property we can infer
+ @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
removes the equation @{text "Y = yrhs"} from the system, and therefore
the cardinality of @{const Iter} strictly decreases.\qed
@@ -733,7 +763,24 @@
\end{lemma}
\begin{proof}
- ???
+ In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
+ Therefore our invariant is cannot be just @{term "invariant ES"}, but must be
+ @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
+ does not hols. By the stronger invariant we know there exists such a @{text "rhs"}
+ with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
+ of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the equation @{text "X = rhs"},
+ for which the invariant holds. This allows us to conclude that
+ @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold.\qed
\end{proof}
\noindent
@@ -750,7 +797,7 @@
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.~???. Using the validity property for the equation @{text "X = rhs"},
+ 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
removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
@@ -765,7 +812,7 @@
\begin{proof}[of Thm.~\ref{myhillnerodeone}]
By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for
every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
- a subset of @{term "UNIV // \<approx>A"}, we also know that for every equvalence class
+ a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
in @{term "finals A"} there exists a regular language. Moreover by assumption
we know that @{term "finals A"} must be finite, and therefore there must be a finite
set of regular expressions @{text "rs"} such that