# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1462696370 -3600
# Node ID 072a701bb1535208ff7da76baff2c43de4713fa0
# Parent  6b0a1976f89a9cc6872712c35e6f2578b8bed301
updated

diff -r 6b0a1976f89a -r 072a701bb153 progs/scala/tests.scala
--- a/progs/scala/tests.scala	Fri May 06 11:33:21 2016 +0100
+++ b/progs/scala/tests.scala	Sun May 08 09:32:50 2016 +0100
@@ -31,18 +31,17 @@
   def Regex() : Rexp = {
     val t = Term();
     if (more() && peek() == '|') {
-      eat ('|') ;
-      val r = Regex();
-      ALT(t, r) 
+      eat ('|') ; 
+      ALT(t, Regex()) 
     } 
     else t
   }
 
   def Term() : Rexp = {
-    var f : Rexp = if (more() && peek() != ')' && peek() != '|') Factor() else ZERO;
+    var f : Rexp = 
+      if (more() && peek() != ')' && peek() != '|') Factor() else ZERO;
     while (more() && peek() != ')' && peek() != '|') {
-      var nextf = Factor();
-      f = SEQ(f, nextf) ;
+      f = SEQ(f, Factor()) ;
     }
 
     f
diff -r 6b0a1976f89a -r 072a701bb153 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri May 06 11:33:21 2016 +0100
+++ b/thys/Paper/Paper.thy	Sun May 08 09:32:50 2016 +0100
@@ -84,7 +84,8 @@
 just consist of inductive datatypes and simple recursive functions. A
 completely formalised correctness proof of this matcher in for example HOL4
 has been mentioned by Owens and Slind~\cite{Owens2008}. Another one in Isabelle/HOL is part
-of the work by Krauss and Nipkow \cite{Krauss2011}.
+of the work by Krauss and Nipkow \cite{Krauss2011}. And another one in Coq is given
+by Coquand and Siles \cite{Coquand2012}.
 
 One limitation of Brzozowski's matcher is that it only generates a YES/NO
 answer for whether a string is being matched by a regular expression.
@@ -102,20 +103,10 @@
 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. Beginning with our
-observations that, without evidence that it is transitive, it cannot be
-called an ``order relation'', and that the relation is called a ``total
-order'' despite being evidently not total\footnote{The relation @{text
-"\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014} is a relation on the
-values for the regular expression @{term r}; but it only holds between
-@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
-the same flattening (underlying string). So a counterexample to totality is
-given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
-have different flattenings (see Section~\ref{posixsec}). A different
-relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
-with flattening @{term s} is definable by the same approach, and is indeed
-total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}, we
-identify problems with this approach (of which some of the proofs are not
+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
@@ -126,6 +117,18 @@
 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
+%values for the regular expression @{term r}; but it only holds between
+%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
+%the same flattening (underlying string). So a counterexample to totality is
+%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
+%have different flattenings (see Section~\ref{posixsec}). A different
+%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
+%with flattening @{term s} is definable by the same approach, and is indeed
+%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}
+
+
 If a regular expression matches a string, then in general there is more than
 one way of how the string is matched. There are two commonly used
 disambiguation strategies to generate a unique answer: one is called GREEDY
@@ -902,7 +905,7 @@
 
 *}
 
-section {* The Correctness Argument by Sulzmmann and Lu *}
+section {* The Correctness Argument by Sulzmmann and Lu\label{argu} *}
 
 text {*
 %  \newcommand{\greedy}{\succcurlyeq_{gr}}
diff -r 6b0a1976f89a -r 072a701bb153 thys/paper.pdf
Binary file thys/paper.pdf has changed