# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1463399437 -3600
# Node ID 2835d13be7027885cc3035d0b5de349f857b5f28
# Parent  e85d10b238d02b772d5e3c5a38f82161325a7dd4
update

diff -r e85d10b238d0 -r 2835d13be702 Literature/sulzmann-lexing-automata-part-der.pdf
Binary file Literature/sulzmann-lexing-automata-part-der.pdf has changed
diff -r e85d10b238d0 -r 2835d13be702 progs/scala/re-basic.scala
--- a/progs/scala/re-basic.scala	Wed May 11 13:12:30 2016 +0100
+++ b/progs/scala/re-basic.scala	Mon May 16 12:50:37 2016 +0100
@@ -156,6 +156,16 @@
 println(lexing((K2 | I2).%, "abaa"))
 println(env(lexing((K2 | I2).%, "abaa")))
 
+val r1: Rexp = "abc"
+val r2: Rexp = der('a', r1)
+val r3: Rexp = der('b', r2)
+val r4: Rexp = der('c', r3)
+println(r1)
+println(r2)
+println(r3)
+println(r4)
+
+
 // time keeping
 def time_needed[T](i: Int, code: => T) = {
   val start = System.nanoTime()
diff -r e85d10b238d0 -r 2835d13be702 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Wed May 11 13:12:30 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 16 12:50:37 2016 +0100
@@ -200,7 +200,8 @@
 \noindent {\bf Contributions:} We have implemented in Isabelle/HOL the
 derivative-based regular expression matching algorithm of
 Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this
-algorithm according to our specification of what a POSIX value is. Sulzmann
+algorithm according to our specification of what a POSIX value is (inspired
+by work of Vansummeren \cite{Vansummeren2006}). Sulzmann
 and Lu sketch in \cite{Sulzmann2014} an informal correctness proof: but to
 us it contains unfillable gaps.\footnote{An extended version of
 \cite{Sulzmann2014} is available at the website of its first author; this
@@ -242,7 +243,7 @@
   not match any string, @{const ONE} for the regular expression that matches
   only the empty string and @{term c} for matching a character literal. The
   language of a regular expression is also defined as usual by the
-  recursive function @{term L} with the clauses:
+  recursive function @{term L} with the six clauses:
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{3mm}}rcl}
@@ -492,7 +493,7 @@
   \noindent Note that this function needs only to be partially defined,
   namely only for regular expressions that are nullable. In case @{const
   nullable} fails, the string @{term "[a,b,c]"} cannot be matched by @{term
-  "r\<^sub>1"} and an error is raised instead. Note also how this function
+  "r\<^sub>1"} and the null value @{term "None"} is returned. Note also how this function
   makes some subtle choices leading to a POSIX value: for example if an
   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
@@ -774,7 +775,7 @@
   \noindent
   With Lem.~\ref{Posix2} in place, it is completely routine to establish
   that the Sulzmann and Lu lexer satisfies our specification (returning
-  an ``error'' iff the string is not in the language of the regular expression,
+  the null value @{term "None"} iff the string is not in the language of the regular expression,
   and returning a unique POSIX value iff the string \emph{is} in the language):
 
   \begin{theorem}\mbox{}\smallskip\\
diff -r e85d10b238d0 -r 2835d13be702 thys/paper.pdf
Binary file thys/paper.pdf has changed