# HG changeset patch # User urbanc # Date 1315232132 0 # Node ID 13de6a49294ef57448966bd73b629ae07beabbdf # Parent a6513d0b16fccd73eed9d017240031ef94f33f97 polished SUBSEQ diff -r a6513d0b16fc -r 13de6a49294e Journal/Paper.thy --- a/Journal/Paper.thy Mon Sep 05 13:44:01 2011 +0000 +++ b/Journal/Paper.thy Mon Sep 05 14:15:32 2011 +0000 @@ -36,7 +36,7 @@ abbreviation "TIMES \ Times" abbreviation "TIMESS \ Timess" abbreviation "STAR \ Star" -abbreviation "ALLREG \ Allreg" +abbreviation "ALLS \ Star Allreg" definition Delta :: "'a lang \ 'a lang" @@ -91,7 +91,8 @@ pderivs_set ("pderss") and SUBSEQ ("Subseq") and SUPSEQ ("Supseq") and - UP ("'(_')\") + UP ("'(_')\") and + ALLS ("ALL") lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union @@ -494,7 +495,7 @@ rest being in @{term "A\"}. 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} @@ -2143,8 +2144,8 @@ \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 - lemma allows us to infer that every set @{text A} of antichains, namely + 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 \begin{equation}\label{higman} @{text "\x, y \ A."}~@{term "x \ y \ \(x \ y) \ \(y \ x)"} @@ -2175,16 +2176,15 @@ \end{lmm} \begin{proof} - Since our alphabet is finite, we can find a regular expression, written @{const Allreg}, that - matches every single-character string. With this regular expression we can inductively define - the operation @{text "r\"} over regular expressions + Since our alphabet is finite, we have a regular expression, written @{text ALL}, that + matches every string. With this regular expression we can inductively define + the operation @{text "r\"} \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @{thm (lhs) UP.simps(1)} & @{text "\"} & @{thm (rhs) UP.simps(1)}\\ @{thm (lhs) UP.simps(2)} & @{text "\"} & @{thm (rhs) UP.simps(2)}\\ - @{thm (lhs) UP.simps(3)} & @{text "\"} &\\ - \multicolumn{3}{r}{@{thm (rhs) UP.simps(3)}}\\ + @{thm (lhs) UP.simps(3)} & @{text "\"} & @{thm (rhs) UP.simps(3)}\\ @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\"} & @{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"]} & @@ -2194,12 +2194,12 @@ \end{center} \noindent - and use \eqref{supseqprops} establish that @{thm lang_UP} holds. This shows - that @{term "SUBSEQ A"} is regular provided @{text A} is. + and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows + 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 @@ -2217,7 +2217,7 @@ \end{center} \noindent - By Higman's lemma \eqref{higman} we know + By Higman's Lemma \eqref{higman} we know that @{term "M \ {x \ 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 \ SUPSEQ A"}. For @@ -2236,7 +2236,7 @@ \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. @@ -2251,9 +2251,9 @@ \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"} @@ -2419,12 +2419,13 @@ 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. *} diff -r a6513d0b16fc -r 13de6a49294e Journal/document/root.bib --- a/Journal/document/root.bib Mon Sep 05 13:44:01 2011 +0000 +++ b/Journal/document/root.bib Mon Sep 05 14:15:32 2011 +0000 @@ -27,7 +27,7 @@ title = {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, booktitle = {The Archive of Formal Proofs}, editor = {G.~Klein and T.~Nipkow and L.~Paulson}, - publisher = {\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}}, + publisher = {\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}}, month = Aug, year = 2011, note = {Formal proof development},