diff -r 4d25a9919688 -r 4294abb1f38c all_sobj_prop.thy
--- a/all_sobj_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/all_sobj_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -248,8 +248,10 @@
         by (auto split:option.splits if_splits simp:obj2sobj.simps 
                   dest:current_proc_has_sproc)
       have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os
-        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
-        apply (rule ai_cipc) using SP sproc rc ev by auto
+        apply (auto simp:obj2sobj.simps split:option.splits)
+        apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+)      
+        using SP sproc rc ev 
+        by (auto intro:ai_cipc)
       with True show ?thesis by simp
     next
       case False 
@@ -271,7 +273,7 @@
         by (auto split:option.splits if_splits simp:obj2sobj.simps 
                   dest:current_proc_has_sproc)
       have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os 
-        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+        apply (auto simp:obj2sobj.simps split:option.splits)
         apply (rule ap_crole) using SP sproc rc ev srproc by auto
       with True show ?thesis by simp
     next
@@ -652,7 +654,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1179,7 +1181,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1305,7 +1307,7 @@
     have valid: "valid (e#\<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau exp by (simp)
+        using ev tau exp by (simp add:np_notin_curp)
       moreover have "rc_grant \<tau> e" 
         using ev tau ap'_crole(3) SPab 
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1420,7 +1422,7 @@
     have valid: "valid (e#\<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau exp ap'_chown(3) by (simp)
+        using ev tau exp ap'_chown(3) by (simp add:np_notin_curp)
       moreover have "rc_grant \<tau> e" 
         using ev tau ap'_chown(5) SPab 
         by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
@@ -1927,7 +1929,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)