--- a/Co2sobj_prop.thy	Tue Jun 04 15:37:49 2013 +0800
+++ b/Co2sobj_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -852,39 +852,6 @@
 
 (********** cph2spshs simpset **********)
 
-  (*???*) lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
-apply (induct s arbitrary:p_flag)
-apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
-apply (induct s arbitrary:p flag)
-apply (simp, drule init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-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>
-  \<Longrightarrow> flag = flag'"
-apply (induct s arbitrary:p flag flag')
-apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
-done
-
-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"
-apply (induct s arbitrary:p flag)
-apply (simp, drule init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
-done
-
-lemma procs_of_shm_prop4':
-  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
-by (auto dest:procs_of_shm_prop4)
-
 lemma cph2spshs_attach:
   "valid (Attach p h flag # s) \<Longrightarrow> 
    cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := 
@@ -1102,14 +1069,6 @@
 
 (******** cp2sproc simpset *********)
 
-lemma not_init_intro_proc: (*???*)
-  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
-using not_deleted_init_proc by auto
-
-lemma not_init_intro_proc': (*???*)
-  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
-using not_deleted_init_proc by auto
-
 lemma cp2sproc_clone:
   "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := 
      case (sectxt_of_obj s (O_proc p)) of