
diff -r 90fe1a1d7d0e -r 8b41d01b5e5d thys/Paper/Paper.thy
--- 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




