--- a/thys/Paper/Paper.thy	Sun May 08 09:49:21 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 09 12:09:56 2016 +0100
@@ -62,6 +62,29 @@
 definition 
   "match r s \<equiv> nullable (ders s r)"
 
+(*
+comments not implemented
+
+p9. "None is returned, indicating an error is raised" : there is no error
+
+p9. The condtion "not exists s3 s4..." appears often enough (in particular in
+the proof of Lemma 3) to warrant a definition.
+
+p9. "The POSIX value v" : at this point the existence of a POSIX value is yet
+to be shown
+
+p10. (proof Lemma 3) : separating the cases with description/itemize would greatly
+improve readability
+
+p11. Theorem 2(2) : Stressing the uniqueness is strange, given that it follows
+trivially from the fact that "lexer" is a function. Maybe state the existence of
+a unique POSIX value as corollary.
+
+p14. Proposition 3 is evidently false and Proposition 4 is a conjecture.
+I find it confusing that Propositions 1 and 2, which are proven facts, are also called propositions.
+
+*)
+
 (*>*)
 
 section {* Introduction *}
@@ -414,7 +437,7 @@
   can match the empty string. If yes, we call the function @{const mkeps}
   that produces a value @{term "v\<^sub>4"} for how @{term "r\<^sub>4"} can
   match the empty string (taking into account the POSIX constraints in case
-  there are several ways). This functions is defined by the clauses:
+  there are several ways). This function is defined by the clauses:
 
 \begin{figure}[t]
 \begin{center}
@@ -519,7 +542,7 @@
 
   \noindent Consider first the @{text "else"}-branch where the derivative is @{term
   "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore
-  be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand
+  be of the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand
   side in clause~(4) of @{term inj}. In the @{text "if"}-branch the derivative is an
   alternative, namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c
   r\<^sub>2)"}. This means we either have to consider a @{text Left}- or
@@ -559,7 +582,7 @@
 
   \begin{proof}
   Both properties are by routine inductions: the first one can, for example,
-  be proved by an induction over the definition of @{term derivatives}; the second by
+  be proved by induction over the definition of @{term derivatives}; the second by
   an induction on @{term r}. There are no interesting cases.\qed
   \end{proof}
 
@@ -684,7 +707,7 @@
   preserves POSIX values.
 
   \begin{lemma}\label{Posix2}
-  @{thm[mode=IfThen] Posix2_roy_version}
+  @{thm[mode=IfThen] Posix_injval}
   \end{lemma}
 
   \begin{proof}
@@ -722,7 +745,7 @@
   \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain
   @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer
   @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}. The case @{text "(c)"}
-  is similarly.
+  is similar.
 
   For @{text "(b)"} we know @{term "s \<in> der c r\<^sub>2 \<rightarrow> v\<^sub>1"} and 
   @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former
@@ -760,8 +783,8 @@
   \end{proof}
 
   \noindent This concludes our correctness proof. Note that we have not
-  changed the algorithm of Sulzmann and Lu,\footnote{Any deviation we
-  introduced is harmless.} but introduced our own specification for what a
+  changed the algorithm of Sulzmann and Lu,\footnote{All deviations we
+  introduced are harmless.} but introduced our own specification for what a
   correct result---a POSIX value---should be. A strong point in favour of
   Sulzmann and Lu's algorithm is that it can be extended in various ways.
 
@@ -891,23 +914,23 @@
   \end{center}
 
   \noindent
-  In the second clause we first calculate the derivative @{text "r \\ c"}
+  In the second clause we first calculate the derivative @{term "der c r"}
   and then simplify the result. This gives us a simplified derivative
   @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer
   is then recursively called with the simplified derivative, but before
-  we inject the character @{term c} into value, we need to rectify
+  we inject the character @{term c} into the value, we need to rectify
   it (that is construct @{term "f\<^sub>r v"}). We can prove that
 
-  \begin{lemma}
+  \begin{theorem}
   @{thm slexer_correctness}
-  \end{lemma}
+  \end{theorem}
 
   \noindent
   holds but for lack of space refer the reader to our mechanisation for details.
 
 *}
 
-section {* The Correctness Argument by Sulzmmann and Lu\label{argu} *}
+section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 
 text {*
 %  \newcommand{\greedy}{\succcurlyeq_{gr}}

--- a/thys/Paper/document/root.bib	Sun May 08 09:49:21 2016 +0100
+++ b/thys/Paper/document/root.bib	Mon May 09 12:09:56 2016 +0100
@@ -219,7 +219,7 @@
 @InProceedings{Coquand2012,
   author =       {T.~Coquand and V.~Siles},
   title =        {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
-  booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs (CPP)},
+  booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},
   pages =     {119--134},
   year =      {2011},
   volume =    {7086},

--- a/thys/Paper/document/root.tex	Sun May 08 09:49:21 2016 +0100
+++ b/thys/Paper/document/root.tex	Mon May 09 12:09:56 2016 +0100
@@ -68,8 +68,7 @@
 algorithm. Our definitions and proof are much simpler than those by
 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
 second part we analyse the correctness argument by Sulzmann and Lu and
-explain why it seems hard to turn it into a proof rigorous enough to
-be accepted by a system such as Isabelle/HOL.\smallskip
+explain why the gaps in this argument cannot be filled easily.\smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL

--- a/thys/ReStar.thy	Sun May 08 09:49:21 2016 +0100
+++ b/thys/ReStar.thy	Mon May 09 12:09:56 2016 +0100
@@ -170,8 +170,6 @@
 | Left val
 | Stars "val list"
 
-datatype_compat val
-
 
 section {* The string behind a value *}
 
@@ -215,9 +213,8 @@
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-apply(induct v r rule: Prf.induct)
-apply(auto simp add: Sequ_def)
-done
+by(induct v r rule: Prf.induct)
+  (auto simp add: Sequ_def)
 
 lemma Prf_Stars:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
@@ -457,8 +454,7 @@
 qed
 
 
-(* a proof that does not need proj *)
-lemma Posix2_roy_version:
+lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v"
   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
@@ -636,7 +632,7 @@
 apply(drule_tac x="der a r" in meta_spec)
 apply(simp add: der_correctness Der_def)
 apply(rule iffI)
-apply(auto intro: Posix2_roy_version simp add: Posix1(1))
+apply(auto intro: Posix_injval simp add: Posix1(1))
 done 
 
 

Binary file thys/paper.pdf has changed