(*<*)+
−
theory Paper+
−
imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar"+
−
begin+
−
+
−
declare [[show_question_marks = false]]+
−
+
−
abbreviation +
−
 "der_syn r c \<equiv> der c r"+
−
+
−
notation (latex output)+
−
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and+
−
  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [78,77] 73) and+
−
  ZERO ("\<^raw:\textrm{0}>" 78) and +
−
  ONE ("\<^raw:\textrm{1}>" 78) and +
−
  CHAR ("_" [1000] 10) and+
−
  ALT ("_ + _" [77,77] 78) and+
−
  SEQ ("_ \<cdot> _" [77,77] 78) and+
−
  STAR ("_\<^sup>\<star>" [1000] 78) and+
−
  val.Char ("Char _" [1000] 78) and+
−
  val.Left ("Left _" [1000] 78) and+
−
  val.Right ("Right _" [1000] 78) and+
−
  L ("L'(_')" [10] 78) and+
−
  der_syn ("_\\_" [1000, 1000] 78) and+
−
  flat ("|_|" [70] 73) and+
−
  Sequ ("_ @ _" [78,77] 63) and+
−
  injval ("inj _ _ _" [1000,77,1000] 77) and +
−
  projval ("proj _ _ _" [1000,77,1000] 77) and +
−
  length ("len _" [78] 73) +
−
  (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
+
−
Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em+
−
derivative} @{term "der c r"} of a regular expression @{text r} w.r.t.\ a+
−
character~@{text c}, and showed that it gave a simple solution to the+
−
problem of matching a string @{term s} with a regular expression @{term r}:+
−
if the derivative of @{term r} w.r.t.\ (in succession) all the characters of+
−
the string matches the empty string $\mts$, then @{term r} matches @{term s}+
−
(and {\em vice versa}). The derivative has the property (which may be+
−
regarded as its specification) that, for every string @{term s} and regular+
−
expression @{term r} and character @{term c}, one has @{term "cs \<in> L(r)"} if+
−
and only if \mbox{@{term "s \<in> L(der c r)"}}. The beauty of Brzozowski's+
−
derivatives is that they are neatly expressible in any functional language, and+
−
very easy to be defined and reasoned about in a theorem prover---the+
−
definitions consist just of inductive datatypes and recursive functions. A+
−
completely formalised proof of this matcher has for example been given in+
−
\cite{Owens2008}.+
−
+
−
One limitation of Brzozowski's matcher is that it only generates a YES/NO+
−
answer for a string being matched by a regular expression. Sulzmann and Lu+
−
\cite{Sulzmann2014} extended this matcher to allow generation not just of a+
−
YES/NO answer but of an actual matching, called a [lexical] {\em value}.+
−
They give a still very simple algorithm to calculate a value that appears to+
−
be the value associated with POSIX lexing (posix) %%\cite{posix}. The+
−
challenge then is to specify that value, in an algorithm-independent+
−
fashion, and to show that Sulzamman and Lu's derivative-based algorithm does+
−
indeed calculate a value that is correct according to the specification.+
−
+
−
Inspired by work of Frisch and Cardelli \cite{Frisch2004} on a GREEDY+
−
regular expression matching algorithm, the answer given in+
−
\cite{Sulzmann2014} is to define a relation (called an ``Order Relation'')+
−
on the set of values of @{term r}, and to show that (once a string to be+
−
matched is chosen) there is a maximum element and that it is computed by the+
−
derivative-based algorithm. Beginning with our observations that, without+
−
evidence that it is transitive, it cannot be called an ``order relation'',+
−
and that the relation is called a ``total order'' despite being evidently+
−
not total\footnote{\textcolor{green}{Why is it not total?}}, we identify+
−
problems with this approach (of which some of the proofs are not published+
−
in \cite{Sulzmann2014}); perhaps more importantly, we give a simple+
−
inductive (and algorithm-independent) definition of what we call being a+
−
{\em POSIX value} for a regular expression @{term r} and a string @{term s};+
−
we show that the algorithm computes such a value and that such a value is+
−
unique. Proofs are both done by hand and checked in {\em Isabelle}+
−
%\cite{isabelle}. Our experience of doing our proofs has been that this+
−
mechanical checking was absolutely essential: this subject area has hidden+
−
snares. This was also noted by Kuklewitz \cite{Kuklewicz} who found that+
−
nearly all POSIX matching implementations are ``buggy'' \cite[Page+
−
203]{Sulzmann2014}.+
−
+
−
\textcolor{green}{Say something about POSIX lexing}+
−
+
−
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 rather than to discuss details of unpublished work.+
−
+
−
Derivatives as calculated by Brzozowski's method are usually more+
−
complex regular expressions than the initial one; various optimisations+
−
are possible, such as the simplifications of @{term "ALT ZERO r"},+
−
@{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to+
−
@{term r}. One of the advantages of having a simple specification and+
−
correctness proof is that the latter can be refined to allow for such+
−
optimisations and simple correctness proof.+
−
+
−
+
−
Sulzmann and Lu \cite{Sulzmann2014}+
−
\cite{Brzozowski1964}+
−
+
−
there are two commonly used+
−
disambiguation strategies to create a unique matching tree:+
−
one is called \emph{greedy} matching \cite{Frisch2004} and the+
−
other is \emph{POSIX} matching~\cite{Kuklewicz,Sulzmann2014}.+
−
For the latter there are two rough rules:  +
−
+
−
\begin{itemize}+
−
\item The Longest Match Rule (or ``maximal munch rule''):\smallskip\\ The+
−
      longest initial substring matched by any regular+
−
      expression is taken as next token.+
−
+
−
\item Rule Priority:\smallskip\\ For a particular longest initial+
−
      substring, the first regular expression that can match+
−
      determines the token.+
−
\end{itemize}+
−
+
−
\noindent In the context of lexing, POSIX is the more+
−
interesting disambiguation strategy as it produces longest+
−
matches, which is necessary for tokenising programs. For+
−
example the string \textit{iffoo} should not match the keyword+
−
\textit{if} and the rest, but as one string \textit{iffoo},+
−
which might be a variable name in a program. As another+
−
example consider the string $xy$ and the regular expression+
−
\mbox{$(x + y + xy)^*$}. Either the input string can be+
−
matched in two `iterations' by the single letter-regular+
−
expressions $x$ and $y$, or directly in one iteration by $xy$.+
−
The first case corresponds to greedy matching, which first+
−
matches with the left-most symbol and only matches the next+
−
symbol in case of a mismatch. The second case is POSIX+
−
matching, which prefers the longest match. In case more than+
−
one (longest) matches exist, only then it prefers the+
−
left-most match. While POSIX matching seems natural, it turns+
−
out to be much more subtle than greedy matching in terms of+
−
implementations and in terms of proving properties about it.+
−
If POSIX matching is implemented using automata, then one has+
−
to follow transitions (according to the input string) until+
−
one finds an accepting state, record this state and look for+
−
further transition which might lead to another accepting state+
−
that represents a longer input initial substring to be+
−
matched. Only if none can be found, the last accepting state+
−
is returned.+
−
+
−
+
−
Sulzmann and Lu's paper \cite{Sulzmann2014} targets POSIX+
−
regular expression matching. They write that it is known to be+
−
to be a non-trivial problem and nearly all POSIX matching+
−
implementations are ``buggy'' \cite[Page 203]{Sulzmann2014}.+
−
For this they cite a study by Kuklewicz \cite{Kuklewicz}. My+
−
current work is about formalising the proofs in the paper by+
−
Sulzmann and Lu. Specifically, they propose in this paper a+
−
POSIX matching algorithm and give some details of a+
−
correctness proof for this algorithm inside the paper and some+
−
more details in an appendix. This correctness proof is+
−
unformalised, meaning it is just a ``pencil-and-paper'' proof,+
−
not done in a theorem prover. Though, the paper and presumably+
−
the proof have been peer-reviewed. Unfortunately their proof+
−
does not give enough details such that it can be+
−
straightforwardly implemented in a theorem prover, say+
−
Isabelle. In fact, the purported proof they outline does not+
−
work in central places. We discovered this when filling in+
−
many gaps and attempting to formalise the proof in Isabelle. +
−
+
−
+
−
\medskip\noindent+
−
{\bf Contributions:}+
−
+
−
*}+
−
+
−
section {* Preliminaries *}+
−
+
−
text {* \noindent Strings in Isabelle/HOL are lists of characters with+
−
  the empty string being represented by the empty list, written @{term+
−
  "[]"}, and list-cons being written as @{term "DUMMY # DUMMY"}.+
−
  Often we use the usual bracket notation for strings; for example a+
−
  string consiting of a single character is written @{term "[c]"}.  By+
−
  using the type @{type char} for characters we have a supply of+
−
  finitely many characters roughly corresponding to the ASCII+
−
  character set.  Regular expression are as usual and defined as the+
−
  following inductive datatype:+
−
+
−
  \begin{center}+
−
  @{text "r :="}+
−
  @{const "ZERO"} $\mid$+
−
  @{const "ONE"} $\mid$+
−
  @{term "CHAR c"} $\mid$+
−
  @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$+
−
  @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$+
−
  @{term "STAR r"} +
−
  \end{center}+
−
+
−
  \noindent where @{const ZERO} stands for the regular expression that+
−
  does not macth any string and @{const ONE} for the regular+
−
  expression that matches only the empty string. The language of a regular expression+
−
  is again defined as usual by the following clauses+
−
+
−
  \begin{center}+
−
  \begin{tabular}{rcl}+
−
  @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\+
−
  @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\+
−
  @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\+
−
  @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
  +
−
  \noindent We use the star-notation for regular expressions and sets of strings.+
−
  The Kleene-star on sets is defined inductively.+
−
  +
−
  \emph{Semantic derivatives} of sets of strings are defined as+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) Der_def} & $\dn$ & @{thm (rhs) Der_def}\\+
−
  @{thm (lhs) Ders_def} & $\dn$ & @{thm (rhs) Ders_def}\\+
−
  \end{tabular}+
−
  \end{center}+
−
  +
−
  \noindent where the second definitions lifts the notion of semantic+
−
  derivatives from characters to strings.  +
−
+
−
  \noindent+
−
  The nullable function+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\+
−
  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\+
−
  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\+
−
  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The derivative function for characters and strings+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcp{7.5cm}}+
−
  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\+
−
  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\+
−
  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\+
−
  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\+
−
+
−
  @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\+
−
  @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  It is a relatively easy exercise to prove that+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  @{thm[mode=IfThen] nullable_correctness}\\+
−
  @{thm[mode=IfThen] der_correctness}\\+
−
  \end{tabular}+
−
  \end{center}+
−
*}+
−
+
−
section {* POSIX Regular Expression Matching *}+
−
+
−
section {* The Argument by Sulzmmann and Lu *}+
−
+
−
section {* Conclusion *}+
−
+
−
text {*+
−
+
−
  Nipkow lexer from 2000+
−
+
−
*}+
−
+
−
+
−
text {*+
−
+
−
+
−
+
−
+
−
  \noindent+
−
  Values+
−
+
−
  \begin{center}+
−
  @{text "v :="}+
−
  @{const "Void"} $\mid$+
−
  @{term "val.Char c"} $\mid$+
−
  @{term "Left v"} $\mid$+
−
  @{term "Right v"} $\mid$+
−
  @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ +
−
  @{term "Stars vs"} +
−
  \end{center}  +
−
+
−
  \noindent+
−
  The language of a regular expression+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\+
−
  @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\+
−
  @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\+
−
  @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
 +
−
+
−
  \noindent+
−
  The @{const flat} function for values+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\+
−
  @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\+
−
  @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\+
−
  @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\+
−
  @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\+
−
  @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\+
−
  @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The @{const mkeps} function+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\+
−
  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The @{text inj} function+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\+
−
  @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & +
−
      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\+
−
  @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & +
−
      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\+
−
  @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\+
−
  @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\+
−
  @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\+
−
  @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The inhabitation relation:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\ +
−
  @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad +
−
  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\+
−
  @{thm[mode=Axiom] Prf.intros(4)} \qquad +
−
  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\+
−
  @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad +
−
  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  We have also introduced a slightly restricted version of this relation+
−
  where the last rule is restricted so that @{term "flat v \<noteq> []"}.+
−
  This relation for \emph{non-problematic} is written @{term "\<Turnstile> v : r"}.+
−
  \bigskip+
−
+
−
+
−
  \noindent+
−
  Our Posix relation @{term "s \<in> r \<rightarrow> v"}+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Axiom] PMatch.intros(1)} \qquad+
−
  @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\+
−
  @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad+
−
  @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\+
−
  \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\+
−
  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}\medskip\\+
−
  @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  Our version of Sulzmann's ordering relation+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Rule] ValOrd.intros(2)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]} \qquad+
−
  @{thm[mode=Rule] ValOrd.intros(1)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}\medskip\\+
−
  @{thm[mode=Rule] ValOrd.intros(3)[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]} \qquad+
−
  @{thm[mode=Rule] ValOrd.intros(4)[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ +
−
  @{thm[mode=Rule] ValOrd.intros(5)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "r\<^sub>1"]} \qquad+
−
  @{thm[mode=Rule] ValOrd.intros(6)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'"  "r\<^sub>2"]} \medskip\\+
−
  @{thm[mode=Axiom] ValOrd.intros(7)}\qquad+
−
  @{thm[mode=Axiom] ValOrd.intros(8)[of "c"]}\medskip\\+
−
  @{thm[mode=Rule] ValOrd.intros(9)[of "v" "vs" "r"]}\qquad+
−
  @{thm[mode=Rule] ValOrd.intros(10)[of "v" "vs" "r"]}\medskip\\+
−
  @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\+
−
  @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad+
−
  @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  A prefix of a string s+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm prefix_def[of "s\<^sub>1" "s\<^sub>2"]}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  Values and non-problematic values+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm Values_def}\medskip\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
+
−
  \noindent+
−
  The point is that for a given @{text s} and @{text r} there are only finitely many+
−
  non-problematic values.+
−
*} +
−
+
−
text {* +
−
  \noindent+
−
  Some lemmas we have proved:\bigskip+
−
  +
−
  @{thm L_flat_Prf}+
−
+
−
  @{thm L_flat_NPrf}+
−
+
−
  @{thm[mode=IfThen] mkeps_nullable}+
−
+
−
  @{thm[mode=IfThen] mkeps_flat}+
−
+
−
  @{thm[mode=IfThen] Prf_injval}+
−
+
−
  @{thm[mode=IfThen] Prf_injval_flat}+
−
  +
−
  @{thm[mode=IfThen] PMatch_mkeps}+
−
  +
−
  @{thm[mode=IfThen] PMatch1(2)}+
−
+
−
  @{thm[mode=IfThen] PMatch1N}+
−
+
−
  @{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]}+
−
+
−
  \medskip+
−
  \noindent+
−
  This is the main theorem that lets us prove that the algorithm is correct according to+
−
  @{term "s \<in> r \<rightarrow> v"}:+
−
+
−
  @{thm[mode=IfThen] PMatch2}+
−
+
−
  \mbox{}\bigskip+
−
  +
−
  \noindent {\bf Proof} The proof is by induction on the definition of+
−
  @{const der}. Other inductions would go through as well. The+
−
  interesting case is for @{term "SEQ r\<^sub>1 r\<^sub>2"}. First we analyse the+
−
  case where @{term "nullable r\<^sub>1"}. We have by induction hypothesis+
−
+
−
  \[+
−
  \begin{array}{l}+
−
  (IH1)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>1 \<rightarrow> v"} +
−
  \text{\;then\;} @{term "(c # s) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v"}\\+
−
  (IH2)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>2 \<rightarrow> v"} +
−
  \text{\;then\;} @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> injval r\<^sub>2 c v"}+
−
  \end{array}+
−
  \]+
−
  +
−
  \noindent+
−
  and have +
−
+
−
  \[+
−
  @{term "s \<in> ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2) \<rightarrow> v"}+
−
  \]+
−
  +
−
  \noindent+
−
  There are two cases what @{term v} can be: (1) @{term "Left v'"} and (2) @{term "Right v'"}.+
−
+
−
  \begin{itemize}+
−
  \item[(1)] We know @{term "s \<in> SEQ (der c r\<^sub>1) r\<^sub>2 \<rightarrow> v'"} holds, from which we+
−
  can infer that there are @{text "s\<^sub>1"}, @{term "s\<^sub>2"}, @{text "v\<^sub>1"}, @{term "v\<^sub>2"}+
−
  with+
−
+
−
  \[+
−
  @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} \qquad\text{and}\qquad @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"}+
−
  \]+
−
+
−
  and also+
−
+
−
  \[+
−
  @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}+
−
  \]+
−
+
−
  \noindent+
−
  and have to prove+
−
  +
−
  \[+
−
  @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}+
−
  \]+
−
+
−
  \noindent+
−
  The two requirements @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"} and +
−
  @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} can be proved by the induction hypothese (IH1) and the+
−
  fact above.+
−
+
−
  \noindent+
−
  This leaves to prove+
−
  +
−
  \[+
−
  @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}+
−
  \]+
−
  +
−
  \noindent+
−
  which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "}+
−
+
−
  \item[(2)] This case is similar.+
−
  \end{itemize}+
−
+
−
  \noindent +
−
  The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar+
−
  to the cases above.+
−
*}+
−
+
−
+
−
text {*+
−
  %\noindent+
−
  %{\bf Acknowledgements:}+
−
  %We are grateful for the comments we received from anonymous+
−
  %referees.+
−
+
−
  \bibliographystyle{plain}+
−
  \bibliography{root}+
−
+
−
  \section{Roy's Rules}+
−
+
−
   \newcommand{\abs}[1]{\mid\!\! #1\!\! \mid}+
−
   %%\newcommand{\mts}{\textit{``''}+
−
   \newcommand{\tl}{\ \triangleleft\ }+
−
   $$\inferrule[]{Void \tl \epsilon}{}+
−
            \quad\quad+
−
     \inferrule[]{Char\ c \tl Lit\ c}{}+
−
   $$+
−
   $$\inferrule+
−
       {v_1 \tl r_1}+
−
       {Left\ v_1 \tl r_1 + r_2}+
−
   \quad\quad+
−
     \inferrule[]+
−
       { v_2 \tl r_2 \\ \abs{v_2}\ \not\in\ L(r_1)}+
−
       {Right\ v_2 \tl r_1 + r_2}+
−
   $$+
−
   $$+
−
   \inferrule+
−
       {v_1 \tl r_1\\+
−
        v_2 \tl r_2\\+
−
        s \in\  L(r_1\backslash\! \abs{v_1}) \ \land\+
−
        \abs{v_2}\!\backslash s\ \epsilon\ L(r_2)+
−
        \ \Rightarrow\ s = []+
−
       }+
−
       {(v_1, v_2) \tl r_1 \cdot r_2}+
−
   $$+
−
   $$\inferrule+
−
         { v \tl r \\ vs \tl r^* \\ \abs{v}\ \not=\ []} +
−
         { (v :: vs) \tl r^* }+
−
   \quad\quad+
−
       \inferrule{}+
−
         { []  \tl r^* }       +
−
   $$+
−
+
−
*}+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−