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