938 unfolding PosOrd_ex_eq_def using cond2 |
938 unfolding PosOrd_ex_eq_def using cond2 |
939 by (simp add: PosOrd_shorterI) |
939 by (simp add: PosOrd_shorterI) |
940 qed |
940 qed |
941 next |
941 next |
942 case (Posix_NMTIMES2 vs r n m v2) |
942 case (Posix_NMTIMES2 vs r n m v2) |
943 then show "Stars vs :\<sqsubseteq>val v2" sorry |
943 then show "Stars vs :\<sqsubseteq>val v2" |
|
944 apply(auto simp add: LV_def) |
|
945 apply(erule Prf_elims) |
|
946 apply(simp) |
|
947 apply(rule PosOrd_eq_Stars_zipI) |
|
948 apply(auto) |
|
949 apply (meson in_set_zipE) |
|
950 by (metis Posix1(2) flats_empty) |
944 next |
951 next |
945 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
952 case (Posix_NMTIMES1 s1 r v s2 n m vs v3) |
946 then show "Stars (v # vs) :\<sqsubseteq>val v2" sorry |
953 have "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" by fact+ |
|
954 then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2)) |
|
955 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
956 have IH2: "\<And>v3. v3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
957 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact |
|
958 have cond2: "flat v \<noteq> []" by fact |
|
959 have "v3 \<in> LV (NMTIMES r n m) (s1 @ s2)" by fact |
|
960 then consider |
|
961 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
962 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NMTIMES r (n - 1) (m - 1)" |
|
963 "flats (v3a # vs3) = s1 @ s2" |
|
964 | (Empty) "v3 = Stars []" |
|
965 unfolding LV_def |
|
966 apply(auto) |
|
967 apply(erule Prf.cases) |
|
968 apply(auto) |
|
969 apply(case_tac n) |
|
970 apply(auto intro: Prf.intros) |
|
971 apply(case_tac vs1) |
|
972 apply(auto intro: Prf.intros) |
|
973 apply (simp add: as1(1) cond2 flats_empty) |
|
974 apply (simp add: Prf.intros(11)) |
|
975 apply(case_tac n) |
|
976 apply(simp) |
|
977 using Posix_NMTIMES1.hyps(6) apply blast |
|
978 apply(simp) |
|
979 apply(case_tac vs) |
|
980 apply(auto) |
|
981 by (simp add: Prf.intros(12)) |
|
982 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
983 proof (cases) |
|
984 case (NonEmpty v3a vs3) |
|
985 have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . |
|
986 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
987 unfolding prefix_list_def |
|
988 by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars) |
|
989 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
990 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
991 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
992 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
993 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2)" |
|
994 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
995 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
996 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
997 unfolding PosOrd_ex_eq_def by auto |
|
998 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
999 unfolding PosOrd_ex_eq_def |
|
1000 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
1001 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
1002 next |
|
1003 case Empty |
|
1004 have "v3 = Stars []" by fact |
|
1005 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
1006 unfolding PosOrd_ex_eq_def using cond2 |
|
1007 by (simp add: PosOrd_shorterI) |
|
1008 qed |
|
1009 next |
|
1010 case (Posix_NMTIMES3 s1 r v s2 m vs v3) |
|
1011 have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact+ |
|
1012 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
|
1013 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
1014 have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
1015 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" by fact |
|
1016 have cond2: "flat v \<noteq> []" by fact |
|
1017 have "v3 \<in> LV (NMTIMES r 0 m) (s1 @ s2)" by fact |
|
1018 then consider |
|
1019 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
1020 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (m - 1)" |
|
1021 "flats (v3a # vs3) = s1 @ s2" |
|
1022 | (Empty) "v3 = Stars []" |
|
1023 unfolding LV_def |
|
1024 apply(auto) |
|
1025 apply(erule Prf.cases) |
|
1026 apply(auto) |
|
1027 apply(case_tac vs) |
|
1028 apply(auto intro: Prf.intros) |
|
1029 by (simp add: Prf.intros(7) as1(1) cond2) |
|
1030 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
1031 proof (cases) |
|
1032 case (NonEmpty v3a vs3) |
|
1033 have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . |
|
1034 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
1035 unfolding prefix_list_def |
|
1036 apply(simp) |
|
1037 apply(simp add: append_eq_append_conv2) |
|
1038 apply(auto) |
|
1039 by (metis L_flat_Prf1 One_nat_def cond flat_Stars) |
|
1040 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
1041 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
1042 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
1043 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
1044 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (m - 1)) s2)" |
|
1045 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
1046 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
1047 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
1048 unfolding PosOrd_ex_eq_def by auto |
|
1049 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
1050 unfolding PosOrd_ex_eq_def |
|
1051 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
1052 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
1053 next |
|
1054 case Empty |
|
1055 have "v3 = Stars []" by fact |
|
1056 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
1057 unfolding PosOrd_ex_eq_def using cond2 |
|
1058 by (simp add: PosOrd_shorterI) |
|
1059 qed |
947 qed |
1060 qed |
948 |
1061 |
949 |
1062 |
950 lemma Posix_PosOrd_reverse: |
1063 lemma Posix_PosOrd_reverse: |
951 assumes "s \<in> r \<rightarrow> v1" |
1064 assumes "s \<in> r \<rightarrow> v1" |