--- a/tainted_vs_tainted_s.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/tainted_vs_tainted_s.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -105,7 +105,7 @@
   with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
     by (auto simp:obj2sobj.simps cp2sproc.simps)
   show ?case using p3 sproc os rc TP 
-    by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps 
+    by (auto simp:obj2sobj.simps cp2sproc.simps dest:not_deleted_imp_exists
             split:option.splits intro!:ts_cipc)
 next
   case (t_read f s p)
@@ -211,9 +211,8 @@
   next
     case (IPC i) 
     have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC
-      by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps 
-                          split:option.splits
-                          dest!:current_proc_has_role')
+      by (case_tac e, auto simp:obj2sobj.simps dest:not_deleted_imp_exists
+                          split:option.splits  dest!:current_proc_has_role')
     with IPC t_remain(2) show ?thesis by simp
   next
     case (Proc p) 
@@ -298,7 +297,7 @@
       have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk>
         \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
         using t_remain(2,3,4) os p5 Proc
-        by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp 
+        by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps dest:not_deleted_imp_exists 
                              simp del:cp2sproc.simps  split:option.splits) 
       ultimately show ?thesis using Proc
         by (case_tac e, auto simp del:obj2sobj.simps) 
@@ -588,7 +587,7 @@
   have valid: "valid (e # s)" 
   proof-
     have "os_grant s e"
-      using ev exp by (simp)
+      using ev exp by (simp add:ni_notin_curi)
     moreover have "rc_grant s e" 
       using ev ts'_cipc(3) SP
       by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1141,7 +1140,7 @@
   have valid: "valid (e # s)" 
   proof-
     have "os_grant s e"
-      using ev exp by (simp)
+      using ev exp by (simp add:ni_notin_curi)
     moreover have "rc_grant s e" 
       using ev ts'_cipc(3) SP
       by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)