--- a/thys/Journal/Paper.thy Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Journal/Paper.thy Tue Jul 18 18:39:20 2017 +0100
@@ -3,17 +3,28 @@
imports
"../Lexer"
"../Simplifying"
- "../Sulzmann"
+ "../Positions"
"~~/src/HOL/Library/LaTeXsugar"
begin
+lemma Suc_0_fold:
+ "Suc 0 = 1"
+by simp
+
+
+
declare [[show_question_marks = false]]
abbreviation
- "der_syn r c \<equiv> der c r"
+ "der_syn r c \<equiv> der c r"
abbreviation
- "ders_syn r s \<equiv> ders s r"
+ "ders_syn r s \<equiv> ders s r"
+
+
+abbreviation
+ "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"
+
notation (latex output)
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
@@ -26,7 +37,7 @@
SEQ ("_ \<cdot> _" [77,77] 78) and
STAR ("_\<^sup>\<star>" [1000] 78) and
- val.Void ("'(')" 1000) and
+ val.Void ("Empty" 78) and
val.Char ("Char _" [1000] 78) and
val.Left ("Left _" [79] 78) and
val.Right ("Right _" [1000] 78) and
@@ -56,8 +67,18 @@
simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
slexer ("lexer\<^sup>+" 1000) and
+ at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and
+ lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
+ PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
+ PosOrd_ex ("_ \<prec> _" [77,77] 77) and
+ PosOrd_ex1 ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
+ pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
+ nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77)
+
+ (*
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)"
@@ -99,7 +120,7 @@
one way of how the string is matched. There are two commonly used
disambiguation strategies to generate a unique answer: one is called GREEDY
matching \cite{Frisch2004} and the other is POSIX
-matching~\cite{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider
+matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2013,Sulzmann2014,Vansummeren2006}. For example consider
the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT
(ALT x y) xy)"}}. Either the string can be matched in two `iterations' by
the single letter-regular expressions @{term x} and @{term y}, or directly
@@ -114,18 +135,24 @@
what programmers consider basic syntactic building blocks in their programs.
These building blocks are often specified by some regular expressions, say
@{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and
-identifiers, respectively. There are two underlying (informal) rules behind
-tokenising a string in a POSIX fashion according to a collection of regular
+identifiers, respectively. There are a few underlying (informal) rules behind
+tokenising a string in a POSIX \cite{POSIX} fashion according to a collection of regular
expressions:
\begin{itemize}
-\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):
+\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``{M}aximal {M}unch {R}ule''}):
The longest initial substring matched by any regular expression is taken as
next token.\smallskip
\item[$\bullet$] \emph{Priority Rule:}
-For a particular longest initial substring, the first regular expression
-that can match determines the token.
+For a particular longest initial substring, the first (leftmost) regular expression
+that can match determines the token.\smallskip
+
+\item[$\bullet$] \emph{Star Rule:} A subexpression repeated by ${}^\star$ shall
+not match an empty string unless this is the only match for the repetition.\smallskip
+
+\item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to
+be longer than no match at all.
\end{itemize}
\noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords
@@ -157,7 +184,7 @@
algorithm. This proof idea is inspired by work of Frisch and Cardelli
\cite{Frisch2004} on a 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
+totality for the ``order relation'' by Sulzmann and Lu. ??In Section
\ref{argu} we identify some inherent 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
@@ -1008,6 +1035,104 @@
\end{proof}
*}
+section {* Ordering of Values according to Okui and Suzuki*}
+
+text {*
+
+ Positions are lists of natural numbers.
+
+ The subvalue at position @{text p}, written @{term "at v p"}, is defined
+
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{0mm}}lcl}
+ @{term v} & @{text "\<downharpoonleft>\<^bsub>[]\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(1)}\\
+ @{term "Left v"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(2)}\\
+ @{term "Right v"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"} & @{text "\<equiv>"} &
+ @{thm (rhs) at.simps(3)[simplified Suc_0_fold]}\\
+ @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"} &
+ @{thm (rhs) at.simps(4)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \\
+ @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"}
+ & @{text "\<equiv>"} &
+ @{thm (rhs) at.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2", simplified Suc_0_fold]} \\
+ @{term "Stars vs"} & @{text "\<downharpoonleft>\<^bsub>n::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(6)}\\
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) Pos.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(1)}\\
+ @{thm (lhs) Pos.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(2)}\\
+ @{thm (lhs) Pos.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(3)}\\
+ @{thm (lhs) Pos.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(4)}\\
+ @{thm (lhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+ & @{text "\<equiv>"}
+ & @{thm (rhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\
+ @{thm (lhs) Pos_stars} & @{text "\<equiv>"} & @{thm (rhs) Pos_stars}\\
+ \end{tabular}
+ \end{center}
+
+ @{thm pflat_len_def}
+
+
+ \begin{center}
+ \begin{tabular}{ccc}
+ @{thm [mode=Axiom] lex_list.intros(1)}\hspace{1cm} &
+ @{thm [mode=Rule] lex_list.intros(2)[where ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}\hspace{1cm} &
+ @{thm [mode=Rule] lex_list.intros(3)[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2" and
+ ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}
+ \end{tabular}
+ \end{center}
+
+
+ Main definition by Okui and Suzuki.
+
+ \begin{center}
+ \begin{tabular}{ccl}
+ @{thm (lhs) PosOrd_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} &
+ @{text "\<equiv>"} &
+ @{term "pflat_len v\<^sub>1 p > pflat_len v\<^sub>2 p"} and\\
+ & & @{term "(\<forall>q \<in> Pos v\<^sub>1 \<union> Pos v\<^sub>2. q \<sqsubset>lex p --> pflat_len v\<^sub>1 q = pflat_len v\<^sub>2 q)"}
+ \end{tabular}
+ \end{center}
+
+ @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ @{thm PosOrd_ex1_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Lemma 1
+
+ @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ but in the other direction only
+
+ @{thm [mode=IfThen] PosOrd_shorterI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Lemma Transitivity:
+
+ @{thm [mode=IfThen] PosOrd_trans[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and ?v3.0="v\<^sub>3"]}
+
+
+*}
+
+text {*
+
+ Theorems:
+
+ @{thm [mode=IfThen] Posix_CPT}
+
+ @{thm [mode=IfThen] Posix_PosOrd[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Corrollary from the last one
+
+ @{thm [mode=IfThen] Posix_PosOrd_stronger[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Theorem
+
+ @{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]}
+*}
+
+
section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
text {*
@@ -1022,24 +1147,7 @@
Their central definition is an ``ordering relation'' defined by the
rules (slightly adapted to fit our notation):
-\begin{center}
-\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "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\\
-
-@{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\\
-
-@{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
@{text Left}-value is bigger than a @{text Right}-value, if the underlying
@@ -1062,143 +1170,8 @@
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, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}.
- To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
- not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{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{falsehood}
- 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{falsehood}
-
- \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}
-
- \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:
-
- \begin{conject}
- 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{conject}
-
- \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 @{term 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}{@ {}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}{@ {}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}
- @{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:
- %
- \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}
-
- \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
-
- \[
- @{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 @{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
-
- \[
- @{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.
-
-*}
section {* Conclusion *}