--- a/Co2sobj_prop.thy	Tue May 21 10:19:51 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 22 15:22:50 2013 +0800
@@ -603,23 +603,10 @@
   "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)
 
-definition cpfd2sfds' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
-where
-  "cpfd2sfds' s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
-
-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}"
-
-lemma "x \<in> cph2spshs' s p \<Longrightarrow> False"
-apply (simp add:cph2spshs'_def)
-apply (case_tac x, simp)
-
-
-lemma cpfd2sfds_open_some1:
-  "valid (Open p f flags fd (Some inum) # s) \<Longrightarrow>
-   cpfd2sfds (Open p f flags fd (Some inum) # s) p = (
-    case (cfd2sfd (Open p f flags fd (Some inum) # s) p fd) of
+lemma cpfd2sfds_open1:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow>
+   cpfd2sfds (Open p f flags fd opt # s) p = (
+    case (cfd2sfd (Open p f flags fd opt # s) p fd) of
         Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}
       | _ \<Rightarrow> cpfd2sfds s p)"
 apply (frule vd_cons, frule vt_grant_os)
@@ -627,32 +614,43 @@
 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)
 apply (rule allI, rule impI)
 apply (rule set_eqI, rule iffI)
+apply (case_tac "x = a", simp)
 unfolding cpfd2sfds_def
-thm CollectE
-apply (erule CollectE)
 apply (erule CollectE, (erule conjE|erule exE)+)
-apply (simp only:file_of_proc_fd.simps split:if_splits)
-apply (simp add:cpfd2sfds_def)
+apply (simp split:if_splits)
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
+apply (case_tac "x = a", simp)
+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)
+done
 
-apply (auto simp:cpfd2sfds_def split:option.splits if_splits dest:file_of_proc_fd_in_curf proc_fd_in_fds proc_fd_in_procs)
-
-lemma cpfd2sfds_open1:
+lemma cpfd2sfds_open1':
   "valid (Open p f flags fd opt # s) \<Longrightarrow>
    cpfd2sfds (Open p f flags fd opt # s) p = (
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p)"
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac opt)
-apply (auto simp:sectxt_of_obj_simps current_files_simps dest!:current_has_sec' current_file_has_sfile'
-  split:option.splits)
-apply (auto simp:cpfd2sfds_def split:if_splits)
-apply (auto simp:cfd2sfd_open cf2sfile_open sectxt_of_obj_simps current_files_simps split:option.splits if_splits dest!:current_has_sec' current_file_has_sfile')
 apply (frule cfd2sfd_open1)
-apply (
-apply (simp add:cpfd2sfds_def)
-apply (auto simp add:cpfd2sfds_def split:option.splits)
-apply (auto dest!:current_has_sec')
+apply (auto dest:cpfd2sfds_open1 split:option.splits)
+done
+
+lemma cpfd2sfds_open2:
+  "\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'"
+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 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 add:cfd2sfd_open2)
+done
 
 lemma cpfd2sfds_open:
   "valid (Open p f flags fd opt # s)
@@ -660,12 +658,21 @@
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p))"
-apply (frule cfd2sfd_open1)
 apply (rule ext)
-apply (simp add:cpfd2sfds_def)
-apply (auto simp add:cpfd2sfds_def split:option.splits)
+apply (case_tac "x \<noteq> p")
+apply (simp add:cpfd2sfds_open2)
+apply (simp add:cpfd2sfds_open1')
+done
 
-lemma cpfd2sfds_simps = 
+lemma cpfd2sfds_execve:
+  "valid (Execve p fds # s) 
+   \<Longrightarrow> cpfd2sfds (Execve p fds # s)  = (cpfd2sfds s) (p := "
+
+lemma cpfd2sfds_other:
+  "\<lbrakk>valid (e # s);
+    \<forall> 
+
+lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other
 
 (******** cp2sproc simpset *********)