563 apply(simp) |
543 apply(simp) |
564 apply(auto) |
544 apply(auto) |
565 apply(case_tac "length (flat v1') < length (flat v1)") |
545 apply(case_tac "length (flat v1') < length (flat v1)") |
566 using PosOrd_shorterI apply blast |
546 using PosOrd_shorterI apply blast |
567 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2)) |
547 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2)) |
568 |
|
569 |
|
570 section {* CPT and CPTpre *} |
|
571 |
|
572 |
|
573 inductive |
|
574 CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
|
575 where |
|
576 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
577 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
578 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
579 | "\<Turnstile> Void : ONE" |
|
580 | "\<Turnstile> Char c : CHAR c" |
|
581 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
|
582 |
|
583 lemma Prf_CPrf: |
|
584 assumes "\<Turnstile> v : r" |
|
585 shows "\<turnstile> v : r" |
|
586 using assms |
|
587 by (induct)(auto intro: Prf.intros) |
|
588 |
|
589 lemma CPrf_stars: |
|
590 assumes "\<Turnstile> Stars vs : STAR r" |
|
591 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
592 using assms |
|
593 apply(erule_tac CPrf.cases) |
|
594 apply(simp_all) |
|
595 done |
|
596 |
|
597 lemma CPrf_Stars_appendE: |
|
598 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
599 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
600 using assms |
|
601 apply(erule_tac CPrf.cases) |
|
602 apply(auto intro: CPrf.intros elim: Prf.cases) |
|
603 done |
|
604 |
|
605 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
606 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
607 |
|
608 definition |
|
609 "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}" |
|
610 |
|
611 definition |
|
612 "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}" |
|
613 |
|
614 lemma CPT_CPTpre_subset: |
|
615 shows "CPT r s \<subseteq> CPTpre r s" |
|
616 by(auto simp add: CPT_def CPTpre_def) |
|
617 |
|
618 lemma CPT_simps: |
|
619 shows "CPT ZERO s = {}" |
|
620 and "CPT ONE s = (if s = [] then {Void} else {})" |
|
621 and "CPT (CHAR c) s = (if s = [c] then {Char c} else {})" |
|
622 and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
623 and "CPT (SEQ r1 r2) s = |
|
624 {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}" |
|
625 and "CPT (STAR r) s = |
|
626 Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}" |
|
627 apply - |
|
628 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
629 apply(erule CPrf.cases) |
|
630 apply(simp_all)[6] |
|
631 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
632 apply(erule CPrf.cases) |
|
633 apply(simp_all)[6] |
|
634 apply(erule CPrf.cases) |
|
635 apply(simp_all)[6] |
|
636 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
637 apply(erule CPrf.cases) |
|
638 apply(simp_all)[6] |
|
639 apply(erule CPrf.cases) |
|
640 apply(simp_all)[6] |
|
641 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
642 apply(erule CPrf.cases) |
|
643 apply(simp_all)[6] |
|
644 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
645 apply(erule CPrf.cases) |
|
646 apply(simp_all)[6] |
|
647 (* STAR case *) |
|
648 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
649 apply(erule CPrf.cases) |
|
650 apply(simp_all)[6] |
|
651 done |
|
652 |
|
653 (* |
|
654 lemma CPTpre_STAR_finite: |
|
655 assumes "\<And>s. finite (CPT r s)" |
|
656 shows "finite (CPT (STAR r) s)" |
|
657 apply(induct s rule: length_induct) |
|
658 apply(case_tac xs) |
|
659 apply(simp) |
|
660 apply(simp add: CPT_simps) |
|
661 apply(auto) |
|
662 apply(rule finite_imageI) |
|
663 using assms |
|
664 thm finite_Un |
|
665 prefer 2 |
|
666 apply(simp add: CPT_simps) |
|
667 apply(rule finite_imageI) |
|
668 apply(rule finite_subset) |
|
669 apply(rule CPTpre_subsets) |
|
670 apply(simp) |
|
671 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) |
|
672 apply(auto)[1] |
|
673 apply(rule finite_imageI) |
|
674 apply(simp add: Collect_case_prod_Sigma) |
|
675 apply(rule finite_SigmaI) |
|
676 apply(rule assms) |
|
677 apply(case_tac "flat v = []") |
|
678 apply(simp) |
|
679 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
680 apply(simp) |
|
681 apply(auto)[1] |
|
682 apply(rule test) |
|
683 apply(simp) |
|
684 done |
|
685 |
|
686 lemma CPTpre_subsets: |
|
687 "CPTpre ZERO s = {}" |
|
688 "CPTpre ONE s \<subseteq> {Void}" |
|
689 "CPTpre (CHAR c) s \<subseteq> {Char c}" |
|
690 "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
691 "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
692 "CPTpre (STAR r) s \<subseteq> {Stars []} \<union> |
|
693 {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}" |
|
694 "CPTpre (STAR r) [] = {Stars []}" |
|
695 apply(auto simp add: CPTpre_def) |
|
696 apply(erule CPrf.cases) |
|
697 apply(simp_all) |
|
698 apply(erule CPrf.cases) |
|
699 apply(simp_all) |
|
700 apply(erule CPrf.cases) |
|
701 apply(simp_all) |
|
702 apply(erule CPrf.cases) |
|
703 apply(simp_all) |
|
704 apply(erule CPrf.cases) |
|
705 apply(simp_all) |
|
706 |
|
707 apply(erule CPrf.cases) |
|
708 apply(simp_all) |
|
709 apply(erule CPrf.cases) |
|
710 apply(simp_all) |
|
711 apply(rule CPrf.intros) |
|
712 done |
|
713 |
|
714 |
|
715 lemma CPTpre_simps: |
|
716 shows "CPTpre ONE s = {Void}" |
|
717 and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})" |
|
718 and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
719 and "CPTpre (SEQ r1 r2) s = |
|
720 {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
721 apply - |
|
722 apply(rule subset_antisym) |
|
723 apply(rule CPTpre_subsets) |
|
724 apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1] |
|
725 apply(case_tac "c = d") |
|
726 apply(simp) |
|
727 apply(rule subset_antisym) |
|
728 apply(rule CPTpre_subsets) |
|
729 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
730 apply(simp) |
|
731 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
732 apply(erule CPrf.cases) |
|
733 apply(simp_all) |
|
734 apply(rule subset_antisym) |
|
735 apply(rule CPTpre_subsets) |
|
736 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
737 apply(rule subset_antisym) |
|
738 apply(rule CPTpre_subsets) |
|
739 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
740 done |
|
741 |
|
742 lemma CPT_simps: |
|
743 shows "CPT ONE s = (if s = [] then {Void} else {})" |
|
744 and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})" |
|
745 and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
746 and "CPT (SEQ r1 r2) s = |
|
747 {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}" |
|
748 apply - |
|
749 apply(rule subset_antisym) |
|
750 apply(auto simp add: CPT_def)[1] |
|
751 apply(erule CPrf.cases) |
|
752 apply(simp_all)[7] |
|
753 apply(erule CPrf.cases) |
|
754 apply(simp_all)[7] |
|
755 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
756 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
757 apply(erule CPrf.cases) |
|
758 apply(simp_all)[7] |
|
759 apply(erule CPrf.cases) |
|
760 apply(simp_all)[7] |
|
761 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
762 apply(erule CPrf.cases) |
|
763 apply(simp_all)[7] |
|
764 apply(clarify) |
|
765 apply blast |
|
766 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
767 apply(erule CPrf.cases) |
|
768 apply(simp_all)[7] |
|
769 done |
|
770 |
|
771 lemma test: |
|
772 assumes "finite A" |
|
773 shows "finite {vs. Stars vs \<in> A}" |
|
774 using assms |
|
775 apply(induct A) |
|
776 apply(simp) |
|
777 apply(auto) |
|
778 apply(case_tac x) |
|
779 apply(simp_all) |
|
780 done |
|
781 |
|
782 lemma CPTpre_STAR_finite: |
|
783 assumes "\<And>s. finite (CPTpre r s)" |
|
784 shows "finite (CPTpre (STAR r) s)" |
|
785 apply(induct s rule: length_induct) |
|
786 apply(case_tac xs) |
|
787 apply(simp) |
|
788 apply(simp add: CPTpre_subsets) |
|
789 apply(rule finite_subset) |
|
790 apply(rule CPTpre_subsets) |
|
791 apply(simp) |
|
792 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) |
|
793 apply(auto)[1] |
|
794 apply(rule finite_imageI) |
|
795 apply(simp add: Collect_case_prod_Sigma) |
|
796 apply(rule finite_SigmaI) |
|
797 apply(rule assms) |
|
798 apply(case_tac "flat v = []") |
|
799 apply(simp) |
|
800 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
801 apply(simp) |
|
802 apply(auto)[1] |
|
803 apply(rule test) |
|
804 apply(simp) |
|
805 done |
|
806 |
|
807 lemma CPTpre_finite: |
|
808 shows "finite (CPTpre r s)" |
|
809 apply(induct r arbitrary: s) |
|
810 apply(simp add: CPTpre_subsets) |
|
811 apply(rule finite_subset) |
|
812 apply(rule CPTpre_subsets) |
|
813 apply(simp) |
|
814 apply(rule finite_subset) |
|
815 apply(rule CPTpre_subsets) |
|
816 apply(simp) |
|
817 apply(rule finite_subset) |
|
818 apply(rule CPTpre_subsets) |
|
819 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset) |
|
820 apply(auto)[1] |
|
821 apply(rule finite_imageI) |
|
822 apply(simp add: Collect_case_prod_Sigma) |
|
823 apply(rule finite_subset) |
|
824 apply(rule CPTpre_subsets) |
|
825 apply(simp) |
|
826 by (simp add: CPTpre_STAR_finite) |
|
827 |
|
828 |
|
829 lemma CPT_finite: |
|
830 shows "finite (CPT r s)" |
|
831 apply(rule finite_subset) |
|
832 apply(rule CPT_CPTpre_subset) |
|
833 apply(rule CPTpre_finite) |
|
834 done |
|
835 *) |
|
836 |
|
837 lemma Posix_CPT: |
|
838 assumes "s \<in> r \<rightarrow> v" |
|
839 shows "v \<in> CPT r s" |
|
840 using assms |
|
841 apply(induct rule: Posix.induct) |
|
842 apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases) |
|
843 apply(rotate_tac 5) |
|
844 apply(erule CPrf.cases) |
|
845 apply(simp_all) |
|
846 apply(rule CPrf.intros) |
|
847 apply(simp_all) |
|
848 done |
|
849 |
548 |
850 |
549 |
851 section {* The Posix Value is smaller than any other Value *} |
550 section {* The Posix Value is smaller than any other Value *} |
852 |
551 |
853 |
552 |
1042 shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)" |
741 shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)" |
1043 using assms |
742 using assms |
1044 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def |
743 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def |
1045 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
744 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
1046 |
745 |
1047 (* |
|
1048 lemma PosOrd_Posix_Stars: |
|
1049 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
|
1050 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
1051 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
1052 using assms |
|
1053 apply(induct vs) |
|
1054 apply(simp) |
|
1055 apply(rule Posix.intros) |
|
1056 apply(simp (no_asm)) |
|
1057 apply(rule Posix.intros) |
|
1058 apply(auto)[1] |
|
1059 apply(auto simp add: CPT_def PT_def)[1] |
|
1060 defer |
|
1061 apply(simp) |
|
1062 apply(drule meta_mp) |
|
1063 apply(auto simp add: CPT_def PT_def)[1] |
|
1064 apply(erule CPrf.cases) |
|
1065 apply(simp_all) |
|
1066 apply(drule meta_mp) |
|
1067 apply(auto simp add: CPT_def PT_def)[1] |
|
1068 apply(erule Prf.cases) |
|
1069 apply(simp_all) |
|
1070 using CPrf_stars PosOrd_irrefl apply fastforce |
|
1071 apply(clarify) |
|
1072 apply(drule_tac x="Stars (a#v#vsa)" in spec) |
|
1073 apply(simp) |
|
1074 apply(drule mp) |
|
1075 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
|
1076 apply(subst (asm) (2) PosOrd_ex_def) |
|
1077 apply(simp) |
|
1078 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) |
|
1079 apply(auto simp add: CPT_def PT_def)[1] |
|
1080 using CPrf_stars apply auto[1] |
|
1081 apply(auto)[1] |
|
1082 apply(auto simp add: CPT_def PT_def)[1] |
|
1083 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
|
1084 prefer 2 |
|
1085 apply (meson L_flat_Prf2) |
|
1086 apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)") |
|
1087 apply(clarify) |
|
1088 apply(drule_tac x="Stars (vA # vB)" in spec) |
|
1089 apply(simp) |
|
1090 apply(drule mp) |
|
1091 using Prf.intros(7) apply blast |
|
1092 apply(subst (asm) (2) PosOrd_ex_def) |
|
1093 apply(simp) |
|
1094 prefer 2 |
|
1095 apply(simp) |
|
1096 using Star_values_exists apply blast |
|
1097 prefer 2 |
|
1098 apply(drule meta_mp) |
|
1099 apply(erule CPrf.cases) |
|
1100 apply(simp_all) |
|
1101 apply(drule meta_mp) |
|
1102 apply(auto)[1] |
|
1103 prefer 2 |
|
1104 apply(simp) |
|
1105 apply(erule CPrf.cases) |
|
1106 apply(simp_all) |
|
1107 apply(clarify) |
|
1108 apply(rotate_tac 3) |
|
1109 apply(erule Prf.cases) |
|
1110 apply(simp_all) |
|
1111 apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def PosOrd_ex_def) |
|
1112 apply(drule_tac x="Stars (v#va#vsb)" in spec) |
|
1113 apply(drule mp) |
|
1114 apply (simp add: Posix1a Prf.intros(7)) |
|
1115 apply(simp) |
|
1116 apply(subst (asm) (2) PosOrd_ex_def) |
|
1117 apply(simp) |
|
1118 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) |
|
1119 by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def) |
|
1120 *) |
|
1121 |
|
1122 |
746 |
1123 lemma test2: |
747 lemma test2: |
1124 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
748 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
1125 shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" |
749 shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" |
1126 using assms |
750 using assms |