--- a/thys2/Paper/Paper.thy Sun Mar 20 23:32:45 2022 +0000
+++ b/thys2/Paper/Paper.thy Mon Mar 21 10:44:58 2022 +0000
@@ -331,7 +331,7 @@
@{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}
@@ -682,15 +682,15 @@
\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{ONE}\,bs)$ & $\dn$ & $\textit{true}$\\
- $\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{false}$\\
+ $\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{False}$\\
+ $\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{True}$\\
+ $\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@ {}}
@@ -712,7 +712,7 @@
\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.
@@ -800,9 +800,9 @@
\begin{lemma}\label{bnullable}\mbox{}\smallskip\\
\begin{tabular}{ll}
-\textit{(1)} & $(a\backslash s)^\downarrow = (a^\downarrow)\backslash s$\\
-\textit{(2)} & $\textit{bnullable}(a)$ iff $\textit{nullable}(a^\downarrow)$\\
-\textit{(3)} & $\textit{bmkeps}(a) = \textit{retrieve}\,a\,(\textit{mkeps}\,(a^\downarrow))$ provided $\textit{nullable}(a^\downarrow)$.
+\textit{(1)} & $(r\backslash s)^\downarrow = (r^\downarrow)\backslash s$\\
+\textit{(2)} & $\textit{bnullable}(r)$ iff $\textit{nullable}(r^\downarrow)$\\
+\textit{(3)} & $\textit{bmkeps}(r) = \textit{retrieve}\,r\,(\textit{mkeps}\,(r^\downarrow))$ provided $\textit{nullable}(r^\downarrow)$.
\end{tabular}
\end{lemma}
@@ -923,8 +923,8 @@
by Lemma~\ref{bnullable}\textit{(3)} that
%
\[
- \textit{decode}(\textit{bmkeps}\,r_d)\,r =
- \textit{decode}(\textit{retrieve}\,a\,(\textit{mkeps}\,d))\,r
+ \textit{decode}(\textit{bmkeps}\:r_d)\,r =
+ \textit{decode}(\textit{retrieve}\,r_d\,(\textit{mkeps}\,d))\,r
\]
\noindent
@@ -1014,9 +1014,9 @@
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
@@ -1025,7 +1025,7 @@
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
@@ -1047,7 +1047,7 @@
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
@@ -1067,7 +1067,7 @@
\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