equal
deleted
inserted
replaced
720 apply(drule meta_mp) |
720 apply(drule meta_mp) |
721 apply(auto) |
721 apply(auto) |
722 apply(simp add: der_correctness Der_def) |
722 apply(simp add: der_correctness Der_def) |
723 done |
723 done |
724 |
724 |
|
725 lemma lex_correct1a: |
|
726 shows "s \<notin> L r \<longleftrightarrow> matcher r s = None" |
|
727 using assms |
|
728 apply(induct s arbitrary: r) |
|
729 apply(simp) |
|
730 apply (metis nullable_correctness) |
|
731 apply(auto) |
|
732 apply(drule_tac x="der a r" in meta_spec) |
|
733 apply(auto) |
|
734 apply(simp add: der_correctness Der_def) |
|
735 apply(drule_tac x="der a r" in meta_spec) |
|
736 apply(auto) |
|
737 apply(simp add: der_correctness Der_def) |
|
738 done |
725 |
739 |
726 lemma lex_correct2: |
740 lemma lex_correct2: |
727 assumes "s \<in> L r" |
741 assumes "s \<in> L r" |
728 shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
742 shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
729 using assms |
743 using assms |
748 apply(drule_tac x="der a r" in meta_spec) |
762 apply(drule_tac x="der a r" in meta_spec) |
749 apply(drule meta_mp) |
763 apply(drule meta_mp) |
750 apply(simp add: der_correctness Der_def) |
764 apply(simp add: der_correctness Der_def) |
751 apply(auto) |
765 apply(auto) |
752 by (metis PMatch2_roy_version) |
766 by (metis PMatch2_roy_version) |
|
767 |
|
768 lemma lex_correct3a: |
|
769 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
770 using assms |
|
771 apply(induct s arbitrary: r) |
|
772 apply(simp) |
|
773 apply (metis PMatch_mkeps nullable_correctness) |
|
774 apply(drule_tac x="der a r" in meta_spec) |
|
775 apply(auto) |
|
776 apply(metis PMatch2_roy_version) |
|
777 apply(simp add: der_correctness Der_def) |
|
778 using lex_correct1a |
|
779 apply fastforce |
|
780 apply(simp add: der_correctness Der_def) |
|
781 by (simp add: lex_correct1a) |
753 |
782 |
754 lemma lex_correct5: |
783 lemma lex_correct5: |
755 assumes "s \<in> L r" |
784 assumes "s \<in> L r" |
756 shows "s \<in> r \<rightarrow> (matcher2 r s)" |
785 shows "s \<in> r \<rightarrow> (matcher2 r s)" |
757 using assms |
786 using assms |