--- a/Co2sobj_prop.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Co2sobj_prop.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -1,28 +1,248 @@
 (*<*)
 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
+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
 begin
 (*<*)
 
+ML {*
+fun print_ss ss =
+let
+val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
+in
+simps
+end
+*}
+
+
 context tainting_s begin
 
 (********************* 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"
+lemma cm2smsg_other: 
+  "\<lbrakk>valid (e # s); \<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> cm2smsg (e # s) = cm2smsg s"
 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
+unfolding cm2smsg_def
 apply (case_tac e)
-apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits
-intro:tainted.intro
+apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted 
+           split:t_object.splits option.splits if_splits 
+            dest:not_deleted_init_msg  dest!:current_has_sec')
+done
+
+lemma cm2smsg_sendmsg:
+  "valid (SendMsg p q m # s) \<Longrightarrow> cm2smsg (SendMsg p q m # s) = (\<lambda> q' m'. 
+     if (q' = q \<and> m' = m)
+     then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+             Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))
+           | _ \<Rightarrow> None)
+     else cm2smsg s q' m') "
+apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits
+  dest:not_deleted_init_msg  dest!:current_has_sec')
+done
+
+lemma cm2smsg_recvmsg1:
+  "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg2:
+  "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg1':
+  "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg2':
+  "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_removemsgq:
+  "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
+  cm2smsg_removemsgq cm2smsg_other
+
+lemma init_cm2smsg_has_smsg:
+  "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"
+by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)
+
+lemma hd_set_prop1:
+  "hd l \<notin> set l \<Longrightarrow> l = []"
+by (case_tac l, auto)
+
+lemma tl_set_prop1:
+  "a \<in> set (tl l) \<Longrightarrow> a \<in> set l"
+by (case_tac l, auto)
+
+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 (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_deleted_init_msg tl_set_prop1)
+done 
+
+lemma current_has_smsg':
+  "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)"
+by (auto dest:current_has_smsg)
+
+lemma cqm2sms_has_sms_aux:
+  "\<forall> m \<in> set ms. sectxt_of_obj s (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. cqm2sms s q ms = Some sms)"
+by (induct ms, auto split:option.splits simp:cm2smsg_def)
+
+lemma current_has_sms:
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sms. cqm2sms s q (msgs_of_queue s q) = Some sms"
+apply (rule cqm2sms_has_sms_aux)
+apply (auto dest:current_msg_has_sec)
+done
+
+lemma current_has_sms':
+  "\<lbrakk>cqm2sms s q (msgs_of_queue s q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
+by (auto dest:current_has_sms)
+
+(********************* cqm2sms simpset ***********************) 
+
+lemma cqm2sms_other:
+  "\<lbrakk>valid (e # s); \<forall> p m. 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> cqm2sms (e # s) = cqm2sms s"
+apply (rule ext, rule ext)
+apply (induct_tac xa, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac e)
+apply (auto split:option.splits dest:cm2smsg_other) 
+done
 
-lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+lemma cqm2sms_createmsgq:
+  "valid (CreateMsgq p q # s) \<Longrightarrow> cqm2sms (CreateMsgq p q # s) = (\<lambda> q' ms'. 
+     if (q' = q \<and> ms' = []) then Some []
+     else cqm2sms s q' ms')"
+apply (rule ext, rule ext)
+apply (frule vt_grant_os, frule vd_cons, induct_tac ms')
+apply (auto split:if_splits option.splits dest:cm2smsg_other)
+done
+
+lemma cqm2sms_2:
+  "cqm2sms s q (ms @ [m]) = 
+     (case (cqm2sms s q ms, cm2smsg s q m) of 
+       (Some sms, Some sm) \<Rightarrow> Some (sms @ [sm]) 
+     | _ \<Rightarrow> None)"
+apply (induct ms, simp split:option.splits)
+by (auto split:option.splits)
+
+lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2
+
+declare cqm2sms.simps [simp del]
+
+lemma cqm2sms_prop1:
+  "cqm2sms s q ms = None \<Longrightarrow> \<exists> m \<in> set ms. cm2smsg s q m = None"
+by (induct ms, auto simp:cqm2sms.simps split:option.splits)
+
+lemma cqm2sms_sendmsg1:
+  "\<lbrakk>valid (SendMsg p q m # s); m \<notin> set ms\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)
+done
+
+lemma cqm2sms_sendmsg2:
+  "\<lbrakk>valid (SendMsg p q m # s); q' \<noteq> q\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)
+done
+
+lemma cqm2sms_sendmsg3:
+  "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q ms' = 
+     (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+       (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+     | _ \<Rightarrow> None)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2 cqm2sms_sendmsg1)
+done
+
+lemma cqm2sms_sendmsg:
+  "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\<rbrakk> 
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms' = (
+     if (q' = q) 
+     then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+             (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+           | _ \<Rightarrow> None)
+     else cqm2sms s q' ms' )"
+apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3)
+done
+
+lemma cqm2sms_recvmsg1:
+  "\<lbrakk>valid (RecvMsg p q m # s); m \<notin> set ms\<rbrakk> 
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2')
+done
+
+lemma cqm2sms_recvmsg2:
+  "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk>
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1')
+done
+
+lemma cqm2sms_recvmsg:
+  "\<lbrakk>valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\<rbrakk>
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = (
+     if (q' = q) 
+     then (case (cqm2sms s q (msgs_of_queue s q)) of
+             Some sms \<Rightarrow> Some (tl sms)
+           | _ \<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)
+
+  
+lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg
+
+(********************* 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; 
+    \<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 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') 
 
 
-
-(********************* 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