52 | "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)" |
52 | "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)" |
53 | "all_fds (_ # s) = all_fds s" |
53 | "all_fds (_ # s) = all_fds s" |
54 |
54 |
55 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set" |
55 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set" |
56 where |
56 where |
57 "all_msgqs [] = init_msgqs" |
57 "all_msgqs [] = {}" |
58 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}" |
58 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}" |
59 | "all_msgqs (e # s) = all_msgqs s" |
59 | "all_msgqs (e # s) = all_msgqs s" |
60 |
60 |
61 fun all_msgs:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg set" |
61 fun all_msgs:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg set" |
62 where |
62 where |
63 "all_msgs [] q = set (init_msgs_of_queue q)" |
63 "all_msgs [] q = {}" |
64 | "all_msgs (CreateMsgq p q # s) q' = (if q' = q then {} else all_msgs s q')" |
64 | "all_msgs (CreateMsgq p q # s) q' = (if q' = q then {} else all_msgs s q')" |
65 | "all_msgs (SendMsg p q m # s) q' = (if q' = q then all_msgs s q \<union> {m} else all_msgs s q')" |
65 | "all_msgs (SendMsg p q m # s) q' = (if q' = q then all_msgs s q \<union> {m} else all_msgs s q')" |
66 | "all_msgs (_ # s) q' = all_msgs s q'" |
66 | "all_msgs (_ # s) q' = all_msgs s q'" |
67 |
67 |
68 fun all_files:: "t_state \<Rightarrow> t_file set" |
68 fun all_files:: "t_state \<Rightarrow> t_file set" |
111 "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p" |
111 "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p" |
112 apply (induct s, rule notI, simp) |
112 apply (induct s, rule notI, simp) |
113 apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI) |
113 apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI) |
114 apply (case_tac a, auto) |
114 apply (case_tac a, auto) |
115 done |
115 done |
116 |
|
117 lemma not_all_msgqs_prop2: |
|
118 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs" |
|
119 apply (induct s, simp) |
|
120 by (case_tac a, auto) |
|
121 |
116 |
122 lemma not_all_msgqs_prop3: |
117 lemma not_all_msgqs_prop3: |
123 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s" |
118 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s" |
124 apply (induct s, simp) |
119 apply (induct s, simp) |
125 by (case_tac a, auto) |
120 by (case_tac a, auto) |
1069 by (simp add:SendMsg) |
1064 by (simp add:SendMsg) |
1070 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in |
1065 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in |
1071 apply (erule_tac x = "E_msg q m" in allE) |
1066 apply (erule_tac x = "E_msg q m" in allE) |
1072 apply (case_tac obj', auto dest:not_all_msgqs_prop3) |
1067 apply (case_tac obj', auto dest:not_all_msgqs_prop3) |
1073 done |
1068 done |
1074 have "os_grant s' e" using p_in q_in m_not_in |
1069 have "os_grant s' e" using p_in q_in m_not_in sms_remain os |
1075 by (simp add:SendMsg) |
1070 by (simp add:SendMsg) |
1076 moreover have "grant s' e" |
1071 moreover have "grant s' e" |
1077 proof- |
1072 proof- |
1078 from grant obtain up rp tp uq rq tq |
1073 from grant obtain up rp tp uq rq tq |
1079 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
1074 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
1131 apply (simp add:cq2smsgq_def split:option.splits if_splits) |
1126 apply (simp add:cq2smsgq_def split:option.splits if_splits) |
1132 apply (drule current_has_sms', simp, simp) |
1127 apply (drule current_has_sms', simp, simp) |
1133 apply (case_tac "msgs_of_queue s q", simp) |
1128 apply (case_tac "msgs_of_queue s q", simp) |
1134 apply (simp add:cqm2sms.simps split:option.splits) |
1129 apply (simp add:cqm2sms.simps split:option.splits) |
1135 apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] |
1130 apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] |
1136 apply (case_tac "msgs_of_queue s q", simp) |
|
1137 apply (simp add:cqm2sms.simps split:option.splits) |
|
1138 apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] |
|
1139 done |
1131 done |
1140 show ?thesis using p1' p2' p3' grant p1 p2 p3 |
1132 show ?thesis using p1' p2' p3' grant p1 p2 p3 |
1141 by (simp add:RecvMsg) |
1133 by (simp add:RecvMsg) |
1142 qed |
1134 qed |
1143 ultimately show ?thesis using vs' |
1135 ultimately show ?thesis using vs' |