--- a/Co2sobj_prop.thy	Thu May 30 15:28:57 2013 +0800
+++ b/Co2sobj_prop.thy	Mon Jun 03 10:34:58 2013 +0800
@@ -868,13 +868,22 @@
 
 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 (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)
+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> 
@@ -901,27 +910,58 @@
 
 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}
+    (case (ch2sshm s h, flag_of_proc_shm s p h) of 
+       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+                  then cph2spshs s p else cph2spshs s p - {(sh, flag)}
      | _       \<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 (case_tac "x = p")  defer
+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)
+dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
+apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
 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)
+
+apply (clarsimp)
+apply (frule current_shm_has_sh, simp, erule exE)
+apply (frule procs_of_shm_prop4, simp, simp)
+apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
+
+apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
+apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
+apply (case_tac "ha = h", simp)
+apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
+
+apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
+apply (case_tac "ha = h", simp)
+apply (rule_tac x = h' in exI, simp)
+apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+)
+apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
+apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
+
+apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
+apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
+apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
+apply (simp split:if_splits)
+apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (rule notI, simp split:if_splits)
+apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
+apply (simp split:if_splits)
+apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
+apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
 done
 
+
+
 lemma cph2spshs_other:
   "\<lbrakk>valid (e # s); "
 
@@ -947,23 +987,6 @@
 
 lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other
 
-(******************** ch2sshm simpset **************************)
-
-lemma ch2sshm_nil: "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = SInit h"
-by (simp add:ch2sshm_def index_of_shm.simps)
-
-lemma ch2sshm_nil': "h \<in> current_shms [] \<Longrightarrow> ch2sshm [] h = SInit h"
-by (simp add:ch2sshm_nil current_shms.simps)
-
-lemma ch2sshm_createshm: "ch2sshm (CreateShM p h # \<tau>) h' = (if (h' = h) then SCrea (Suc (length \<tau>)) else ch2sshm \<tau> h')"
-by (simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps) 
-
-lemma ch2sshm_other: "\<forall> p h. e \<noteq> CreateShM p h \<Longrightarrow> ch2sshm (e # \<tau>) h' = ch2sshm \<tau> h'"
-apply (case_tac e)
-by (auto simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps) 
-
-lemmas ch2sshm_simps = ch2sshm_nil ch2sshm_nil' ch2sshm_createshm ch2sshm_other
-
 (********************* cm2smsg simpset ***********************)
 
 lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"
@@ -981,120 +1004,7 @@
 
 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
 
-(********************** cfd2fd_s simpset ******************************)
 
-lemma cfd2fd_s_nil: "fd \<in> init_fds_of_proc p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"
-by (simp add:cfd2fd_s_def index_of_fd.simps)
-
-lemma cfd2fd_s_nil': "fd \<in> current_proc_fds [] p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"
-by (simp add:cfd2fd_s_nil current_proc_fds.simps)
-
-lemma cfd2fd_s_open: "cfd2fd_s (Open p f flags fd opt # \<tau>) p' fd' = (
-                        if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) 
-                                          else cfd2fd_s \<tau> p' fd')
-                        else cfd2fd_s \<tau> p' fd'                      )"
-by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
-
-lemma cfd2fd_s_createsock: "cfd2fd_s (CreateSock p af st fd im # \<tau>) p' fd' = (
-                              if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) 
-                                          else cfd2fd_s \<tau> p' fd')
-                              else cfd2fd_s \<tau> p' fd'                         )"
-by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
-
-lemma cfd2fd_s_accept: "cfd2fd_s (Accept p fd addr port fd' im # \<tau>) p' fd'' = (
-                          if (p' = p) then (if (fd'' = fd') then SCrea (Suc (length \<tau>))
-                                            else cfd2fd_s \<tau> p' fd'')
-                          else cfd2fd_s \<tau> p' fd''                             )"
-by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
-
-lemma cfd2fd_s_clone: "cfd2fd_s (Clone p p' # \<tau>) p'' fd = (if (p'' = p') then cfd2fd_s \<tau> p fd else cfd2fd_s \<tau> p'' fd)"
-by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
-
-lemma cfd2fd_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
-                        \<forall> p af st fd im. e \<noteq> CreateSock p af st fd im;
-                        \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im;
-                        \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> cfd2fd_s (e # \<tau>) p'' fd'' = cfd2fd_s \<tau> p'' fd''"
-by (case_tac e, auto simp:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
-
-lemmas cfd2fd_s_simps = cfd2fd_s_nil cfd2fd_s_nil' cfd2fd_s_open cfd2fd_s_createsock cfd2fd_s_accept cfd2fd_s_clone cfd2fd_s_other
-
-(************* cim2im_s simpset **************************)
-
-(* no such lemma
-lemma cim2im_s_nil: "init_itag_of_inum im = Some tag \<Longrightarrow> cim2im_s [] im = SInit im"
-by (simp add:cim2im_s_def)
-*)
-
-lemma cim2im_s_open: "cim2im_s (Open p f flags fd (Some im) # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
-by (simp add:cim2im_s_def)
-
-lemma cim2im_s_open': "cim2im_s (Open p f flags fd None # \<tau>) im = cim2im_s \<tau> im"
-by (simp add:cim2im_s_def)
-
-lemma cim2im_s_mkdir: "cim2im_s (Mkdir p f im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
-by (simp add:cim2im_s_def)
-
-lemma cim2im_s_createsock: "cim2im_s (CreateSock p sf st fd im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
-by (simp add:cim2im_s_def)
-
-lemma cim2im_s_accept: "cim2im_s (Accept p fd addr port fd' im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
-by (simp add:cim2im_s_def)
-
-lemma cim2im_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
-                        \<forall> p f im. e \<noteq> Mkdir p f im;
-                        \<forall> p sf st fd im. e \<noteq> CreateSock p sf st fd im;
-                        \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im\<rbrakk> \<Longrightarrow> cim2im_s (e # \<tau>) im = cim2im_s \<tau> im"
-by (case_tac e, auto simp:cim2im_s_def)
-
-lemmas cim2im_s_simps = cim2im_s_open cim2im_s_open' cim2im_s_mkdir cim2im_s_createsock cim2im_s_accept cim2im_s_other
-
-
-lemma cig2ig_s_simp: "cig2ig_s (e # \<tau>) tag = cig2ig_s \<tau> tag"
-apply (case_tac tag)
-by auto
-
-(******************* cobj2sobj no Suc (length \<tau>) ***********************)
-
-lemma cf2sfile_le_len: "\<lbrakk>cf2sfile \<tau> f = SCrea (Suc (length \<tau>)) # spf; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"
-apply (case_tac f, (simp add:cf2sfile.simps d2s_aux.simps)+)
-apply (case_tac "index_of_file \<tau> (a # list)", (simp add:d2s_aux.simps)+)
-by (drule index_of_file_le_length', simp+)
-
-lemma cf2sfile_le_len': "\<lbrakk>SCrea (Suc (length \<tau>)) # spf \<preceq> cf2sfile \<tau> f; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"
-apply (induct f)
-apply (simp add:no_junior_def cf2sfile.simps d2s_aux.simps)
-apply (case_tac "cf2sfile \<tau> (a # f) = SCrea (Suc (length \<tau>)) # spf") 
-apply (drule_tac f = "a # f" in cf2sfile_le_len, simp+)
-apply (simp only:cf2sfile.simps d2s_aux.simps)
-apply (drule_tac no_junior_noteq, simp+)
-apply (rule impI, erule impE, simp+)
-apply (drule parentf_in_current', simp+)
-done
-
-lemma cp2sproc_le_len: "cp2sproc \<tau> p = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
-apply (simp add:cp2sproc_def, case_tac "index_of_proc \<tau> p")
-apply (simp add:d2s_aux.simps)+
-by (drule index_of_proc_le_length', simp)
-
-lemma ch2sshm_le_len: "ch2sshm \<tau> h = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
-apply (simp add:ch2sshm_def, case_tac "index_of_shm \<tau> h")
-apply (simp add:d2s_aux.simps)+
-by (drule index_of_shm_le_length', simp)
-
-lemma cm2smsg_le_len: "cm2smsg \<tau> m = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
-apply (simp add:cm2smsg_def, case_tac "index_of_msg \<tau> m")
-apply (simp add:d2s_aux.simps)+
-by (drule index_of_msg_le_length', simp)
-
-lemma cim2im_s_le_len: "cim2im_s \<tau> im = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
-apply (simp add:cim2im_s_def, case_tac "inum2ind \<tau> im")
-apply (simp add:d2s_aux.simps)+
-by (drule inum2ind_le_length', simp)
-
-lemma cfd2fd_s_le_len: "cfd2fd_s \<tau> p fd = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
-apply (simp add:cfd2fd_s_def, case_tac "index_of_fd \<tau> p fd")
-apply (simp add:d2s_aux.simps)+
-by (drule index_of_fd_le_length', simp)
 
 end