# HG changeset patch
# User chunhan
# Date 1369102791 -28800
# Node ID 3e7617baa6a372bbed321cf54b572c6cf0b97993
# Parent  ac66d8ba86d9d17b13cf218bbc868515562a9d29
update

diff -r ac66d8ba86d9 -r 3e7617baa6a3 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Co2sobj_prop.thy	Tue May 21 10:19:51 2013 +0800
@@ -8,6 +8,8 @@
 
 (****************** cf2sfile path simpset ***************)
 
+thm cpfd2sfds_def
+
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)
diff -r ac66d8ba86d9 -r 3e7617baa6a3 Init_prop.thy
--- a/Init_prop.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Init_prop.thy	Tue May 21 10:19:51 2013 +0800
@@ -709,10 +709,11 @@
 apply (simp only:cpfd2sfds_def init_cfds2sfds_def)
 apply (rule set_eqI, rule iffI)
 apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) defer
+apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer
 apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI)
-using cfd2sfd_nil_prop by auto
+apply (rule_tac x = fd in exI, rule_tac x = f in exI)
+using cfd2sfd_nil_prop 
+by auto
 
 lemma ch2sshm_nil_prop:
   "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h"
diff -r ac66d8ba86d9 -r 3e7617baa6a3 ROOT
--- a/ROOT	Tue May 21 08:01:33 2013 +0800
+++ b/ROOT	Tue May 21 10:19:51 2013 +0800
@@ -12,6 +12,8 @@
 session "alive" = "dynamic" + 
   options [document = false]
   theories
+    Static_type
+    Static
     Valid_prop
     Init_prop
     Current_files_prop
@@ -19,4 +21,4 @@
     Alive_prop
     Proc_fd_of_file_prop
     Finite_current
-    New_obj_prop
\ No newline at end of file
+    New_obj_prop
diff -r ac66d8ba86d9 -r 3e7617baa6a3 Static.thy
--- a/Static.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Static.thy	Tue May 21 10:19:51 2013 +0800
@@ -47,7 +47,7 @@
 
 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
 where
-  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd sfd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
+  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
 
 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
 where
@@ -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)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
+  "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> 
                                              init_ch2sshm h = Some sh}"
 
 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"