diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/S2ss_prop.thy
--- a/simple_selinux/S2ss_prop.thy	Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/S2ss_prop.thy	Tue Dec 03 22:42:48 2013 +0800
@@ -10,7 +10,7 @@
 
 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> h. obj = O_shm h \<Longrightarrow> P (O_shm h);
+    \<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"
 by (case_tac obj, auto)
@@ -25,11 +25,11 @@
   "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)}
+             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)}
+             (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)
 
@@ -42,15 +42,15 @@
 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 tainted_eq_Tainted split:if_splits)
+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 add:tainted_eq_Tainted)
+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 tainted_eq_Tainted cp2sproc_execve)
+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)
@@ -62,45 +62,45 @@
 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 add:tainted_eq_Tainted)
+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 add:tainted_eq_Tainted, (simp split:option.splits)+)
+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 add:tainted_eq_Tainted)
+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 add:tainted_eq_Tainted, 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 shms # s)\<rbrakk>
-   \<Longrightarrow> alive (Clone p p' fds shms # s) obj"
+  "\<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 shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = (
-     case (cp2sproc (Clone p p' fds shms # s) p') of
-       Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)}
+  "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 add:tainted_eq_Tainted)
-apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+)
+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 add:tainted_eq_Tainted, rule disjI2)
+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 add:tainted_eq_Tainted)
-apply (rule impI, rule notI, drule Tainted_in_current, 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)
@@ -108,46 +108,6 @@
 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 tainted_eq_Tainted 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 tainted_eq_Tainted 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>
@@ -156,14 +116,14 @@
 apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
 done  
 
-lemma Tainted_ptrace':
-  "valid s \<Longrightarrow> 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'' | p''. info_flow_shm s p' p''}
-      else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
-           then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
-                else Tainted s)"
-using info_flow_shm_Tainted by auto
+lemma tainted_ptrace':
+  "valid s \<Longrightarrow> 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'' | p''. info_flow_shm s p' p''}
+      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
+           then tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
+                else tainted s)"
+using info_flow_shm_tainted 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);
@@ -177,25 +137,25 @@
 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>
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> tainted s; O_proc p' \<notin> tainted s\<rbrakk>
    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"
 unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def 
 apply (frule vd_cons, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
 apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (case_tac "info_flow_shm s p' pa")
 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (rule_tac x = a in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (rule UnI1, simp)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits)
 apply (erule_tac x = pa in allE, simp)
 
 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
@@ -214,17 +174,17 @@
 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (clarsimp simp cp2sproc_other split:option.splits)
 apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
 apply (rule_tac x = "O_proc p'a" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 
 apply (rule_tac x = obj in exI,
        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
@@ -237,29 +197,29 @@
 
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs)
 done
 
 lemma s2ss_ptrace2:
-  "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> tainted s; O_proc p \<notin> tainted s\<rbrakk>
    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"
 unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def
 apply (frule vd_cons, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
 apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (case_tac "info_flow_shm s p pa")
 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (rule_tac x = a in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (rule UnI1, simp)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits)
 apply (erule_tac x = pa in allE, simp)
 
 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
@@ -278,17 +238,17 @@
 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (clarsimp simp cp2sproc_other split:option.splits)
 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
 apply (rule_tac x = "O_proc p'a" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
 
 apply (rule_tac x = obj in exI,
        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
@@ -301,11 +261,11 @@
 
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs)
 done
 
 lemma s2ss_ptrace3:
-  "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk>
+  "\<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, rule set_eqI, rule iffI)
@@ -313,22 +273,22 @@
 apply (rule_tac x = obj in exI)
 apply (frule alive_other, simp+)
 apply (frule_tac obj = obj in co2sobj_ptrace, simp)
-apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits
-  intro:info_flow_shm_Tainted)[1]
+apply (auto simp split:t_object.splits option.splits if_splits
+  intro:info_flow_shm_tainted)[1]
 
 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 simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits 
-  intro:info_flow_shm_Tainted)
+apply (auto simp split:t_object.splits option.splits if_splits 
+  intro:info_flow_shm_tainted)
 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) 
+     if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 
      then update_s2ss_shm s p'
-     else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+     else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
           then update_s2ss_shm s p
           else s2ss s                                   )"
 apply (frule vt_grant_os, frule vd_cons)
@@ -351,15 +311,15 @@
 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 tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+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 tainted_eq_Tainted alive_kill
+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 tainted_eq_Tainted alive_kill
+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)+
 
@@ -367,18 +327,18 @@
 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 tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:option.splits)
+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 tainted_eq_Tainted alive_kill
+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 tainted_eq_Tainted alive_kill
+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
@@ -399,15 +359,15 @@
 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 tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+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 tainted_eq_Tainted alive_exit
+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 tainted_eq_Tainted alive_exit
+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)+
 
@@ -415,18 +375,18 @@
 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 tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:option.splits)
+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 tainted_eq_Tainted alive_exit
+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 tainted_eq_Tainted alive_exit
+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
@@ -443,7 +403,7 @@
   "\<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))
+              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)
@@ -455,11 +415,11 @@
   "\<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))
+              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))
+                   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)
@@ -607,7 +567,7 @@
 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)
+       Some f \<Rightarrow> if (O_file f \<in> tainted s)
                  then update_s2ss_shm s p
                  else s2ss s
      | _      \<Rightarrow> {})"
@@ -618,18 +578,18 @@
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
 apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
 apply (case_tac "info_flow_shm s p pa")
 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (rule_tac x = ab in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:cp2sproc_other split:option.splits)
 apply (rule UnI1, simp)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
 apply (erule_tac x = pa in allE, simp)
 
 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
@@ -644,17 +604,17 @@
 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_eq_tainted cp2sproc_other co2sobj.simps split:option.splits)
 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
 apply (rule_tac x = "O_proc p'" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits)
 
 apply (rule_tac x = obj in exI,
        auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
@@ -667,7 +627,7 @@
 
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs co2sobj.simps)
 
 
 apply (rule impI, rule impI)
@@ -695,18 +655,18 @@
 
 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> 
+    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:tainted_eq_Tainted same_inodes_Tainted)+
+apply (case_tac "O_proc p \<in> tainted s")
+apply (simp 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)
+       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}
@@ -744,7 +704,7 @@
 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 tainted_eq_Tainted same_inodes_Tainted)
+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)
@@ -754,8 +714,8 @@
 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 tainted_eq_Tainted same_inodes_Tainted)
-apply (case_tac "O_proc p \<in> Tainted s", simp, simp)
+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)
@@ -769,7 +729,7 @@
 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:tainted_eq_Tainted same_inode_files_prop5)
+apply (erule_tac x = list in allE, simp 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)
@@ -789,7 +749,7 @@
 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 tainted_eq_Tainted same_inodes_Tainted)
+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)
@@ -818,7 +778,7 @@
   "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)}"
+     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
@@ -827,7 +787,7 @@
       then ss
       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
            then update_s2ss_sfile_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)"
+           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; 
@@ -921,14 +881,14 @@
                          (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)
+                                 (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)))
+                               (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)
@@ -942,12 +902,12 @@
 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted 
+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")
@@ -965,58 +925,58 @@
 apply (tactic {*my_seteq_tac 1*})
 apply simp
 apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted)
+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)
@@ -1030,14 +990,14 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+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)
@@ -1050,7 +1010,7 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule impI, rule conjI, rule impI)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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)
@@ -1069,16 +1029,16 @@
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 apply (rule impI)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+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)
@@ -1095,34 +1055,34 @@
 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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)
@@ -1130,16 +1090,16 @@
 apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
 apply (simp add:alive_simps)+
 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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)
@@ -1147,7 +1107,7 @@
 apply (rule_tac x = "O_file f'" in exI)
 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
-apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule 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)
@@ -1162,15 +1122,15 @@
 apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
 apply (simp add:alive_simps)+
 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (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 tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
 apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+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)
@@ -1178,7 +1138,7 @@
 apply (rule_tac x = "O_file f'" in exI)
 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
-apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule 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)
@@ -1191,7 +1151,7 @@
 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 tainted_eq_Tainted)
+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)
@@ -1205,18 +1165,18 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+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 tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
+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)
@@ -1233,47 +1193,47 @@
 
 apply (erule bexE, erule conjE)
 apply (simp add:update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+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 (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (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 tainted_eq_Tainted)
+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)
@@ -1287,25 +1247,25 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp)
 apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits)
-apply (erule_tac x= f in allE, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted) 
+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)
@@ -1318,11 +1278,11 @@
 apply (rule impI, rule conjI, rule impI)
 
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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)
@@ -1331,10 +1291,10 @@
 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 tainted_eq_Tainted)
+apply (simp add:is_file_simps co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps)
-apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+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)+
@@ -1346,23 +1306,23 @@
 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+apply (simp add:is_file_simps co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps)
-apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+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)+
@@ -1375,26 +1335,26 @@
 
 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
 apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)[1]
+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)
@@ -1402,26 +1362,26 @@
 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 tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted same_inodes_Tainted)
+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)
@@ -1433,20 +1393,20 @@
 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 tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+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 tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted same_inodes_Tainted)
+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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
@@ -1459,40 +1419,40 @@
 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 tainted_eq_Tainted split:if_splits)
+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 tainted_eq_Tainted)
+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:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted 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:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted 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 tainted_eq_Tainted split:if_splits)
+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:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted 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 tainted_eq_Tainted)
+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:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
+                simp:tainted_eq_tainted co2sobj.simps alive_co2sobj_closefd1)
 done
 
 lemma alive_co2sobj_unlink:
@@ -1525,13 +1485,13 @@
 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 tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)
+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 tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps split:t_object.splits if_splits)
 
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
 
@@ -1545,7 +1505,7 @@
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1)
 apply (simp add:co2sobj_unlink)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+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)
@@ -1556,7 +1516,7 @@
 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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 
+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)
@@ -1566,13 +1526,13 @@
 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 tainted_eq_Tainted)
+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 tainted_eq_Tainted is_file_simps cf2sfiles_prop same_inodes_Tainted)
+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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1591,12 +1551,12 @@
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1)
 apply (simp add:co2sobj_unlink)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+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 tainted_eq_Tainted)
-apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps tainted_eq_Tainted)
+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)
 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 is_dir_simps)
@@ -1607,16 +1567,16 @@
 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 tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 
+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 tainted_eq_Tainted)
+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 tainted_eq_Tainted)
+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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1668,7 +1628,7 @@
 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:tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp: 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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1687,7 +1647,7 @@
 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 tainted_eq_Tainted)
+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)
@@ -1698,7 +1658,7 @@
 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 tainted_eq_Tainted)
+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)
@@ -1783,97 +1743,9 @@
 where
  "update_s2ss_sfile 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 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_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 tainted_eq_Tainted
-  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 tainted_eq_Tainted 
-  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)
-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 tainted_eq_Tainted 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_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 tainted_eq_Tainted
-  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 tainted_eq_Tainted 
-  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 tainted_eq_Tainted)
-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 (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 tainted_eq_Tainted 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_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-done
+       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 same_inode_files_prop12:
   "is_file s f \<Longrightarrow> f \<in> same_inode_files s f "
@@ -1889,7 +1761,7 @@
                \<union> {S_file (cf2sfiles s f) True}"
 
 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)
+  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)
@@ -1900,11 +1772,11 @@
 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 tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
+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 tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+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)
@@ -1915,14 +1787,14 @@
 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 tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
+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 tainted_eq_Tainted cf2sfiles_prop)
+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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -1932,12 +1804,12 @@
 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 tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
+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 tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+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)
@@ -1954,12 +1826,12 @@
 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 tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
+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 tainted_eq_Tainted cf2sfiles_prop)
+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)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -1969,13 +1841,13 @@
 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 tainted_eq_Tainted)
-apply (case_tac "O_proc p \<in> Tainted s", simp add:same_inodes_Tainted)
+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 tainted_eq_Tainted same_inodes_Tainted)
+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) = 
@@ -2116,17 +1988,17 @@
 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
 
 lemma s2ss_shm_no_bk_elim':
-  "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> Tainted s;
+  "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> tainted s;
     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 x"
-apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)
+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_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) of
-    (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+    (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> tainted s \<and> O_proc p \<notin> tainted s)
                           then update_s2ss_obj s (update_s2ss_shm s p) (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> {})"
@@ -2175,7 +2047,7 @@
   split:t_object.splits if_splits option.splits)
 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
 apply (erule exE|erule conjE)+
 apply (rule_tac x = "O_proc p'" in exI)
@@ -2184,7 +2056,7 @@
 apply (case_tac "info_flow_shm s p pa", simp)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
 apply (rule_tac x = obj in exI)
@@ -2203,7 +2075,7 @@
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
 apply (simp add:co2sobj.simps)
 apply (simp add:co2sobj.simps)
 apply (case_tac "msgs_of_queue s q", simp, simp)
@@ -2219,7 +2091,7 @@
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
   split:t_object.splits if_splits option.splits)
-apply (auto simp:co2sobj.simps is_file_simps is_dir_simps tainted_eq_Tainted info_flow_shm_Tainted)[1]
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps info_flow_shm_tainted)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (tactic {*my_seteq_tac 1*})
@@ -2228,14 +2100,14 @@
 apply (rule disjI2)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule DiffI, rule UnI1, simp)
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (erule s2ss_shm_no_bk_intro2, simp, simp)
 apply (rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
 apply (rule_tac x = ab in exI, simp)
 apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2272,7 +2144,7 @@
   split:t_object.splits if_splits option.splits)
 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
 apply (erule exE|erule conjE)+
 apply (rule_tac x = "O_proc p'" in exI)
@@ -2281,7 +2153,7 @@
 apply (case_tac "info_flow_shm s p pa", simp)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
 apply (rule_tac x = obj in exI)
@@ -2301,7 +2173,7 @@
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
   split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
 apply (simp add:co2sobj_recvmsg)
 apply (simp add:alive_recvmsg split:if_splits)
 apply (erule_tac x = obj in allE, simp split:t_object.splits if_splits option.splits)
@@ -2322,7 +2194,7 @@
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
 apply (rule conjI)
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (tactic {*my_seteq_tac 1*})
@@ -2331,14 +2203,14 @@
 apply (rule disjI2)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule DiffI, rule UnI1, simp)
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (erule s2ss_shm_no_bk_intro2, simp, simp)
 apply (rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
 apply (rule_tac x = ab in exI, simp)
 apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2374,7 +2246,7 @@
   split:t_object.splits if_splits option.splits)
 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
 apply (erule exE|erule conjE)+
 apply (rule_tac x = "O_proc p'" in exI)
@@ -2383,7 +2255,7 @@
 apply (case_tac "info_flow_shm s p pa", simp)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
 apply (rule_tac x = obj in exI)
@@ -2403,7 +2275,7 @@
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
   split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = "O_msgq q" in exI)
 apply (simp add:co2sobj.simps)
@@ -2418,7 +2290,7 @@
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
 apply (rule conjI)
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (tactic {*my_seteq_tac 1*})
@@ -2427,15 +2299,15 @@
 apply (rule disjI2)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
 apply (rule DiffI, rule DiffI, rule UnI1, simp)
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
 apply (erule s2ss_shm_no_bk_intro2, simp, simp)
 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule DiffI, rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
 apply (rule_tac x = ab in exI, simp)
 apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2475,7 +2347,7 @@
 apply (case_tac "obj = O_msgq q")
 apply (simp add:co2sobj.simps)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
 apply (erule exE|erule conjE)+
 apply (rule_tac x = "O_proc p'" in exI)
@@ -2484,7 +2356,7 @@
 apply (case_tac "info_flow_shm s p pa", simp)
 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
 apply (rule_tac x = obj in exI)
@@ -2504,7 +2376,7 @@
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
   split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
 apply (rule notI, simp)
 apply (frule co2sobj_smsgq_imp, erule exE, simp)
 apply (simp add:co2sobj_recvmsg)
@@ -2521,7 +2393,7 @@
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
 apply (rule conjI)
 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted intro: info_flow_shm_Tainted 
+apply (auto simp:co2sobj.simps intro: info_flow_shm_tainted 
 split:t_object.splits option.splits if_splits)[1]
 done