lexing: comparison thys2/Paper/Paper.thy

equal deleted inserted replaced

-:c2c9ab378e70
+:30c91ea7095b
 \begin{tabular}{c}
 \\[-8mm]
 @{thm[mode=Axiom] Prf.intros(4)} \qquad
 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm]
 @{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"]}\\[4mm]
+@{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>2" "r\<^sub>1"]}\\[4mm]
 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]} \qquad
 @{thm[mode=Rule] Prf.intros(6)[of "vs" "r"]}
 \end{tabular}
 \end{center}
 bitcoded regular expressions.
 %
 \begin{center}
 \begin{tabular}{@ {}c@ {}c@ {}}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-$\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{false}$\\
+$\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{False}$\\
-$\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{true}$\\
+$\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{True}$\\
-$\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{false}$\\
+$\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{False}$\\
 $\textit{bnullable}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ &
 $\exists\, r \in \rs. \,\textit{bnullable}\,r$\\
 $\textit{bnullable}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &
 $\textit{bnullable}\,r_1\wedge \textit{bnullable}\,r_2$\\
 $\textit{bnullable}\,(\textit{STAR}\,bs\,r)$ & $\dn$ &
-$\textit{true}$
+$\textit{True}$
 \end{tabular}
 &
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
 $\textit{bmkeps}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ &
 \end{center}
 \noindent
 The key function in the bitcoded algorithm is the derivative of a
-bitcoded regular expression. This derivative calculates the
+bitcoded regular expression. This derivative function calculates the
 derivative but at the same time also the incremental part of the bitsequences
 that contribute to constructing a POSIX value.
 \begin{center}
 \begin{tabular}{@ {}lcl@ {}}
 is the same as if we first erase the bitcoded regular expression and
 then perform the ``standard'' derivative operation.
 \begin{lemma}\label{bnullable}\mbox{}\smallskip\\
 \begin{tabular}{ll}
-\textit{(1)} & $(a\backslash s)^\downarrow = (a^\downarrow)\backslash s$\\
+\textit{(1)} & $(r\backslash s)^\downarrow = (r^\downarrow)\backslash s$\\
-\textit{(2)} & $\textit{bnullable}(a)$ iff $\textit{nullable}(a^\downarrow)$\\
+\textit{(2)} & $\textit{bnullable}(r)$ iff $\textit{nullable}(r^\downarrow)$\\
-\textit{(3)} & $\textit{bmkeps}(a) = \textit{retrieve}\,a\,(\textit{mkeps}\,(a^\downarrow))$ provided $\textit{nullable}(a^\downarrow)$.
+\textit{(3)} & $\textit{bmkeps}(r) = \textit{retrieve}\,r\,(\textit{mkeps}\,(r^\downarrow))$ provided $\textit{nullable}(r^\downarrow)$.
 \end{tabular}
 \end{lemma}
 \begin{proof}
 All properties are by induction on annotated regular expressions. There are no
 For the \textit{if}-branch suppose $r_d \dn r^\uparrow\backslash s$ and
 $d \dn r\backslash s$. We have (*) @{text "nullable d"}. We can then show
 by Lemma~\ref{bnullable}\textit{(3)} that
 %
 \[
-\textit{decode}(\textit{bmkeps}\,r_d)\,r =
+\textit{decode}(\textit{bmkeps}\:r_d)\,r =
-\textit{decode}(\textit{retrieve}\,a\,(\textit{mkeps}\,d))\,r
+\textit{decode}(\textit{retrieve}\,r_d\,(\textit{mkeps}\,d))\,r
 \]
 \noindent
 where the right-hand side is equal to
 $\textit{Some}\,(\textit{flex}\,r\,\textit{id}\,s\,(\textit{mkeps}\,
 aggressive simplification rules described by Sulzmann and Lu. Recasting
 their definition with our syntax they define the step of removing
 duplicates as
 %
 \[ @{text "bsimp (ALTs bs rs)"} \dn @{text "ALTs
-bs (nup (map bsimp rs))"}
+bs (nub (map bsimp rs))"}
 \]
 \noindent where they first recursively simplify the regular
 expressions in @{text rs} (using @{text map}) and then use
 Haskell's @{text nub}-function to remove potential
 duplicates. While this makes sense when considering the example
 shown in \eqref{derivex}, @{text nub} is the inappropriate
 function in the case of bitcoded regular expressions. The reason
 is that in general the elements in @{text rs} will have a
 different annotated bitsequence and in this way @{text nub}
-will never find a duplicate to be removed. The correct way to
+will never find a duplicate to be removed. One correct way to
 handle this situation is to first \emph{erase} the regular
 expressions when comparing potential duplicates. This is inspired
 by Scala's list functions of the form \mbox{@{text "distinctBy rs f
 acc"}} where a function is applied first before two elements
 are compared. We define this function in Isabelle/HOL as
 expressions---essentially a set of regular expressions that we have already seen
 while scanning the list. Therefore we delete an element, say @{text x},
 from the list provided @{text "f x"} is already in the accumulator;
 otherwise we keep @{text x} and scan the rest of the list but
 add @{text "f x"} as another ``seen'' element to @{text acc}. We will use
-@{term distinctBy} where @{text f} is the erase functions, @{term "erase (DUMMY)"},
+@{term distinctBy} where @{text f} is the erase function, @{term "erase (DUMMY)"},
 that deletes bitsequences from bitcoded regular expressions.
 This is clearly a computationally more expensive operation, than @{text nub},
 but is needed in order to make the removal of unnecessary copies
 to work properly.
 \end{tabular}
 \end{center}
 \noindent
 The second clause of @{text flts} removes all instances of @{text ZERO} in alternatives and
-the second ``spills'' out nested alternatives (but retaining the
+the third ``spills'' out nested alternatives (but retaining the
 bitsequence @{text "bs'"} accumulated in the inner alternative). There are
 some corner cases to be considered when the resulting list inside an alternative is
 empty or a singleton list. We take care of those cases in the
 @{text "bsimpALTs"} function; similarly we define a helper function that simplifies
 sequences according to the usual rules about @{text ZERO}s and @{text ONE}s:

changeset 458	30c91ea7095b
parent 436	222333d2bdc2
child 459	484403cf0c9d