diff -r f27ba31b7e96 -r 6f7b9039715f no_shm_selinux/S2ss_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/S2ss_prop.thy	Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,2341 @@
+(*<*)
+theory S2ss_prop
+imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop
+begin
+(*>*)
+
+context tainting_s begin
+
+(* simpset for s2ss*)
+
+lemma co2sobj_some_case:
+  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);
+    \<And> f. obj = O_file f \<Longrightarrow> P (O_file f);
+    \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>
+   \<Longrightarrow> P obj" (*  \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h); *)
+by (case_tac obj, auto)
+
+lemma co2sobj_execve_alive:
+  "\<lbrakk>alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\<rbrakk>
+   \<Longrightarrow> alive (Execve p f fds # s) obj"
+apply (erule co2sobj_some_case)
+by (auto simp:alive_simps simp del:alive.simps)
+
+lemma s2ss_execve':
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
+     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     then (case (cp2sproc (Execve p f fds # s) p) of
+             Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}
+           | _ \<Rightarrow> {} )
+     else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of
+             (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> tainted s)}
+                                    \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}
+           | _ \<Rightarrow> {} ) )"
+apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)
+
+apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)
+apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)
+apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)")
+apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
+apply (erule exE, simp)
+apply (simp add:s2ss_def, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj_execve split:if_splits)
+apply (simp add:co2sobj_execve, rule disjI2)
+apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]
+apply (simp, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp)
+apply (erule exE| erule conjE)+
+apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:alive_execve co2sobj_execve cp2sproc_execve)
+apply (case_tac "obj = O_proc p", simp)
+apply (frule co2sobj_execve_alive, simp, simp)
+apply (frule_tac obj = obj in co2sobj_execve, simp)
+apply (rule_tac x = obj in exI, simp, simp)
+
+apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)
+apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") 
+apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
+apply (erule exE, erule conjE, simp)
+apply (simp add:s2ss_def, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p", simp)
+apply (rule disjI1, simp split:if_splits)
+apply (simp add:co2sobj_execve, rule disjI2)
+apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE, simp, (simp split:option.splits)+)
+apply (erule disjE, simp)
+apply (rule_tac x = "O_proc p" in exI, simp)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = obj in exI)
+apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)
+apply (frule_tac obj = obj in co2sobj_execve, simp, simp)
+apply (rule impI, simp, simp)
+done
+
+lemma s2ss_clone_alive:
+  "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds # s)\<rbrakk>
+   \<Longrightarrow> alive (Clone p p' fds # s) obj"
+by (erule co2sobj_some_case, auto simp:alive_clone)
+
+lemma s2ss_clone:
+  "valid (Clone p p' fds # s) \<Longrightarrow> s2ss (Clone p p' fds # s) = (
+     case (cp2sproc (Clone p p' fds # s) p') of
+       Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s)}
+     | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, split option.splits)
+apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
+apply (rule allI, rule impI, simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p'", simp)
+apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)
+apply (rule disjI1, simp split:if_splits)
+apply (simp, rule disjI2)
+apply (frule co2sobj_clone, simp)
+apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+
+apply (simp, erule disjE, simp)
+apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (rule impI, rule notI, drule tainted_in_current, simp+)
+apply (erule exE| erule conjE)+
+apply (case_tac "obj = O_proc p'", simp)
+apply (rule_tac x = obj in exI)
+apply (frule s2ss_clone_alive, simp+)
+apply (auto simp:co2sobj_clone alive_simps)
+done
+
+(*
+definition s2ss_shm_no_backup:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"
+where
+  "s2ss_shm_no_backup s pfrom \<equiv> {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and>
+     (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)))}"
+
+definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 
+where
+  "update_s2ss_shm s pfrom \<equiv> s2ss s 
+     \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}
+     - (s2ss_shm_no_backup s pfrom)"
+
+lemma s2ss_shm_no_bk_elim:
+  "\<lbrakk>S_proc sp False \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False); 
+    valid s; info_flow_shm s pfrom p\<rbrakk>
+   \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)"
+apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
+apply (erule_tac x = p in allE, auto)
+apply (rule_tac x = p' in exI, auto)
+done
+
+lemma s2ss_shm_no_bk_intro1:
+  "\<lbrakk>co2sobj s' obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (case_tac obj)
+apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)
+done
+
+lemma s2ss_shm_no_bk_intro2:
+  "\<lbrakk>co2sobj s' obj = Some x; obj \<in> tainted s'; valid s'\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (case_tac obj)
+
+apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)
+done
+
+lemma s2ss_shm_no_bk_intro3:
+  "\<lbrakk>co2sobj s (O_proc p) = Some x; \<not> info_flow_shm s pfrom p; p \<in> current_procs s
+   \<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (auto simp add:s2ss_shm_no_backup_def split:option.splits)
+apply (rule_tac x = p in exI, simp)
+done
+
+lemma s2ss_shm_no_bk_intro4:
+  "\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; 
+    \<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>
+   \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (rule notI)
+apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
+done  
+*)
+
+lemma tainted_ptrace':
+  "tainted (Ptrace p p' # s) = 
+     (if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s)
+      then tainted s \<union> {O_proc p'}
+      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
+           then tainted s \<union> {O_proc p}
+                else tainted s)"
+by auto
+
+lemma co2sobj_some_caseD:
+  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);
+    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 
+    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); 
+    \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>
+   \<Longrightarrow> P obj"
+by (case_tac obj, auto)
+
+definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "update_s2ss_obj s ss obj sobj sobj' = 
+     (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+      then ss \<union> {sobj'}
+      else ss - {sobj} \<union> {sobj'})"
+
+ML {*
+fun my_setiff_tac i = 
+     (etac @{thm CollectE} i 
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i
+              THEN etac @{thm disjE} i)
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i
+              THEN etac @{thm conjE} i 
+              THEN (REPEAT (etac @{thm CollectE} i))))
+THEN (REPEAT ((        etac @{thm exE} 
+               ORELSE' etac @{thm conjE}
+               ORELSE' etac @{thm bexE}) i))
+THEN (rtac @{thm CollectI} i
+      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))
+
+*}
+
+ML {*
+fun my_seteq_tac i = 
+     (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)
+THEN (rtac @{thm set_eqI} i)
+THEN (rtac @{thm iffI} i)
+THEN my_setiff_tac i
+*}
+
+ML {*fun my_clarify_tac i = 
+REPEAT ((  rtac @{thm impI}
+   ORELSE' rtac @{thm allI}
+   ORELSE' rtac @{thm ballI}
+   ORELSE' rtac @{thm conjI}
+   ORELSE' etac @{thm conjE}
+   ORELSE' etac @{thm exE}
+   ORELSE' etac @{thm bexE}
+   ORELSE' etac @{thm disjE}) i)
+*}
+
+lemma co2sobj_sproc_imp:
+  "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sfile_imp:
+  "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sdir_imp:
+  "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_smsgq_imp:
+  "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 s2ss_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> 
+     (case (cp2sproc s p, cp2sproc (Execve p f fds # s) p) of
+        (Some sp, Some sp') \<Rightarrow> s2ss (Execve p f fds # s) = 
+            update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))
+                          (S_proc sp' (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
+      | _ \<Rightarrow> s2ss (Execve p f fds # s) = {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "cp2sproc (Execve p f fds # s) p")
+apply (drule current_proc_has_sp', simp, simp, simp)
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)
+apply (simp add:s2ss_execve')
+apply (rule impI)
+apply (erule_tac x = pa in allE, simp)
+apply (rule impI)
+apply (simp add:s2ss_execve')
+apply (rule impI)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp split:option.splits)
+apply (erule_tac x = "O_proc p'" in allE, simp)
+done
+
+lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp
+
+lemma s2ss_ptrace1:
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> tainted s; O_proc p' \<notin> tainted s\<rbrakk>
+   \<Longrightarrow> (case (cp2sproc s p') of 
+          Some sp' \<Rightarrow> s2ss (Ptrace p p' # s) = 
+                     update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp' False) (S_proc sp' True)
+        | _        \<Rightarrow> s2ss (Ptrace p p' # s) = {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (case_tac "cp2sproc s p'")
+apply (drule current_proc_has_sp', simp+)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp+)
+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p'")
+apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p'")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p'")
+apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (rule notI, simp)
+apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)
+apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p'")
+apply (simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+done
+
+lemma s2ss_ptrace2:
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> tainted s; O_proc p \<notin> tainted s\<rbrakk>
+   \<Longrightarrow> (case (cp2sproc s p) of 
+          Some sp \<Rightarrow> s2ss (Ptrace p p' # s) = 
+                    update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+        | _       \<Rightarrow> s2ss (Ptrace p p' # s) = {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (case_tac "cp2sproc s p'")
+apply (drule current_proc_has_sp', simp+)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp+)
+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (rule notI, simp)
+apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)
+apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+done
+
+lemma s2ss_ptrace3:
+  "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> tainted s) = (O_proc p \<in> tainted s)\<rbrakk>
+   \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"
+unfolding s2ss_def
+apply (frule vd_cons, frule vt_grant_os, rule set_eqI, rule iffI)
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (frule alive_other, simp+)
+apply (frule_tac obj = obj in co2sobj_ptrace, simp)
+apply (auto split:t_object.splits option.splits if_splits)[1]
+
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (frule alive_other, simp+)
+apply (frule_tac obj = obj in co2sobj_ptrace, simp)
+apply (case_tac "cp2sproc s p'")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "O_proc p' \<in> tainted s")
+apply (auto split:t_object.splits option.splits if_splits simp:co2sobj.simps)
+done
+
+lemma s2ss_ptrace:
+  "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (
+     if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 
+     then (case (cp2sproc s p') of 
+             Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp False) (S_proc sp True)
+           | _       \<Rightarrow> {})
+     else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
+          then (case (cp2sproc s p) of 
+                  Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+                | _       \<Rightarrow> {})
+          else s2ss s                                   )"
+apply (case_tac "O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s")
+apply (drule s2ss_ptrace1, simp, simp, simp split:option.splits)
+apply (case_tac "O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s")
+apply (drule s2ss_ptrace2, simp, simp, simp split:option.splits)
+apply (drule s2ss_ptrace3, auto)
+done
+
+lemma s2ss_kill':
+  "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (
+     if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))
+     then s2ss s 
+     else (case (co2sobj s (O_proc p')) of
+             Some sp \<Rightarrow> s2ss s - {sp}
+           | _       \<Rightarrow> {}))"
+apply (frule vt_grant_os, frule vd_cons)
+unfolding s2ss_def
+apply (simp split:if_splits, rule conjI)
+apply (rule impI, (erule exE|erule conjE)+)
+apply (split option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (simp split: option.splits, (erule conjE)+)
+apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p'")
+apply (rule_tac x = "O_proc p''" in exI)
+apply (simp add:cp2sproc_kill alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_kill alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+
+apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)
+apply (rule set_eqI, rule iffI)
+apply (erule CollectE, erule exE, erule conjE, rule DiffI)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE)
+apply (simp add:co2sobj_kill cp2sproc_kill split:option.splits)
+apply (simp split:option.splits)+
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p'")
+apply (rule_tac x = "O_proc p''" in exI)
+apply (simp add:cp2sproc_kill alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_kill alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+done
+
+definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "del_s2ss_obj s ss obj sobj \<equiv> 
+     if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+     then ss
+     else ss - {sobj}"
+
+lemma del_update_s2ss_obj:
+  "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"
+by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)
+
+lemma s2ss_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> (
+      case (cp2sproc s p') of 
+        Some sp \<Rightarrow> s2ss (Kill p p' # s) = del_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp (O_proc p' \<in> tainted s))
+      | _       \<Rightarrow> s2ss (Kill p p' # s) = {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (split option.splits, rule conjI, rule impI)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule allI, rule impI)
+apply (simp add:del_s2ss_obj_def split:option.splits)
+apply (tactic {*my_clarify_tac 1*})
+apply (frule co2sobj_sproc_imp, erule exE)
+apply (simp add:s2ss_kill')
+apply (rule impI)
+apply (erule_tac x = pa in allE, simp)
+apply (rule impI)
+apply (simp add:s2ss_kill')
+apply (rule impI)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp split:option.splits)
+apply (erule_tac x = "O_proc p''" in allE, simp)
+done
+
+lemma s2ss_exit':
+  "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (
+     if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     then s2ss s 
+     else (case (co2sobj s (O_proc p)) of
+             Some sp \<Rightarrow> s2ss s - {sp}
+           | _       \<Rightarrow> {}))"
+apply (frule vt_grant_os, frule vd_cons)
+unfolding s2ss_def
+apply (simp split:if_splits, rule conjI)
+apply (rule impI, (erule exE|erule conjE)+)
+apply (split option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (simp split: option.splits, (erule conjE)+)
+apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:cp2sproc_exit alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_exit alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+
+apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)
+apply (rule set_eqI, rule iffI)
+apply (erule CollectE, erule exE, erule conjE, rule DiffI)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE)
+apply (simp add:co2sobj_exit cp2sproc_exit split:option.splits)
+apply (simp split:option.splits)+
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:cp2sproc_exit alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_exit alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+done
+
+lemma s2ss_exit:
+  "valid (Exit p # s) \<Longrightarrow> (
+      case (cp2sproc s p) of 
+        Some sp \<Rightarrow> s2ss (Exit p # s) = del_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))
+      | _       \<Rightarrow> s2ss (Exit p # s) = {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (split option.splits, rule conjI, rule impI)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule allI, rule impI)
+apply (simp add:del_s2ss_obj_def split:option.splits)
+apply (tactic {*my_clarify_tac 1*})
+apply (frule co2sobj_sproc_imp, erule exE)
+apply (simp add:s2ss_exit')
+apply (rule impI)
+apply (erule_tac x = pa in allE, simp)
+apply (rule impI)
+apply (simp add:s2ss_exit')
+apply (rule impI)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp split:option.splits)
+apply (erule_tac x = "O_proc p'" in allE, simp)
+done
+
+lemma alive_has_sobj':
+  "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
+apply (case_tac obj)
+apply (auto split:option.splits)
+oops
+
+declare co2sobj.simps [simp del]
+
+lemma co2sobj_open_none:
+  "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
+      if (obj = O_proc p) 
+      then (case (cp2sproc (Open p f flag fd None # s) p) of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
+           | _       \<Rightarrow> None)
+      else co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
+apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+done
+
+lemma co2sobj_open_some:
+  "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (
+      if (obj = O_proc p) 
+      then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
+           | _       \<Rightarrow> None)
+      else if (obj = O_file f) 
+           then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of
+                   Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))
+                 | _       \<Rightarrow> None)
+           else co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
+apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+done
+
+lemma alive_co2sobj_some_open_none:
+  "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>
+   \<Longrightarrow> alive (Open p f flag fd None # s) obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma alive_co2sobj_some_open_none':
+  "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 
+    valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma co2sobj_proc_obj:
+  "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma s2ss_open_none:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (
+      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of
+        (Some sp, Some sp') \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp'}
+           else s2ss s - {sp} \<union> {sp'} 
+      | _                   \<Rightarrow> {} )"
+unfolding s2ss_def
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)
+apply (rule conjI, rule impI, erule exE, (erule conjE)+)
+apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (rule impI)
+apply (case_tac "obj = O_proc p", simp)
+apply (rule Meson.disj_comm, rule disjCI, rule conjI)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (simp add:co2sobj_open_none split:option.splits)
+apply (rule notI)
+apply (frule co2sobj_proc_obj, simp, erule exE)
+apply (erule_tac x = p' in allE, simp)
+
+apply (simp split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule exE, erule conjE, case_tac "obj = O_proc p")
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
+done
+
+lemma alive_co2sobj_some_open_some:
+  "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>
+   \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"
+by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma alive_co2sobj_some_open_some':
+  "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 
+    valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma s2ss_open_some:
+  "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (
+      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),
+            co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of
+        (Some sp, Some sp', Some sf) \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp', sf} 
+           else s2ss s - {sp} \<union> {sp', sf} 
+      | _                   \<Rightarrow> {} )"
+unfolding s2ss_def
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (clarsimp split del:if_splits)
+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)
+apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
+apply (simp add:co2sobj_open split:t_object.splits)
+apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
+apply (simp add:co2sobj_open split:t_object.splits)
+apply (frule_tac obj = obj in co2sobj_open_some, simp+)
+apply (simp add:alive_co2sobj_some_open_some', simp)
+apply (rule notI)
+apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)
+apply (erule_tac x = p' in allE, simp)
+
+apply (simp split:if_splits, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp)
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)
+apply (case_tac "obj = O_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp)
+apply (case_tac "obj = O_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
+done
+
+lemma s2ss_open':
+  "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (
+     if opt = None
+     then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of
+        (Some sp, Some sp') \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp'}
+           else s2ss s - {sp} \<union> {sp'} 
+      | _                   \<Rightarrow> {} )
+     else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),
+            co2sobj (Open p f flag fd opt # s) (O_file f)) of
+        (Some sp, Some sp', Some sf) \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp', sf} 
+           else s2ss s - {sp} \<union> {sp', sf} 
+      | _                   \<Rightarrow> {} ) )"
+apply (case_tac opt)
+apply (simp add:s2ss_open_some s2ss_open_none)+
+done
+
+lemma co2sobj_proc_eq_some:
+  "\<lbrakk>co2sobj s (O_proc p) = Some sp; co2sobj s obj = Some sp\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+apply (case_tac obj, case_tac[!] sp)
+by (auto simp:co2sobj.simps split:option.splits)
+
+lemma s2ss_open:
+  "valid (Open p f flag fd opt # s) \<Longrightarrow> 
+    (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p), 
+           co2sobj (Open p f flag fd opt # s) (O_file f)) of
+       (Some sp, Some sp', Some sf) \<Rightarrow> s2ss (Open p f flag fd opt # s) = (
+       if opt = None
+       then update_s2ss_obj s (s2ss s) (O_proc p) sp sp'
+       else update_s2ss_obj s (s2ss s) (O_proc p) sp sp' \<union> {sf})
+     | _ \<Rightarrow> s2ss (Open p f flag fd opt # s) = {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)
+apply (case_tac "co2sobj s (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_file f)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (simp split:option.splits add:s2ss_open' update_s2ss_obj_def)
+apply (auto)
+apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
+apply (erule_tac x = "p'" in allE, simp)
+apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
+apply (erule_tac x = "p'" in allE, simp)
+apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
+apply (erule_tac x = "p'" in allE, simp)
+done
+
+lemma s2ss_readfile:
+  "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (
+     case (file_of_proc_fd s p fd) of 
+       Some f \<Rightarrow> if (O_file f \<in> tainted s \<and> O_proc p \<notin> tainted s)
+                 then (case (cp2sproc s p) of 
+                         Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+                       | _       \<Rightarrow> {})
+                 else s2ss s
+     | _      \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp+)
+apply (rule conjI, rule impI, erule conjE)
+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj_readfile)
+apply (rule disjI2, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x= "O_proc p" in exI, simp add:alive_other co2sobj_readfile)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = "O_proc pa" in exI, simp add:alive_other co2sobj_readfile)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj_readfile)
+apply (rule disjI2, rule DiffI)
+apply (simp, rule_tac x = obj in exI)
+apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)
+apply (rule notI, erule_tac x = obj in allE)
+apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:alive_other co2sobj_readfile)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (simp add:co2sobj.simps)
+
+apply (simp add:s2ss_def, rule impI)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)
+apply (simp add:co2sobj.simps)
+done
+
+lemma same_inode_files_prop9:
+  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"
+by (simp add:same_inode_files_def)
+
+lemma cf2sfiles_prop:
+  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"
+apply (auto simp:cf2sfiles_def)
+apply (rule_tac x = f'a in bexI, simp)
+apply (erule same_inode_files_prop4, simp)
+apply (rule_tac x = f'a in bexI, simp)
+apply (drule same_inode_files_prop5)
+apply (erule same_inode_files_prop4, simp)
+done
+
+lemma co2sobj_writefile_unchange:
+  "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;
+    O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk> 
+   \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"
+apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (case_tac "O_proc p \<in> tainted s")
+apply (simp add:same_inodes_tainted)+
+done
+
+lemma s2ss_writefile':
+  "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)
+                 then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>
+                                 co2sobj s (O_file f') = co2sobj s (O_file f))
+                       then s2ss s \<union> {S_file (cf2sfiles s f) True}
+                       else s2ss s - {S_file (cf2sfiles s f) False} 
+                                   \<union> {S_file (cf2sfiles s f) True})
+                 else s2ss s
+     | _      \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp split:option.splits)
+unfolding s2ss_def
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)
+apply (simp split:t_object.splits if_splits)
+apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)
+apply (rule disjI1, simp add:cf2sfiles_prop)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp)
+apply (rule disjI2, rule_tac x = obj in exI, simp)
+apply (simp add:co2sobj.simps)
+
+apply (erule disjE)
+apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)
+apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)
+apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)
+apply (erule exE, erule conjE, erule conjE)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (case_tac "fa \<in> same_inode_files s aa")
+apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)
+apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule conjI, rule impI, simp add:same_inode_files_prop5)
+apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)
+apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule impI, simp add:same_inode_files_prop5)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+
+apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)
+apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)
+apply (simp add:co2sobj_writefile split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps same_inodes_tainted)
+apply (case_tac "O_proc p \<in> tainted s", simp, simp)
+apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+
+apply (rule impI| rule conjI|erule conjE)+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp split:if_splits)
+apply (rule disjI1, simp add:cf2sfiles_prop)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (erule_tac x = list in allE, simp add:same_inode_files_prop5)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp add:co2sobj.simps)
+apply (erule disjE)
+apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)
+apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)
+apply (erule exE|erule conjE)+
+apply (erule co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (case_tac "fa \<in> same_inode_files s aa")
+apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule impI, simp add:same_inode_files_prop5)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (rule impI, rule impI)
+
+apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+apply (erule CollectE, erule exE, erule conjE)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+done
+
+definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
+where
+ "update_s2ss_sfile_tainted s ss f tag \<equiv>
+    if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> 
+              co2sobj s (O_file f') = Some (S_file (cf2sfiles s f) False))
+       then ss \<union> {S_file (cf2sfiles s f) True}
+       else ss - {S_file (cf2sfiles s f) False} 
+               \<union> {S_file (cf2sfiles s f) True}"
+
+lemma s2ss_writefile:
+  "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)
+                 then update_s2ss_sfile_tainted s (s2ss s) f True
+                 else s2ss s
+     | _      \<Rightarrow> {})"
+apply (drule s2ss_writefile')
+apply (simp)
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (simp add:update_s2ss_sfile_tainted_def)
+apply auto
+apply (erule_tac x = f' in allE, simp add:co2sobj.simps)+
+done
+
+definition update_s2ss_sfile_del :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where 
+  "update_s2ss_sfile_del s ss f sf \<equiv> 
+     if (same_inode_files s f = {f})
+     then ss
+     else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> tainted s)}"
+
+definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+  "del_s2ss_file s ss f sf = 
+     (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
+      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_del s ss f sf
+           else update_s2ss_sfile_del 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; 
+    file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd3:
+  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;
+    file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd2:
+  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>
+   \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd':
+  "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 
+    valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)
+
+ML {*asm_full_simp_tac*}
+
+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
+       Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
+                 then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
+                         (Some sf, Some sp, Some sp') \<Rightarrow> 
+                            (del_s2ss_file s (
+                               update_s2ss_obj s (s2ss s) (O_proc p) 
+                                 (S_proc sp (O_proc p \<in> tainted s))
+                                 (S_proc sp' (O_proc p \<in> tainted s))) f sf)
+                      | _ \<Rightarrow> {})
+                 else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 
+                         (Some sp, Some sp') \<Rightarrow> 
+                            (update_s2ss_obj s (s2ss s) (O_proc p)
+                               (S_proc sp (O_proc p \<in> tainted s))
+                               (S_proc sp' (O_proc p \<in> tainted s)))
+                      | _ \<Rightarrow> {})
+      | _     \<Rightarrow> s2ss s)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (frule current_proc_has_sp, simp, erule exE)
+apply (case_tac "file_of_proc_fd s p fd")
+
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule co2sobj_closefd, simp)
+apply (frule cp2sproc_closefd, simp)
+apply (simp add:proc_file_fds_def split:t_object.splits)
+apply (simp split:if_splits add:co2sobj.simps)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
+apply (frule cp2sproc_closefd, simp)
+apply (auto simp add:proc_file_fds_def co2sobj.simps 
+            split:t_object.splits option.splits if_splits)[1]
+
+apply (case_tac "cp2sproc (CloseFd p fd # s) p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "cf2sfile s a")
+apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)
+apply (simp)
+
+apply (rule conjI, rule impI, erule conjE)
+apply (simp add:del_s2ss_file_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+apply (tactic {*my_seteq_tac 1*})
+apply simp
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+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)
+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 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 split:t_object.splits if_splits)[1]
+
+apply (rule impI)+
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2)
+apply (case_tac "obj = O_file a", simp add:alive_simps)
+apply (rule DiffI, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (erule_tac x = "O_proc pa" in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
+apply (case_tac "obj = O_file a", 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 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:co2sobj.simps split:t_object.splits if_splits)[1]
+
+apply (rule impI, tactic {*my_seteq_tac 1*})
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_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)
+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 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)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+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 disjI2, 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 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)
+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 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)
+apply (rule disjI2, 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 split:t_object.splits if_splits)[1]
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = obj in allE, simp)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+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 add:is_file_simps)
+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 add:is_dir_simps)
+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 (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+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)
+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 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 split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+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 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 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 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)
+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)
+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 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 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 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)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+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 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 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_del_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)
+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 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)
+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 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 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 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 (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)
+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)
+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 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 split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+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 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 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_del_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)
+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 (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)
+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)
+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 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 disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps) 
+apply (rule disjI2, rule conjI, rule disjI2, 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 disjI2, 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 impI, rule conjI, rule impI)
+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (rule notI, simp)
+apply (rule conjI, 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 split:t_object.splits if_splits)[1]
+apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
+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 conjI, rule disjI2, rule conjI)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
+apply (rule conjI, 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 conjI, 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 impI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (rule disjI2, rule notI, simp)
+apply (rule disjI2, rule conjI, 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 split:t_object.splits if_splits)[1]
+apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
+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 disjI1)
+apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
+apply (rule disjI2, rule conjI, 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 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 (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
+apply (erule conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
+apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (erule conjE|erule exE|erule disjE)+
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (erule conjE|erule exE|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'" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop 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 conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
+apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+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 = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a")
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+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'" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop 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 conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
+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 (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps)
+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)
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI, rule impI, erule exE, erule conjE)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps split:if_splits)
+apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
+apply (simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
+apply (simp, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp: co2sobj.simps)
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps split:if_splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp: co2sobj.simps)
+apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits)
+apply (simp)
+apply (erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits 
+                simp: co2sobj.simps alive_co2sobj_closefd1)
+done
+
+lemma alive_co2sobj_unlink:
+  "\<lbrakk>alive s obj; valid (UnLink p f # s); obj \<noteq> O_file f\<rbrakk>
+   \<Longrightarrow> alive (UnLink p f # s) obj"
+by (auto simp add:alive_simps split:t_object.splits)
+
+lemma s2ss_unlink:
+  "valid (UnLink p f # s) \<Longrightarrow> s2ss (UnLink p f # s) = (
+     if (proc_fd_of_file s f = {}) 
+     then (case (cf2sfile s f) of 
+             Some sf \<Rightarrow> del_s2ss_file s (s2ss s) f sf
+           | _       \<Rightarrow> {})
+     else s2ss s)"
+apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)
+apply (frule is_file_has_sfile', simp, erule exE, simp)
+apply (rule conjI, rule impI)
+apply (simp add:update_s2ss_sfile_del_def del_s2ss_file_def)
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:is_file_simps)
+apply simp
+apply (rule conjI)
+apply (rule_tac x = obj in exI,simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp)
+apply (frule_tac obj = obj in co2sobj_unlink, simp)
+apply (erule_tac x = fa in allE, simp add:is_file_simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
+apply (frule_tac alive_co2sobj_unlink, simp, simp)
+apply (frule_tac obj = obj in co2sobj_unlink, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj.simps split:t_object.splits if_splits)
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1)
+apply (simp add:co2sobj_unlink)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (tactic {*my_setiff_tac 1*})
+apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop 
+  is_file_simps same_inode_files_prop11 split:if_splits)
+apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "f' = f", simp add:same_inode_files_prop9) 
+apply (case_tac "obj= O_file f")
+apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
+apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
+apply (simp add:co2sobj.simps)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1)
+apply (simp add:co2sobj_unlink)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps)
+apply (rule notI, simp add:co2sobj_unlink)
+apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop 
+  is_file_simps same_inode_files_prop11 split:if_splits)
+apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (subgoal_tac "alive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (rule_tac x =obj in exI)
+apply (subgoal_tac "alive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps same_inode_files_prop9 split:t_object.splits)[1]
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (simp add:alive_simps co2sobj.simps)
+apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
+apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink)
+apply (simp add:current_files_simps is_file_simps is_file_in_current)
+apply (simp add:same_inodes_tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (simp split:if_splits option.splits add:is_file_simps)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (auto split:t_sobject.splits)[1]
+apply (simp add:is_file_simps same_inode_files_prop11)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (simp split:if_splits option.splits add:is_file_simps)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (auto split:t_sobject.splits)[1]
+apply (simp add:is_file_simps same_inode_files_prop11)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+done
+
+lemma s2ss_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> s2ss (Rmdir p f # s) = (
+  case (co2sobj s (O_dir f)) of
+    Some sdir \<Rightarrow> del_s2ss_obj s (s2ss s) (O_dir f) sdir
+  | _         \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp:dir_is_empty_def)
+apply (frule is_dir_has_sdir', simp, erule exE)
+apply (simp split:option.splits, rule conjI, rule impI, simp add:co2sobj.simps)
+apply (rule allI, rule impI)
+
+apply (simp add:del_s2ss_obj_def)
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_rmdir is_file_simps is_dir_simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_dir f")
+apply (rule_tac x = obj' in exI)
+apply (subgoal_tac "alive (Rmdir p f # s) obj'")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:alive_rmdir)
+apply (rule_tac x = obj in exI)
+apply (subgoal_tac "alive (Rmdir p f # s) obj")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:alive_rmdir)
+
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply simp
+apply (case_tac "obj = O_dir f", simp add:alive_rmdir)
+apply (rule conjI)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+apply (simp add:co2sobj_rmdir)
+apply (simp add:alive_rmdir, erule_tac x = obj in allE, simp)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (case_tac "obj = O_dir f", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+done
+
+lemma s2ss_mkdir: "valid (Mkdir p f inum # s) \<Longrightarrow> s2ss (Mkdir p f inum # s) = (
+  case (cf2sfile (Mkdir p f inum # s) f) of
+    Some sf \<Rightarrow> (s2ss s) \<union> {S_dir sf}
+  | _       \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp)
+apply (case_tac "cf2sfile (Mkdir p f inum # s) f")
+apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*}, simp)
+apply (case_tac "obj = O_dir f")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_simps)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (rule_tac x = "O_dir f" in exI, simp add:alive_mkdir co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
+done
+
+definition update_s2ss_sfile_add :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+ "update_s2ss_sfile_add s ss f sf \<equiv>
+    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 ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}
+       else ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)} 
+               \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}"
+
+lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
+  case (cf2sfile (LinkHard p f f' # s) f') of
+    Some sf \<Rightarrow> update_s2ss_sfile_add s (s2ss s) f sf
+  | _       \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp)
+apply (split option.splits)
+apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
+apply (rule allI, rule impI)
+
+apply (simp add:update_s2ss_sfile_add_def)
+apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f'")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard
+  same_inode_files_linkhard split:if_splits)
+apply (case_tac "O_file f' \<in> tainted s")
+apply (drule tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard 
+  same_inodes_tainted split:if_splits)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
+apply (simp add:alive_linkhard)
+apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule conjI, rule impI, simp add:is_file_in_current)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f'", simp)
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard
+  same_inode_files_linkhard split:if_splits)
+apply (case_tac "O_file f' \<in> tainted s")
+apply (drule tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD, simp)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_linkhard alive_linkhard)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard 
+  same_inodes_tainted split:if_splits)
+apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
+apply (erule_tac x = fa in allE, rule notI)
+apply (simp add:co2sobj_linkhard is_file_simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
+apply (simp add:alive_linkhard)
+apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+done
+
+lemma same_inode_files_prop12:
+  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f "
+by (auto simp:is_file_def  same_inode_files_def split:option.splits)
+
+lemma s2ss_truncate: "valid (Truncate p f len # s) \<Longrightarrow> s2ss (Truncate p f len # s) = (
+  if (O_file f \<notin> tainted s \<and> O_proc p \<in> tainted s \<and> len > 0)
+  then update_s2ss_sfile_tainted s (s2ss s) f True
+  else s2ss s)"
+apply (frule vt_grant_os, frule vd_cons, simp split:if_splits)
+apply (rule conjI, rule impI, (erule conjE)+)
+
+apply (simp add:update_s2ss_sfile_tainted_def)
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_file_simps)
+apply (rule notI, simp add:co2sobj_truncate is_file_simps)
+apply (erule_tac x = fa in allE)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+
+apply (rule impI, simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_truncate)
+apply (simp split:t_object.splits if_splits add:co2sobj.simps)
+apply (case_tac "O_proc p \<in> tainted s", simp add:same_inodes_tainted)
+apply simp
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_truncate)
+apply (auto split:t_object.splits if_splits simp:co2sobj.simps same_inodes_tainted)
+done
+
+lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \<Longrightarrow> s2ss (CreateMsgq p q # s) = 
+  (case (cq2smsgq (CreateMsgq p q # s) q) of 
+     Some sq \<Rightarrow> s2ss s \<union> {S_msgq sq}
+   | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (case_tac "cq2smsgq (CreateMsgq p q # s) q")
+apply (drule current_has_smsgq', simp+)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_createmsgq is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply simp
+apply (rule_tac x = obj in exI)
+apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_sendmsg: "valid (SendMsg p q m # s) \<Longrightarrow> s2ss (SendMsg p q m # s) = (
+  case (cq2smsgq s q, cq2smsgq (SendMsg p q m # s) q) of
+    (Some sq, Some sq') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+  | _  \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (case_tac "cq2smsgq s q")
+apply (drule current_has_smsgq', simp+)
+apply (case_tac "cq2smsgq (SendMsg p q m # s) q")
+apply (drule current_has_smsgq', simp+)
+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp)
+apply (frule_tac obj = obj in co2sobj_smsgq_imp, erule exE, simp)
+apply (erule_tac x = obj in allE, simp add:co2sobj_sendmsg)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+done
+
+lemma alive_co2sobj_removemsgq:
+  "\<lbrakk>alive s obj; valid (RemoveMsgq p q # s); co2sobj s obj = Some sobj; obj \<noteq> O_msgq q\<rbrakk> 
+   \<Longrightarrow> alive (RemoveMsgq p q # s) obj"
+apply (erule co2sobj_some_caseD)
+apply (auto simp:is_file_simps is_dir_simps)
+done
+
+lemma s2ss_removemsgq: "valid (RemoveMsgq p q # s) \<Longrightarrow> s2ss (RemoveMsgq p q # s) = 
+  (case (cq2smsgq s q) of
+     Some sq \<Rightarrow> del_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq)
+   | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (split option.splits, rule conjI, rule impI)
+apply (drule current_has_smsgq', simp, simp)
+apply (rule allI, rule impI)
+
+apply (simp add:del_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (rule_tac x = obj' in exI)
+apply (frule_tac obj = obj' in co2sobj_smsgq_imp, erule exE)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (rule notI, simp, frule_tac obj = obj in co2sobj_smsgq_imp, erule exE)
+apply (erule_tac x = obj in allE, simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+done
+
+declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
+
+lemma s2ss_recvmsg: "valid (RecvMsg p q m # s) \<Longrightarrow> s2ss (RecvMsg p q m # s) = (
+  case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q, cp2sproc s p) of
+    (Some sq, Some sq', Some sp) \<Rightarrow> if (O_msg q m \<in> tainted s \<and> O_proc p \<notin> tainted s)
+                                    then update_s2ss_obj s (update_s2ss_obj s (s2ss s)
+                                                            (O_proc p) (S_proc sp False) (S_proc sp True))
+                                         (O_msgq q) (S_msgq sq) (S_msgq sq')
+                                    else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+  | _ \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "cq2smsgq s q")
+apply (drule current_has_smsgq', simp, simp)
+apply (case_tac "cq2smsgq (RecvMsg p q m # s) q")
+apply (drule current_has_smsgq', simp, simp)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp, simp+)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:update_s2ss_obj_def)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI2, rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, rule disjI2, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (frule co2sobj_smsgq_imp, erule exE)
+apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (frule co2sobj_sproc_imp, erule exE)
+apply (rule_tac x = "O_proc pa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI2,  simp add:co2sobj.simps cp2sproc_other)
+apply (rule notI, simp)
+apply (rule disjI2, simp, rule conjI, rule disjI2)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (rule notI, simp)
+apply (frule co2sobj_smsgq_imp, erule exE)
+apply (erule_tac x = "O_msgq qa" in allE, simp add:alive_recvmsg co2sobj_recvmsg split:if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*}, simp, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_msgq q", simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (frule_tac co2sobj_sproc_imp, erule exE)
+apply (rule_tac x = "O_proc pa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI2, rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, rule disjI2, simp, rule conjI)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (rule notI, simp)
+apply (frule co2sobj_sproc_imp, erule exE)
+apply (erule_tac x = "O_proc pa" in allE, simp add:co2sobj_recvmsg split:t_object.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (frule co2sobj_smsgq_imp, erule exE)
+apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI2, simp, rule conjI)
+apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
+apply (rule notI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule disjI2, simp, rule conjI, rule disjI2, rule conjI)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (rule notI, simp, frule co2sobj_sproc_imp, erule exE)
+apply (erule_tac x = "O_proc pa" in allE, simp add:co2sobj_recvmsg)
+apply (rule notI, simp, frule co2sobj_smsgq_imp, erule exE)
+apply (rotate_tac 12, erule_tac x = "O_msgq qa" in allE, simp add:co2sobj_recvmsg)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (tactic {*my_clarify_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (tactic {*my_clarify_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+
+apply (simp add:update_s2ss_obj_def)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (frule co2sobj_smsgq_imp, erule exE)
+apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI)
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp)
+apply (frule co2sobj_smsgq_imp, erule exE, erule_tac x = "O_msgq qa" in allE)
+apply (simp add:co2sobj_recvmsg)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+done
+
+end
+
+end
\ No newline at end of file