--- a/simple_selinux/Delete_prop.thy	Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/Delete_prop.thy	Tue Dec 03 22:42:48 2013 +0800
@@ -106,11 +106,6 @@
    \<Longrightarrow> \<not> deleted (O_proc p) s"
 by (auto dest:not_deleted_init_udp_aux)
 
-lemma not_deleted_init_shm:
-  "\<lbrakk>\<not> deleted (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
-apply (induct s, simp)
-by (case_tac a, auto)
-
 lemma not_deleted_init_msgq:
   "\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
 apply (induct s, simp)
@@ -136,7 +131,7 @@
   "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
 apply (case_tac obj)
 apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc
-  not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm 
+  not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 
   not_deleted_init_msgq 
            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 
   current_msg_imp_current_msgq)
@@ -189,11 +184,6 @@
 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 
          dest:is_udp_sock_imp_curernt_proc)
 
-lemma not_deleted_cur_shm_app:
-  "\<lbrakk>\<not> deleted (O_shm h) (s' @ s); h \<in> current_shms s\<rbrakk> \<Longrightarrow> h \<in> current_shms (s' @ s)"
-apply (induct s', simp, simp add:cons_app_simp_aux)
-by (case_tac a, auto)
-
 lemma not_deleted_cur_msgq_app:
   "\<lbrakk>\<not> deleted (O_msgq q) (s' @ s); q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (s' @ s)"
 apply (induct s', simp, simp add:cons_app_simp_aux)
@@ -213,7 +203,7 @@
 apply (case_tac obj)
 apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app
   not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app 
-  not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app
+  not_deleted_cur_udp_app not_deleted_cur_msgq_app
            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 
   current_msg_imp_current_msgq)
 done