--- 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>\<star>" [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 ("'(_, _') \<rightarrow> _" [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 ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
definition
"match r s \<equiv> 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 \<ge>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) \<and> (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 \<ge>(r::rexp)
+ (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
+ formulation, for example:
+
+ \begin{proposition}
+ Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> 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)\<cdot>(a + \<zero>))"}
+ 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 "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> 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 "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\
+ & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}
+ @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}
+ @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\
+ & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
+ & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> 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 "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\
+ & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}
+ @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}
+ @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\
+ & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
+ & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> 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) \<noteq> flat(v\<^sub>2\<^sub>l)"}
+ \qquad\textrm{and}\qquad
+ @{term "flat(v\<^sub>1\<^sub>r) \<noteq> 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.
*}