--- 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
 

--- a/Flask.thy	Thu May 30 15:28:57 2013 +0800
+++ b/Flask.thy	Mon Jun 03 10:34:58 2013 +0800
@@ -139,6 +139,7 @@
   and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
   and init_shms :: "t_shm set"
   and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" 
+  and init_flag_of_proc_shm :: "t_process \<Rightarrow> t_shm \<rightharpoonup> t_shm_attach_flag"
 
   assumes
       parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"
@@ -156,8 +157,8 @@
   and init_filefd_valid:       "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"
   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_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_flag_of_proc_shm p h = Some flag"
+  and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
   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"
 
@@ -427,7 +428,30 @@
 | "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 flag_of_proc_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag option"
+where
+  "flag_of_proc_shm [] = init_flag_of_proc_shm"
+| "flag_of_proc_shm (Attach p h flag # s) = (\<lambda> p' h'. 
+     if (p' = p \<and> h' = h) then Some flag else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (Detach p h # s) = (\<lambda> p' h'. 
+     if (p' = p \<and> h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (CreateShM p h # s) = (\<lambda> p' h'. 
+     if (h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (DeleteShM p h # s) = (\<lambda> p' h'. 
+     if (h' = h) then None else flag_of_proc_shm s p' h')"
+| "flag_of_proc_shm (Clone p p' fds shms # s) = (\<lambda> p'' h.
+     if (p'' = p' \<and> h \<in> shms) then flag_of_proc_shm s p h
+     else if (p'' = p') then None
+     else flag_of_proc_shm s p'' h)"
+| "flag_of_proc_shm (Execve p f fds # s) = (\<lambda> p' h. 
+     if (p' = p) then None else flag_of_proc_shm s p' h)"
+| "flag_of_proc_shm (Kill p p' # s) = (\<lambda> p'' h. 
+     if (p'' = p') then None else flag_of_proc_shm s p'' h)"
+| "flag_of_proc_shm (Exit p # s) = (\<lambda> p' h. 
+     if (p' = p) then None else flag_of_proc_shm s p' h)"
+| "flag_of_proc_shm (e # s) = flag_of_proc_shm s"
+
+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>) = 

--- a/Static.thy	Thu May 30 15:28:57 2013 +0800
+++ b/Static.thy	Mon Jun 03 10:34:58 2013 +0800
@@ -58,7 +58,7 @@
 definition init_cph2spshs 
   :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
 where
-  "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> 
+  "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
                                              init_ch2sshm h = Some sh}"
 
 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
@@ -723,7 +723,7 @@
 
 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
 where
-  "cph2spshs s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
+  "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
 
 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
 where