--- a/Co2sobj_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Co2sobj_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -6,9 +6,35 @@
 
 context tainting_s begin
 
-(****************** cf2sfile path simpset ***************)
+(********************* cm2smsg simpset ***********************)
+
+lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
+apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
+apply (case_tac e)
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits
+intro:tainted.intro
+
+lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+
+
+
+(********************* cq2smsgq simpset ***********************) 
 
-thm cpfd2sfds_def
+lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
+apply (case_tac e) 
+by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
+
+lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
+
+
+lemma sm_in_sqsms:
+  "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms);
+    cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms"
+sorry
+
+
+
+(****************** cf2sfile path simpset ***************)
 
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
@@ -1243,24 +1269,6 @@
 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
   cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other 
 
-(********************* cm2smsg simpset ***********************)
-
-lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
-apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
-apply (case_tac e)
-apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits)
-
-lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
-
-
-
-(********************* cq2smsgq simpset ***********************) 
-
-lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
-apply (case_tac e) 
-by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
-
-lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other