# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1647859498 0
# Node ID 30c91ea7095b64b19818d0a4f1cf2a145657cd1c
# Parent  c2c9ab378e702662cd97b8b10095f9ef2c1e886a
updated paper

diff -r c2c9ab378e70 -r 30c91ea7095b thys2/Paper/Paper.thy
--- 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
diff -r c2c9ab378e70 -r 30c91ea7095b thys2/paper.pdf
Binary file thys2/paper.pdf has changed