# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457397909 0
# Node ID ff084486098171a9121787040df719ee4e339fb1
# Parent  5378ddbd1381116ac32f8bab08c93eb7c4cd9c8e
updated

diff -r 5378ddbd1381 -r ff0844860981 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 00:34:15 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 00:45:09 2016 +0000
@@ -670,7 +670,7 @@
   \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v'"} by induction hypothesis and hence @{term "(c #
   s) \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> injval (ALT r\<^sub>1 r\<^sub>2) c (Left v')"} as needed. Similarly
   in subcase @{text "(b)"} where, however, in addition we have to use
-  Prop~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term
+  Prop.~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term
   "s \<notin> L (der c r\<^sub>1)"}.
 
   Suppose @{term "r = SEQ r\<^sub>1 r\<^sub>2"}. There are three subcases:
@@ -688,7 +688,7 @@
   
   \[@{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):
+  \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)"}\]
 
@@ -737,6 +737,25 @@
   what a correct result---a POSIX value---should be.
 *}
 
+section {* Extensions *}
+
+text {*
+
+  Derivatives as calculated by \Brz's method are usually more complex
+  regular expressions than the initial one; the result is that the matching
+  and lexing algorithms are often absymally slow. 
+
+
+  various optimisations are
+  possible, such as the simplifications of @{term "ALT ZERO r"}, @{term "ALT
+  r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to @{term r}. One of
+  the advantages of having a simple specification and correctness proof is
+  that the latter can be refined to allow for such optimisations and simple
+  correctness proof.
+
+
+*}
+
 section {* The Argument by Sulzmmann and Lu *}
 
 section {* Conclusion *}
diff -r 5378ddbd1381 -r ff0844860981 thys/paper.pdf
Binary file thys/paper.pdf has changed