# HG changeset patch
# User chunhan
# Date 1380037143 -28800
# Node ID bf8c09ec11867af44d11886e96148f49e963fcad
# Parent  0960686df575f0b189914e9f61c559d8fff5267d
update

diff -r 0960686df575 -r bf8c09ec1186 S2ss_prop.thy
--- a/S2ss_prop.thy	Tue Sep 24 14:02:15 2013 +0800
+++ b/S2ss_prop.thy	Tue Sep 24 23:39:03 2013 +0800
@@ -788,7 +788,7 @@
       then ss
       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
            then update_s2ss_sfile s ss f sf
-           else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf"
+           else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
 
 lemma alive_co2sobj_closefd1:
   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
@@ -862,6 +862,18 @@
   "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
+lemma same_inode_files_prop10:
+  "\<lbrakk>same_inode_files s f \<noteq> {f}; is_file s f\<rbrakk> \<Longrightarrow> \<exists> f'. f' \<in> same_inode_files s f \<and> f' \<noteq> f"
+by (auto simp:same_inode_files_def split:if_splits)
+
+lemma same_inode_files_prop11:
+  "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
+lemma same_inode_files_prop11':
+  "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f'"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
 lemma s2ss_closefd:
   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
      case (file_of_proc_fd s p fd) of
@@ -962,8 +974,22 @@
 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
 apply (rule impI, tactic {*my_seteq_tac 1*})
-apply (simp add:update_s2ss_obj_def)
-apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
@@ -983,6 +1009,25 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule impI, rule conjI, rule impI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 apply (rule impI)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
@@ -1009,11 +1054,275 @@
 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
-apply (tactic {*my_setiff_tac 1*})
+
+apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule disjE)
+apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'a" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd)
+apply (case_tac "f \<in> same_inode_files s a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
+apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd is_file_simps)
+apply (rule notI, simp add:same_inode_files_prop9)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+
+apply (erule disjE)
+apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'a" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule disjE)
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd)
+apply (case_tac "f \<in> same_inode_files s a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
+apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd is_file_simps)
+apply (rule notI, simp add:same_inode_files_prop9)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+
+apply (rule impI, rule conjI, rule impI)
+apply (tactic {*my_seteq_tac 1*})
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (rule notI, simp, erule_tac x = "O_proc pa" in allE, simp add:co2sobj_closefd)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (rule conjI, rule_tac x = "O_file f''" in exI)
+apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
+apply (rule notI, simp)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+
+apply (erule bexE, erule conjE)
+apply (simp add:update_s2ss_obj_def split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule conjI)
+apply (rule impI)
+apply (rule_tac x = f' in ballE, simp, simp, simp)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule conjI)
+apply (rule impI)
+apply (rule_tac x = f' in ballE, simp, simp, simp)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+
+apply (rule impI)
+apply (tactic {*my_seteq_tac 1*})
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp)
+apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits)
+apply (erule_tac x= f in allE, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule conjI| rule impI|erule exE|erule conjE)+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule notI, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+
+
+apply (erule bexE, erule conjE)
+apply (rule conjI, rule_tac x = "O_file f''" in exI)
+apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
+apply (rule notI, simp)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+
+apply (erule bexE, erule conjE)
+apply (simp add:update_s2ss_obj_def split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule conjI)
+apply (rule impI)
+apply (rule_tac x = f' in ballE, simp, simp, simp)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule conjI)
+apply (rule impI)
+apply (rule_tac x = f' in ballE, simp, simp, simp)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
 
 
 
+
+apply 
+
 defer
 apply (rule impI)
 apply (simp add:update_s2ss_obj_def)