regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:73127f5db18f
+:bea94f1e6771
 text {*
 \noindent
 Regular languages are an important and well-understood subject in Computer
 Science, with many beautiful theorems and many useful algorithms. There is a
 wide range of textbooks on this subject, many of which are aimed at students
-and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97,
+and contain very detailed `pencil-and-paper' proofs
-HopcroftUllman69}). It seems natural to exercise theorem provers by
+(e.g.~\cite{HopcroftUllman69,Kozen97}). It seems natural to exercise theorem provers by
 formalising the theorems and by verifying formally the algorithms.
 A popular choice for a theorem prover would be one based on Higher-Order
 Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
 presented in this paper we will use the Isabelle/HOL. HOL is a predicate calculus
 \noindent
 This approach has many benefits. Among them is the fact that it is easy to
 convince oneself that regular languages are closed under complementation:
 one just has to exchange the accepting and non-accepting states in the
 corresponding automaton to obtain an automaton for the complement language.
-The problem, however, lies with formalising such reasoning in a HOL-based
+The problem, however, lies with formalising such reasoning in a
-theorem prover. Automata are built up from states and transitions that need
+theorem prover. Automata are built up from states and transitions that are
-to be represented as graphs, matrices or functions, none of which can be
+usually represented as graphs, matrices or functions, none of which can be
 defined as an inductive datatype.
 In case of graphs and matrices, this means we have to build our own
 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
 HOLlight support them with libraries. Even worse, reasoning about graphs and
-matrices can be a real hassle in HOL-based theorem provers, because
+matrices can be a real hassle in theorem provers, because
 we have to be able to combine automata.  Consider for
 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
 connecting the accepting states of $A_1$ to the initial state of $A_2$:
 \begin{center}
 carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
 the link between regular expressions and automata in the context of
 lexing. Berghofer and Reiter \cite{BerghoferReiter09} formalise automata
 working over bit strings in the context of Presburger arithmetic.  The only
 larger formalisations of automata theory are carried out in Nuprl
-\cite{Constable00} and in Coq, e.g.~\cite{Filliatre97,Almeidaetal10}.
+\cite{Constable00} and in Coq, e.g.~\cite{Almeidaetal10,Filliatre97}.
 Also, one might consider automata as just convenient `vehicles' for
 establishing properties about regular languages.  However, paper proofs
 about automata often involve subtle side-conditions which are easily
 overlooked, but which make formal reasoning rather painful. For example
 involving equivalence classes of languages. For this we will use Arden's Lemma
 (see for example \cite[Page 100]{Sakarovitch09}),
 which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
 @{term "[] \<notin> A"}. However we will need the following `reversed'
 version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to
-\mbox{@{term "X \<cdot> A"}}).
+\mbox{@{term "X \<cdot> A"}}).\footnote{The details of its proof are given in the Appendix.}
-\begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
+\begin{lmm}[(Reversed Arden's Lemma)]\label{arden}\mbox{}\\
 If @{thm (prem 1) reversed_Arden} then
 @{thm (lhs) reversed_Arden} if and only if
 @{thm (rhs) reversed_Arden}.
 \end{lmm}
-\begin{proof}
-For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
-that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"}
-we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
-which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
-sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
-is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation
-completes this direction.
-For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
-on @{text n}, we can establish the property
-\begin{center}
-@{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
-\end{center}
-\noindent
-Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
-all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
-of @{text "\<star>"}.
-For the inclusion in the other direction we assume a string @{text s}
-with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
-we know by Property~\ref{langprops}@{text "(ii)"} that
-@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
-(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
-From @{text "(*)"} it follows then that
-@{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
-implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"}
-this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
-\end{proof}
 \noindent
 Regular expressions are defined as the inductive datatype
 \begin{center}
 @{thm (rhs) lang.simps(6)[where r="r"]}\\
 \end{tabular}
 \end{center}
 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
-a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+a regular expression that matches the union of all languages of @{text rs}.
+This definion is not trivial in a theorem prover, but since
+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
+of such a regular expression, we can use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const PLUS} over the
 set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
 %
 \begin{equation}\label{uplus}
 \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
 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
 language. This can be defined as a ternary relation.
-\begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel}
+\begin{dfntn}[(Myhill-Nerode Relation)]\label{myhillneroderel}
 Given a language @{text A}, two strings @{text x} and
 @{text y} are Myhill-Nerode related provided
 \begin{center}
 @{thm str_eq_def'}
 \end{center}
 \end{proof}
 \noindent
 We also need the fact that @{text Iter} decreases the termination measure.
-\begin{lmm}\label{itertwo}
+\begin{lmm}\label{itertwo}\mbox{}\\
 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
 \end{lmm}
 \begin{proof}
 By assumption we know that @{text "ES"} is finite and has more than one element.
 \noindent
 Lemma~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
 of the Myhill-Nerode Theorem.
-\begin{proof}[Proof of Theorem~\ref{myhillnerodeone}]
+\begin{proof}[of Theorem~\ref{myhillnerodeone}]
 By Lemma~\ref{every_eqcl_has_reg} we know that there exists a regular expression 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 equivalence class
 in @{term "finals A"} there exists a regular expression. Moreover by assumption
 we know that @{term "finals A"} must be finite, and therefore there must be a finite
 \noindent
 The proof will be by induction on the structure of @{text r}. It turns out
 the base cases are straightforward.
-\begin{proof}[Base Cases]
+\begin{proof}[(Base Cases)]
 The cases for @{const ZERO}, @{const ONE} and @{const ATOM} are routine, because
 we can easily establish that
 \begin{center}
 \begin{tabular}{l}
 @{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
 also be finite.  We formally define the notion of a \emph{tagging-relation}
 as follows.
-\begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+\begin{dfntn}[(Tagging-Relation)] Given a tagging-function @{text tag}, then two strings @{text x}
 and @{text y} are \emph{tag-related} provided
 \begin{center}
 @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
 \end{center}
 \end{dfntn}
 is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}.
 This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
 @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will
 provide us with just the right assumptions in order to get the proof through.
-\begin{proof}[@{const "PLUS"}-Case]
+\begin{proof}[(@{const "PLUS"}-Case)]
 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
 (UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"}
 holds. The range of @{term "tag_Plus A B"} is a subset of this product
 set---so finite. For the refinement proof-obligation, we know that @{term
 "(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
 this string to be in @{term "A \<cdot> B"}:
 %
 \begin{center}
 \begin{tabular}{c}
 \scalebox{1}{
-\begin{tikzpicture}[fill=gray!20]
+\begin{tikzpicture}[scale=0.8,fill=gray!20]
 \node[draw,minimum height=3.8ex, fill] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$  };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
 node[midway, below=0.5em]{@{text "z\<^isub>s \<in> B"}};
 \end{tikzpicture}}
 \\[2mm]
 \scalebox{1}{
-\begin{tikzpicture}[fill=gray!20]
+\begin{tikzpicture}[scale=0.8,fill=gray!20]
 \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 Note that we have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do
 not know anything about how the string @{term x} is partitioned.
 With this definition in place, let us prove the @{const "Times"}-case.
-\begin{proof}[@{const TIMES}-Case]
+\begin{proof}[(@{const TIMES}-Case)]
 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
 @{term "tag_Times A B"} is a subset of this product set, and therefore finite.
 For the refinement of @{term "\<approx>(A \<cdot> B)"} and @{text "\<^raw:$\threesim$>\<^bsub>\<times>tag A B\<^esub>"},
 we have by Lemma \ref{refinement}
 When analysing the case of @{text "x @ z"} being an element in @{term "A\<star>"}
 and @{text x} is not the empty string, we have the following picture:
 \begin{center}
 \scalebox{1}{
-\begin{tikzpicture}[fill=gray!20]
+\begin{tikzpicture}[scale=0.8,fill=gray!20]
 \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
 \begin{center}
 @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
 @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
 \end{center}
-\begin{proof}[@{const Star}-Case]
+\begin{proof}[(@{const Star}-Case)]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
 @{term "tag_Star A"} is a subset of this set, and therefore finite.
 Again we have to show under the assumption @{term "x"}~@{term "=(tag_Star A)="}~@{term y}
 that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}.
 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
 @{text "A"} to @{term "lang r"} and thus complete the proof.
 \end{proof}
 *}
-section {* Second Part proved using Partial Derivatives\label{derivatives} *}
+section {* Second Part proved using Partial Derivatives *}
 text {*
+\label{derivatives}
 \noindent
 As we have seen in the previous section, in order to establish
 the second direction of the Myhill-Nerode Theorem, it is sufficient to find
 a more refined relation than @{term "\<approx>(lang r)"} for which we can
 show that there are only finitely many equivalence classes. So far we
 regular expressions can be calculated directly using the notion of
 \emph{derivatives of a regular expression} \cite{Brzozowski64}. We define
 this notion in Isabelle/HOL as follows:
 \begin{center}
-\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+\begin{longtable}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{thm (lhs) deriv.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
 @{thm (lhs) deriv.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
 @{thm (lhs) deriv.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
 @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
 & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
 &             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
 @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\
 @{thm (lhs) deriv.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
 @{thm (lhs) derivs.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
-@{thm (lhs) derivs.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}\\
+@{thm (lhs) derivs.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}
-\end{tabular}
+\end{longtable}
 \end{center}
 \noindent
 The last two clauses extend derivatives from characters to strings. The
 boolean function @{term "nullable r"} needed in the @{const Times}-case tests
 \begin{equation}\label{Pdersdef}
 @{thm pderivs_lang_def}
 \end{equation}
-\begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
+\begin{thrm}[(Antimirov \cite{Antimirov95})]\label{antimirov}
 For every language @{text A} and every regular expression @{text r},
 \mbox{@{thm finite_pderivs_lang}}.
 \end{thrm}
 \noindent
 Let us now return to our proof for the second direction in the Myhill-Nerode
 Theorem. The point of the above calculations is to use
 @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} as tagging-relation.
-\begin{proof}[Proof of Theorem~\ref{myhillnerodetwo} (second version)]
+\begin{proof}[of Theorem~\ref{myhillnerodetwo} (second version)]
 Using \eqref{mhders}
 and \eqref{Derspders} we can easily infer that
 \begin{center}
 @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pderivs x r = pderivs y r"}
 This relation refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the
 second part of the Myhill-Nerode Theorem.
 \end{proof}
 *}
-section {* Closure Properties of Regular Languages\label{closure} *}
+section {* Closure Properties of Regular Languages *}
 text {*
+\label{closure}
 \noindent
 The beauty of regular languages is that they are closed under many set
 operations. Closure under union, concatenation and Kleene-star are trivial
 to establish given our definition of regularity (recall Definition~\ref{regular}).
 More interesting in our setting is the closure under complement, because it seems difficult
 Calculating such a regular expression via
 automata using the standard method would be quite involved. It includes the
 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
 regular expression. Clearly not something you want to formalise in a theorem
-prover in which it is cumbersome to reason about automata.
+prover if it is cumbersome to reason about automata.
 Once closure under complement is established, closure under intersection
 and set difference is also easy, because
 \begin{center}
 r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
 @{term "Deriv_lang B A"} is regular.
 Even more surprising is the fact that for \emph{every} language @{text A}, the language
 consisting of all (scattered) substrings of @{text A} is regular \cite{Haines69} (see also
-\cite{Shallit08, Gasarch09}).
+\cite{Shallit08,Gasarch09}).
 A \emph{(scattered) substring} can be obtained
 by striking out zero or more characters from a string. This can be defined
 inductively in Isabelle/HOL by the following three rules:
 \begin{center}
 \end{center}
 \noindent
 We like to establish
-\begin{thrm}[Haines \cite{Haines69}]\label{subseqreg}
+\begin{thrm}[(Haines \cite{Haines69})]\label{subseqreg}
 For every language @{text A}, the languages @{text "(i)"} @{term "SUBSEQ A"} and
 @{text "(ii)"} @{term "SUPSEQ A"}
 are regular.
 \end{thrm}
 \end{proof}
 \noindent
 This lemma allows us to establish the second part of Theorem~\ref{subseqreg}.
-\begin{proof}[Proof of the Second Part of Theorem~\ref{subseqreg}]
+\begin{proof}[of the Second Part of Theorem~\ref{subseqreg}]
 Given any language @{text A}, by Lemma~\ref{mset} we know there exists
 a finite, and thus regular, language @{text M}. We further have @{term "SUPSEQ M = SUPSEQ A"},
 which establishes the second part.
 \end{proof}
 \end{equation}
 \noindent
 holds. Now the first part of Theorem~\ref{subseqreg} is a simple consequence of the second part.
-\begin{proof}[Proof of the First Part of Theorem~\ref{subseqreg}]
+\begin{proof}[of the First Part of Theorem~\ref{subseqreg}]
 By the second part, we know the right-hand side of \eqref{compl}
 is regular, which means @{term "- SUBSEQ A"} is regular. But since
 we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
 must be regular.
 \end{proof}
 Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing
 the non-regularity of languages. For this we use the following version of the Continuation
 Lemma (see for example~\cite{Rosenberg06}).
-\begin{lmm}[Continuation Lemma]
+\begin{lmm}[(Continuation Lemma)]
 If a language @{text A} is regular and a set of strings @{text B} is infinite,
 then there exist two distinct strings @{text x} and @{text y} in @{text B}
 such that @{term "x \<approx>A y"}.
 \end{lmm}
 text {*
 \noindent
 In this paper we took the view that a regular language is one where there
 exists a regular expression that matches all of its strings. Regular
-expressions can conveniently be defined as a datatype in HOL-based theorem
+expressions can conveniently be defined as a datatype in theorem
 provers. For us it was therefore interesting to find out how far we can push
 this point of view. We have established in Isabelle/HOL both directions
 of the Myhill-Nerode Theorem.
 %
-\begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
+\begin{thrm}[(The Myhill-Nerode Theorem)]\mbox{}\\
 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
 \end{thrm}
 \noindent
 Having formalised this theorem means we pushed our point of view quite
 construct a regular expression for the complement language by direct
 means. However the existence of such a regular expression can be easily
 proved using the Myhill-Nerode Theorem.
 Our insistence on regular expressions for proving the Myhill-Nerode Theorem
-arose from the limitations of HOL, which is the logic underlying the popular theorem provers HOL4,
+arose from the problem of defining formally the regularity of a language.
-HOLlight and Isabelle/HOL. In order to guarantee consistency,
+In order to guarantee consistency,
 formalisations in HOL can only extend the logic with definitions that introduce a new concept in
 terms of already existing notions. A convenient definition for automata
 (based on graphs) uses a polymorphic type for the state nodes. This allows
 us to use the standard operation for disjoint union whenever we need to compose two
 automata. Unfortunately, we cannot use such a polymorphic definition
 @{text "M"} (indicated by dependency on the type-variable @{text "\<alpha>"}), but the definiendum
 @{text "is_regular"} is not. Such definitions are excluded from HOL, because
 they can lead easily to inconsistencies (see \cite{PittsHOL4} for a simple
 example). Also HOL does not contain type-quantifiers which would allow us to
 get rid of the polymorphism by quantifying over the type-variable @{text
-"\<alpha>"}. Therefore when defining regularity in terms of automata, the only
+"\<alpha>"}. Therefore when defining regularity in terms of automata, the
 natural way out in HOL is to resort to state nodes with an identity, for
 example a natural number. Unfortunatly, the consequence is that we have to
 be careful when combining two automata so that there is no clash between two
 such states. This makes formalisations quite fiddly and rather
 unpleasant. Regular expressions proved much more convenient for reasoning in
 \cite{Filliatre97}. More recently, Almeida et al reported about another
 formalisation of regular languages in Coq \cite{Almeidaetal10}. Their
 main result is the
 correctness of Mirkin's construction of an automaton from a regular
 expression using partial derivatives. This took approximately 10600 lines
-of code.  In terms of time, the estimate for our formalisation is that we
+of code.  Also Braibant formalised a large part of regular language
+theory and Kleene algebras in Coq \cite{Braibant12}. While he is mainly interested
+in implementing decision procedures for Kleene algebras, his library
+includes a proof of the Myhill-Nerode theorem. He reckons that our
+``development is more concise'' than his one based on matrices \cite[Page 67]{Braibant12}.
+In terms of time, the estimate for our formalisation is that we
 needed approximately 3 months and this included the time to find our proof
 arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode
 proof from \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the
 formalisation was not the bottleneck.  The code of
 our formalisation can be found in the Archive of Formal Proofs at
 \noindent
 {\bf Acknowledgements:}
 We are grateful for the comments we received from Larry Paulson.  Tobias
 Nipkow made us aware of the properties in Theorem~\ref{subseqreg} and Tjark
 Weber helped us with proving them.
+\bibliographystyle{plain}
+\bibliography{root}
+\newpage
+\begin{appendix}
+\section{Appendix$^\star$}
+\renewcommand{\thefootnote}{\mbox{$\star$}}
+\footnotetext{If the reviewers deem more suitable, the authors are
+prepared to drop material or move it to an electronic appendix.}
+\begin{proof}[of Lemma~\ref{arden}]
+For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"}
+we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
+which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
+sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
+is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation
+completes this direction.
+For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
+on @{text n}, we can establish the property
+\begin{center}
+@{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
+\end{center}
+\noindent
+Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
+all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
+of @{text "\<star>"}.
+For the inclusion in the other direction we assume a string @{text s}
+with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
+we know by Property~\ref{langprops}@{text "(ii)"} that
+@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
+(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
+From @{text "(*)"} it follows then that
+@{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
+implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"}
+this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
+\end{proof}
+\end{appendix}
 *}
 (*<*)
 end

changeset 348	bea94f1e6771
parent 338	e7504bfdbd50
child 350	8ce9a432680b