--- a/thys/Paper/Paper.thy	Tue Mar 08 06:30:48 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 07:13:20 2016 +0000
@@ -896,58 +896,201 @@
 
 text {*
   \newcommand{\greedy}{\succcurlyeq_{gr}}
-  \newcommand{\posix}{\succcurlyeq_{PX}}
+  \newcommand{\posix}{>}
 
   An extended version of \cite{Sulzmann2014} is available at the website of
   its first author; this includes some ``proofs'', claimed in
   \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in
   final form, we make no comment thereon, preferring to give general reasons
   for our belief that the approach of \cite{Sulzmann2014} is problematic.
+  Their central definition is an ``ordering relation''
+
+\begin{center}  
+\begin{tabular}{c@ {\hspace{5mm}}c}		 
+$\infer{v_{1} \posix_{r_{1}} v'_{1}} 
+       {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$
+&
+$\infer{v_{2} \posix_{r_{2}} v'_{2}} 
+       {Seq\,v_{1}\,v_{2}) \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$
+\medskip\\
+		
+		
+$\infer{ len |v_{2}| > len |v_{1}|} 
+       {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$ 
+&
+$\infer{ len |v_{1}| \geq len |v_{2}|} 
+       {Left \; v_{1} \posix_{r_{1}+r_{2}} Right \; v_{2}} (A2)$ 
+\medskip\\	
+
+$\infer{ v_{2} \posix_{r_{2}} v'_{2}} 
+       {Right \; v_{2} \posix_{r_{1}+r_{2}} Right \; v'_{2}}(A3)$ & 
+
+$\infer{ v_{1} \posix_{r_{1}} v'_{1}} 
+       {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ 
+\medskip\\
+
+ $\infer{|v :: vs| = []} {[] \posix_{r^{\star}} v :: vs}(K1)$ & 
+ $\infer{|v :: vs| \neq []} { v :: vs \posix_{r^{\star}} []}(K2)$
+\medskip\\
+	
+$\infer{ v_{1} \posix_{r} v_{2}} 
+       {v_{1} :: vs_{1} \posix_{r^{\star}} v_{2} :: vs_{2}}(K3)$ & 
+$\infer{ vs_{1} \posix_{r^{\star}} vs_{2}} 
+       {v :: vs_{1} \posix_{r^{\star}} v :: vs_{2}}(K4)$	
+\end{tabular}
+\end{center}
 
   Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch
   and Cardelli from where they have taken their main idea for their
-  correctness proof of the POSIX algorithm. Frisch and Cardelli introduced
-  an ordering, written $\greedy$, for values and they show that their greedy
-  matching algorithm always produces a maximal element according to this
-  ordering (from all possible solutions). The ordering $\greedy$ is defined
-  by the following rules:
+  correctness proof of the POSIX value algorithm. Frisch and Cardelli
+  introduced an ordering, written $\greedy$, for values and they show that
+  their greedy matching algorithm always produces a maximal element
+  according to this ordering (from all possible solutions). The only
+  difference between their greedy ordering and the ``ordering'' by Sulzmann
+  and Lu is that GREEDY always prefers a $Left$-value over a $Right-value$.
+  What is interesting for our purposes is that the properties reflexivity,
+  totality and transitivity for this GREEDY ordering can be proved
+  relatively easily by induction.
+
+  These properties of GREEDY, however, do not transfer to POSIX by 
+  Sulzmann and Lu. To start with, transitivity does not hold anymore in the
+``normal'' formulation, that is:
+
+\begin{property}
+Suppose $v_1 : r$, $v_2 : r$ and $v_3 : r$.
+If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
+then $v_1 \posix_r v_3$.
+\end{property}
+
+\noindent If formulated like this, then there are various counter examples:
+Suppose $r$ is $a + ((a + a)(a + \textbf{0}))$ then the $v_1$, $v_2$ and $v_3$
+below are values of $r$:
 
 \begin{center}
-\begin{tabular}{cc}
-\infer{v_{1} \greedy v'_{1}} {(v_{1},v_{2}) \greedy (v'_{1},v'_{2})}
-&
-\infer{v_{2} \greedy v'_{2}} {(v_{1},v_{2}) \greedy (v_{1},v'_{2})}
-\smallskip\\
-\infer{v_{1} \greedy v_{2}} {Left \; v_{1} \greedy Left \; v_{2}}
-&
-\infer{v_{1} \greedy v_{2}} {Right \; v_{1} \greedy Right \; v_{2}}
-\\
-
-\infer{\mbox{}}{Left \; v_{2}\greedy Right \; v_{1} }
-\medskip\\
-
-$\infer{ v_{1} \greedy v_{2}} {v_{1} :: vs_{1} \greedy v_{2} :: vs_{2}} $ & 
-$\infer{ vs_{1} \greedy vs_{2}} {v :: vs_{1} \greedy v :: vs_{2}}$
-\\
-
-& 
-$\infer{\mbox{}} { v::vs \greedy []}$
-\\
-
-\infer{\mbox{}}{Char \; c \greedy Char \; c}
-&
-\infer{\mbox{}}{Void \greedy Void}\\
-
+\begin{tabular}{lcl}
+ $v_1$ & $=$ & $Left(Char\;a)$\\
+ $v_2$ & $=$ & $Right((Left(Char\;a), Right(Void)))$\\
+ $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$
 \end{tabular}
 \end{center}
 
-\noindent That these rules realise a greedy ordering can be
-seen in the first rule in the third line where a $Left$-value
-is always bigger than (or preferred over) a $Right$-value.
-What is interesting for our purposes is that the properties
-reflexivity, totality and transitivity for this greedy
-ordering can be proved relatively easily by
-induction.
+\noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,
+but \emph{not} $v_1 \posix_r v_3$! The reason is that although
+$v_3$ is a $Right$-value, it can match a longer string, namely
+$|v_3| = aa$, while $|v_1|$ (and $|v_2|$) matches only $a$. So
+transitivity in this formulation does not hold---in this
+example actually $v_3 \posix_r v_1$!
+
+Sulzmann and Lu ``fix'' this problem by weakening the
+transitivity property. They require in addition that the
+underlying strings are of the same length. This excludes the
+counter example above and any counter-example we could find
+with our implementation. Thus the transitivity lemma in
+\cite{Sulzmann2014} is:
+
+\begin{property}
+Suppose $v_1 : r$, $v_2 : r$ and 
+$v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\
+If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
+then $v_1 \posix_r v_3$.
+\end{property}
+
+\noindent While we agree with Sulzmann and Lu that this
+property probably holds, proving it seems not so
+straightforward. Sulzmann and Lu do not give an explicit proof
+of the transitivity property, but give a closely related
+property about the existence of maximal elements. They state
+that this can be verified by an induction on $r$. We disagree
+with this as we shall show next in case of transitivity.
+
+The case where the reasoning breaks down is the sequence case,
+say $r_1\,r_2$. The induction hypotheses in this case
+are
+
+\begin{center}
+\begin{tabular}{@ {}cc@ {}}
+\begin{tabular}{@ {}ll@ {}}
+IH $r_1$:\\
+$\forall v_1, v_2, v_3.$ 
+  & $\vdash v_1 : r_1\;\wedge$\\
+  & $\vdash v_2 : r_1\;\wedge$\\
+  & $\vdash 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$
+\end{tabular} &
+\begin{tabular}{@ {}ll@ {}}
+IH $r_2$:\\
+$\forall v_1, v_2, v_3.$ 
+  & $\vdash v_1 : r_2\;\wedge$\\
+  & $\vdash v_2 : r_2\;\wedge$\\
+  & $\vdash 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$
+\end{tabular}
+\end{tabular}
+\end{center} 
+
+\noindent
+We can assume that 
+
+\begin{equation}
+(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{2l}, v_{2r})
+\qquad\textrm{and}\qquad
+(v_{2l}, v_{2r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+\label{assms}
+\end{equation}
+
+\noindent
+hold, and furthermore that the values have equal length, 
+namely:
+
+\begin{equation}
+|(v_{1l}, v_{1r})| = |(v_{2l}, v_{2r})|
+\qquad\textrm{and}\qquad
+|(v_{2l}, v_{2r})| = |(v_{3l}, v_{3r})|
+\label{lens}
+\end{equation}
+
+\noindent
+We need to show that
+
+\[
+(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (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 
+
+\[
+v_{1l} \posix^{r_1} v_{2l}
+\qquad\textrm{and}\qquad
+v_{2l} \posix^{r_1} v_{3l}
+\]
+
+\noindent and also know the corresponding typing judgements.
+This is exactly a case where we would like to apply the
+induction hypothesis IH~$r_1$. But we cannot! We still need to
+show that $|v_{1l}| = |v_{2l}|$ and $|v_{2l}| = |v_{3l}|$. We
+know from \eqref{lens} that the lengths of the sequence values
+are equal, but from this we cannot infer anything about the
+lengths of the component values. Indeed in general they will
+be unequal, that is 
+
+\[
+|v_{1l}| \not= |v_{2l}|  
+\qquad\textrm{and}\qquad
+|v_{1r}| \not= |v_{2r}|
+\]
+
+\noindent but still \eqref{lens} will hold. Now we are stuck,
+since the IH does not apply. Sulzmann and Lu overlook this
+fact and just apply the IHs. Obviously nothing which a 
+theorem prover allows us to do.
+
 
 *}