# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1463736132 -3600
# Node ID 0b94800eb61643b693e1aad705353d8a24ff9104
# Parent  841f7b9c0a6a32a1a2509711d334a4cec5b0579a
added corollary

diff -r 841f7b9c0a6a -r 0b94800eb616 thys/Lexer.thy
--- a/thys/Lexer.thy	Wed May 18 15:57:46 2016 +0100
+++ b/thys/Lexer.thy	Fri May 20 10:22:12 2016 +0100
@@ -638,5 +638,11 @@
 apply(auto intro: Posix_injval simp add: Posix1(1))
 done 
 
+lemma lexer_correctness:
+  shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
+  and   "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
+using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
+using Posix1(1) lexer_correct_None lexer_correct_Some by blast
+
 
 end
\ No newline at end of file
diff -r 841f7b9c0a6a -r 0b94800eb616 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Wed May 18 15:57:46 2016 +0100
+++ b/thys/Paper/Paper.thy	Fri May 20 10:22:12 2016 +0100
@@ -1,7 +1,7 @@
 (*<*)
 theory Paper
 imports 
-   "../ReStar"
+   "../Lexer"
    "../Simplifying" 
    "../Sulzmann" 
    "~~/src/HOL/Library/LaTeXsugar"
@@ -68,13 +68,6 @@
 p9. The condtion "not exists s3 s4..." appears often enough (in particular in
 the proof of Lemma 3) to warrant a definition.
 
-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.
-
 *)
 
 (*>*)
@@ -653,15 +646,17 @@
    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}\label{posixdeterm}
-  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
+  \begin{theorem}\mbox{}\smallskip\\\label{posixdeterm}
+  \begin{tabular}{ll}
+  @{text "(1)"} & If @{thm (prem 1) Posix1(1)} then @{thm (concl)
+  Posix1(1)} and @{thm (concl) Posix1(2)}.\\
+  @{text "(2)"} & @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v" "v'"]}
+  \end{tabular}
   \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 
+  \begin{proof} Both by induction on the definition of @{term "s \<in> r \<rightarrow> v"}. 
+  The second parts follows by a case analysis of @{term "s \<in> r \<rightarrow> v'"} and
+  the first part.\qed
   \end{proof}
 
   \noindent
@@ -793,7 +788,18 @@
   \end{proof}
 
   \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the
-  value returned by the lexer must be unique.  This concludes our
+  value returned by the lexer must be unique.   A simple corollary 
+  of our two theorems yis:
+
+  \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
+  \begin{tabular}{ll}
+  (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 
+  (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\
+  \end{tabular}
+  \end{corollary}
+
+  \noindent
+  This concludes our
   correctness proof. Note that we have not changed the algorithm of
   Sulzmann and Lu,\footnote{All deviations we introduced are
   harmless.} but introduced our own specification for what a correct
@@ -1060,8 +1066,8 @@
   These properties of GREEDY, however, do not transfer to the POSIX
   ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
   To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
-  not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r
-  v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1
+  not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r
+  v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1
   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
   formulation, for example:
diff -r 841f7b9c0a6a -r 0b94800eb616 thys/paper.pdf
Binary file thys/paper.pdf has changed