regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:a6513d0b16fc
+:13de6a49294e
 abbreviation "ATOM \<equiv> Atom"
 abbreviation "PLUS \<equiv> Plus"
 abbreviation "TIMES \<equiv> Times"
 abbreviation "TIMESS \<equiv> Timess"
 abbreviation "STAR \<equiv> Star"
-abbreviation "ALLREG \<equiv> Allreg"
+abbreviation "ALLS \<equiv> Star Allreg"
 definition
 Delta :: "'a lang \<Rightarrow> 'a lang"
 where
 "Delta A = (if [] \<in> A then {[]} else {})"
 pderiv ("pder") and
 pderivs ("pders") and
 pderivs_set ("pderss") and
 SUBSEQ ("Subseq") and
 SUPSEQ ("Supseq") and
-UP ("'(_')\<up>")
+UP ("'(_')\<up>") and
+ALLS ("ALL")
 lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
 definition
 Property @{text "(iv)"} states that a non-empty string in @{term "A\<star>"} can
 always be split up into a non-empty prefix belonging to @{text "A"} and the
 rest being in @{term "A\<star>"}. We omit
 the proofs for these properties, but invite the reader to consult our
 formalisation.\footnote{Available in the Archive of Formal Proofs at
-\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}
+\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}
 \cite{myhillnerodeafp11}.}
 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
 are regular.
 \end{lmm}
 \noindent
 Our proof follows the one given in \cite[92--95]{Shallit08}, except that we use
-Higman's lemma, which is already proved in the Isabelle/HOL library. Higman's
+Higman's Lemma, which is already proved in the Isabelle/HOL library. Higman's
-lemma allows us to infer that every set @{text A} of antichains, namely
+Lemma allows us to infer that every set @{text A} of antichains, namely
 \begin{equation}\label{higman}
 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"}
 \end{equation}
 \begin{lmm}
 If @{text A} is regular, then also @{term "SUPSEQ A"}.
 \end{lmm}
 \begin{proof}
-Since our alphabet is finite, we can find a regular expression, written @{const Allreg}, that
+Since our alphabet is finite, we have a regular expression, written @{text ALL}, that
-matches every single-character string. With this regular expression we can inductively define
+matches every string. With this regular expression we can inductively define
-the operation @{text "r\<up>"} over regular expressions
+the operation @{text "r\<up>"}
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\
 @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\
-@{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} &\\
+@{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\
-\multicolumn{3}{r}{@{thm (rhs) UP.simps(3)}}\\
 @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
 @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
 @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{thm (lhs) UP.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(6)}
 \end{tabular}
 \end{center}
 \noindent
-and use \eqref{supseqprops} establish that @{thm lang_UP} holds. This shows
+and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows
-that @{term "SUBSEQ A"} is regular provided @{text A} is.
+that @{term "SUBSEQ A"} is regular, provided @{text A} is.
 \end{proof}
 \noindent
-Now we can prove our main lemma, namely
+Now we can prove our main lemma w.r.t.~@{const "SUPSEQ"}, namely
 \begin{lmm}\label{mset}
 For every language @{text A}, there exists a finite language @{text M} such that
 \begin{center}
 \mbox{@{term "SUPSEQ M = SUPSEQ A"}}\;.
 \begin{center}
 @{thm minimal_def}
 \end{center}
 \noindent
-By Higman's lemma \eqref{higman} we know
+By Higman's Lemma \eqref{higman} we know
 that @{term "M \<equiv> {x \<in> A. minimal x A}"} is finite, since every minimal element is incomparable,
 except with itself.
 It is also straightforward to show that @{term "SUPSEQ M \<subseteq> SUPSEQ A"}. For
 the other direction we have  @{term "x \<in> SUPSEQ A"}. From this we can obtain
 a @{text y} such that @{term "y \<in> A"} and @{term "y \<preceq> x"}. Since we know that
 \end{proof}
 \noindent
 This lemma allows us to establish the second part of Lemma~\ref{subseqreg}.
-\begin{proof}[The Second Part of Lemma~\ref{subseqreg}]
+\begin{proof}[Proof of the Second Part of Lemma~\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}
 \begin{equation}\label{compl}
 @{thm SUBSEQ_complement}
 \end{equation}
 \noindent
-holds. Now the first part is a simple consequence of the second part.
+holds. Now the first part of~\ref{subseqreg} is a simple consequence of the second part.
-\begin{proof}[The First Part of Lemma~\ref{subseqreg}]
+\begin{proof}[Proof of the First Part of Lemma~\ref{subseqreg}]
 By the second part of Lemma~\ref{subseqreg}, 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}
 formalisation in Nurpl, but from what is shown in the Nuprl Math Library
 about their development it seems substantially larger than ours. We attribute
 this to our use of regular expressions, which meant we did not need to `fight'
 the theorem prover. The code of
 our formalisation can be found in the Archive of Formal Proofs at
-\mbox{\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip
+\mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip
 \noindent
 {\bf Acknowledgements:}
 We are grateful for the comments we received from Larry
-Paulson.
+Paulson, Tobias Nipkow made us aware of the properties in Lemma~\ref{subseqreg}
+and Tjark Weber helped us with their proofs.
 *}
 (*<*)

changeset 239	13de6a49294e
parent 238	a6513d0b16fc
child 240	17aa8c8fbe7d