--- a/no_shm_selinux/Enrich.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -54,13 +54,13 @@
 
 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set"
 where
-  "all_msgqs [] = init_msgqs"
+  "all_msgqs [] = {}"
 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}"
 | "all_msgqs (e # s) = all_msgqs s"
 
 fun all_msgs:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg set"
 where
-  "all_msgs [] q = set (init_msgs_of_queue q)"
+  "all_msgs [] q = {}"
 | "all_msgs (CreateMsgq p q # s) q' = (if q' = q then {} else all_msgs s q')"
 | "all_msgs (SendMsg p q m # s) q' = (if q' = q then all_msgs s q \<union> {m} else all_msgs s q')"
 | "all_msgs (_ # s) q' = all_msgs s q'"
@@ -114,11 +114,6 @@
 apply (case_tac a, auto)
 done
 
-lemma not_all_msgqs_prop2:
-  "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs"
-apply (induct s, simp)
-by (case_tac a, auto)
-
 lemma not_all_msgqs_prop3:
   "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"
 apply (induct s, simp)
@@ -1071,7 +1066,7 @@
       apply (erule_tac x = "E_msg q m" in allE)
       apply (case_tac obj', auto dest:not_all_msgqs_prop3)
       done
-    have "os_grant s' e" using p_in q_in m_not_in
+    have "os_grant s' e" using p_in q_in m_not_in sms_remain os
       by (simp add:SendMsg)
     moreover have "grant s' e" 
     proof-
@@ -1133,9 +1128,6 @@
         apply (case_tac "msgs_of_queue s q", simp)
         apply (simp add:cqm2sms.simps split:option.splits)
         apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]
-        apply (case_tac "msgs_of_queue s q", simp)
-        apply (simp add:cqm2sms.simps split:option.splits)
-        apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]
         done
       show ?thesis using p1' p2' p3' grant p1 p2 p3
         by (simp add:RecvMsg)