--- a/Co2sobj_prop.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 30 09:15:19 2013 +0800
@@ -616,15 +616,17 @@
 apply (rule set_eqI, rule iffI)
 apply (case_tac "x = a", simp)
 unfolding cpfd2sfds_def
-apply (erule CollectE, (erule conjE|erule exE)+)
-apply (simp split:if_splits)
-apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
-apply (case_tac "x = a", simp)
+apply (erule CollectE, (erule conjE|erule bexE)+)
+apply (simp add:proc_file_fds_def split:if_splits)
+apply (erule exE, rule_tac x = fda in exI)
+apply (simp add:cfd2sfd_open2)
+apply (case_tac "x = a", simp add:proc_file_fds_def)
 apply (rule_tac x = fd in exI, simp+)
-apply (erule conjE|erule exE)+
-apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
-apply (rule impI, drule proc_fd_in_fds, simp)
-apply (simp split:option.splits)
+apply (erule conjE|erule bexE)+
+apply (rule_tac x = fda in bexI)
+apply (simp add:proc_file_fds_def, erule exE)
+apply (simp add:cfd2sfd_open2)
+apply (simp add:proc_file_fds_def)
 done
 
 lemma cpfd2sfds_open1':
@@ -642,13 +644,12 @@
 apply (frule vt_grant_os, frule vd_cons)
 unfolding cpfd2sfds_def
 apply (rule set_eqI, rule iffI)
-apply (erule CollectE, (erule exE|erule conjE)+)
+apply (simp add:proc_file_fds_def)
+apply (erule exE|erule conjE)+
 apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)
-apply (rule CollectI)
-apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp)
-apply (erule CollectE, (erule exE|erule conjE)+)
-apply (simp only:file_of_proc_fd.simps split:if_splits)
-apply (rule CollectI)
+apply (rule_tac x = fda in exI, simp)
+apply (simp add:proc_file_fds_def)
+apply (erule exE|erule conjE)+
 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
 done
 
@@ -665,14 +666,235 @@
 done
 
 lemma cpfd2sfds_execve:
-  "valid (Execve p fds # s) 
-   \<Longrightarrow> cpfd2sfds (Execve p fds # s)  = (cpfd2sfds s) (p := "
+  "valid (Execve p f fds # s) 
+   \<Longrightarrow> cpfd2sfds (Execve p f fds # s) = (cpfd2sfds s) (p := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)
+apply (rule_tac x = fd in bexI, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (rule_tac x = fd in exI, simp)
+apply (simp split:if_splits)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_clone:
+  "valid (Clone p p' fds shms # s) 
+   \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)
+apply (rule_tac x = fd in bexI, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)
+apply (rule_tac x = fd in exI, simp)
+apply (simp split:if_splits)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)
+done
 
 lemma cpfd2sfds_other:
   "\<lbrakk>valid (e # s);
-    \<forall> 
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p;
+    \<forall> p fd. e \<noteq> CloseFd p fd;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (case_tac e)
+using cfd2sfd_other
+by auto
+
+lemma cpfd2sfds_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule set_eqI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (rule iffI)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_exit:
+  "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule set_eqI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (rule iffI)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := 
+     if (fd \<in> proc_file_fds s p)
+     then (case (cfd2sfd s p fd) of 
+             Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)
+                          then cpfd2sfds s p else cpfd2sfds s p - {sfd})
+           | _        \<Rightarrow> cpfd2sfds s p)
+     else cpfd2sfds s p)"
+apply (frule vd_cons)
+apply (rule ext, rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (rule conjI, rule impI, rule conjI, rule impI, erule exE)
+apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)
+apply (erule exE, simp)
+apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)
+
+apply (rule impI, rule conjI)
+apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (erule_tac x = fda in allE, simp add:cfd2sfd_closefd)
+
+apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule exE, rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+
+apply (rule impI| rule conjI)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+
+apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
 
-lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other
+apply (simp split:if_splits)
+apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)
+apply (erule exE, simp)
+apply (case_tac "\<exists>fd'. fd' \<noteq> fd \<and> (\<exists>f'. file_of_proc_fd s p fd' = Some f') \<and> cfd2sfd s p fd' = Some sfd")
+apply simp
+apply (case_tac "xa = sfd")
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fd' in exI, simp add:cfd2sfd_closefd)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (simp, (erule exE|erule conjE)+)
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+done
+
+lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit
+  cpfd2sfds_closefd cpfd2sfds_other
+
+(********* ch2sshm simpset ********)
+
+lemma ch2sshm_createshm:
+  "valid (CreateShM p h # s) 
+   \<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h := 
+     (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of
+                    Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
+                  | _ \<Rightarrow> None))"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
+done
+
+lemma ch2sshm_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h. e \<noteq> CreateShM p h; 
+    h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac e)
+apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
+done
+
+lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other
+
+lemma current_shm_has_sh:
+  "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"
+by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')
+
+lemma current_shm_has_sh':
+  "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
+by (auto dest:current_shm_has_sh)
+
+(********** 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
+
+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)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
+
+lemma cph2spshs_createshm:
+  "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
+
+lemma cph2spshs_other:
+  "\<lbrakk>valid (e # s); "
+
+lemmas cph2spshs_simps = cph2spshs_other
 
 (******** cp2sproc simpset *********)