--- a/no_shm_selinux/Co2sobj_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -38,8 +38,7 @@
      else cm2smsg s q' m') "
 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 
-  split:if_splits option.splits dest:not_died_init_msg
-  dest!:current_has_sec')
+  split:if_splits option.splits dest!:current_has_sec')
 done
 
 lemma cm2smsg_recvmsg1:
@@ -77,7 +76,7 @@
   split:if_splits option.splits)
 done
 
-lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
+lemmas cm2smsg_simps = cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
   cm2smsg_removemsgq cm2smsg_other
 
 (*
@@ -97,11 +96,11 @@
 lemma current_has_smsg:
   "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sm. cm2smsg s q m = Some sm"
 apply (induct s)
-apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg)
+apply (simp add:msgs_of_queue.simps current_msgqs.simps)
 
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits
-  dest!:current_has_sec' hd_set_prop1 dest:not_died_init_msg tl_set_prop1)
+  dest!:current_has_sec' hd_set_prop1 dest:tl_set_prop1)
 done 
 
 lemma current_has_smsg':
@@ -251,8 +250,7 @@
 apply (frule cqm2sms_other, simp+)
 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) 
 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps 
-           split:t_object.splits option.splits if_splits 
-            dest:not_died_init_msg) 
+           split:t_object.splits option.splits if_splits)
 done
 
 lemma cq2smsg_createmsgq:
@@ -283,7 +281,8 @@
 
 lemma current_has_smsgq:
   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"
-by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')
+by (auto simp:cq2smsgq_def split:option.splits 
+  dest!:current_has_sec' current_has_sms' dest:current_has_sec)
 
 lemma current_has_smsgq':
   "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
@@ -311,6 +310,7 @@
 
 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq
 
+(*
 lemma sm_in_sqsms_init_aux:
   "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; 
     init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
@@ -321,6 +321,7 @@
   "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; 
     init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
 by (simp add:sm_in_sqsms_init_aux)
+*)
 
 lemma cqm2sms_prop0:
   "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
@@ -334,8 +335,7 @@
 proof (induct s arbitrary:m q qi qsec sms sm)
   case Nil
   thus ?case 
-    by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 
-           split:option.splits)
+    by (simp split:option.splits)
 next
   case (Cons e s)
   hence p1:"\<And> m q qi qsec sms sm. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s;