diff -r aa1375b6c0eb -r 705e1e41faf7 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Tue Aug 27 08:50:53 2013 +0800
+++ b/Co2sobj_prop.thy	Wed Aug 28 08:59:12 2013 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop Alive_prop
 begin
 (*<*)
 
@@ -222,37 +222,148 @@
            | _ \<Rightarrow> None)
      else cqm2sms s q' ms)"
 apply (frule vt_grant_os, frule vd_cons)
-apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2)
-using cm2smsg_recvmsg1 cm2smsg_recvmsg2
-apply (auto split:if_splits option.splits)
+apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2 
+     dest!:current_has_sms')
+apply (case_tac "msgs_of_queue s q", simp)
+apply (frule_tac ms = "tl (msgs_of_queue s q)" in cqm2sms_recvmsg1)
+apply (drule_tac q = q in distinct_queue_msgs, simp+)
+apply (case_tac a, auto simp:cqm2sms.simps split:option.splits if_splits)
+done
 
+lemma cqm2sms_removemsgq:
+  "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk> 
+   \<Longrightarrow> cqm2sms (RemoveMsgq p q # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto simp:cqm2sms_simps2 cm2smsg_removemsgq split:option.splits if_splits)
+done
   
-lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg
+lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq
 
 (********************* cq2smsgq simpset ***********************) 
  
 lemma cq2smsgq_other: 
-  "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 
+  "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 
     \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 
    \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" 
+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_deleted_init_msg  dest!:current_has_sec') 
+            dest:not_deleted_init_msg) 
+done
+
+lemma cq2smsg_createmsgq:
+  "valid (CreateMsgq p q # s)
+   \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := 
+     case (sectxt_of_obj s (O_proc p)) of
+       Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), [])
+     | None     \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule cqm2sms_createmsgq)
+apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 
+  split:option.splits if_splits dest:not_deleted_init_msgq)
+done
 
+lemma cq2smsg_sendmsg:
+  "valid (SendMsg p q m # s) 
+   \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := 
+     case (cq2smsgq s q, sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of 
+       (Some (qi, sec, sms), Some msec) \<Rightarrow> 
+          Some (qi, sec, sms @ [(Created, msec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+     | _ \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (frule_tac q' = x in cqm2sms_sendmsg, simp)
+apply (auto simp:cq2smsgq_def sectxt_of_obj_simps  split:option.splits if_splits
+  dest!:current_has_sms' current_has_sec')
+done
+
+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')
+
+lemma current_has_smsgq':
+  "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
+by (auto dest:current_has_smsgq)
 
-  
-
+lemma cq2smsg_recvmsg:
+  "valid (RecvMsg p q m # s) 
+   \<Longrightarrow> cq2smsgq (RecvMsg p q m # s) = (cq2smsgq s) (q := 
+    case (cq2smsgq s q) of
+      Some (qi, sec, sms) \<Rightarrow> Some (qi, sec, tl sms)
+    | _ \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, frule_tac q' = x in cqm2sms_recvmsg, simp)
+apply (auto simp add:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits 
+  dest!:current_has_sec' current_has_sms' current_has_smsgq')
+done
 
-lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
+lemma cq2smsg_removemsgq:
+  "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>
+   \<Longrightarrow> cq2smsgq (RemoveMsgq p q # s) q' = cq2smsgq s q'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cq2smsgq_def sectxt_of_obj_simps cqm2sms_removemsgq split:if_splits option.splits 
+  dest!:current_has_sec' current_has_sms' current_has_smsgq')
+done
+
+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"
+apply (induct ms arbitrary:m sm sms)
+by (auto split:if_splits option.splits)
+
+lemma sm_in_sqsms_init:
+  "\<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"
+apply (induct ms arbitrary:m sm sms)
+apply (auto simp:cqm2sms.simps split:option.splits)
+done
 
 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
+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)
+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; 
+    cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>
+    \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" 
+    and p3: "q \<in> current_msgqs (e # s)" and p4: "valid (e # s)"
+    and p5: "cq2smsgq (e # s) q = Some (qi, qsec, sms)"
+    and p6: "cm2smsg (e # s) q m = Some sm" by auto
+  from p4 have os: "os_grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os)
+(*
+  from p1 have p1':
+    "\<And> m q qi qsec sms sm ms. \<lbrakk>m \<in> set ms; set ms \<subseteq> 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 "
+*)
+  show ?case using p2 p3 p4 p5 p6 vd os
+    apply (case_tac e)
+    apply (auto simp:cq2smsgq_simps cm2smsg_simps split:if_splits option.splits intro:p1)
 
+    apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)
+    apply (case_tac "q = nat2", simp)
+    apply (drule cq2smsg_createmsgq, simp, simp)
 
+    apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
+
+    apply (simp add:cq2smsgq_def split:option.splits)
+    apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)
+    apply (simp add:cqm2sms_recvmsg)
+    done
+qed
 
 (****************** cf2sfile path simpset ***************)
 
@@ -1489,10 +1600,6 @@
 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
   cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other 
 
-
-
-
-
 end
 
 (*<*)