# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457519606 0
# Node ID 879d43256063dd39f16938ad21e3d44b33c986e1
# Parent  a05b3c89e8aa60b37ad9416598b2eddd3244c36e
updated

diff -r a05b3c89e8aa -r 879d43256063 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 12:02:25 2016 +0000
+++ b/thys/Paper/Paper.thy	Wed Mar 09 10:33:26 2016 +0000
@@ -1032,9 +1032,9 @@
 \begin{tabular}{@ {}ll@ {}}
 IH $r_1$:\\
 $\forall v_1, v_2, v_3.$ 
-  & $v_1 : r_1\;\wedge$\\
-  & $v_2 : r_1\;\wedge$\\
-  & $v_3 : r_1\;\wedge$\\
+  & $v_1 : r_1\;\wedge$
+    $v_2 : r_1\;\wedge$
+    $v_3 : r_1\;\wedge$\\
   & $|v_1|=|v_2|=|v_3|\;\wedge$\\
   & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\
   & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$
@@ -1042,9 +1042,9 @@
 \begin{tabular}{@ {}ll@ {}}
 IH $r_2$:\\
 $\forall v_1, v_2, v_3.$ 
-  & $v_1 : r_2\;\wedge$\\
-  & $v_2 : r_2\;\wedge$\\
-  & $v_3 : r_2\;\wedge$\\
+  & $v_1 : r_2\;\wedge$
+    $v_2 : r_2\;\wedge$
+    $v_3 : r_2\;\wedge$\\
   & $|v_1|=|v_2|=|v_3|\;\wedge$\\
   & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\
   & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$
@@ -1073,17 +1073,10 @@
 \label{lens}
 \end{equation}
 
-\noindent
-We need to show that
-
-\[
-Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r}
-\]
-
-\noindent holds. We can proceed by analysing how the
-assumptions in \eqref{assms} have arisen. There are four
-cases. Let us assume we are in the case where
-we know 
+\noindent We need to show that $Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2}
+Seq\, v_{3l}\, v_{3r}$ holds. We can proceed by analysing how the
+assumptions in \eqref{assms} have arisen. There are four cases. Let us
+assume we are in the case where we know
 
 \[
 v_{1l} \posix_{r_1} v_{2l}
@@ -1130,6 +1123,20 @@
   already acknowledge some small problems, but our experience suggests
   that there are more serious problems. 
   
+  Having proved the correctness of the POSIX lexing algorithm in
+  \cite{Sulzmann2014}, which lessons have we learned? Well, this is a
+  perfect example for the importance of the \emph{right} definitions. We
+  have (on and off) banged our heads on doors as soon as as first versions
+  of \cite{Sulzmann2014} appeared, but have made little progress with
+  turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a
+  formalisable proof. Having seen \cite{Vansummeren2006} and adapting the
+  POSIX definition given there for the algorithm by Sulzmann and Lu made all
+  the difference: the proofs, as said, are nearly straightforward. The
+  question remains whether the original proof idea of \cite{Sulzmann2014},
+  potentially using our result as a stepping stone, can be made to work?
+  Alas, we really do not know despite considerable effort and door banging.
+
+
   Closely related to our work is an automata-based lexer formalised by
   Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest
   initial substrings, but Nipkow's algorithm is not completely
@@ -1145,6 +1152,7 @@
   %{\bf Acknowledgements:}
   %We are grateful for the comments we received from anonymous
   %referees.
+  \small
   \bibliographystyle{plain}
   \bibliography{root}
 
diff -r a05b3c89e8aa -r 879d43256063 thys/paper.pdf
Binary file thys/paper.pdf has changed