--- a/no_shm_selinux/Delete_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Delete_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -112,19 +112,21 @@
 by (case_tac a, auto)
 *)
 
+(*
 lemma not_died_init_msgq:
   "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
 apply (induct s, simp)
 by (case_tac a, auto)
+*)
 
 lemma current_msg_imp_current_msgq:
   "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
-apply (induct s)
-apply (simp add:init_msgs_valid)
+apply (induct s, simp)
 apply (frule vd_cons, drule vt_grant_os)
 apply (case_tac a, auto split:if_splits)
 done
 
+(*
 lemma not_died_init_msg:
   "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"
 apply (induct s, simp)
@@ -132,13 +134,14 @@
 apply (case_tac a, auto dest:current_msg_imp_current_msgq)
 apply (case_tac "msgs_of_queue s q", simp+)
 done
+*)
 
 lemma not_died_imp_alive: (* init_alive obj;  *)
   "\<lbrakk>\<not> died obj s;  valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
 apply (case_tac obj)
 apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc
-  not_died_init_msg not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 (* not_died_init_shm *)
-  not_died_init_msgq 
+   not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 
+  (* not_died_init_shm not_died_init_msg not_died_init_msgq*) 
            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current
   current_msg_imp_current_msgq)
 done