44 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
57 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
45 qed "lift_set_sub2"; |
58 qed "lift_set_sub2"; |
46 |
59 |
47 Goalw [Increasing_def] |
60 Goalw [Increasing_def] |
48 "[| i: I; finite I |] \ |
61 "[| i: I; finite I |] \ |
49 \ ==> ((PPI x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"; |
62 \ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"; |
50 by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1); |
63 by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1); |
51 by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2); |
64 by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2); |
52 by (asm_full_simp_tac (simpset() addsimps [PFUN_Stable]) 1); |
65 by (asm_full_simp_tac (simpset() addsimps [const_PLam_Stable]) 1); |
53 qed "PFUN_Increasing"; |
66 qed "const_PLam_Increasing"; |
54 |
67 |
55 |
68 |
56 (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not |
69 (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not |
57 ensure that F has the form lift_prog i F for some F.*) |
70 ensure that F has the form lift_prog i F for some F.*) |
58 Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}"; |
71 Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}"; |
126 Goalw [Stable_def] |
139 Goalw [Stable_def] |
127 "drop_prog i F : Stable A ==> F : Stable (lift_set i A)"; |
140 "drop_prog i F : Stable A ==> F : Stable (lift_set i A)"; |
128 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1); |
141 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1); |
129 qed "drop_prog_Stable_D"; |
142 qed "drop_prog_Stable_D"; |
130 |
143 |
131 (***???????????????? |
144 (***????????????? |
132 Goal "i ~= j ==> lift_prog i `` UNIV <= stable {s. P (f (s j))}"; |
145 Goal "i ~= j ==> lift_prog i `` UNIV <= stable {s. P (f (s j))}"; |
133 by Auto_tac; |
146 by Auto_tac; |
134 by (stac (lift_set_sub2 RS sym) 1); |
147 by (stac (lift_set_sub2 RS sym) 1); |
135 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
148 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
136 qed "image_lift_prog_Stable"; |
149 qed "image_lift_prog_Stable"; |
137 ????????????????*) |
150 ??????????????*) |
138 |
151 |
139 |
152 |
140 |
153 |
141 (****UNITY.ML?****) |
154 (****UNITY.ML? BUT it's not clear that Idle is good for anything. |
|
155 Could equally want to forbid actions that are subsets of Id |
|
156 OR can simple constraints on actions prevent this?****) |
142 Goalw [constrains_def, Idle_def] "F : Idle ==> (F : A co B) = (A<=B)"; |
157 Goalw [constrains_def, Idle_def] "F : Idle ==> (F : A co B) = (A<=B)"; |
143 by (Blast_tac 1); |
158 by (Blast_tac 1); |
144 qed "constrains_Idle_iff"; |
159 qed "constrains_Idle_iff"; |
145 |
160 |
146 Goalw [stable_def,constrains_def,Idle_def] "F : Idle ==> F : stable A"; |
161 Goalw [stable_def,constrains_def,Idle_def] "F : Idle ==> F : stable A"; |
177 Goal "drop_prog i G : Idle ==> G : stable (lift_set i A)"; |
193 Goal "drop_prog i G : Idle ==> G : stable (lift_set i A)"; |
178 by (simp_tac (simpset() addsimps [drop_prog_stable_eq RS sym]) 1); |
194 by (simp_tac (simpset() addsimps [drop_prog_stable_eq RS sym]) 1); |
179 by (blast_tac (claset() addIs [stable_Idle]) 1); |
195 by (blast_tac (claset() addIs [stable_Idle]) 1); |
180 qed "Idle_imp_stable_lift_set"; |
196 qed "Idle_imp_stable_lift_set"; |
181 |
197 |
|
198 (*like neq_drop_act_lift_act but stronger premises and conclusion*) |
|
199 Goal "[| i~=j; act ~= {} |] ==> drop_act i (lift_act j act) = Id"; |
|
200 br equalityI 1; |
|
201 be neq_drop_act_lift_act 1; |
|
202 by (asm_simp_tac (simpset() addsimps [drop_act_def, lift_act_def]) 1); |
|
203 by Auto_tac; |
|
204 ren "s s'" 1; |
|
205 by (dres_inst_tac [("x", "f(i:=x,j:=s)")] spec 1); |
|
206 by (Asm_full_simp_tac 1); |
|
207 by (dres_inst_tac [("x", "f(i:=x,j:=s')")] spec 1); |
|
208 by (Asm_full_simp_tac 1); |
|
209 by (swap_res_tac [ext] 1); |
|
210 by (Asm_simp_tac 1); |
|
211 qed "neq_drop_act_lift_act_eq"; |
|
212 |
|
213 |
|
214 Goal "act ~= {} ==> drop_act i (lift_act j act) = (if i=j then act else Id)"; |
|
215 by (asm_simp_tac (simpset() addsimps [neq_drop_act_lift_act_eq]) 1); |
|
216 qed "drop_act_lift_act_eq"; |
|
217 |
|
218 |
|
219 (*first premise says that the system has an initial state*) |
|
220 Goalw [PLam_def] |
|
221 "[| ALL j:I. f0 j : Init (F j); \ |
|
222 \ ALL j:I. {} ~: Acts (F j); i: I |] \ |
|
223 \ ==> drop_prog i (plam j:I. F j) = F i"; |
|
224 by (simp_tac (simpset() addsimps [Acts_JN, lift_prog_def, drop_prog_def]) 1); |
|
225 by (rtac program_equalityI 1); |
|
226 by (asm_simp_tac (simpset() addsimps [drop_set_INT_lift_set]) 1); |
|
227 by (Asm_simp_tac 1); |
|
228 by (subgoal_tac |
|
229 "drop_act i `` (UN i:I. lift_act i `` Acts (F i)) = Acts (F i)" 1); |
|
230 by (Asm_simp_tac 1); |
|
231 by Auto_tac; |
|
232 ren "act" 1; |
|
233 by (subgoal_tac "act ~= {}" 1); |
|
234 by (Blast_tac 2); |
|
235 by (asm_simp_tac (simpset() addsimps [drop_act_lift_act_eq]) 1); |
|
236 br image_eqI 1; |
|
237 br (lift_act_inverse RS sym) 1; |
|
238 by Auto_tac; |
|
239 qed "drop_prog_plam_eq"; |
|
240 |
182 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
241 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
|
242 |
|
243 (**STILL trying to lift the guarantees propery from one client to a family. |
|
244 first with a "localTo" precondition. Then to look at the void (UNIV) |
|
245 precondition.**) |
|
246 |
|
247 (*CANNOT be proved because the premise tells us NOTHING AT ALL about |
|
248 actions outside i [rather than telling us there aren't any] |
|
249 MAY UNIVERSALLY QUANTIFY both premise and conclusion???**) |
|
250 Goal "F : stable (lift_set i A) ==> x = lift_prog i (drop_prog i x)"; |
|
251 |
|
252 (*I.E TRY THIS*) |
|
253 Goal "{F. F = (plam j:UNIV. drop_prog j F)} Int (INT i. stable (lift_set i A)) \ |
|
254 \ <= (INT i. lift_prog i `` stable A)"; |
|
255 |
|
256 |
|
257 Goal "{F. F = (plam j:UNIV. drop_prog j F)} Int stable (lift_set i A) \ |
|
258 \ <= lift_prog i `` stable A"; |
|
259 by Auto_tac; |
|
260 fr image_eqI; |
|
261 be (drop_prog_stable_eq RS iffD2) 2; |
|
262 be ssubst 1; |
|
263 by (stac drop_prog_plam_eq 1); |
|
264 by Auto_tac; |
|
265 |
|
266 |
|
267 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
|
268 qed "image_lift_prog_Stable"; |
|
269 |
|
270 |
|
271 Goal "{F. F = (plam i:UNIV. drop_prog i F)} Int stable {s. P (f (s i))} \ |
|
272 \ <= lift_prog i `` stable {s. P (f s)}"; |
|
273 by (stac (lift_set_sub2 RS sym) 1); |
|
274 |
|
275 |
|
276 Goal "Cl : (f localTo F) guar Increasing f ==> \ |
|
277 \ lift_prog i Cl : (f o sub i) localTo (lift_prog i F) \ |
|
278 \ guar Increasing (f o sub i)"; |
|
279 by (dtac lift_prog_guarantees 1); |
|
280 by (etac guarantees_weaken 1); |
|
281 by (rtac image_lift_prog_Increasing 2); |
|
282 |
|
283 |
|
284 |
|
285 |
|
286 |
|
287 |
|
288 |
|
289 Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)"; |
|
290 |
|
291 |
|
292 |
|
293 |
|
294 |
|
295 |
|
296 Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)"; |
|
297 by (simp_tac (simpset() addsimps [localTo_def]) 1); |
|
298 by Auto_tac; |
|
299 by (dres_inst_tac [("x","z")] spec 1); |
|
300 by Auto_tac; |
|
301 by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym, |
|
302 lift_prog_stable_eq]) 1); |
|
303 qed "image_lift_prog_?"; |
|
304 |
|
305 Goal "{GX. EX G: UNIV. lift_prog i G component GX} = UNIV"; |
|
306 by Auto_tac; |
|
307 by (asm_full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
308 by (asm_full_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
309 ren "GX" 1; |
|
310 by (res_inst_tac [("x", "mk_program((%f. f i)``(Init GX), drop_act i `` Acts GX)")] exI 1); |
|
311 by Auto_tac; |
|
312 |
|
313 |
|
314 |
|
315 |
|
316 (*quantified formula's too strong and yet too weak. |
|
317 Close to what's needed, but maybe need further restrictions on X, Y*) |
|
318 Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y); \ |
|
319 \ ALL j: -{i}. drop_prog j `` X <= drop_prog j `` Y |] \ |
|
320 \ ==> lift_prog i F : X guar Y"; |
|
321 by (rtac guaranteesI 1); |
|
322 by (dtac guaranteesD 1); |
|
323 by (rtac image_eqI 1); |
|
324 by (rtac (drop_prog_lift_prog_Join RS sym) 1); |
|
325 by (assume_tac 1); |
|
326 by Auto_tac; |
|
327 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1); |
|
328 by (subgoal_tac "ALL k. drop_prog k (lift_prog i F Join G) = drop_prog k x" 1); |
|
329 by (Clarify_tac 2); |
|
330 by (case_tac "k=i" 2); |
|
331 by (Blast_tac 2); |
|
332 |
|
333 by (dres_inst_tac [("f", "lift_prog i")] arg_cong 1); |
|
334 by (asm_full_simp_tac (simpset() addsimps [singleton_drop_prog_inverse]) 1); |
|
335 |
|
336 by (dtac sym 1); |
|
337 by (Blast_tac 1); |
|
338 qed "drop_prog_guarantees"; |
183 |
339 |
184 Goalw [guarantees_def] |
340 Goalw [guarantees_def] |
185 "[| F : (X Int A) guar (Y Int A); \ |
341 "[| F : (X Int A) guar (Y Int A); \ |
186 \ F : (X Int B) guar (Y Int B); \ |
342 \ F : (X Int B) guar (Y Int B); \ |
187 \ UNIV <= A Un B |] \ |
343 \ UNIV <= A Un B |] \ |
220 by (rtac (impOfSubs image_lift_prog_Increasing) 1); |
376 by (rtac (impOfSubs image_lift_prog_Increasing) 1); |
221 by Auto_tac; |
377 by Auto_tac; |
222 result(); |
378 result(); |
223 |
379 |
224 |
380 |
225 |
|
226 |
|
227 |
|
228 |
|
229 ????????????????????????????????????????????????????????????????; |
|
230 |
|
231 |
|
232 |
|
233 |
|
234 Goal "drop_prog i `` UNIV = UNIV"; |
381 Goal "drop_prog i `` UNIV = UNIV"; |
235 by Auto_tac; |
382 by Auto_tac; |
236 fr image_eqI; |
383 fr image_eqI; |
237 by (rtac (lift_prog_inverse RS sym) 1); |
384 by (rtac (lift_prog_inverse RS sym) 1); |
238 by Auto_tac; |
385 by Auto_tac; |
239 result(); |
386 result(); |
240 |
|
241 |
|
242 Goal "[| F : (drop_prog i `` XX) guar Y; \ |
|
243 \ ALL Z:XX. Z component (JN i:UNIV. JN G:UNIV. lift_prog i G) |] \ |
|
244 \ ==> lift_prog i F : XX guar (lift_prog i `` Y)"; |
|
245 by (rtac guaranteesI 1); |
|
246 by (dtac guaranteesD 1); |
|
247 by (ball_tac 1); |
|
248 by (full_simp_tac (simpset() addsimps [Join_component_iff]) 1); |
|
249 by (full_simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); |
|
250 |
|
251 by (rtac image_eqI 2); |
|
252 by (assume_tac 3); |
|
253 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 2); |
|
254 |
|
255 by (rtac (drop_prog_lift_prog_Join RS sym) 1); |
|
256 by (assume_tac 1); |
|
257 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1); |
|
258 by (rtac image_eqI 1); |
|
259 by (assume_tac 2); |
|
260 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
261 |
|
262 by (rtac guaranteesI 1); |
|
263 by (dtac guaranteesD 1); |
|
264 by (rtac image_eqI 1); |
|
265 by (rtac (drop_prog_lift_prog_Join RS sym) 1); |
|
266 by (assume_tac 1); |
|
267 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1); |
|
268 by (rtac image_eqI 1); |
|
269 by (assume_tac 2); |
|
270 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
271 |
|
272 |
|
273 by (dtac sym 1); |
|
274 by (Blast_tac 1); |
|
275 |
|
276 |
|
277 by (rtac guaranteesI 1); |
|
278 by (dtac guaranteesD 1); |
|
279 by (rtac image_eqI 2); |
|
280 by (assume_tac 3); |
|
281 |
|
282 |
|
283 Goal "F : X guar Y \ |
|
284 \ ==> lift_prog i F : XX guar (lift_prog i `` Y)"; |
|
285 by (rtac guaranteesI 1); |
|
286 by (dtac guaranteesD 1); |
|
287 by (rtac image_eqI 2); |
|
288 by (assume_tac 3); |
|
289 |
|
290 by Auto_tac; |
|
291 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
292 qed "lift_prog_guarantees"; |
|
293 |
|
294 |
|
295 |
|
296 |
387 |
297 |
388 |
298 Goal "x : reachable (drop_prog i F) ==> x : drop_set i (reachable F)"; |
389 Goal "x : reachable (drop_prog i F) ==> x : drop_set i (reachable F)"; |
299 by (etac reachable.induct 1); |
390 by (etac reachable.induct 1); |
300 by Auto_tac; |
391 by Auto_tac; |
437 by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 1); |
518 by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 1); |
438 by Auto_tac; |
519 by Auto_tac; |
439 result(); |
520 result(); |
440 |
521 |
441 |
522 |
442 Goal "H : lift_prog i `` drop_prog i `` X"; |
|
443 |
|
444 |
|
445 Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y); \ |
|
446 \ X <= lift_prog i `` drop_prog i `` X; \ |
|
447 \ Y <= lift_prog i `` drop_prog i `` Y |] \ |
|
448 \ ==> lift_prog i F : X guar Y"; |
|
449 by (rtac guaranteesI 1); |
|
450 by (set_mp_tac 1); |
|
451 by (ALLGOALS Clarify_tac); |
|
452 by (dtac guaranteesD 1); |
|
453 by (rtac image_eqI 1); |
|
454 by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
|
455 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
456 by (assume_tac 1); |
|
457 by (ALLGOALS Clarify_tac); |
|
458 by (set_mp_tac 1); |
|
459 by (ALLGOALS Clarify_tac); |
|
460 by Auto_tac; |
|
461 by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
|
462 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
463 by Auto_tac; |
|
464 qed "drop_prog_guarantees"; |
|
465 |
523 |
466 |
524 |
467 |
525 |
468 (*FAILS*) |
526 (*FAILS*) |
469 Goal "modular i (lift_prog i `` Y)"; |
527 Goal "modular i (lift_prog i `` Y)"; |
470 |
528 |
|
529 |
|
530 |
|
531 |
|
532 |
|
533 Goal "Cl : UNIV guar Increasing f \ |
|
534 \ ==>lift_prog i Cl : UNIV guar Increasing (f o sub i)"; |
|
535 by (rtac drop_prog_guarantees 1); |
|
536 by (rewtac Increasing_def); |
|
537 by (etac guarantees_weaken 1); |
|
538 by Auto_tac; |
|
539 by (rtac image_eqI 1); |
|
540 by (rtac (lift_prog_inverse RS sym) 1); |
|
541 by Auto_tac; |
|
542 by (stac (lift_set_sub2 RS sym) 1); |
|
543 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
|
544 |
|
545 |
|
546 |
|
547 (*could move to PPROD.ML, but function "sub" is needed there*) |
|
548 Goalw [drop_set_def] "drop_set i {s. P (f (sub i s))} = {s. P (f s)}"; |
|
549 by Auto_tac; |
|
550 qed "drop_set_sub"; |
|
551 |
|
552 Goal "lift_set i (reachable (drop_prog i F)) = reachable F"; |
|
553 |
|
554 (*False?*) |
|
555 Goal "modular i ((f o sub i) localTo (lift_prog i F))"; |
|
556 by (simp_tac (simpset() addsimps [localTo_def, modular_def]) 1); |
|
557 by Auto_tac; |
|
558 |
|
559 |
|
560 |
|
561 (*FAILS*) |
|
562 Goal "(drop_prog i F : A Co B) = \ |
|
563 \ (F : (lift_set i A) Co (lift_set i B))"; |
|
564 by (simp_tac (simpset() addsimps [Constrains_def, drop_prog_constrains_eq, |
|
565 lift_set_Int]) 1); |
|
566 |
|
567 ?? |
|
568 by (simp_tac (simpset() addsimps [Constrains_def, reachable_drop_prog, |
|
569 drop_set_Int RS sym, |
|
570 drop_prog_constrains_eq]) 1); |
|
571 qed "drop_prog_Constrains_eq"; |
|
572 |
|
573 (*FAILS*) |
|
574 Goal "(drop_prog i F : Stable A) = (F : Stable (lift_set i A))"; |
|
575 by (simp_tac (simpset() addsimps [Stable_def, drop_prog_Constrains_eq]) 1); |
|
576 qed "drop_prog_Stable_eq"; |
|
577 |
|
578 |
|
579 (*FAILS*) |
|
580 Goal "modular i (Stable {s. P(s i)})"; |
|
581 by (full_simp_tac (simpset() addsimps [modular_def, |
|
582 drop_prog_lift_prog_Join RS sym]) 1); |
|
583 by (full_simp_tac (simpset() addsimps [lift_set_sub2 RS sym, |
|
584 lift_prog_Stable_eq]) 1); |
|
585 by Auto_tac; |
|
586 |
|
587 |
|
588 |
|
589 Goal "modular i (Increasing (rel o sub i))"; |
|
590 by (full_simp_tac (simpset() addsimps [modular_def, Increasing_def, |
|
591 drop_prog_lift_prog_Join RS sym]) 1); |
|
592 |
|
593 |
|
594 Goal "modular i (lift_prog i `` X)"; |
|
595 by (full_simp_tac (simpset() addsimps [modular_def, |
|
596 drop_prog_lift_prog_Join RS sym]) 1); |
|
597 |
|
598 |
|
599 |
|
600 Goal "i < Nclients ==> \ |
|
601 \ lift_prog i Client : UNIV guar Increasing (rel o sub i)"; |
|
602 |
|
603 |
|
604 |
|
605 |
|
606 |
|
607 |
|
608 |
|
609 |
|
610 by (stac Acts_eq 1); |
|
611 |
|
612 fr conjI; |
|
613 by (Clarify_tac 1); |
|
614 by (stac Init_eq 1); |
|
615 |
|
616 |
|
617 {GX. EX G:X. lift_prog i G component GX} |
|
618 {GY. EX G:Y. lift_prog i G component GY} |
|
619 |
|
620 |
|
621 |
|
622 uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu; |
|
623 |
|
624 |
|
625 |
|
626 |
|
627 Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
|
628 by (cut_facts_tac [Client] 1); |
|
629 by (full_simp_tac |
|
630 (simpset() addsimps [System_def, |
|
631 client_spec_def, client_increasing_def, |
|
632 guarantees_Int_right]) 1); |
|
633 by Auto_tac; |
|
634 by (dtac lift_prog_guarantees 1); |
|
635 by (dtac (UNIV_I RSN (2, guaranteesD)) 1); |
|
636 back(); |
|
637 by (dtac (lessThan_iff RS iffD2 RS const_PLam_Increasing RS iffD2) 1); |
|
638 by Auto_tac; |
|
639 |
|
640 |
|
641 by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (const_PLam_Increasing RS sym)]) 1); |
|
642 |
|
643 yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy; |
471 |
644 |
472 |
645 |
473 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!; |
646 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!; |
474 (*Precondition is TOO STRONG*) |
647 (*Precondition is TOO STRONG*) |
475 Goal "Cl : UNIV guar Increasing f \ |
648 Goal "Cl : UNIV guar Increasing f \ |
487 by (stac (lift_set_sub2 RS sym) 1); |
660 by (stac (lift_set_sub2 RS sym) 1); |
488 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
661 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
489 |
662 |
490 |
663 |
491 |
664 |
492 |
|
493 |
|
494 |
|
495 Goal "Cl : UNIV guar Increasing f \ |
|
496 \ ==>lift_prog i Cl : UNIV guar Increasing (f o sub i)"; |
|
497 by (rtac drop_prog_guarantees 1); |
|
498 by (rewtac Increasing_def); |
|
499 by (etac guarantees_weaken 1); |
|
500 by Auto_tac; |
|
501 by (rtac image_eqI 1); |
|
502 by (rtac (lift_prog_inverse RS sym) 1); |
|
503 by Auto_tac; |
|
504 by (stac (lift_set_sub2 RS sym) 1); |
|
505 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1); |
|
506 |
|
507 |
|
508 |
|
509 (*could move to PPROD.ML, but function "sub" is needed there*) |
|
510 Goalw [drop_set_def] "drop_set i {s. P (f (sub i s))} = {s. P (f s)}"; |
|
511 by Auto_tac; |
|
512 qed "drop_set_sub"; |
|
513 |
|
514 Goal "lift_set i (reachable (drop_prog i F)) = reachable F"; |
|
515 |
|
516 (*False?*) |
|
517 Goal "modular i ((f o sub i) localTo (lift_prog i F))"; |
|
518 by (simp_tac (simpset() addsimps [localTo_def, modular_def]) 1); |
|
519 by Auto_tac; |
|
520 |
|
521 |
|
522 |
|
523 (*FAILS*) |
|
524 Goal "(drop_prog i F : A Co B) = \ |
|
525 \ (F : (lift_set i A) Co (lift_set i B))"; |
|
526 by (simp_tac (simpset() addsimps [Constrains_def, drop_prog_constrains_eq, |
|
527 lift_set_Int]) 1); |
|
528 |
|
529 ?? |
|
530 by (simp_tac (simpset() addsimps [Constrains_def, reachable_drop_prog, |
|
531 drop_set_Int RS sym, |
|
532 drop_prog_constrains_eq]) 1); |
|
533 qed "drop_prog_Constrains_eq"; |
|
534 |
|
535 (*FAILS*) |
|
536 Goal "(drop_prog i F : Stable A) = (F : Stable (lift_set i A))"; |
|
537 by (simp_tac (simpset() addsimps [Stable_def, drop_prog_Constrains_eq]) 1); |
|
538 qed "drop_prog_Stable_eq"; |
|
539 |
|
540 |
|
541 (*FAILS*) |
|
542 Goal "modular i (Stable {s. P(s i)})"; |
|
543 by (full_simp_tac (simpset() addsimps [modular_def, |
|
544 drop_prog_lift_prog_Join RS sym]) 1); |
|
545 by (full_simp_tac (simpset() addsimps [lift_set_sub2 RS sym, |
|
546 lift_prog_Stable_eq]) 1); |
|
547 by Auto_tac; |
|
548 |
|
549 |
|
550 |
|
551 Goal "modular i (Increasing (rel o sub i))"; |
|
552 by (full_simp_tac (simpset() addsimps [modular_def, Increasing_def, |
|
553 drop_prog_lift_prog_Join RS sym]) 1); |
|
554 |
|
555 |
|
556 Goal "modular i (lift_prog i `` X)"; |
|
557 by (full_simp_tac (simpset() addsimps [modular_def, |
|
558 drop_prog_lift_prog_Join RS sym]) 1); |
|
559 |
|
560 |
|
561 |
|
562 Goal "i < Nclients ==> \ |
|
563 \ lift_prog i Client : UNIV guar Increasing (rel o sub i)"; |
|
564 |
|
565 |
|
566 |
|
567 |
|
568 |
|
569 |
|
570 Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)"; |
|
571 |
|
572 |
|
573 |
|
574 |
|
575 |
|
576 |
|
577 Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)"; |
|
578 by (simp_tac (simpset() addsimps [localTo_def]) 1); |
|
579 by Auto_tac; |
|
580 by (dres_inst_tac [("x","z")] spec 1); |
|
581 by Auto_tac; |
|
582 by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym, |
|
583 lift_prog_stable_eq]) 1); |
|
584 qed "image_lift_prog_?"; |
|
585 |
|
586 Goal "{GX. EX G: UNIV. lift_prog i G component GX} = UNIV"; |
|
587 by Auto_tac; |
|
588 by (asm_full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
589 by (asm_full_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
590 ren "GX" 1; |
|
591 by (res_inst_tac [("x", "mk_program((%f. f i)``(Init GX), drop_act i `` Acts GX)")] exI 1); |
|
592 by Auto_tac; |
|
593 |
|
594 |
|
595 by (stac Acts_eq 1); |
|
596 |
|
597 fr conjI; |
|
598 by (Clarify_tac 1); |
|
599 by (stac Init_eq 1); |
|
600 |
|
601 |
|
602 {GX. EX G:X. lift_prog i G component GX} |
|
603 {GY. EX G:Y. lift_prog i G component GY} |
|
604 |
|
605 |
|
606 |
|
607 uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu; |
|
608 |
|
609 |
|
610 |
|
611 |
|
612 Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
|
613 by (cut_facts_tac [Client] 1); |
|
614 by (full_simp_tac |
|
615 (simpset() addsimps [System_def, |
|
616 client_spec_def, client_increasing_def, |
|
617 guarantees_Int_right]) 1); |
|
618 by Auto_tac; |
|
619 by (dtac lift_prog_guarantees 1); |
|
620 by (dtac (UNIV_I RSN (2, guaranteesD)) 1); |
|
621 back(); |
|
622 by (dtac (lessThan_iff RS iffD2 RS PFUN_Increasing RS iffD2) 1); |
|
623 by Auto_tac; |
|
624 |
|
625 |
|
626 by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (PFUN_Increasing RS sym)]) 1); |
|
627 |
|
628 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
|
629 |
|
630 |
|
631 Goal "System : system_spec"; |
|
632 |
|
633 by (full_simp_tac |
665 by (full_simp_tac |
634 (simpset() addsimps [alloc_spec_def, alloc_safety_def, System_def]) 1); |
666 (simpset() addsimps [alloc_spec_def, alloc_safety_def, System_def]) 1); |
|
667 |
|
668 |
|
669 |
|
670 |
|
671 Goal "[| F : (drop_prog i `` XX) guar Y; \ |
|
672 \ ALL Z:XX. Z component (JN i:UNIV. JN G:UNIV. lift_prog i G) |] \ |
|
673 \ ==> lift_prog i F : XX guar (lift_prog i `` Y)"; |
|
674 by (rtac guaranteesI 1); |
|
675 by (dtac guaranteesD 1); |
|
676 by (ball_tac 1); |
|
677 by (full_simp_tac (simpset() addsimps [Join_component_iff]) 1); |
|
678 by (full_simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); |
|
679 |
|
680 by (rtac image_eqI 2); |
|
681 by (assume_tac 3); |
|
682 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 2); |
|
683 |
|
684 by (rtac (drop_prog_lift_prog_Join RS sym) 1); |
|
685 by (assume_tac 1); |
|
686 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1); |
|
687 by (rtac image_eqI 1); |
|
688 by (assume_tac 2); |
|
689 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
690 |
|
691 by (rtac guaranteesI 1); |
|
692 by (dtac guaranteesD 1); |
|
693 by (rtac image_eqI 1); |
|
694 by (rtac (drop_prog_lift_prog_Join RS sym) 1); |
|
695 by (assume_tac 1); |
|
696 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1); |
|
697 by (rtac image_eqI 1); |
|
698 by (assume_tac 2); |
|
699 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
700 |
|
701 |
|
702 by (dtac sym 1); |
|
703 by (Blast_tac 1); |
|
704 |
|
705 |
|
706 by (rtac guaranteesI 1); |
|
707 by (dtac guaranteesD 1); |
|
708 by (rtac image_eqI 2); |
|
709 by (assume_tac 3); |
|
710 |
|
711 |
|
712 Goal "F : X guar Y \ |
|
713 \ ==> lift_prog i F : XX guar (lift_prog i `` Y)"; |
|
714 by (rtac guaranteesI 1); |
|
715 by (dtac guaranteesD 1); |
|
716 by (rtac image_eqI 2); |
|
717 by (assume_tac 3); |
|
718 |
|
719 by Auto_tac; |
|
720 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
721 qed "lift_prog_guarantees"; |
|
722 |
|
723 |
635 |
724 |
636 |
725 |
637 |
726 |
638 |
727 |
639 |
728 |
642 Goal "[| Alloc : alloc_spec; Network : network_spec |] \ |
731 Goal "[| Alloc : alloc_spec; Network : network_spec |] \ |
643 \ ==> (extend sysOfAlloc Alloc) Join Network : system_spec"; |
732 \ ==> (extend sysOfAlloc Alloc) Join Network : system_spec"; |
644 |
733 |
645 (*partial system...*) |
734 (*partial system...*) |
646 Goal "[| Client : client_spec; Network : network_spec |] \ |
735 Goal "[| Client : client_spec; Network : network_spec |] \ |
647 \ ==> (extend sysOfClient (PPI x: lessThan Nclients. Client)) \ |
736 \ ==> (extend sysOfClient (plam x: lessThan Nclients. Client)) \ |
648 \ Join Network : system_spec"; |
737 \ Join Network : system_spec"; |
649 |
738 |
650 |
739 |
651 |
740 |
652 Goal "[| Alloc : alloc_spec; Client : client_spec; \ |
741 Goal "[| Alloc : alloc_spec; Client : client_spec; \ |
653 \ Network : network_spec |] \ |
742 \ Network : network_spec |] \ |
654 \ ==> (extend sysOfAlloc Alloc) \ |
743 \ ==> (extend sysOfAlloc Alloc) \ |
655 \ Join (extend sysOfClient (PPI x: lessThan Nclients. Client)) \ |
744 \ Join (extend sysOfClient (plam x: lessThan Nclients. Client)) \ |
656 \ Join Network : system_spec"; |
745 \ Join Network : system_spec"; |
657 by (full_simp_tac |
746 by (full_simp_tac |
658 (simpset() addsimps [system_spec_def, system_safety_def]) 1); |
747 (simpset() addsimps [system_spec_def, system_safety_def]) 1); |
659 by Auto_tac; |
748 by Auto_tac; |
660 by (full_simp_tac |
749 by (full_simp_tac |
674 by (Simp_tac 1); |
763 by (Simp_tac 1); |
675 |
764 |
676 |
765 |
677 |
766 |
678 |
767 |
679 (*Generalized version allowing different clients*) |
768 Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y); \ |
680 Goal "[| Alloc : alloc_spec; \ |
769 \ X <= lift_prog i `` drop_prog i `` X; \ |
681 \ Client : (lessThan Nclients) funcset client_spec; \ |
770 \ Y <= lift_prog i `` drop_prog i `` Y |] \ |
682 \ Network : network_spec |] \ |
771 \ ==> lift_prog i F : X guar Y"; |
683 \ ==> (extend sysOfAlloc Alloc) \ |
772 by (rtac guaranteesI 1); |
684 \ Join (extend sysOfClient (PPROD (lessThan Nclients) Client)) \ |
773 by (set_mp_tac 1); |
685 \ Join Network : system_spec"; |
774 by (ALLGOALS Clarify_tac); |
686 |
775 by (dtac guaranteesD 1); |
|
776 by (rtac image_eqI 1); |
|
777 by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
|
778 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
779 by (assume_tac 1); |
|
780 by (ALLGOALS Clarify_tac); |
|
781 by (set_mp_tac 1); |
|
782 by (ALLGOALS Clarify_tac); |
|
783 by Auto_tac; |
|
784 by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
|
785 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
786 by Auto_tac; |
|
787 qed "drop_prog_guarantees"; |
|
788 |
|
789 |
|
790 |
|
791 |
|
792 (*****SINGLETON LEMMAS: GOOD FOR ANYTHING??????***) |
|
793 |
|
794 (*Because A and B could differ outside i, cannot generalize result to |
|
795 drop_set i (A Int B) = drop_set i A Int drop_set i B |
|
796 *) |
|
797 Goal "[| ALL j. j = i; f i = g i |] ==> f = g"; |
|
798 br ext 1; |
|
799 by (dres_inst_tac [("x", "x")] spec 1); |
|
800 by Auto_tac; |
|
801 qed "singleton_ext"; |
|
802 |
|
803 Goalw [lift_set_def, drop_set_def] |
|
804 "ALL j. j = i ==> lift_set i (drop_set i A) = A"; |
|
805 by (blast_tac (claset() addSDs [singleton_ext]) 1); |
|
806 qed "singleton_drop_set_inverse"; |
|
807 |
|
808 Goal "ALL j. j = i ==> f(i:= g i) = g"; |
|
809 by (dres_inst_tac [("x", "x")] spec 1); |
|
810 by Auto_tac; |
|
811 qed "singleton_update_eq"; |
|
812 |
|
813 Goalw [lift_act_def, drop_act_def] |
|
814 "ALL j. j = i ==> lift_act i (drop_act i act) = act"; |
|
815 by Auto_tac; |
|
816 by (asm_simp_tac (simpset() addsimps [singleton_update_eq]) 1); |
|
817 bd singleton_ext 1; |
|
818 ba 1; |
|
819 by (auto_tac (claset() addSIs [exI, image_eqI], |
|
820 simpset() addsimps [singleton_update_eq])); |
|
821 qed "singleton_drop_act_inverse"; |
|
822 |
|
823 Goal "ALL j. j = i ==> lift_prog i (drop_prog i F) = F"; |
|
824 by (rtac program_equalityI 1); |
|
825 by (asm_simp_tac (simpset() addsimps [singleton_drop_set_inverse]) 1); |
|
826 by (asm_simp_tac (simpset() addsimps [image_compose RS sym, o_def, |
|
827 singleton_drop_act_inverse]) 1); |
|
828 qed "singleton_drop_prog_inverse"; |
|
829 |