equal
deleted
inserted
replaced
636 apply(simp add: der_correctness Der_def) |
636 apply(simp add: der_correctness Der_def) |
637 apply(rule iffI) |
637 apply(rule iffI) |
638 apply(auto intro: Posix_injval simp add: Posix1(1)) |
638 apply(auto intro: Posix_injval simp add: Posix1(1)) |
639 done |
639 done |
640 |
640 |
|
641 lemma lexer_correctness: |
|
642 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
|
643 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
|
644 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
|
645 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
|
646 |
641 |
647 |
642 end |
648 end |