--- a/Sectxt_prop.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Sectxt_prop.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -600,8 +600,92 @@
            dest!:current_has_type' current_proc_has_role' current_has_user')
 done
 
+lemma sec_kill: 
+  "valid (Kill p p' # s) \<Longrightarrow> sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_ptrace:
+  "valid (Ptrace p p' # s) \<Longrightarrow> sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_exit:
+  "valid (Exit p # s) \<Longrightarrow> sectxt_of_obj (Exit p # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_readfile:
+  "valid (ReadFile p fd # s) \<Longrightarrow> sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_writefile:
+  "valid (WriteFile p fd # s) \<Longrightarrow> sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_unlink:
+  "valid (UnLink p f # s) \<Longrightarrow> sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_Rmdir:
+  "valid (Rmdir p f # s) \<Longrightarrow> sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_truncate:
+  "valid (Truncate p f len # s) \<Longrightarrow> sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvmsg:
+  "valid (RecvMsg p q m # s) \<Longrightarrow> sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_removemsgq:
+  "valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_detach:
+  "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_sendsock:
+  "valid (SendSock p fd # s) \<Longrightarrow> sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvsock:
+  "valid (RecvSock p fd # s) \<Longrightarrow> sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_shutdown:
+  "valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
 lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg
-  sec_createshm sec_createsock sec_accept sec_clone sec_others (* init_sectxt_prop *)
+  sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile
+  sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq
+  sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock
+  sec_recvsock sec_shutdown
+(* init_sectxt_prop *)
 
 (**************** get_parentfs_ctxts simpset **************)