diff -r 71f4ecc08849 -r 702ed601349b thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Fri Mar 11 21:21:09 2016 +0000 +++ b/thys/Paper/Paper.thy Sun Mar 13 01:07:34 2016 +0000 @@ -1,6 +1,9 @@ (*<*) theory Paper -imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar" +imports + "../ReStar" + "../Sulzmann" + "~~/src/HOL/Library/LaTeXsugar" begin declare [[show_question_marks = false]] @@ -23,7 +26,7 @@ STAR ("_\<^sup>\" [1000] 78) and val.Void ("'(')" 79) and - val.Char ("Char _" [1000] 79) and + val.Char ("Char _" [1000] 78) and val.Left ("Left _" [79] 78) and val.Right ("Right _" [79] 78) and val.Seq ("Seq _ _" [79,79] 78) and @@ -36,7 +39,7 @@ Sequ ("_ @ _" [78,77] 63) and injval ("inj _ _ _" [79,77,79] 76) and mkeps ("mkeps _" [79] 76) and - length ("len _" [78] 73) and + length ("len _" [73] 73) and Prf ("_ : _" [75,75] 75) and Posix ("'(_, _') \ _" [63,75,75] 75) and @@ -50,7 +53,10 @@ F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and - slexer ("lexer\<^sup>+ _ _" [78,78] 77) + slexer ("lexer\<^sup>+ _ _" [78,78] 77) and + + ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and + ValOrdEq ("_ \\<^bsub>_\<^esub> _" [77,77,77] 77) definition "match r s \ nullable (ders s r)" @@ -897,8 +903,8 @@ section {* The Correctness Argument by Sulzmmann and Lu *} text {* - \newcommand{\greedy}{\succcurlyeq_{gr}} - \newcommand{\posix}{>} +% \newcommand{\greedy}{\succcurlyeq_{gr}} + \newcommand{\posix}{>} An extended version of \cite{Sulzmann2014} is available at the website of its first author; this includes some ``proofs'', claimed in @@ -909,198 +915,179 @@ rules (slightly adapted to fit our notation): \begin{center} -\begin{tabular}{@ {}c@ {\hspace{2mm}}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)$ -\smallskip\\ - - -$\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)$ -\smallskip\\ +\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} +@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]}(C2) & +@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}(C1)\smallskip\\ + +@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}(A1) & +@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}(A2)\smallskip\\ -$\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)$ -\smallskip\\ +@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}(A3) & +@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}(A4)\smallskip\\ - $\infer{|v :: vs| = []} {Stars\,[] \posix_{r^{\star}} Stars\,(v :: vs)}(K1)$ & - $\infer{|v :: vs| \neq []} {Stars\,(v :: vs) \posix_{r^{\star}} Stars\,[]}(K2)$ -\smallskip\\ - -$\infer{ v_{1} \posix_{r} v_{2}} - {Stars\,(v_{1} :: vs_{1}) \posix_{r^{\star}} Stars\,(v_{2} :: vs_{2})}(K3)$ & -$\infer{ Stars\,vs_{1} \posix_{r^{\star}} Stars\,vs_{2}} - {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$ +@{thm[mode=Rule] K1[of "v" "vs" "r"]}(K1) & +@{thm[mode=Rule] K2[of "v" "vs" "r"]}(K2)\smallskip\\ + +@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}(K3) & +@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}(K4) \end{tabular} \end{center} - \noindent - The idea behind the rules $(A1)$ and $(A2)$, for example, is that a $Left$-value is - bigger than a $Right$-value, if the underlying string of the $Left$-value is - longer or of equal length to the underlying string of the $Right$-value. The order - is reversed, however, if the $Right$-value can match longer string than a $Left$-value. - In this way the POSIX value is supposed to be the biggest value - for a given string and regular expression. + \noindent The idea behind the rules (A1) and (A2), for example, is that a + @{text Left}-value is bigger than a @{text Right}-value, if the underlying + string of the @{text Left}-value is longer or of equal length to the + underlying string of the @{text Right}-value. The order is reversed, + however, if the @{text Right}-value can match a longer string than a + @{text Left}-value. In this way the POSIX value is supposed to be the + biggest value for a given string and regular expression. Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch and Cardelli from where they have taken the idea for their correctness - proof. Frisch and Cardelli introduced a - similar ordering for GREEDY matching 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, if - possible, always prefers a $Left$-value over a $Right$-value, no matter - what the underlying string is. This seems to be only a very minor - difference, but it has drastic consequences in terms of what - properties both orderings enjoy. 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. + proof. Frisch and Cardelli introduced a similar ordering for GREEDY + matching and they showed 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 @{text + Left}-value over a @{text Right}-value, no matter what the underlying + string is. This seems to be only a very minor difference, but it has + drastic consequences in terms of what properties both orderings enjoy. + 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 the POSIX - ``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v'$ is not - defined inductively, but as $v = v'$ or $v >_r v' \wedge |v| = |v'|$. This - means that $v >_r v'$ does not imply $v \geq_r v'$. Moreover, transitivity - does not hold in the ``usual'' formulation, for example: + ``ordering'' by Sulzmann and Lu. To start with, @{text "v\<^sub>1 \r v\<^sub>2"} is + not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r + v\<^sub>2) \ (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1 + >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \(r::rexp) + (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' + formulation, for example: + + \begin{proposition} + Suppose @{term "\ v\<^sub>1 : r"}, @{term "\ v\<^sub>2 : r"} and @{term "\ v\<^sub>3 : r"}. + If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"} + then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}. + \end{proposition} + + \noindent If formulated in this way, then there are various counter + examples: For example let @{term r} be @{text "a + ((a + a)\(a + \))"} + then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values + of @{term r}: + + \begin{center} + \begin{tabular}{lcl} + @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\ + @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\ + @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"} + \end{tabular} + \end{center} -\begin{proposition} -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{proposition} + \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp) + v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that + although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer + string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and + @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this + formulation does not hold---in this example actually @{term "v\<^sub>3 + >(r::rexp) v\<^sub>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 were able to find (by hand and by machine). Thus the + transitivity lemma should be formulated as: -\noindent If formulated in this way, then there are various counter examples: -For example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$, -$v_2$ and $v_3$ below are values of $r$: + \begin{proposition} + Suppose @{term "\ v\<^sub>1 : r"}, @{term "\ v\<^sub>2 : r"} and @{term "\ v\<^sub>3 : r"}, + and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\ + If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"} + then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}. + \end{proposition} + + \noindent While we agree with Sulzmann and Lu that this property + probably(!) holds, proving it seems not so straightforward: although one + begins with the assumption that the values have the same flattening, this + cannot be maintained as one descends into the induction. This is a problem + that occurs in a number of places in the proofs by Sulzmann and Lu. + + Although they do not give an explicit proof of the transitivity property, + they 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 @{term "SEQ r\<^sub>1 r\<^sub>2"}. + The induction hypotheses in this case are \begin{center} -\begin{tabular}{lcl} - $v_1$ & $=$ & $Left(Char\;a)$\\ - $v_2$ & $=$ & $Right((Left(Char\;a), Right()))$\\ - $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$ -\end{tabular} -\end{center} - -\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| = [a,a]$, 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 were able -to find (by hand and by machine). Thus the transitivity -lemma should be formulated as: - -\begin{proposition} -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{proposition} - -\noindent While we agree with Sulzmann and Lu that this property probably(!) -holds, proving it seems not so straightforward: although one begins with the -assumption that the values have the same flattening, this -cannot be maintained as one descends into the induction. This is -a problem that occurs in a number of places in the proofs by Sulzmann and Lu. - -Although they do not give an explicit proof -of the transitivity property, they 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\cdot 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.$ - & $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$ +\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} +\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}} +IH @{term "r\<^sub>1"}:\\ +@{text "\ v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\ + & @{term "\ v\<^sub>1 : r\<^sub>1"}\;@{text "\"} + @{term "\ v\<^sub>2 : r\<^sub>1"}\;@{text "\"} + @{term "\ v\<^sub>3 : r\<^sub>1"}\\ + & @{text "\"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\ + & @{text "\"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \ v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\ + & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"} \end{tabular} & -\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|=|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$ +\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}} +IH @{term "r\<^sub>2"}:\\ +@{text "\ v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ + & @{term "\ v\<^sub>1 : r\<^sub>2"}\;@{text "\"} + @{term "\ v\<^sub>2 : r\<^sub>2"}\;@{text "\"} + @{term "\ v\<^sub>3 : r\<^sub>2"}\\ + & @{text "\"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\ + & @{text "\"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \ v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\ + & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"} \end{tabular} \end{tabular} \end{center} -\noindent -We can assume that - -\begin{equation} -Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\,v_{2l}\, v_{2r} -\qquad\textrm{and}\qquad -Seq\,v_{2l}\, v_{2r} \posix_{r_1\cdot r_2} Seq\,v_{3l}\, v_{3r} -\label{assms} -\end{equation} + \noindent We can assume that + % + \begin{equation} + @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"} + \qquad\textrm{and}\qquad + @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} + \label{assms} + \end{equation} -\noindent -hold, and furthermore that the values have equal length, -namely: + \noindent hold, and furthermore that the values have equal length, namely: + % + \begin{equation} + @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"} + \qquad\textrm{and}\qquad + @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} + \label{lens} + \end{equation} -\begin{equation} -|Seq\,v_{1l}\, v_{1r}| = |Seq\,v_{2l}\, v_{2r}| -\qquad\textrm{and}\qquad -|Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}| -\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}$ 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 @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) + (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} 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} -\] + \[ + @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"} + \qquad\textrm{and}\qquad + @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"} + \] -\noindent and also know the corresponding inhabitation 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 + \noindent and also know the corresponding inhabitation 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 @{term "flat (v\<^sub>1\<^sub>l) = + flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. 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}| -\] + \[ + @{term "flat(v\<^sub>1\<^sub>l) \ flat(v\<^sub>2\<^sub>l)"} + \qquad\textrm{and}\qquad + @{term "flat(v\<^sub>1\<^sub>r) \ flat(v\<^sub>2\<^sub>r)"} + \] -\noindent but still \eqref{lens} will hold. Now we are stuck, -since the IH does not apply. As said, this problem where the -induction hypothesis does not apply arises in several places in -the proof of Sulzmann and Lu, not just for proving transitivity. + \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH + does not apply. As said, this problem where the induction hypothesis does + not apply arises in several places in the proof of Sulzmann and Lu, not + just for proving transitivity. *}