diff -r d74bfa11802c -r 4c85af262ee7 thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Mon Mar 07 03:23:28 2016 +0000 +++ b/thys/Paper/Paper.thy Mon Mar 07 18:56:41 2016 +0000 @@ -83,7 +83,7 @@ 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}, +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 @@ -152,7 +152,7 @@ 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 -rule priority a keyword token, not an identifier token---even if @{text +the priority rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"} matches also.\bigskip \noindent {\bf Contributions:} (NOT DONE YET) We have implemented in @@ -213,17 +213,17 @@ recursive function @{term L} with the clauses: \begin{center} - \begin{tabular}{rcl} - @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\ - @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\ - @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\ - @{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"]}\\ - @{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"]}\\ - @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\ + \begin{tabular}{l@ {\hspace{5mm}}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)}\\ + (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)}\\ \end{tabular} \end{center} - \noindent In the fourth clause we use the operation @{term "DUMMY ;; + \noindent In clause (4) we use the operation @{term "DUMMY ;; DUMMY"} for the concatenation of two languages (it is also list-append for strings). We use the star-notation for regular expressions and for languages (in the last clause above). The star for languages is defined @@ -310,11 +310,11 @@ \noindent gives a positive answer if and only if @{term "s \ L r"}. Consequently, this regular expression matching algorithm satisfies the - usual specification. While the matcher above calculates a provably correct - YES/NO answer for whether a regular expression matches a string, the novel - idea of Sulzmann and Lu \cite{Sulzmann2014} is to append another phase to - this algorithm in order to calculate a [lexical] value. We will explain - the details next. + usual specification for regular expression matching. While the matcher + above calculates a provably correct YES/NO answer for whether a regular + expression matches a string or not, the novel idea of Sulzmann and Lu + \cite{Sulzmann2014} is to append another phase to this algorithm in order + to calculate a [lexical] value. We will explain the details next. *} @@ -338,11 +338,11 @@ @{term "Stars vs"} \end{center} - \noindent where we use @{term vs} standing for a list of values. (This is + \noindent where we use @{term vs} to stand for a list of values. (This is similar to the approach taken by Frisch and Cardelli for GREEDY matching - \cite{Frisch2004}, and Sulzmann and Lu \cite{Sulzmann2014} for POSIX matching). - The string underlying a value can be calculated by the @{const flat} - function, written @{term "flat DUMMY"} and defined as: + \cite{Frisch2004}, and Sulzmann and Lu \cite{Sulzmann2014} for POSIX + matching). The string underlying a value can be calculated by the @{const + flat} function, written @{term "flat DUMMY"} and defined as: \begin{center} \begin{tabular}{lcl} @@ -422,14 +422,15 @@ \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}}; \end{tikzpicture} \end{center} -\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014} +\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014}, matching the string @{term "[a,b,c]"}. The first phase (the arrows from -left to right) is \Brz's matcher building succesive derivatives. If at the -last regular expression is @{term nullable}, then functions of the -second phase are called: first @{term mkeps} calculates a value witnessing +left to right) is \Brz's matcher building succesive derivatives. If the +last regular expression is @{term nullable}, then the functions of the +second phase are called (the top-down and right-to-left arrows): first +@{term mkeps} calculates a value witnessing how the empty string has been recognised by @{term "r\<^sub>4"}. After that the function @{term inj} `injects back' the characters of the string into -the values (the arrows from right to left). +the values. \label{Sulz}} \end{figure} @@ -450,9 +451,10 @@ alternative regular expression, say @{term "ALT r\<^sub>1 r\<^sub>2"}, can match the empty string and furthermore @{term "r\<^sub>1"} can match the empty string, then we return a @{text Left}-value. The @{text - Right}-value will only be returned if @{term "r\<^sub>1"} is not nullable. + Right}-value will only be returned if @{term "r\<^sub>1"} cannot match the empty + string. - The most interesting novelty from Sulzmann and Lu \cite{Sulzmann2014} is + The most interesting idea from Sulzmann and Lu \cite{Sulzmann2014} is the construction of a value for how @{term "r\<^sub>1"} can match the string @{term "[a,b,c]"} from the value how the last derivative, @{term "r\<^sub>4"} in Fig~\ref{Sulz}, can match the empty string. Sulzmann and @@ -510,9 +512,9 @@ we match in the clause (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while in (6) it is just @{term "Right v\<^sub>2"}. One more interesting point is in the right-hand side of clause (6): since in this case the - regular expression @{text "r\<^sub>1"} does not ``contribute'' for - matching the string, that is only matches the empty string, we need to - call @{const mkeps} in order to construct a value how @{term "r\<^sub>1"} + regular expression @{text "r\<^sub>1"} does not ``contribute'' to + matching the string, that means it only matches the empty string, we need to + call @{const mkeps} in order to construct a value for how @{term "r\<^sub>1"} can match this empty string. A similar argument applies for why we can expect in the left-hand side of clause (7) that the value is of the form @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ r @@ -524,6 +526,18 @@ injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]}, but our deviation is harmless.} + The idea of @{term inj} to ``inject back'' a character into a value can + be made precise by the first part of the following lemma; the second + part shows that the underlying string of an @{const mkeps}-value is + the empty string. + + \begin{lemma}\mbox{}\\\label{Prf_injval_flat} + \begin{tabular}{ll} + (1) & @{thm[mode=IfThen] Prf_injval_flat}\\ + (2) & @{thm[mode=IfThen] mkeps_flat} + \end{tabular} + \end{lemma} + Having defined the @{const mkeps} and @{text inj} function we can extend \Brz's matcher so that a [lexical] value is constructed (assuming the regular expression matches the string). The clauses of the lexer are @@ -599,9 +613,7 @@ @{thm[mode=IfThen] PMatch_mkeps} \end{lemma} - \begin{lemma} - @{thm[mode=IfThen] Prf_injval_flat} - \end{lemma} + \begin{lemma} @{thm[mode=IfThen] PMatch2_roy_version}