57 by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
65 by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
58 by (auto_tac (claset() addSWrapper record_split_wrapper, |
66 by (auto_tac (claset() addSWrapper record_split_wrapper, |
59 simpset() addsimps [sysOfAlloc_def])); |
67 simpset() addsimps [sysOfAlloc_def])); |
60 qed "inv_sysOfAlloc_eq"; |
68 qed "inv_sysOfAlloc_eq"; |
61 |
69 |
|
70 Addsimps [inv_sysOfAlloc_eq]; |
62 |
71 |
63 (**SHOULD NOT BE NECESSARY: The various injections into the system |
72 (**SHOULD NOT BE NECESSARY: The various injections into the system |
64 state need to be treated symmetrically or done automatically*) |
73 state need to be treated symmetrically or done automatically*) |
65 Goalw [sysOfClient_def] "inj sysOfClient"; |
74 Goalw [sysOfClient_def] "inj sysOfClient"; |
66 by (rtac injI 1); |
75 by (rtac injI 1); |
200 by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
209 by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
201 System_Increasing_rel, Network]) 1); |
210 System_Increasing_rel, Network]) 1); |
202 qed "System_Increasing_allocRel"; |
211 qed "System_Increasing_allocRel"; |
203 |
212 |
204 |
213 |
205 (*NEED TO PROVE something like this (maybe without premise)*) |
|
206 Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network"; |
|
207 |
|
208 fun alloc_export th = good_map_sysOfAlloc RS export th; |
214 fun alloc_export th = good_map_sysOfAlloc RS export th; |
209 |
215 |
210 val extend_Alloc_guar_Increasing = |
216 val extend_Alloc_guar_Increasing = |
211 alloc_export extend_guar_Increasing |
217 alloc_export extend_guar_Increasing |
212 |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]); |
218 |> simplify (simpset()); |
213 |
219 |
|
220 (*step 2*) |
214 Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
221 Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
215 \ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
222 \ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
216 by (res_inst_tac |
223 by (res_inst_tac |
217 [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
224 [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
218 component_guaranteesD 1); |
225 component_guaranteesD 1); |
219 by (rtac Alloc_component_System 3); |
226 by (rtac Alloc_component_System 3); |
220 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2); |
227 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2); |
221 by (rtac project_guarantees 1); |
228 by (rtac (Alloc_Safety RS project_guarantees) 1); |
222 by (rtac Alloc_Safety 1); |
229 by Auto_tac; |
223 by Auto_tac; |
230 (*1: Increasing precondition*) |
224 by (rtac project_Increasing_I 1); |
231 by (stac (alloc_export project_Increasing) 1); |
225 |
232 by (force_tac |
226 by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 |
233 (claset(), |
227 THEN |
234 simpset() addsimps [o_def, alloc_export project_Increasing]) 1); |
228 full_simp_tac |
235 (*2: Always postcondition*) |
229 (simpset() addsimps [inv_sysOfAlloc_eq, |
236 by (dtac (subset_refl RS alloc_export project_Always_D) 1); |
230 alloc_export Collect_eq_extend_set RS sym]) 2); |
237 by (asm_full_simp_tac |
231 by Auto_tac; |
238 (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1); |
232 |
239 qed "System_sum_bounded"; |
233 by (dtac bspec 1); |
240 |
234 by (Blast_tac 1); |
241 (*step 3*) |
235 |
242 Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients \ |
236 |
243 \ <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"; |
237 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
244 by (rtac (System_sum_bounded RS Always_weaken) 1); |
238 FIRST STEP WAS |
245 by Auto_tac; |
239 by (res_inst_tac |
246 br order_trans 1; |
240 [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \ |
247 br sum_mono 1; |
241 \ Int Increasing (sub i o allocRel))")] |
248 bd order_trans 2; |
242 component_guaranteesD 1); |
249 br add_le_mono 2; |
243 |
250 br order_refl 2; |
244 |
251 br sum_mono 2; |
245 [| i < Nclients; |
252 ba 3; |
246 extend sysOfAlloc Alloc Join G |
253 by Auto_tac; |
247 : (sub i o allocRel) localTo Network & |
254 |
248 extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |] |
|
249 ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel) |
|
250 |
|
251 |
|
252 [| i < Nclients; |
|
253 H : (sub i o allocRel) localTo Network & |
|
254 H : Increasing (sub i o allocRel) |] |
|
255 ==> project sysOfAlloc H : Increasing (sub i o allocRel) |
|
256 |
|
257 Open_locale"Extend"; |
|
258 |
|
259 Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))"; |
|
260 by (asm_full_simp_tac |
|
261 (simpset() addsimps [localTo_def, |
|
262 project_extend_Join RS sym, |
|
263 Diff_project_stable, |
|
264 Collect_eq_extend_set RS sym]) 1); |
|
265 by Auto_tac; |
|
266 by (rtac Diff_project_stable 1); |
|
267 PROBABLY FALSE; |
|
268 |
|
269 by (Clarify_tac 1); |
|
270 by (dres_inst_tac [("x","z")] spec 1); |
|
271 |
|
272 by (rtac (alloc_export project_Always_D) 2); |
|
273 |
|
274 by (rtac (alloc_export extend_Always RS iffD2) 2); |
|
275 |
|
276 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
|
277 |
|
278 by (rtac guaranteesI 1); |
|
279 |
|
280 by (res_inst_tac |
|
281 [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
|
282 component_guaranteesD 1);; |
|
283 |
|
284 |
|
285 by (rtac (Alloc_Safety RS component_guaranteesD) 1); |
|
286 |
|
287 |
|
288 by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1); |
|
289 by (rtac Alloc_Safety 1); |
|