--- a/thys/Paper/Paper.thy Sat Mar 05 04:01:10 2016 +0000
+++ b/thys/Paper/Paper.thy Sat Mar 05 05:41:51 2016 +0000
@@ -8,6 +8,9 @@
abbreviation
"der_syn r c \<equiv> der c r"
+abbreviation
+ "ders_syn r s \<equiv> ders s r"
+
notation (latex output)
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [78,77] 73) and
@@ -25,7 +28,8 @@
val.Right ("Right _" [1000] 78) and
L ("L'(_')" [10] 78) and
- der_syn ("_\\_" [79, 1000] 76) and
+ der_syn ("_\\_" [79, 1000] 76) and
+ ders_syn ("_\\_" [79, 1000] 76) and
flat ("|_|" [75] 73) and
Sequ ("_ @ _" [78,77] 63) and
injval ("inj _ _ _" [78,77,78] 77) and
@@ -35,6 +39,10 @@
Prf ("\<triangleright> _ : _" [75,75] 75) and
PMatch ("_ : _ \<rightarrow> _" [75,75,75] 75)
(* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)
+
+definition
+ "match r s \<equiv> nullable (ders s r)"
+
(*>*)
section {* Introduction *}
@@ -217,9 +225,14 @@
For semantic derivatives we have the following equations (for example
\cite{Krauss2011}):
- \begin{equation}
+ \begin{equation}\label{SemDer}
\begin{array}{lcl}
@{thm (lhs) Der_null} & \dn & @{thm (rhs) Der_null}\\
+ @{thm (lhs) Der_empty} & \dn & @{thm (rhs) Der_empty}\\
+ @{thm (lhs) Der_char} & \dn & @{thm (rhs) Der_char}\\
+ @{thm (lhs) Der_union} & \dn & @{thm (rhs) Der_union}\\
+ @{thm (lhs) Der_Sequ} & \dn & @{thm (rhs) Der_Sequ}\\
+ @{thm (lhs) Der_star} & \dn & @{thm (rhs) Der_star}
\end{array}
\end{equation}
@@ -247,12 +260,21 @@
@{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}
\end{tabular}
\end{center}
-
+
\noindent
- Given the equations in ???,
- it is a relatively easy exercise in mechanical reasoning to establish that
+ We may extend this definition to give derivatives w.r.t.~strings:
- \begin{proposition}
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
+ @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent Given the equations in \eqref{SemDer}, it is a relatively easy
+ exercise in mechanical reasoning to establish that
+
+ \begin{proposition}\mbox{}\\
\begin{tabular}{ll}
@{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if
@{thm (rhs) nullable_correctness} \\
@@ -264,13 +286,14 @@
regular expression matcher defined as
\begin{center}
-
+ @{thm match_def}
\end{center}
- While the matcher above calculates a provably correct a YES/NO answer for
+ \noindent gives a positive answer if and only if @{term "s \<in> L r"}. While
+ the matcher above calculates a provably correct a 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 calculate a
- value.
+ value. We will explain the details next.
*}
@@ -293,7 +316,24 @@
@{term "Stars vs"}
\end{center}
-The inhabitation relation:
+ \noindent where we use @{term vs} standing for a list of values. The string
+ underlying a values can be calculated by the @{const flat} function, written
+ @{term "flat DUMMY"} and defined as:
+
+ \begin{center}
+ \begin{tabular}{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(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)}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent Sulzmann and Lu also define inductively an inhabitation relation
+ that associates values to regular expressions:
\begin{center}
\begin{tabular}{c}
@@ -307,19 +347,67 @@
\end{tabular}
\end{center}
+ \noindent Note that no values are associated with the regular expression
+ @{term ZERO}, and that the only value associated with the regular
+ expression @{term ONE} is @{term Void}, pronounced (if one must) as {\em
+ ``Void''}. It is routine to stablish how values `inhabitated' by a regular
+ expression correspond to the language of a regular expression, namely
-Note that no values are associated with the regular expression $Zero$, and
-that the only value associated with the regular expression $One$ is $Void$,
-pronounced (if one must) as {\em ``Void''}. We use $\in$ for the usual
-membership relation from set theory and take $[]$ as the standard name for
-the empty string (rather than, as in \cite{Sulzmann2014}, the regular
-expression that we call $One$).
+ \begin{proposition}
+ @{thm L_flat_Prf}
+ \end{proposition}
+
+ Graphically the algorithm by Sulzmann \& Lu can be illustrated by the
+ picture in Figure~\ref{Sulz} where the path from the left to the right
+ involving $der/nullable$ is the first phase of the algorithm and
+ $mkeps/inj$, the path from right to left, the second phase. This picture
+ shows the steps required when a regular expression, say $r_1$, matches the
+ string $abc$. We first build the three derivatives (according to $a$, $b$
+ and $c$). We then use $nullable$ to find out whether the resulting regular
+ expression can match the empty string. If yes, we call the function
+ $mkeps$.
-We begin with the case of a nullable regular expression: from
-the nullability we need to construct a value that witnesses the nullability.
-The @{const mkeps} function (from \cite{Sulzmann2014})
-is a partial (but unambiguous) function from regular expressions to values,
-total on exactly the set of nullable regular expressions.
+\begin{figure}[t]
+\begin{center}
+\begin{tikzpicture}[scale=2,node distance=1.2cm,
+ every node/.style={minimum size=7mm}]
+\node (r1) {@{term "r\<^sub>1"}};
+\node (r2) [right=of r1]{@{term "r\<^sub>2"}};
+\draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};
+\node (r3) [right=of r2]{@{term "r\<^sub>3"}};
+\draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}};
+\node (r4) [right=of r3]{@{term "r\<^sub>4"}};
+\draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}};
+\draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}};
+\node (v4) [below=of r4]{@{term "v\<^sub>4"}};
+\draw[->,line width=1mm](r4) -- (v4);
+\node (v3) [left=of v4] {@{term "v\<^sub>3"}};
+\draw[->,line width=1mm](v4)--(v3) node[below,midway] {@{term "inj c"}};
+\node (v2) [left=of v3]{@{term "v\<^sub>2"}};
+\draw[->,line width=1mm](v3)--(v2) node[below,midway] {@{term "inj b"}};
+\node (v1) [left=of v2] {@{term "v\<^sub>1"}};
+\draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{term "inj a"}};
+\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}
+analysing 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
+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).
+\label{Sulz}}
+\end{figure}
+
+ NOT DONE YET
+
+ We begin with the case of a nullable regular expression: from the
+ nullability we need to construct a value that witnesses the nullability.
+ The @{const mkeps} function (from \cite{Sulzmann2014}) is a partial (but
+ unambiguous) function from regular expressions to values, total on exactly
+ the set of nullable regular expressions.
\begin{center}
\begin{tabular}{lcl}
@@ -387,20 +475,7 @@
- \noindent
- The @{const flat} function for values
-
- \begin{center}
- \begin{tabular}{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(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)}\\
- \end{tabular}
- \end{center}
+
\noindent
The @{const mkeps} function