--- 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\\