618                   | Some(v) \<Rightarrow> Some(injval r c v))"

   618                   | Some(v) \<Rightarrow> Some(injval r c v))"

   619 

   619 

   620 

   620 

   621 lemma lexer_correct_None:

   621 lemma lexer_correct_None:

   622   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"

   622   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"

   624 apply(induct s arbitrary: r)

   623 apply(induct s arbitrary: r)

   625 apply(simp add: nullable_correctness)

   624 apply(simp add: nullable_correctness)

   626 apply(drule_tac x="der a r" in meta_spec)

   625 apply(drule_tac x="der a r" in meta_spec)

   627 apply(auto simp add: der_correctness Der_def)

   626 apply(auto simp add: der_correctness Der_def)

   628 done

   627 done

   629 

   628 

   630 lemma lexer_correct_Some:

   629 lemma lexer_correct_Some:

   631   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"

   630   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"

   633 apply(induct s arbitrary: r)

   631 apply(induct s arbitrary: r)

   634 apply(auto simp add: Posix_mkeps nullable_correctness)[1]

   632 apply(auto simp add: Posix_mkeps nullable_correctness)[1]

   635 apply(drule_tac x="der a r" in meta_spec)

   633 apply(drule_tac x="der a r" in meta_spec)

   636 apply(simp add: der_correctness Der_def)

   634 apply(simp add: der_correctness Der_def)

   637 apply(rule iffI)

   635 apply(rule iffI)