--- a/thys/Paper/Paper.thy Mon May 09 15:01:31 2016 +0100
+++ b/thys/Paper/Paper.thy Wed May 11 12:20:16 2016 +0100
@@ -102,50 +102,6 @@
of the work by Krauss and Nipkow \cite{Krauss2011}. And another one in Coq is given
by Coquand and Siles \cite{Coquand2012}.
-One limitation of Brzozowski's matcher is that it only generates a
-YES/NO answer for whether a string is being matched by a regular
-expression. Sulzmann and Lu \cite{Sulzmann2014} extended this matcher
-to allow generation not just of a YES/NO answer but of an actual
-matching, called a [lexical] {\em value}. They give a simple algorithm
-to calculate a value that appears to be the value associated with
-POSIX matching. The challenge then is to specify that value, in an
-algorithm-independent fashion, and to show that Sulzmann and Lu's
-derivative-based algorithm does indeed calculate a value that is
-correct according to the specification.
-
-The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a
-relation (called an ``order relation'') on the set of values of @{term
-r}, and to show that (once a string to be matched is chosen) there is
-a maximum element and that it is computed by their derivative-based
-algorithm. This proof idea is inspired by work of Frisch and Cardelli
-\cite{Frisch2004} on a GREEDY regular expression matching
-algorithm. However, we were not able to establish transitivity and
-totality for the ``order relation'' by Sulzmann and Lu. In Section
-\ref{argu} we identify some inherent problems with their approach (of
-which some of the proofs are not published in \cite{Sulzmann2014});
-perhaps more importantly, we give a simple inductive (and
-algorithm-independent) definition of what we call being a {\em POSIX
-value} for a regular expression @{term r} and a string @{term s}; we
-show that the algorithm computes such a value and that such a value is
-unique. Proofs are both done by hand and checked in Isabelle/HOL. The
-experience of doing our proofs has been that this mechanical checking
-was absolutely essential: this subject area has hidden snares. This
-was also noted by Kuklewicz \cite{Kuklewicz} who found that nearly all
-POSIX matching implementations are ``buggy'' \cite[Page
-203]{Sulzmann2014}.
-
-%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014}
-%is a relation on the
-%values for the regular expression @{term r}; but it only holds between
-%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
-%the same flattening (underlying string). So a counterexample to totality is
-%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
-%have different flattenings (see Section~\ref{posixsec}). A different
-%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
-%with flattening @{term s} is definable by the same approach, and is indeed
-%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}
-
-
If a regular expression matches a string, then in general there is more than
one way of how the string is matched. There are two commonly used
disambiguation strategies to generate a unique answer: one is called GREEDY
@@ -170,26 +126,76 @@
expressions:
\begin{itemize}
-\item[$\bullet$] \underline{The Longest Match Rule (or ``maximal munch rule''):}\smallskip
-
+\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):
The longest initial substring matched by any regular expression is taken as
next token.\smallskip
-\item[$\bullet$] \underline{Priority Rule:}\smallskip
-
+\item[$\bullet$] \emph{Priority Rule:}
For a particular longest initial substring, the first regular expression
that can match determines the token.
\end{itemize}
-
-\noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords such as
-@{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"} recognising
-identifiers (say, a single character followed by characters or numbers).
-Then we can form the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use
-POSIX matching to tokenise strings, say @{text "iffoo"} and @{text "if"}.
-For @{text "iffoo"} we obtain by the longest match rule a single identifier
-token, not a keyword followed by an identifier. For @{text "if"} we obtain by
-the priority rule a keyword token, not an identifier token---even if @{text
-"r\<^bsub>id\<^esub>"} matches also.\bigskip
+
+\noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords
+such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}
+recognising identifiers (say, a single character followed by
+characters or numbers). Then we can form the regular expression
+@{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX matching to tokenise strings,
+say @{text "iffoo"} and @{text "if"}. For @{text "iffoo"} we obtain
+by the Longest Match Rule a single identifier token, not a keyword
+followed by an identifier. For @{text "if"} we obtain by the Priority
+Rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}
+matches also.
+
+One limitation of Brzozowski's matcher is that it only generates a
+YES/NO answer for whether a string is being matched by a regular
+expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher
+to allow generation not just of a YES/NO answer but of an actual
+matching, called a [lexical] {\em value}. They give a simple algorithm
+to calculate a value that appears to be the value associated with
+POSIX matching. The challenge then is to specify that value, in an
+algorithm-independent fashion, and to show that Sulzmann and Lu's
+derivative-based algorithm does indeed calculate a value that is
+correct according to the specification.
+
+The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a
+relation (called an ``order relation'') on the set of values of @{term
+r}, and to show that (once a string to be matched is chosen) there is
+a maximum element and that it is computed by their derivative-based
+algorithm. This proof idea is inspired by work of Frisch and Cardelli
+\cite{Frisch2004} on a GREEDY regular expression matching
+algorithm. However, we were not able to establish transitivity and
+totality for the ``order relation'' by Sulzmann and Lu. In Section
+\ref{argu} we identify some inherent problems with their approach (of
+which some of the proofs are not published in \cite{Sulzmann2014});
+perhaps more importantly, we give a simple inductive (and
+algorithm-independent) definition of what we call being a {\em POSIX
+value} for a regular expression @{term r} and a string @{term s}; we
+show that the algorithm computes such a value and that such a value is
+unique. Our proofs are both done by hand and checked in Isabelle/HOL. The
+experience of doing our proofs has been that this mechanical checking
+was absolutely essential: this subject area has hidden snares. This
+was also noted by Kuklewicz \cite{Kuklewicz} who found that nearly all
+POSIX matching implementations are ``buggy'' \cite[Page
+203]{Sulzmann2014} and by Grathwohl et al \cite[Page 36]{CrashCourse2014}
+who wrote:
+
+\begin{quote}
+\it{}``The POSIX strategy is more complicated than the greedy because of
+the dependence on information about the length of matched strings in the
+various subexpressions.''
+\end{quote}
+
+%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014}
+%is a relation on the
+%values for the regular expression @{term r}; but it only holds between
+%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
+%the same flattening (underlying string). So a counterexample to totality is
+%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
+%have different flattenings (see Section~\ref{posixsec}). A different
+%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
+%with flattening @{term s} is definable by the same approach, and is indeed
+%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}
+
\noindent {\bf Contributions:} We have implemented in Isabelle/HOL the
derivative-based regular expression matching algorithm of
@@ -239,10 +245,13 @@
recursive function @{term L} with the clauses:
\begin{center}
- \begin{tabular}{l@ {\hspace{5mm}}rcl}
+ \begin{tabular}{l@ {\hspace{3mm}}rcl}
(1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
(2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
(3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
+ \end{tabular}
+ \hspace{14mm}
+ \begin{tabular}{l@ {\hspace{3mm}}rcl}
(4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
(5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
(6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
@@ -355,11 +364,11 @@
text {*
- The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to introduce values for encoding
- \emph{how} a regular expression matches a string and then define a
- function on values that mirrors (but inverts) the construction of the
- derivative on regular expressions. \emph{Values} are defined as the
- inductive datatype
+ The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to define
+ values for encoding \emph{how} a regular expression matches a string
+ and then define a function on values that mirrors (but inverts) the
+ construction of the derivative on regular expressions. \emph{Values}
+ are defined as the inductive datatype
\begin{center}
@{text "v :="}
@@ -379,11 +388,13 @@
@{term "flat DUMMY"} and defined as:
\begin{center}
- \begin{tabular}{lcl}
+ \begin{tabular}[t]{lcl}
@{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\
@{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\
@{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\
- @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\
+ @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}
+ \end{tabular}\hspace{14mm}
+ \begin{tabular}[t]{lcl}
@{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
@{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\
@{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\
@@ -395,11 +406,12 @@
\begin{center}
\begin{tabular}{c}
+ \\[-8mm]
@{thm[mode=Axiom] Prf.intros(4)} \qquad
- @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\smallskip\\
+ @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[3mm]
@{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad
- @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\smallskip\\
- @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\smallskip\\
+ @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[3mm]
+ @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[3mm]
@{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad
@{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
\end{tabular}