857 apply (case_tac p_flag, simp, drule init_procs_has_shm, simp) |
857 apply (case_tac p_flag, simp, drule init_procs_has_shm, simp) |
858 apply (frule vd_cons, frule vt_grant_os) |
858 apply (frule vd_cons, frule vt_grant_os) |
859 apply (case_tac a, auto split:if_splits option.splits) |
859 apply (case_tac a, auto split:if_splits option.splits) |
860 done |
860 done |
861 |
861 |
862 definition |
|
863 "fff x z = {xx. \<exists> y. xx = (x,y) \<and> (x, y) \<in> z}" |
|
864 thm fff_def |
|
865 |
|
866 lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
862 lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
867 apply (induct s arbitrary:p flag) |
863 apply (induct s arbitrary:p flag) |
868 apply (simp, drule init_procs_has_shm, simp) |
864 apply (simp, drule init_procs_has_shm, simp) |
869 apply (frule vd_cons, frule vt_grant_os) |
865 apply (frule vd_cons, frule vt_grant_os) |
870 apply (case_tac a, auto split:if_splits option.splits) |
866 apply (case_tac a, auto split:if_splits option.splits) |
871 done |
867 done |
872 |
868 |
873 |
869 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk> |
874 lemma cph2spshs_createshm: |
870 \<Longrightarrow> flag = flag'" |
|
871 apply (induct s arbitrary:p) |
|
872 apply (simp) |
|
873 apply( drule init_procs_has_shm, simp) |
|
874 apply (frule vd_cons, frule vt_grant_os) |
|
875 apply (case_tac a, auto split:if_splits option.splits) |
|
876 done |
|
877 |
|
878 |
|
879 lemma cph2spshs_attach: |
875 "valid (Attach p h flag # s) \<Longrightarrow> |
880 "valid (Attach p h flag # s) \<Longrightarrow> |
876 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
881 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
877 (case (ch2sshm s h) of |
882 (case (ch2sshm s h) of |
878 Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)} |
883 Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)} |
879 | _ \<Rightarrow> cph2spshs s p) )" |
884 | _ \<Rightarrow> cph2spshs s p) )" |
880 apply (frule vd_cons, frule vt_grant_os, rule ext) |
885 apply (frule vd_cons, frule vt_grant_os, rule ext) |
881 unfolding cph2spshs_def |
|
882 using ch2sshm_other[where e = "Attach p h flag" and s = s] |
886 using ch2sshm_other[where e = "Attach p h flag" and s = s] |
883 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits |
887 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits |
884 dest!:current_shm_has_sh' |
888 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def) |
885 ) |
889 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
886 thm current_shm_has_sshm |
890 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
887 apply (rule set_eqI, rule iffI) |
891 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
888 apply (case_tac xa, simp split:if_splits) |
892 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
889 apply (case_tac xa, erule CollectE) |
893 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
890 apply (simp, (erule conjE|erule bexE)+) |
894 apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp) |
891 apply ( |
895 apply (rule_tac x = ha in exI, simp) |
892 apply auto |
896 apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp) |
|
897 apply (rule_tac x = ha in exI, simp) |
|
898 apply (frule procs_of_shm_prop1, simp, simp) |
|
899 apply (rule impI, simp) |
|
900 done |
|
901 |
|
902 lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow> |
|
903 cph2spshs (Detach p h # s) = (cph2spshs s) (p := |
|
904 (case (ch2sshm s h) of |
|
905 Some sh \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> p \<in> procs_of_shm s h' \<and> ch2sshm s p h' = Some sh) |
|
906 then cph2spshs s p else cph2spshs s p - {(sh, flag) | flag. (sh, flag) \<in> cph2spshs s p} |
|
907 | _ \<Rightarrow> cph2spshs s p) )" |
|
908 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
909 using ch2sshm_other[where e = "Detach p h" and s = s] |
|
910 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits |
|
911 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def) |
|
912 apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) |
|
913 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
914 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
915 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
916 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
917 apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp) |
|
918 apply (rule_tac x = ha in exI, simp) |
|
919 apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp) |
|
920 apply (rule_tac x = ha in exI, simp) |
|
921 apply (frule procs_of_shm_prop1, simp, simp) |
|
922 apply (rule impI, simp) |
|
923 done |
893 |
924 |
894 lemma cph2spshs_other: |
925 lemma cph2spshs_other: |
895 "\<lbrakk>valid (e # s); " |
926 "\<lbrakk>valid (e # s); " |
896 |
927 |
897 lemmas cph2spshs_simps = cph2spshs_other |
928 lemmas cph2spshs_simps = cph2spshs_other |