36 Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s)) |
36 Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s)) |
37 | _ \<Rightarrow> None) |
37 | _ \<Rightarrow> None) |
38 else cm2smsg s q' m') " |
38 else cm2smsg s q' m') " |
39 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) |
39 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) |
40 apply (auto simp:cm2smsg_def sectxt_of_obj_simps |
40 apply (auto simp:cm2smsg_def sectxt_of_obj_simps |
41 split:if_splits option.splits dest:not_died_init_msg |
41 split:if_splits option.splits dest!:current_has_sec') |
42 dest!:current_has_sec') |
|
43 done |
42 done |
44 |
43 |
45 lemma cm2smsg_recvmsg1: |
44 lemma cm2smsg_recvmsg1: |
46 "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" |
45 "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" |
47 apply (frule vd_cons, frule vt_grant_os, rule ext) |
46 apply (frule vd_cons, frule vt_grant_os, rule ext) |
75 apply (frule vd_cons, frule vt_grant_os, rule ext) |
74 apply (frule vd_cons, frule vt_grant_os, rule ext) |
76 apply (auto simp:cm2smsg_def sectxt_of_obj_simps |
75 apply (auto simp:cm2smsg_def sectxt_of_obj_simps |
77 split:if_splits option.splits) |
76 split:if_splits option.splits) |
78 done |
77 done |
79 |
78 |
80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' |
79 lemmas cm2smsg_simps = cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' |
81 cm2smsg_removemsgq cm2smsg_other |
80 cm2smsg_removemsgq cm2smsg_other |
82 |
81 |
83 (* |
82 (* |
84 lemma init_cm2smsg_has_smsg: |
83 lemma init_cm2smsg_has_smsg: |
85 "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm" |
84 "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm" |
95 by (case_tac l, auto) |
94 by (case_tac l, auto) |
96 |
95 |
97 lemma current_has_smsg: |
96 lemma current_has_smsg: |
98 "\<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" |
97 "\<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" |
99 apply (induct s) |
98 apply (induct s) |
100 apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg) |
99 apply (simp add:msgs_of_queue.simps current_msgqs.simps) |
101 |
100 |
102 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
101 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
103 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits |
102 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits |
104 dest!:current_has_sec' hd_set_prop1 dest:not_died_init_msg tl_set_prop1) |
103 dest!:current_has_sec' hd_set_prop1 dest:tl_set_prop1) |
105 done |
104 done |
106 |
105 |
107 lemma current_has_smsg': |
106 lemma current_has_smsg': |
108 "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)" |
107 "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)" |
109 by (auto dest:current_has_smsg) |
108 by (auto dest:current_has_smsg) |
249 \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> |
248 \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> |
250 \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" |
249 \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" |
251 apply (frule cqm2sms_other, simp+) |
250 apply (frule cqm2sms_other, simp+) |
252 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) |
251 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) |
253 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps |
252 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps |
254 split:t_object.splits option.splits if_splits |
253 split:t_object.splits option.splits if_splits) |
255 dest:not_died_init_msg) |
|
256 done |
254 done |
257 |
255 |
258 lemma cq2smsg_createmsgq: |
256 lemma cq2smsg_createmsgq: |
259 "valid (CreateMsgq p q # s) |
257 "valid (CreateMsgq p q # s) |
260 \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := |
258 \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := |
281 dest!:current_has_sms' current_has_sec') |
279 dest!:current_has_sms' current_has_sec') |
282 done |
280 done |
283 |
281 |
284 lemma current_has_smsgq: |
282 lemma current_has_smsgq: |
285 "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq" |
283 "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq" |
286 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms') |
284 by (auto simp:cq2smsgq_def split:option.splits |
|
285 dest!:current_has_sec' current_has_sms' dest:current_has_sec) |
287 |
286 |
288 lemma current_has_smsgq': |
287 lemma current_has_smsgq': |
289 "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
288 "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
290 by (auto dest:current_has_smsgq) |
289 by (auto dest:current_has_smsgq) |
291 |
290 |
309 dest!:current_has_sec' current_has_sms' current_has_smsgq') |
308 dest!:current_has_sec' current_has_sms' current_has_smsgq') |
310 done |
309 done |
311 |
310 |
312 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq |
311 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq |
313 |
312 |
|
313 (* |
314 lemma sm_in_sqsms_init_aux: |
314 lemma sm_in_sqsms_init_aux: |
315 "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; |
315 "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; |
316 init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
316 init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
317 apply (induct ms arbitrary:m sm sms) |
317 apply (induct ms arbitrary:m sm sms) |
318 by (auto split:if_splits option.splits) |
318 by (auto split:if_splits option.splits) |
319 |
319 |
320 lemma sm_in_sqsms_init: |
320 lemma sm_in_sqsms_init: |
321 "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; |
321 "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; |
322 init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
322 init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
323 by (simp add:sm_in_sqsms_init_aux) |
323 by (simp add:sm_in_sqsms_init_aux) |
|
324 *) |
324 |
325 |
325 lemma cqm2sms_prop0: |
326 lemma cqm2sms_prop0: |
326 "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
327 "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
327 apply (induct ms arbitrary:m sm sms) |
328 apply (induct ms arbitrary:m sm sms) |
328 apply (auto simp:cqm2sms.simps split:option.splits) |
329 apply (auto simp:cqm2sms.simps split:option.splits) |
332 "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms); |
333 "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms); |
333 cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
334 cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
334 proof (induct s arbitrary:m q qi qsec sms sm) |
335 proof (induct s arbitrary:m q qi qsec sms sm) |
335 case Nil |
336 case Nil |
336 thus ?case |
337 thus ?case |
337 by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init |
338 by (simp split:option.splits) |
338 split:option.splits) |
|
339 next |
339 next |
340 case (Cons e s) |
340 case (Cons e s) |
341 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; |
341 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; |
342 cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk> |
342 cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk> |
343 \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" |
343 \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" |