diff -r 80fe81a28a52 -r 4e3778f4a802 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Mon May 09 12:53:12 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 09 15:00:28 2016 +0100
@@ -65,14 +65,9 @@
 (*
 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
 
@@ -80,9 +75,6 @@
 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.
-
 *)
 
 (*>*)
@@ -602,7 +594,7 @@
   \end{center}
 
   \noindent If the regular expression does not match the string, @{const None} is
-  returned, indicating an error is raised. If the regular expression \emph{does}
+  returned. If the regular expression \emph{does}
   match the string, then @{const Some} value is returned. One important
   virtue of this algorithm is that it can be implemented with ease in any
   functional programming language and also in Isabelle/HOL. In the remaining
@@ -644,7 +636,22 @@
   \end{tabular}
   \end{center}
 
-  \noindent We claim that this relation captures the idea behind the two
+   \noindent
+   We can prove that given a string @{term s} and regular expression @{term
+   r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.
+
+  \begin{theorem}
+  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
+  \end{theorem}
+
+  \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and
+  a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
+  auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
+  Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
+  established by inductions.\qed \end{proof}
+
+
+  We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two
   informal POSIX rules shown in the Introduction: Consider for example the
   rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string
   and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"},
@@ -677,21 +684,6 @@
   be ``chipped'' away; only in case of the empty string we accept @{term
   "Stars []"} as the POSIX value.
 
-   We can prove that given a string @{term s} and regular expression @{term
-   r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow>
-   v"}.
-
-  \begin{theorem}
-  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
-  \end{theorem}
-
-  \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and
-  a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
-  auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
-  Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
-  established by inductions.\qed \end{proof}
-
-  \noindent
   Next is the lemma that shows the function @{term "mkeps"} calculates
   the POSIX value for the empty string and a nullable regular expression.
 
@@ -994,11 +986,11 @@
   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
   formulation, for example:
 
-  \begin{proposition}
+  \begin{falsehood}
   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
-  \end{proposition}
+  \end{falsehood}
 
   \noindent If formulated in this way, then there are various counter
   examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}
@@ -1027,12 +1019,12 @@
   counter-example we were able to find (by hand and by machine). Thus the
   transitivity lemma should be formulated as:
 
-  \begin{proposition}
+  \begin{conject}
   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},
   and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\
   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
-  \end{proposition}
+  \end{conject}
 
   \noindent While we agree with Sulzmann and Lu that this property
   probably(!) holds, proving it seems not so straightforward: although one