737 shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)" |
737 shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)" |
738 using assms |
738 using assms |
739 by (metis Posix_PosOrd less_irrefl PosOrd_def |
739 by (metis Posix_PosOrd less_irrefl PosOrd_def |
740 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
740 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
741 |
741 |
742 |
|
743 |
|
744 lemma PosOrd_Posix_Stars: |
|
745 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
|
746 and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
747 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
748 using assms |
|
749 proof(induct vs) |
|
750 case Nil |
|
751 show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []" |
|
752 by(simp add: Posix.intros) |
|
753 next |
|
754 case (Cons v vs) |
|
755 have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; |
|
756 \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk> |
|
757 \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact |
|
758 have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact |
|
759 have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact |
|
760 have "flat v \<in> r \<rightarrow> v" "flat v \<noteq> []" using as2 by auto |
|
761 moreover |
|
762 have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
763 proof (rule IH) |
|
764 show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp |
|
765 next |
|
766 show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3 |
|
767 apply(auto) |
|
768 apply(subst (asm) (2) LV_def) |
|
769 apply(auto) |
|
770 apply(erule Prf.cases) |
|
771 apply(simp_all) |
|
772 apply(drule_tac x="Stars (v # vs)" in bspec) |
|
773 apply(simp add: LV_def) |
|
774 using Posix_LV Prf.intros(6) calculation |
|
775 apply(rule_tac Prf.intros) |
|
776 apply(simp add:) |
|
777 prefer 2 |
|
778 apply (simp add: PosOrd_StarsI2) |
|
779 apply(drule Posix_LV) |
|
780 apply(simp add: LV_def) |
|
781 done |
|
782 qed |
|
783 moreover |
|
784 have "flat v \<noteq> []" using as2 by simp |
|
785 moreover |
|
786 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
|
787 using as3 |
|
788 apply(auto) |
|
789 apply(drule L_flat_Prf2) |
|
790 apply(erule exE) |
|
791 apply(simp only: L.simps[symmetric]) |
|
792 apply(drule L_flat_Prf2) |
|
793 apply(erule exE) |
|
794 apply(clarify) |
|
795 apply(rotate_tac 5) |
|
796 apply(erule Prf.cases) |
|
797 apply(simp_all) |
|
798 apply(clarify) |
|
799 apply(drule_tac x="Stars (va#vs)" in bspec) |
|
800 apply(auto simp add: LV_def)[1] |
|
801 apply(rule Prf.intros) |
|
802 apply(simp) |
|
803 by (simp add: PosOrd_StarsI PosOrd_shorterI) |
|
804 ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
805 by (simp add: Posix.intros) |
|
806 qed |
|
807 |
|
808 |
|
809 |
|
810 section {* The Smallest Value is indeed the Posix Value *} |
|
811 |
|
812 lemma PosOrd_Posix: |
742 lemma PosOrd_Posix: |
813 assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
743 assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
814 shows "s \<in> r \<rightarrow> v1" |
744 shows "s \<in> r \<rightarrow> v1" |
815 using assms |
745 proof - |
816 proof(induct r arbitrary: s v1) |
746 have "s \<in> L r" using assms(1) unfolding LV_def |
817 case (ZERO s v1) |
747 using L_flat_Prf1 by blast |
818 have "v1 \<in> LV ZERO s" by fact |
748 then obtain vposix where vp: "s \<in> r \<rightarrow> vposix" |
819 then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def |
749 using lexer_correct_Some by blast |
820 by (auto elim: Prf.cases) |
750 with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd) |
821 next |
751 then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto |
822 case (ONE s v1) |
|
823 have "v1 \<in> LV ONE s" by fact |
|
824 then have "v1 = Void" "s = []" unfolding LV_def |
|
825 by(auto elim: Prf.cases) |
|
826 then show "s \<in> ONE \<rightarrow> v1" |
|
827 by(auto intro: Posix.intros) |
|
828 next |
|
829 case (CHAR c s v1) |
|
830 have "v1 \<in> LV (CHAR c) s" by fact |
|
831 then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def |
|
832 by (auto elim!: Prf.cases intro: Posix.intros) |
|
833 next |
|
834 case (ALT r1 r2 s v1) |
|
835 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
|
836 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
|
837 have as1: "\<forall>v2 \<in> LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
|
838 have as2: "v1 \<in> LV (ALT r1 r2) s" by fact |
|
839 then consider |
|
840 (Left) v1' where |
|
841 "v1 = Left v1'" "s = flat v1'" |
|
842 "v1' \<in> LV r1 s" |
|
843 | (Right) v1' where |
|
844 "v1 = Right v1'" "s = flat v1'" |
|
845 "v1' \<in> LV r2 s" |
|
846 unfolding LV_def by (auto elim: Prf.cases) |
|
847 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
|
848 proof (cases) |
|
849 case (Left v1') |
|
850 have "v1' \<in> LV r1 s" using Left(3) . |
|
851 moreover |
|
852 have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
|
853 unfolding Left(1,2) unfolding LV_def |
|
854 using Prf.intros(2) PosOrd_Left_eq by force |
|
855 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
|
856 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
|
857 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
|
858 next |
|
859 case (Right v1') |
|
860 have "v1' \<in> LV r2 s" using Right(3) . |
|
861 moreover |
|
862 have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
|
863 unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
|
864 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
|
865 moreover |
|
866 { assume "s \<in> L r1" |
|
867 then obtain v' where "v' \<in> LV r1 s" |
|
868 unfolding LV_def using L_flat_Prf2 by blast |
|
869 then have "Left v' \<in> LV (ALT r1 r2) s" |
|
870 unfolding LV_def by (auto intro: Prf.intros) |
|
871 with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" |
|
872 unfolding LV_def Right |
|
873 by (auto) |
|
874 then have False using PosOrd_Left_Right Right by blast |
|
875 } |
|
876 then have "s \<notin> L r1" by rule |
|
877 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros) |
|
878 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp |
|
879 qed |
|
880 next |
|
881 case (SEQ r1 r2 s v1) |
|
882 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
|
883 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
|
884 have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
|
885 have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact |
|
886 then obtain |
|
887 v1a v1b where eqs: |
|
888 "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b" |
|
889 "v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" |
|
890 unfolding LV_def by(auto elim: Prf.cases) |
|
891 have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a" |
|
892 proof |
|
893 fix v2 |
|
894 assume "v2 \<in> LV r1 (flat v1a)" |
|
895 with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s" |
|
896 by (simp add: LV_def Prf.intros(1)) |
|
897 with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" |
|
898 using eqs by (simp add: LV_def) |
|
899 then show "\<not> v2 :\<sqsubset>val v1a" |
|
900 using PosOrd_SeqI1 by blast |
|
901 qed |
|
902 then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp |
|
903 moreover |
752 moreover |
904 have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b" |
753 { assume "vposix :\<sqsubset>val v1" |
905 proof |
754 moreover |
906 fix v2 |
755 have "vposix \<in> LV r s" using vp |
907 assume "v2 \<in> LV r2 (flat v1b)" |
756 using Posix_LV by blast |
908 with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s" |
757 ultimately have "False" using assms(2) by blast |
909 by (simp add: LV_def Prf.intros) |
758 } |
910 with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" |
759 ultimately show "s \<in> r \<rightarrow> v1" using vp by blast |
911 using eqs by (simp add: LV_def) |
|
912 then show "\<not> v2 :\<sqsubset>val v1b" |
|
913 using PosOrd_SeqI2 by auto |
|
914 qed |
|
915 then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp |
|
916 moreover |
|
917 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
|
918 proof |
|
919 assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" |
|
920 then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast |
|
921 then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2" |
|
922 using L_flat_Prf2 by blast |
|
923 then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1 |
|
924 by (auto simp add: LV_def intro!: Prf.intros) |
|
925 with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto |
|
926 then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto |
|
927 then show "False" |
|
928 using PosOrd_shorterI by blast |
|
929 qed |
|
930 ultimately |
|
931 show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs |
|
932 by (rule Posix.intros) |
|
933 next |
|
934 case (STAR r s v1) |
|
935 have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact |
|
936 have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact |
|
937 have as2: "v1 \<in> LV (STAR r) s" by fact |
|
938 then obtain |
|
939 vs where eqs: |
|
940 "v1 = Stars vs" "s = flat (Stars vs)" |
|
941 "\<forall>v \<in> set vs. v \<in> LV r (flat v)" |
|
942 unfolding LV_def by (auto elim: Prf.cases) |
|
943 have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
|
944 proof |
|
945 fix v |
|
946 assume a: "v \<in> set vs" |
|
947 then obtain pre post where e: "vs = pre @ [v] @ post" |
|
948 by (metis append_Cons append_Nil in_set_conv_decomp_first) |
|
949 then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" |
|
950 using as1 unfolding eqs by simp |
|
951 have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs |
|
952 proof (rule ballI, rule notI) |
|
953 fix v2 |
|
954 assume w: "v2 :\<sqsubset>val v" |
|
955 assume "v2 \<in> LV r (flat v)" |
|
956 then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" |
|
957 using as2 unfolding e eqs |
|
958 apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE) |
|
959 apply(auto dest!: Prf_Stars_appendE elim: Prf.cases) |
|
960 done |
|
961 then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)" |
|
962 using q by simp |
|
963 with w show "False" |
|
964 using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq |
|
965 PosOrd_StarsI PosOrd_Stars_appendI by auto |
|
966 qed |
|
967 with IH |
|
968 show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def |
|
969 by (auto elim: Prf.cases) |
|
970 qed |
|
971 moreover |
|
972 have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" |
|
973 proof |
|
974 assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs" |
|
975 then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)" |
|
976 "Stars vs2 :\<sqsubset>val Stars vs" |
|
977 unfolding LV_def by (force elim: Prf_elims intro: Prf.intros) |
|
978 then show "False" using as1 unfolding eqs |
|
979 by (auto simp add: LV_def) |
|
980 qed |
|
981 ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
982 thm PosOrd_Posix_Stars |
|
983 by (rule PosOrd_Posix_Stars) |
|
984 then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs . |
|
985 qed |
760 qed |
986 |
761 |
987 lemma Least_existence: |
762 lemma Least_existence: |
988 assumes "LV r s \<noteq> {}" |
763 assumes "LV r s \<noteq> {}" |
989 shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
764 shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |