849 lemma current_shm_has_sh': |
849 lemma current_shm_has_sh': |
850 "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" |
850 "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" |
851 by (auto dest:current_shm_has_sh) |
851 by (auto dest:current_shm_has_sh) |
852 |
852 |
853 (********** cph2spshs simpset **********) |
853 (********** cph2spshs simpset **********) |
854 |
|
855 (*???*) lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
|
856 apply (induct s arbitrary:p_flag) |
|
857 apply (case_tac p_flag, simp, drule init_procs_has_shm, simp) |
|
858 apply (frule vd_cons, frule vt_grant_os) |
|
859 apply (case_tac a, auto split:if_splits option.splits) |
|
860 done |
|
861 |
|
862 lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
863 apply (induct s arbitrary:p flag) |
|
864 apply (simp, drule init_procs_has_shm, simp) |
|
865 apply (frule vd_cons, frule vt_grant_os) |
|
866 apply (case_tac a, auto split:if_splits option.splits) |
|
867 done |
|
868 |
|
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> |
|
870 \<Longrightarrow> flag = flag'" |
|
871 apply (induct s arbitrary:p flag flag') |
|
872 apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp) |
|
873 apply (frule vd_cons, frule vt_grant_os) |
|
874 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) |
|
875 done |
|
876 |
|
877 lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag" |
|
878 apply (induct s arbitrary:p flag) |
|
879 apply (simp, drule init_procs_has_shm, simp) |
|
880 apply (frule vd_cons, frule vt_grant_os) |
|
881 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) |
|
882 done |
|
883 |
|
884 lemma procs_of_shm_prop4': |
|
885 "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h" |
|
886 by (auto dest:procs_of_shm_prop4) |
|
887 |
854 |
888 lemma cph2spshs_attach: |
855 lemma cph2spshs_attach: |
889 "valid (Attach p h flag # s) \<Longrightarrow> |
856 "valid (Attach p h flag # s) \<Longrightarrow> |
890 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
857 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
891 (case (ch2sshm s h) of |
858 (case (ch2sshm s h) of |
1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve |
1067 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve |
1101 cph2spshs_exit cph2spshs_kill cph2spshs_other |
1068 cph2spshs_exit cph2spshs_kill cph2spshs_other |
1102 |
1069 |
1103 (******** cp2sproc simpset *********) |
1070 (******** cp2sproc simpset *********) |
1104 |
1071 |
1105 lemma not_init_intro_proc: (*???*) |
|
1106 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs" |
|
1107 using not_deleted_init_proc by auto |
|
1108 |
|
1109 lemma not_init_intro_proc': (*???*) |
|
1110 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
|
1111 using not_deleted_init_proc by auto |
|
1112 |
|
1113 lemma cp2sproc_clone: |
1072 lemma cp2sproc_clone: |
1114 "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := |
1073 "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := |
1115 case (sectxt_of_obj s (O_proc p)) of |
1074 case (sectxt_of_obj s (O_proc p)) of |
1116 Some sec \<Rightarrow> Some (Created, sec, |
1075 Some sec \<Rightarrow> Some (Created, sec, |
1117 {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, |
1076 {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, |