equal
deleted
inserted
replaced
757 using lex_correct1a |
757 using lex_correct1a |
758 apply fastforce |
758 apply fastforce |
759 apply(simp add: der_correctness Der_def) |
759 apply(simp add: der_correctness Der_def) |
760 by (simp add: lex_correct1a) |
760 by (simp add: lex_correct1a) |
761 |
761 |
|
762 lemma lex_correct3b: |
|
763 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
764 using assms |
|
765 apply(induct s arbitrary: r) |
|
766 apply(simp) |
|
767 apply (metis PMatch_mkeps nullable_correctness) |
|
768 apply(drule_tac x="der a r" in meta_spec) |
|
769 apply(simp add: der_correctness Der_def) |
|
770 apply(case_tac "matcher (der a r) s = None") |
|
771 apply(simp) |
|
772 apply(simp) |
|
773 apply(clarify) |
|
774 apply(rule iffI) |
|
775 apply(auto) |
|
776 apply(rule PMatch2_roy_version) |
|
777 apply(simp) |
|
778 using PMatch1(1) by auto |
|
779 |
762 lemma lex_correct5: |
780 lemma lex_correct5: |
763 assumes "s \<in> L r" |
781 assumes "s \<in> L r" |
764 shows "s \<in> r \<rightarrow> (matcher2 r s)" |
782 shows "s \<in> r \<rightarrow> (matcher2 r s)" |
765 using assms |
783 using assms |
766 apply(induct s arbitrary: r) |
784 apply(induct s arbitrary: r) |