--- 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); "

--- a/Flask.thy	Thu May 30 09:15:19 2013 +0800
+++ b/Flask.thy	Thu May 30 15:28:57 2013 +0800
@@ -157,6 +157,7 @@
   and init_fileflag_valid:     "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"
 
   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"
+  and init_procshm_valid:      "\<And> p h flag flag'. \<lbrakk>(p,flag) \<in> init_procs_of_shm h; (p, flag') \<in> init_procs_of_shm h\<rbrakk> \<Longrightarrow> flag = flag'"
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
 
@@ -426,7 +427,7 @@
 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"
 | "current_shms (e # \<tau>) = current_shms \<tau> "
 
-fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
+fun procs_of_shm : "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
 where
   "procs_of_shm [] = init_procs_of_shm"
 | "procs_of_shm (CreateShM p h # \<tau>) =