diff -r 42ffaca7c85e -r 162f112b814b thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 17 03:47:33 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue May 17 05:14:41 2016 +0100
@@ -26,10 +26,10 @@
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [1000] 78) and
   
-  val.Void ("'(')" 79) and
+  val.Void ("'(')" 1000) and
   val.Char ("Char _" [1000] 78) and
   val.Left ("Left _" [79] 78) and
-  val.Right ("Right _" [79] 78) and
+  val.Right ("Right _" [1000] 78) and
   val.Seq ("Seq _ _" [79,79] 78) and
   val.Stars ("Stars _" [79] 78) and
 
@@ -268,15 +268,8 @@
   language and @{term "s\<^sub>2"} in the star of this language, then also @{term
   "s\<^sub>1 @ s\<^sub>2"} is in the star of this language. It will also be convenient
   to use the following notion of a \emph{semantic derivative} (or \emph{left
-  quotient}) of a language defined as:
-
-  \begin{center}
-  \begin{tabular}{lcl}
-  @{thm (lhs) Der_def} & $\dn$ & @{thm (rhs) Der_def}\\
-  \end{tabular}
-  \end{center}
-  
-  \noindent 
+  quotient}) of a language defined as
+  @{thm (lhs) Der_def} $\dn$ @{thm (rhs) Der_def}.
   For semantic derivatives we have the following equations (for example
   mechanically proved in \cite{Krauss2011}):
 
@@ -329,6 +322,9 @@
   \begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
+  \end{tabular}
+  \hspace{20mm}
+  \begin{tabular}{lcl}
   @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
   \end{tabular}
   \end{center}
@@ -346,7 +342,7 @@
 
   \noindent With this in place it is also very routine to prove that the
   regular expression matcher defined as
-
+  %
   \begin{center}
   @{thm match_def}
   \end{center}
@@ -625,20 +621,20 @@
   \cite{Vansummeren2006}. The relation we define is ternary and written as
   \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and
   values.
-
-  \begin{center}
+  %
+  \begin{center}\small
   \begin{tabular}{c}
   @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
-  @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\bigskip\\
+  @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\medskip\\
   @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad
-  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\bigskip\\
+  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\medskip\\
   $\mprset{flushleft}
    \inferrule
    {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
     @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
     @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
    {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\
-  @{thm[mode=Axiom] Posix.intros(7)}@{text "P[]"}\bigskip\\
+  @{thm[mode=Axiom] Posix.intros(7)}@{text "P[]"}\medskip\\
   $\mprset{flushleft}
    \inferrule
    {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
@@ -742,11 +738,11 @@
 
   \noindent For @{text "(a)"} we know @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} and
   @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} as well as
-  
+  %
   \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]
 
   \noindent From the latter we can infer by Prop.~\ref{derprop}(2):
-
+  %
   \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]
 
   \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain
@@ -758,7 +754,7 @@
   @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former
   we have @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> (injval r\<^sub>2 c v\<^sub>1)"} by induction hypothesis
   for @{term "r\<^sub>2"}. From the latter we can infer
-
+  %
   \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]
 
   \noindent By Lem.~\ref{lemmkeps} we know @{term "[] \<in> r\<^sub>1 \<rightarrow> (mkeps r\<^sub>1)"}
@@ -851,10 +847,10 @@
   rules like
 
   \begin{equation}\label{Simpl}
-  \begin{array}{lcl}
-  @{term "ALT ZERO r"} & @{text "\<Rightarrow>"} & @{term r}\\
-  @{term "ALT r ZERO"} & @{text "\<Rightarrow>"} & @{term r}\\
-  @{term "SEQ ONE r"}  & @{text "\<Rightarrow>"} & @{term r}\\
+  \begin{array}{lcllcllcllcl}
+  @{term "ALT ZERO r"} & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\
+  @{term "ALT r ZERO"} & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\
+  @{term "SEQ ONE r"}  & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\
   @{term "SEQ r ONE"}  & @{text "\<Rightarrow>"} & @{term r}
   \end{array}
   \end{equation}
@@ -870,7 +866,8 @@
   The rectification functions can be (slightly clumsily) implemented  in
   Isabelle/HOL as follows using some auxiliary functions:
 
-  \begin{center}
+  \begin{center}\small
+  \begin{tabular}{cc}
   \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)"}\\
@@ -880,8 +877,10 @@
   
   @{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)"}%\bigskip\\
+  \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)"}\\
   @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"}\\
@@ -889,6 +888,7 @@
   @{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
@@ -930,7 +930,7 @@
   @{term v} (that is construct @{term "f\<^sub>r v"}). Before we can establish the correctness
   of @{term "slexer"}, we need to show that simplification preserves the language
   and simplification preserves our POSIX relation once the value is rectified
-  (recall @{const "simp"} generates a regular expression, rectification function pair):
+  (recall @{const "simp"} generates a regular expression / rectification function pair):
 
   \begin{lemma}\mbox{}\smallskip\\\label{slexeraux}
   \begin{tabular}{ll}
@@ -939,11 +939,22 @@
   \end{tabular}
   \end{lemma}
 
-  \begin{proof}
-  Both are by induction on @{text r}. There is no interesting case for the
-  first statement. For the second statement of interest are the @{term "r = SEQ r\<^sub>1 r\<^sub>2"}
-  and @{term "r = ALT r\<^sub>1 r\<^sub>2"} cases.
-  
+  \begin{proof} Both are by induction on @{text r}. There is no
+  interesting case for the first statement. For the second statement,
+  of interest are the @{term "r = ALT r\<^sub>1 r\<^sub>2"} and @{term "r = SEQ r\<^sub>1
+  r\<^sub>2"} cases. In each case we have to analyse four subcases whether
+  @{term "fst (simp r\<^sub>1)"} and @{term "fst (simp r\<^sub>2)"} equals @{const
+  ZERO} (respectively @{const ONE}). For example for @{term "r = ALT
+  r\<^sub>1 r\<^sub>2"}, considder the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and
+  @{term "fst (simp r\<^sub>2) \<noteq> ZERO"}. By assumption we know @{term "s \<in>
+  fst (simp (ALT r\<^sub>1 r\<^sub>2)) \<rightarrow> v"}. From this we can infer @{term "s \<in> fst (simp r\<^sub>2) \<rightarrow> v"}
+  and by IH also (*) @{term "s \<in> r\<^sub>2 \<rightarrow> (snd (simp r\<^sub>2) v)"}. Given @{term "fst (simp r\<^sub>1) = ZERO"}
+  we know @{term "L (fst (simp r\<^sub>1)) = {}"}. By the first statement
+  @{term "L r\<^sub>1"} is the empty set, meaning (**) @{term "s \<notin> L r\<^sub>1"}.
+  Taking (*) and (**) together gives by the \mbox{@{text "P+R"}}-rule 
+  @{term "s \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> Right (snd (simp r\<^sub>2) v)"}. In turn this
+  gives @{term "s \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> snd (simp (ALT r\<^sub>1 r\<^sub>2)) v"} as we need to show.
+  The other cases are similar.\qed
   \end{proof}
 
   \noindent We can now prove relatively straightforwardly that the
@@ -999,7 +1010,7 @@
   Their central definition is an ``ordering relation'' defined by the
   rules (slightly adapted to fit our notation):
 
-\begin{center}  
+\begin{center}\small  
 \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\\