--- a/thys2/Journal/Paper.thy~ Thu Nov 04 13:52:17 2021 +0000
+++ b/thys2/Journal/Paper.thy~ Tue Dec 14 16:06:42 2021 +0000
@@ -131,19 +131,11 @@
(*>*)
-
-
-section \<open>Introduction\<close>
-
-
+section\<open>Core of the proof\<close>
text \<open>
-Trying out after lualatex.
-
-
-uhuhuhu
-This works builds on previous work by Ausaf and Urban using
+This paper builds on previous work by Ausaf and Urban using
regular expression'd bit-coded derivatives to do lexing that
-is both fast and satisfied the POSIX specification.
+is both fast and satisfies the POSIX specification.
In their work, a bit-coded algorithm introduced by Sulzmann and Lu
was formally verified in Isabelle, by a very clever use of
flex function and retrieve to carefully mimic the way a value is
@@ -151,10 +143,138 @@
In the previous work, Ausaf and Urban established the below equality:
\begin{lemma}
-@{thm [mode=IfThen] bder_retrieve}
+@{thm [mode=IfThen] MAIN_decode}
+\end{lemma}
+
+This lemma establishes a link with the lexer without bit-codes.
+
+With it we get the correctness of bit-coded algorithm.
+\begin{lemma}
+@{thm [mode=IfThen] blexer_correctness}
+\end{lemma}
+
+However what is not certain is whether we can add simplification
+to the bit-coded algorithm, without breaking the correct lexing output.
+
+
+The reason that we do need to add a simplification phase
+after each derivative step of $\textit{blexer}$ is
+because it produces intermediate
+regular expressions that can grow exponentially.
+For example, the regular expression $(a+aa)^*$ after taking
+derivative against just 10 $a$s will have size 8192.
+
+%TODO: add figure for this?
+
+
+Therefore, we insert a simplification phase
+after each derivation step, as defined below:
+\begin{lemma}
+@{thm blexer_simp_def}
\end{lemma}
-This lemma links the regular expression
+The simplification function is given as follows:
+
+\begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\
+ @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
+ @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
+
+\end{tabular}
+\end{center}
+
+And the two helper functions are:
+\begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) bsimp_AALTs.simps(2)[of "bs\<^sub>1" "r" ]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs\<^sub>1" "r" ]}\\
+ @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
+ @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
+
+\end{tabular}
+\end{center}
+
+
+This might sound trivial in the case of producing a YES/NO answer,
+but once we require a lexing output to be produced (which is required
+in applications like compiler front-end, malicious attack domain extraction,
+etc.), it is not straightforward if we still extract what is needed according
+to the POSIX standard.
+
+
+
+
+
+By simplification, we mean specifically the following rules:
+
+\begin{center}
+ \begin{tabular}{lcl}
+ @{thm[mode=Axiom] rrewrite.intros(1)[of "bs" "r\<^sub>2"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(2)[of "bs" "r\<^sub>1"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(3)[of "bs" "bs\<^sub>1" "r\<^sub>1"]}\\
+ @{thm[mode=Rule] rrewrite.intros(4)[of "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\
+ @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\
+ @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\
+ @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\
+ @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\
+ @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
+
+ \end{tabular}
+\end{center}
+
+
+And these can be made compact by the following simplification function:
+
+where the function $\mathit{bsimp_AALTs}$
+
+The core idea of the proof is that two regular expressions,
+if "isomorphic" up to a finite number of rewrite steps, will
+remain "isomorphic" when we take the same sequence of
+derivatives on both of them.
+This can be expressed by the following rewrite relation lemma:
+\begin{lemma}
+@{thm [mode=IfThen] central}
+\end{lemma}
+
+This isomorphic relation implies a property that leads to the
+correctness result:
+if two (nullable) regular expressions are "rewritable" in many steps
+from one another,
+then a call to function $\textit{bmkeps}$ gives the same
+bit-sequence :
+\begin{lemma}
+@{thm [mode=IfThen] rewrites_bmkeps}
+\end{lemma}
+
+Given the same bit-sequence, the decode function
+will give out the same value, which is the output
+of both lexers:
+\begin{lemma}
+@{thm blexer_def}
+\end{lemma}
+
+\begin{lemma}
+@{thm blexer_simp_def}
+\end{lemma}
+
+And that yields the correctness result:
+\begin{lemma}
+@{thm blexersimp_correctness}
+\end{lemma}
+
+The nice thing about the aove
+\<close>
+
+
+
+section \<open>Introduction\<close>
+
+
+text \<open>
+
Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em
derivative} @{term "der c r"} of a regular expression \<open>r\<close> w.r.t.\
@@ -334,6 +454,9 @@
\<close>
+
+
+
section \<open>Preliminaries\<close>
text \<open>\noindent Strings in Isabelle/HOL are lists of characters with
@@ -1416,111 +1539,6 @@
@{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 "ACH bs c"}\\
- & $\mid$ & @{term "AALT bs r1 r2"}\\
- & $\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 \<open>r\<close>
-
-\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}
\<close>
@@ -1643,7 +1661,7 @@
\begin{tabular}{lcl}
@{term areg} & $::=$ & @{term "AZERO"}\\
& $\mid$ & @{term "AONE bs"}\\
- & $\mid$ & @{term "ACH bs c"}\\
+ & $\mid$ & @{term "ACHAR bs c"}\\
& $\mid$ & @{term "AALT bs r1 r2"}\\
& $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
& $\mid$ & @{term "ASTAR bs r"}
@@ -1977,19 +1995,6 @@
section \<open>HERE\<close>
text \<open>
- \begin{center}
- \begin{tabular}{llcl}
- 1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\
- 2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\
- 3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\
- 4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\
- 4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\
- 4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ &
- @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\
- 5) & @{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"]}\\
- 6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\
- \end{tabular}
- \end{center}
\begin{lemma}
@{thm [mode=IfThen] bder_retrieve}
@@ -1999,7 +2004,7 @@
By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are
straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to
@{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)
- where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption
+ where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption
we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by
simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again
@{term "\<Turnstile> v : ZERO"}, which cannot hold.
@@ -2040,7 +2045,7 @@
and right-hand side are equal. This completes the proof.
\end{proof}
-
+
\bibliographystyle{plain}
\bibliography{root}
@@ -2048,4 +2053,225 @@
\<close>
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
+
+(*
+
+\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 r1 r2"}\\
+ & $\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 \<open>r\<close>
+
+\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}
+
+
+
+
+
+\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 r1 r2"}\\
+ & $\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 \<open>r\<close>
+
+\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}
+
+\<close>
+\<close>*)
\ No newline at end of file