37   injval ("inj _ _ _" [79,77,79] 76) and 

    37   injval ("inj _ _ _" [79,77,79] 76) and 

    38   mkeps ("mkeps _" [79] 76) and 

    38   mkeps ("mkeps _" [79] 76) and 

    39   length ("len _" [78] 73) and

    39   length ("len _" [78] 73) and

    40  

    40  

    41   Prf ("_ : _" [75,75] 75) and  

    41   Prf ("_ : _" [75,75] 75) and  

    43  

    43  

    44   lexer ("lexer _ _" [78,78] 77) and 

    44   lexer ("lexer _ _" [78,78] 77) and 

    45   F_RIGHT ("F\<^bsub>Right\<^esub> _") and

    45   F_RIGHT ("F\<^bsub>Right\<^esub> _") and

    46   F_LEFT ("F\<^bsub>Left\<^esub> _") and  

    46   F_LEFT ("F\<^bsub>Left\<^esub> _") and  

    47   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

    47   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

   584   \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and

   584   \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and

   585   values.

   585   values.

   586 

   586 

   587   \begin{center}

   587   \begin{center}

   588   \begin{tabular}{c}

   588   \begin{tabular}{c}

   593   $\mprset{flushleft}

   593   $\mprset{flushleft}

   594    \inferrule

   594    \inferrule

   600   $\mprset{flushleft}

   600   $\mprset{flushleft}

   601    \inferrule

   601    \inferrule

   607   \end{tabular}

   607   \end{tabular}

   608   \end{center}

   608   \end{center}

   609 

   609 

   610   \noindent We claim that this relation captures the idea behind the two

   610   \noindent We claim that this relation captures the idea behind the two

   611   informal POSIX rules shown in the Introduction: Consider for example the

   611   informal POSIX rules shown in the Introduction: Consider for example the

   643    We can prove that given a string @{term s} and regular expression @{term

   643    We can prove that given a string @{term s} and regular expression @{term

   644    r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow>

   644    r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow>

   645    v"}.

   645    v"}.

   646 

   646 

   647   \begin{theorem}

   647   \begin{theorem}

   649   \end{theorem}

   649   \end{theorem}

   650 

   650 

   651   \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and

   651   \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and

   652   a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the

   652   a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the

   655   established by inductions.\qed \end{proof}

   655   established by inductions.\qed \end{proof}

   656 

   656 

   657   \noindent

   657   \noindent

   658   Next is the lemma that shows the function @{term "mkeps"} calculates

   658   Next is the lemma that shows the function @{term "mkeps"} calculates

   659   the POSIX value for the empty string and a nullable regular expression.

   659   the POSIX value for the empty string and a nullable regular expression.

   660 

   660 

   661   \begin{lemma}\label{lemmkeps}

   661   \begin{lemma}\label{lemmkeps}

   663   \end{lemma}

   663   \end{lemma}

   664 

   664 

   665   \begin{proof}

   665   \begin{proof}

   666   By routine induction on @{term r}.\qed 

   666   By routine induction on @{term r}.\qed 

   667   \end{proof}

   667   \end{proof}

   668 

   668 

   669   \noindent

   669   \noindent

   670   The central lemma for our POSIX relation is that the @{text inj}-function

   670   The central lemma for our POSIX relation is that the @{text inj}-function

   671   preserves POSIX values.

   671   preserves POSIX values.

   672 

   672 

   675   \end{lemma}

   675   \end{lemma}

   676 

   676 

   677   \begin{proof}

   677   \begin{proof}

   678 

   678 

   679   By induction on @{text r}. Suppose @{term "r = ALT r\<^sub>1 r\<^sub>2"}. There are

   679   By induction on @{text r}. Suppose @{term "r = ALT r\<^sub>1 r\<^sub>2"}. There are

   728   \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}  (which in turn follows from @{term "s\<^sub>1 \<in> der c

   728   \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}  (which in turn follows from @{term "s\<^sub>1 \<in> der c

   729   r\<^sub>1 \<rightarrow> v\<^sub>1"} and the induction hypothesis).\qed

   729   r\<^sub>1 \<rightarrow> v\<^sub>1"} and the induction hypothesis).\qed

   730   \end{proof}

   730   \end{proof}

   731 

   731 

   732   \noindent

   732   \noindent

   734   that the Sulzmann and Lu lexer satisfies our specification (returning

   734   that the Sulzmann and Lu lexer satisfies our specification (returning

   735   an ``error'' iff the string is not in the language of the regular expression,

   735   an ``error'' iff the string is not in the language of the regular expression,

   736   and returning a unique POSIX value iff the string \emph{is} in the language):

   736   and returning a unique POSIX value iff the string \emph{is} in the language):

   737 

   737 

   738   \begin{theorem}\mbox{}\smallskip\\

   738   \begin{theorem}\mbox{}\smallskip\\

   741   (2) & @{thm (lhs) lex_correct3b} if and only if @{thm (rhs) lex_correct3b}\\

   741   (2) & @{thm (lhs) lex_correct3b} if and only if @{thm (rhs) lex_correct3b}\\

   742   \end{tabular}

   742   \end{tabular}

   743   \end{theorem}

   743   \end{theorem}

   744 

   744 

   745   \begin{proof}

   745   \begin{proof}

   747   \end{proof}

   747   \end{proof}

   748 

   748 

   749   \noindent This concludes our correctness proof. Note that we have not

   749   \noindent This concludes our correctness proof. Note that we have not

   750   changed the algorithm by Sulzmann and Lu,\footnote{Any deviation we introduced is harmless.} 

   750   changed the algorithm by Sulzmann and Lu,\footnote{Any deviation we introduced is harmless.} 

   751   but introduced our own

   751   but introduced our own