diff -r 9ab8609c66c5 -r 807acaf7f599 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Fri Aug 17 12:00:25 2018 +0100
+++ b/thys/Journal/Paper.thy	Sat Aug 18 01:54:44 2018 +0100
@@ -31,6 +31,12 @@
 abbreviation 
   "ders_syn r s \<equiv> ders s r"
 
+  abbreviation 
+  "bder_syn r c \<equiv> bder c r"
+
+abbreviation 
+  "bders_syn r s \<equiv> bders r s"
+
 
 abbreviation
   "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"
@@ -91,6 +97,15 @@
   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
   nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and
 
+  bder_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and  
+  bders_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and
+  intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and
+  erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and
+  bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and
+  bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and
+  blexer ("lexer\<^latex>\<open>\\mbox{$_b$}\<close> _ _" [77, 77] 80) and
+  code ("code _" [79] 74) and
+
   DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")
 
 
@@ -710,10 +725,10 @@
   The idea of the @{term inj}-function to ``inject'' a character, say
   @{term c}, into a value can be made precise by the first part of the
   following lemma, which shows that the underlying string of an injected
-  value has a prepended character @{term c}; the second part shows that the
-  underlying string of an @{const mkeps}-value is always the empty string
-  (given the regular expression is nullable since otherwise @{text mkeps}
-  might not be defined).
+  value has a prepended character @{term c}; the second part shows that
+  the underlying string of an @{const mkeps}-value is always the empty
+  string (given the regular expression is nullable since otherwise
+  @{text mkeps} might not be defined).
 
   \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat}
   \begin{tabular}{ll}
@@ -1385,6 +1400,126 @@
 
 *}
 
+section {* Bitcoded Lexing *}
+
+
+text {*
+
+Incremental calculation of the value. To simplify the proof we first define the function
+@{const flex} which calculates the ``iterated'' injection function. With this we can 
+rewrite the lexer as
+
+\begin{center}
+@{thm lexer_flex}
+\end{center}
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\
+  @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\
+  @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\
+  @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\
+  @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\
+  @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)}
+\end{tabular}
+\end{center}
+
+\begin{center}
+\begin{tabular}{lcl}
+  @{term areg} & $::=$ & @{term "AZERO"}\\
+               & $\mid$ & @{term "AONE bs"}\\
+               & $\mid$ & @{term "ACHAR bs c"}\\
+               & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\
+               & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
+               & $\mid$ & @{term "ASTAR bs r"}
+\end{tabular}
+\end{center}
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\
+  @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\
+  @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\
+  @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\
+\end{tabular}
+\end{center}
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\
+  @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\
+  @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\
+  @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\
+\end{tabular}
+\end{center}
+
+Some simple facts about erase
+
+\begin{lemma}\mbox{}\\
+@{thm erase_bder}\\
+@{thm erase_intern}
+\end{lemma}
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\
+  @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\
+  @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\
+  @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\
+
+%  \end{tabular}
+%  \end{center}
+
+%  \begin{center}
+%  \begin{tabular}{lcl}
+
+  @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\
+  @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\
+  @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\
+  @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)}
+  \end{tabular}
+  \end{center}
+
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\
+  @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\
+\end{tabular}
+\end{center}
+
+
+@{thm [mode=IfThen] bder_retrieve}
+
+By induction on @{text r}
+
+\begin{theorem}[Main Lemma]\mbox{}\\
+@{thm [mode=IfThen] MAIN_decode}
+\end{theorem}
+
+\noindent
+Definition of the bitcoded lexer
+
+@{thm blexer_def}
+
+
+\begin{theorem}
+@{thm blexer_correctness}
+\end{theorem}
+
+*}
+
 section {* Optimisations *}
 
 text {*