--- a/no_shm_selinux/Init_prop.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Init_prop.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -334,13 +334,13 @@
 lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp
 (*
 lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp
-*)
 lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp
 lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>
   \<Longrightarrow> init_alive (O_msg q m)" by simp
+*)
 
 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 
-  init_alive_tcp init_alive_udp init_alive_node  init_alive_msgq init_alive_msg (*init_alive_shm*)
+  init_alive_tcp init_alive_udp init_alive_node (*init_alive_msgq init_alive_msg*) (*init_alive_shm*)
 
 
 lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"
@@ -541,6 +541,7 @@
 by (rule notI, drule init_shm_has_ctxt, simp)
 *)
 
+(*
 lemma init_msgq_has_ctxt:
   "q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"
 apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -560,6 +561,7 @@
 lemma init_msg_has_ctxt':
   "init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"
 by (auto dest:init_msg_has_ctxt)
+*)
 
 lemma init_rootf_has_ctxt:
   "\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"
@@ -571,12 +573,12 @@
 using init_rootf_has_ctxt by auto
 
 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt
-  init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) init_msgq_has_ctxt
-  init_msg_has_ctxt init_rootf_has_ctxt
+  init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) (* init_msgq_has_ctxt
+  init_msg_has_ctxt*) init_rootf_has_ctxt
 
 lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'
-  init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) init_msgq_has_ctxt'
-  init_msg_has_ctxt' init_rootf_has_ctxt'
+  init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) (*init_msgq_has_ctxt'
+  init_msg_has_ctxt'*) init_rootf_has_ctxt'
 
 lemma sec_of_root_valid:
   "init_sectxt_of_obj (O_dir []) = Some sec_of_root"
@@ -668,6 +670,7 @@
 apply (simp add:init_cp2sproc_def)
 by (case_tac sec, simp+)
 
+(*
 lemma init_cqm2sms_has_sms_aux:
   "\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"
 by (induct ms, auto split:option.splits simp:init_cm2smsg_def)
@@ -682,6 +685,7 @@
 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
 apply (simp add:init_cq2smsgq_def)
 by (case_tac sec, simp+)
+*)
 
 lemma cf2sfile_nil_prop:
   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
@@ -758,6 +762,7 @@
 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cpfd2sfds_nil_prop (*cph2spshs_nil_prop*)
          split:option.splits)
 
+(*
 lemma msg_has_sec_imp_init: 
   "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
 apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -783,14 +788,15 @@
   "cq2smsgq [] q = init_cq2smsgq q"
 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
             intro:msgq_has_sec_imp_init split:option.splits)
+*)
 
 lemma co2sobj_nil_prop:
   "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
 apply (case_tac obj)
-apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 
+apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop 
                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *)
-                     same_inode_nil_prop  cm2smsg_nil_prop 
+                     same_inode_nil_prop  (*cm2smsg_nil_prop *)
             dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)