--- a/thys/Paper/Paper.thy Tue May 17 10:53:34 2016 +0100
+++ b/thys/Paper/Paper.thy Tue May 17 11:16:56 2016 +0100
@@ -624,7 +624,7 @@
\mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and
values.
%
- \begin{center}\small
+ \begin{center}
\begin{tabular}{c}
@{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
@{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\medskip\\
@@ -868,8 +868,7 @@
The rectification functions can be (slightly clumsily) implemented in
Isabelle/HOL as follows using some auxiliary functions:
- \begin{center}\small
- \begin{tabular}{cc}
+ \begin{center}
\begin{tabular}{lcl}
@{thm (lhs) F_RIGHT.simps(1)} & $\dn$ & @{text "Right (f v)"}\\
@{thm (lhs) F_LEFT.simps(1)} & $\dn$ & @{text "Left (f v)"}\\
@@ -879,9 +878,9 @@
@{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\
@{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\
- @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}%\bigskip\\
+ @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\
\end{tabular}
- &
+
\begin{tabular}{lcl}
@{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\
@{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\
@@ -890,7 +889,6 @@
@{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"}\\
@{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"}\\
\end{tabular}
- \end{tabular}
\end{center}
\noindent
@@ -960,7 +958,7 @@
\end{proof}
\noindent We can now prove relatively straightforwardly that the
- optimised lexer produce the expected result:
+ optimised lexer produces the expected result:
\begin{theorem}
@{thm slexer_correctness}
@@ -971,27 +969,27 @@
string is of the form @{term "c # s"}. By induction hypothesis we
know @{term "slexer r s = lexer r s"} holds for all @{term r} (in
particular for @{term "r"} being the derivative @{term "der c
- r"}). Let @{term "r\<^sub>s"} be the simplified derivative regular expression, @{term
+ r"}). Let @{term "r\<^sub>s"} be the simplified derivative regular expression, that is @{term
"fst (simp (der c r))"}, and @{term "f\<^sub>r"} be the rectification
- function, @{term "snd (simp (der c r))"}. We distinguish the cases
+ function, that is @{term "snd (simp (der c r))"}. We distinguish the cases
whether (*) @{term "s \<in> L (der c r)"} or not. In the first case we
- have by Thm~\ref{lexercorrect}(2) a value @{term "v"} so that @{term
+ have by Thm.~\ref{lexercorrect}(2) a value @{term "v"} so that @{term
"lexer (der c r) s = Some v"} and @{term "s \<in> der c r \<rightarrow> v"} hold.
- By Lem~\ref{slexeraux}(1) we can also infer from~(*) that @{term "s
- \<in> L r\<^sub>s"} holds. Hence we know by Thm~\ref{lexercorrect}(2) that
+ By Lem.~\ref{slexeraux}(1) we can also infer from~(*) that @{term "s
+ \<in> L r\<^sub>s"} holds. Hence we know by Thm.~\ref{lexercorrect}(2) that
there exists a @{term "v'"} with @{term "lexer r\<^sub>s s = Some v'"} and
@{term "s \<in> r\<^sub>s \<rightarrow> v'"}. From the latter we know by
- Lem~\ref{slexeraux}(2) that @{term "s \<in> der c r \<rightarrow> (f\<^sub>r v')"} holds.
- By the uniqueness of the POSIX relation (Thm~\ref{posixdeterm}) we
+ Lem.~\ref{slexeraux}(2) that @{term "s \<in> der c r \<rightarrow> (f\<^sub>r v')"} holds.
+ By the uniqueness of the POSIX relation (Thm.~\ref{posixdeterm}) we
can infer that @{term v} is equal to @{term "f\<^sub>r v'"}---that is the
rectification function applied to @{term "v'"}
produces the original @{term "v"}. Now the case follows by the
definitions of @{const lexer} and @{const slexer}.
In the second case where @{term "s \<notin> L (der c r)"} we have that
- @{term "lexer (der c r) s = None"} by Thm~\ref{lexercorrect}(1). We
- also know by Lem~\ref{slexeraux}(1) that @{term "s \<notin> L r\<^sub>s"}. Hence
- @{term "lexer r\<^sub>s s = None"} by Thm~\ref{lexercorrect}(1) and
+ @{term "lexer (der c r) s = None"} by Thm.~\ref{lexercorrect}(1). We
+ also know by Lem.~\ref{slexeraux}(1) that @{term "s \<notin> L r\<^sub>s"}. Hence
+ @{term "lexer r\<^sub>s s = None"} by Thm.~\ref{lexercorrect}(1) and
by IH then also @{term "slexer r\<^sub>s s = None"}. With this we can
conclude in this case too.\qed
@@ -1012,7 +1010,7 @@
Their central definition is an ``ordering relation'' defined by the
rules (slightly adapted to fit our notation):
-\begin{center}\small
+\begin{center}
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\