# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1462697361 -3600
# Node ID 91647a8d84a30a96511fa61612b8e6be59bf2335
# Parent  baef08fdbccc9dc75a113ad06209eeefb2b43bd6
updated

diff -r baef08fdbccc -r 91647a8d84a3 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Sun May 08 09:34:00 2016 +0100
+++ b/thys/Paper/Paper.thy	Sun May 08 09:49:21 2016 +0100
@@ -99,23 +99,25 @@
 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{arg} we
-identify 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}.
+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
diff -r baef08fdbccc -r 91647a8d84a3 thys/paper.pdf
Binary file thys/paper.pdf has changed