539   \end{lemma}

   539   \end{lemma}

   540 

   540 

   541   \begin{proof}

   541   \begin{proof}

   542   Both properties are by routine inductions: the first one, for example,

   542   Both properties are by routine inductions: the first one, for example,

   543   by an induction over the definition of @{term derivatives}; the second by

   543   by an induction over the definition of @{term derivatives}; the second by

   545   \end{proof}

   545   \end{proof}

   546 

   546 

   547   Having defined the @{const mkeps} and @{text inj} function we can extend

   547   Having defined the @{const mkeps} and @{text inj} function we can extend

   548   \Brz's matcher so that a [lexical] value is constructed (assuming the

   548   \Brz's matcher so that a [lexical] value is constructed (assuming the

   549   regular expression matches the string). The clauses of the lexer are

   549   regular expression matches the string). The clauses of the lexer are

   639   @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}

   639   @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}

   640   \end{theorem}

   640   \end{theorem}

   641 

   641 

   642   \begin{proof}

   642   \begin{proof}

   643   By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and a case

   643   By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and a case

   645   \end{proof}

   645   \end{proof}

   646 

   646 

   647   \begin{lemma}

   647   \begin{lemma}

   648   @{thm[mode=IfThen] PMatch_mkeps}

   648   @{thm[mode=IfThen] PMatch_mkeps}

   649   \end{lemma}

   649   \end{lemma}

   650 

   650 

   652 

   654 

   653   \begin{lemma}

   655   \begin{lemma}

   654   @{thm[mode=IfThen] PMatch2_roy_version}

   656   @{thm[mode=IfThen] PMatch2_roy_version}

   655   \end{lemma}

   657   \end{lemma}

   656 

   658