1    

     1    

     2 theory Lexer

     2 theory Lexer

     4 begin

     4 begin

     5 

     5 

     6 

     6 

     7 section {* Sequential Composition of Languages *}

     7 section {* Sequential Composition of Languages *}

     8 

     8 

   699   shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"

   699   shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"

   700   and   "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"

   700   and   "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"

   701 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce

   701 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce

   702 using Posix1(1) lexer_correct_None lexer_correct_Some by blast

   702 using Posix1(1) lexer_correct_None lexer_correct_Some by blast

   703 

   703 

   705 end

   704 end