--- a/Co2sobj_prop.thy	Thu May 30 09:15:19 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 30 15:28:57 2013 +0800
@@ -859,10 +859,6 @@
 apply (case_tac a, auto split:if_splits option.splits)
 done
 
-definition
-  "fff x z = {xx. \<exists> y. xx = (x,y) \<and> (x, y) \<in> z}"
-thm fff_def
-
 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)
@@ -870,26 +866,61 @@
 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)
+apply (simp)
+apply( 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 cph2spshs_createshm:
+
+lemma cph2spshs_attach:
   "valid (Attach p h flag # s) \<Longrightarrow> 
    cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := 
      (case (ch2sshm s h) of 
         Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}
       | _       \<Rightarrow> cph2spshs s p) )"
 apply (frule vd_cons, frule vt_grant_os, rule ext)
-unfolding cph2spshs_def
 using ch2sshm_other[where e = "Attach p h flag" and s = s]
 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh'
-)
-thm current_shm_has_sshm
-apply (rule set_eqI, rule iffI)
-apply (case_tac xa, simp split:if_splits)
-apply (case_tac xa, erule CollectE)
-apply (simp, (erule conjE|erule bexE)+)
-apply (
-apply auto
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp)
+apply (rule_tac x = ha in exI, simp)
+apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp)
+apply (rule_tac x = ha in exI, simp)
+apply (frule procs_of_shm_prop1, simp, simp)
+apply (rule impI, simp)
+done
+
+lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow> 
+  cph2spshs (Detach p h # s) = (cph2spshs s) (p := 
+    (case (ch2sshm s h) of 
+       Some sh \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> p \<in> procs_of_shm s h' \<and> ch2sshm s p h' = Some sh)
+                  then cph2spshs s p else cph2spshs s p - {(sh, flag) | flag. (sh, flag) \<in> cph2spshs s p}
+     | _       \<Rightarrow> cph2spshs s p)             )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+using ch2sshm_other[where e = "Detach p h" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def)
+apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
+apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp)
+apply (rule_tac x = ha in exI, simp)
+apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp)
+apply (rule_tac x = ha in exI, simp)
+apply (frule procs_of_shm_prop1, simp, simp)
+apply (rule impI, simp)
+done
 
 lemma cph2spshs_other:
   "\<lbrakk>valid (e # s); "