(*<*)
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
(*>*)