equal
deleted
inserted
replaced
78 done |
78 done |
79 |
79 |
80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' |
80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' |
81 cm2smsg_removemsgq cm2smsg_other |
81 cm2smsg_removemsgq cm2smsg_other |
82 |
82 |
|
83 (* |
83 lemma init_cm2smsg_has_smsg: |
84 lemma init_cm2smsg_has_smsg: |
84 "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm" |
85 "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm" |
85 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt) |
86 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt) |
|
87 *) |
86 |
88 |
87 lemma hd_set_prop1: |
89 lemma hd_set_prop1: |
88 "hd l \<notin> set l \<Longrightarrow> l = []" |
90 "hd l \<notin> set l \<Longrightarrow> l = []" |
89 by (case_tac l, auto) |
91 by (case_tac l, auto) |
90 |
92 |
260 Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), []) |
262 Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), []) |
261 | None \<Rightarrow> None)" |
263 | None \<Rightarrow> None)" |
262 apply (frule vd_cons, frule vt_grant_os) |
264 apply (frule vd_cons, frule vt_grant_os) |
263 apply (frule cqm2sms_createmsgq) |
265 apply (frule cqm2sms_createmsgq) |
264 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq |
266 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq |
265 split:option.splits if_splits dest:not_died_init_msgq) |
267 split:option.splits if_splits) |
266 done |
268 done |
267 |
269 |
268 lemma cq2smsg_sendmsg: |
270 lemma cq2smsg_sendmsg: |
269 "valid (SendMsg p q m # s) |
271 "valid (SendMsg p q m # s) |
270 \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := |
272 \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := |