328 qed "extend_invariant"; |
328 qed "extend_invariant"; |
329 |
329 |
330 (** Safety and project **) |
330 (** Safety and project **) |
331 |
331 |
332 Goalw [constrains_def] |
332 Goalw [constrains_def] |
333 "(project C h F : A co B) = \ |
333 "(F Join project C h G : A co B) = \ |
|
334 \ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ |
|
335 \ F : A co B)"; |
|
336 by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un])); |
|
337 by (force_tac (claset() addIs [extend_act_D], simpset()) 1); |
|
338 by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1); |
|
339 (*the <== direction*) |
|
340 by (ball_tac 1); |
|
341 by (rewtac project_act_def); |
|
342 by Auto_tac; |
|
343 by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1); |
|
344 by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
|
345 qed "Join_project_constrains"; |
|
346 |
|
347 (*The condition is required to prove the left-to-right direction; |
|
348 could weaken it to G : (C Int extend_set h A) co C*) |
|
349 Goalw [stable_def] |
|
350 "extend h F Join G : stable C \ |
|
351 \ ==> (F Join project C h G : stable A) = \ |
|
352 \ (extend h F Join G : stable (C Int extend_set h A) & \ |
|
353 \ F : stable A)"; |
|
354 by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
355 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
|
356 qed "Join_project_stable"; |
|
357 |
|
358 Goal "(F Join project UNIV h G : increasing func) = \ |
|
359 \ (extend h F Join G : increasing (func o f))"; |
|
360 by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1); |
|
361 by (auto_tac (claset(), |
|
362 simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
|
363 extend_stable RS iffD1])); |
|
364 |
|
365 qed "Join_project_increasing"; |
|
366 |
|
367 Goal "(project C h F : A co B) = \ |
334 \ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
368 \ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
335 by (auto_tac (claset() addSIs [project_act_I], simpset())); |
369 by (cut_inst_tac [("F", "SKIP")] Join_project_constrains 1); |
336 by (rewtac project_act_def); |
370 by (asm_full_simp_tac (simpset() addsimps [extend_SKIP]) 1); |
337 by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1); |
|
338 (*the <== direction*) |
|
339 by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
|
340 qed "project_constrains"; |
371 qed "project_constrains"; |
341 |
|
342 (*The condition is required to prove the left-to-right direction; |
|
343 could weaken it to F : (C Int extend_set h A) co C*) |
|
344 Goalw [stable_def] |
|
345 "F : stable C \ |
|
346 \ ==> (project C h F : stable A) = (F : stable (C Int extend_set h A))"; |
|
347 by (simp_tac (simpset() addsimps [project_constrains]) 1); |
|
348 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
|
349 qed "project_stable"; |
|
350 |
|
351 Goal "(project UNIV h F : increasing func) = \ |
|
352 \ (F : increasing (func o f))"; |
|
353 by (asm_simp_tac (simpset() addsimps [increasing_def, project_stable, |
|
354 Collect_eq_extend_set RS sym]) 1); |
|
355 qed "project_increasing"; |
|
356 |
372 |
357 |
373 |
358 (*** Diff, needed for localTo ***) |
374 (*** Diff, needed for localTo ***) |
359 |
375 |
360 (** project versions **) |
376 (** project versions **) |
460 qed "extend_Always"; |
476 qed "extend_Always"; |
461 |
477 |
462 |
478 |
463 (** Reachability and project **) |
479 (** Reachability and project **) |
464 |
480 |
465 Goal "[| reachable F <= C; z : reachable F |] \ |
481 Goal "[| reachable (extend h F Join G) <= C; \ |
466 \ ==> f z : reachable (project C h F)"; |
482 \ z : reachable (extend h F Join G) |] \ |
|
483 \ ==> f z : reachable (F Join project C h G)"; |
467 by (etac reachable.induct 1); |
484 by (etac reachable.induct 1); |
468 by (force_tac (claset() addIs [reachable.Acts, project_act_I], |
485 by (force_tac (claset() delrules [Id_in_Acts] |
|
486 addIs [reachable.Acts, project_act_I, extend_act_D], |
469 simpset()) 2); |
487 simpset()) 2); |
470 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
488 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
471 simpset()) 1); |
489 simpset()) 1); |
472 qed "reachable_imp_reachable_project"; |
490 qed "reachable_imp_reachable_project"; |
473 |
491 |
474 Goalw [Constrains_def] |
492 Goalw [Constrains_def] |
475 "[| reachable F <= C; project C h F : A Co B |] \ |
493 "[| reachable (extend h F Join G) <= C; \ |
476 \ ==> F : (extend_set h A) Co (extend_set h B)"; |
494 \ F Join project C h G : A Co B |] \ |
477 by (full_simp_tac (simpset() addsimps [project_constrains]) 1); |
495 \ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
|
496 by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
478 by (Clarify_tac 1); |
497 by (Clarify_tac 1); |
479 by (etac constrains_weaken_L 1); |
498 by (etac constrains_weaken 1); |
480 by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset())); |
499 by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset())); |
481 qed "project_Constrains_D"; |
500 qed "project_Constrains_D"; |
482 |
501 |
483 Goalw [Stable_def] |
502 Goalw [Stable_def] |
484 "[| reachable F <= C; project C h F : Stable A |] \ |
503 "[| reachable (extend h F Join G) <= C; \ |
485 \ ==> F : Stable (extend_set h A)"; |
504 \ F Join project C h G : Stable A |] \ |
|
505 \ ==> extend h F Join G : Stable (extend_set h A)"; |
486 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
506 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
487 qed "project_Stable_D"; |
507 qed "project_Stable_D"; |
488 |
508 |
489 Goalw [Always_def] |
509 Goalw [Always_def] |
490 "[| reachable F <= C; project C h F : Always A |] \ |
510 "[| reachable (extend h F Join G) <= C; \ |
491 \ ==> F : Always (extend_set h A)"; |
511 \ F Join project C h G : Always A |] \ |
|
512 \ ==> extend h F Join G : Always (extend_set h A)"; |
492 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
513 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
493 simpset() addsimps [project_Stable_D]) 1); |
514 simpset() addsimps [project_Stable_D]) 1); |
494 qed "project_Always_D"; |
515 qed "project_Always_D"; |
495 |
516 |
496 Goalw [Increasing_def] |
517 Goalw [Increasing_def] |
497 "[| reachable F <= C; project C h F : Increasing func |] \ |
518 "[| reachable (extend h F Join G) <= C; \ |
498 \ ==> F : Increasing (func o f)"; |
519 \ F Join project C h G : Increasing func |] \ |
|
520 \ ==> extend h F Join G : Increasing (func o f)"; |
499 by Auto_tac; |
521 by Auto_tac; |
500 by (stac Collect_eq_extend_set 1); |
522 by (stac Collect_eq_extend_set 1); |
501 by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
523 by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
502 qed "project_Increasing_D"; |
524 qed "project_Increasing_D"; |
503 |
525 |
504 |
526 |
505 (** Converse results for weak safety: benefits of the argument C *) |
527 (** Converse results for weak safety: benefits of the argument C *) |
506 |
528 |
507 Goal "[| C <= reachable F; x : reachable (project C h F) |] \ |
529 Goal "[| C <= reachable(extend h F Join G); \ |
508 \ ==> EX y. h(x,y) : reachable F"; |
530 \ x : reachable (F Join project C h G) |] \ |
|
531 \ ==> EX y. h(x,y) : reachable (extend h F Join G)"; |
509 by (etac reachable.induct 1); |
532 by (etac reachable.induct 1); |
510 by (ALLGOALS |
533 by (ALLGOALS Asm_full_simp_tac); |
511 (asm_full_simp_tac |
534 (*SLOW: 6.7s*) |
512 (simpset() addsimps [project_set_def, project_act_def]))); |
535 by (force_tac (claset() delrules [Id_in_Acts] |
513 by (force_tac (claset() addIs [reachable.Acts], |
536 addIs [reachable.Acts, extend_act_D], |
514 simpset() addsimps [project_act_def]) 2); |
537 simpset() addsimps [project_act_def]) 2); |
515 by (force_tac (claset() addIs [reachable.Init], |
538 by (force_tac (claset() addIs [reachable.Init], |
516 simpset() addsimps [project_set_def]) 1); |
539 simpset() addsimps [project_set_def]) 1); |
517 qed "reachable_project_imp_reachable"; |
540 qed "reachable_project_imp_reachable"; |
518 |
541 |
519 Goalw [Constrains_def] |
542 Goalw [Constrains_def] |
520 "[| C <= reachable F; F : (extend_set h A) Co (extend_set h B) |] \ |
543 "[| C <= reachable (extend h F Join G); \ |
521 \ ==> project C h F : A Co B"; |
544 \ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \ |
522 by (full_simp_tac (simpset() addsimps [project_constrains, |
545 \ ==> F Join project C h G : A Co B"; |
|
546 by (full_simp_tac (simpset() addsimps [Join_project_constrains, |
523 extend_set_Int_distrib]) 1); |
547 extend_set_Int_distrib]) 1); |
524 by (rtac conjI 1); |
548 by (rtac conjI 1); |
525 by (force_tac (claset() addSDs [constrains_imp_subset, |
|
526 reachable_project_imp_reachable], |
|
527 simpset()) 2); |
|
528 by (etac constrains_weaken 1); |
549 by (etac constrains_weaken 1); |
529 by Auto_tac; |
550 by Auto_tac; |
|
551 by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1); |
|
552 (*Some generalization of constrains_weaken_L would be better, but what is it?*) |
|
553 by (rewtac constrains_def); |
|
554 by Auto_tac; |
|
555 by (thin_tac "ALL act : Acts G. ?P act" 1); |
|
556 by (force_tac (claset() addSDs [reachable_project_imp_reachable], |
|
557 simpset()) 1); |
530 qed "project_Constrains_I"; |
558 qed "project_Constrains_I"; |
531 |
559 |
532 Goalw [Stable_def] |
560 Goalw [Stable_def] |
533 "[| C <= reachable F; F : Stable (extend_set h A) |] \ |
561 "[| C <= reachable (extend h F Join G); \ |
534 \ ==> project C h F : Stable A"; |
562 \ extend h F Join G : Stable (extend_set h A) |] \ |
|
563 \ ==> F Join project C h G : Stable A"; |
535 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
564 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
536 qed "project_Stable_I"; |
565 qed "project_Stable_I"; |
537 |
566 |
538 Goalw [Increasing_def] |
567 Goalw [Increasing_def] |
539 "[| C <= reachable F; F : Increasing (func o f) |] \ |
568 "[| C <= reachable (extend h F Join G); \ |
540 \ ==> project C h F : Increasing func"; |
569 \ extend h F Join G : Increasing (func o f) |] \ |
|
570 \ ==> F Join project C h G : Increasing func"; |
541 by Auto_tac; |
571 by Auto_tac; |
542 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym, |
572 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym, |
543 project_Stable_I]) 1); |
573 project_Stable_I]) 1); |
544 qed "project_Increasing_I"; |
574 qed "project_Increasing_I"; |
545 |
575 |
546 Goal "(project (reachable F) h F : A Co B) = \ |
576 Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B) = \ |
547 \ (F : (extend_set h A) Co (extend_set h B))"; |
577 \ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; |
548 by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
578 by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
549 qed "project_Constrains"; |
579 qed "project_Constrains"; |
550 |
580 |
551 Goalw [Stable_def] |
581 Goalw [Stable_def] |
552 "(project (reachable F) h F : Stable A) = \ |
582 "(F Join project (reachable (extend h F Join G)) h G : Stable A) = \ |
553 \ (F : Stable (extend_set h A))"; |
583 \ (extend h F Join G : Stable (extend_set h A))"; |
554 by (rtac project_Constrains 1); |
584 by (rtac project_Constrains 1); |
555 qed "project_Stable"; |
585 qed "project_Stable"; |
556 |
586 |
557 Goal "(project (reachable F) h F : Increasing func) = \ |
587 Goal |
558 \ (F : Increasing (func o f))"; |
588 "(F Join project (reachable (extend h F Join G)) h G : Increasing func) = \ |
|
589 \ (extend h F Join G : Increasing (func o f))"; |
559 by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
590 by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
560 Collect_eq_extend_set RS sym]) 1); |
591 Collect_eq_extend_set RS sym]) 1); |
561 qed "project_Increasing"; |
592 qed "project_Increasing"; |
562 |
593 |
563 (** |
|
564 (*NOT useful in its own right, but a guarantees rule likes premises |
|
565 in this form*) |
|
566 Goal "F Join project C h G : A Co B \ |
|
567 \ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
|
568 by (asm_simp_tac |
|
569 (simpset() addsimps [project_extend_Join, project_Constrains_D]) 1); |
|
570 qed "extend_Join_Constrains"; |
|
571 **) |
|
572 |
594 |
573 (*** Progress: transient, ensures ***) |
595 (*** Progress: transient, ensures ***) |
574 |
596 |
575 Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
597 Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
576 by (auto_tac (claset(), |
598 by (auto_tac (claset(), |
712 (*** guarantees corollaries ***) |
734 (*** guarantees corollaries ***) |
713 |
735 |
714 Goal "F : UNIV guarantees increasing func \ |
736 Goal "F : UNIV guarantees increasing func \ |
715 \ ==> extend h F : UNIV guarantees increasing (func o f)"; |
737 \ ==> extend h F : UNIV guarantees increasing (func o f)"; |
716 by (etac project_guarantees 1); |
738 by (etac project_guarantees 1); |
717 by (asm_simp_tac (simpset() addsimps [project_increasing RS sym]) 2); |
739 by (ALLGOALS |
718 by (stac (project_set_UNIV RS project_extend_Join) 2); |
740 (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]))); |
719 by Auto_tac; |
|
720 qed "extend_guar_increasing"; |
741 qed "extend_guar_increasing"; |
721 |
742 |
722 Goal "F : UNIV guarantees Increasing func \ |
743 Goal "F : UNIV guarantees Increasing func \ |
723 \ ==> extend h F : UNIV guarantees Increasing (func o f)"; |
744 \ ==> extend h F : UNIV guarantees Increasing (func o f)"; |
724 by (etac project_guarantees 1); |
745 by (etac project_guarantees 1); |
725 by (rtac (subset_UNIV RS project_Increasing_D) 2); |
746 by (rtac (subset_UNIV RS project_Increasing_D) 2); |
726 by (stac (project_set_UNIV RS project_extend_Join) 2); |
|
727 by Auto_tac; |
747 by Auto_tac; |
728 qed "extend_guar_Increasing"; |
748 qed "extend_guar_Increasing"; |
729 |
749 |
730 Goal "F : (func localTo G) guarantees increasing func \ |
750 Goal "F : (func localTo G) guarantees increasing func \ |
731 \ ==> extend h F : (func o f) localTo (extend h G) \ |
751 \ ==> extend h F : (func o f) localTo (extend h G) \ |
732 \ guarantees increasing (func o f)"; |
752 \ guarantees increasing (func o f)"; |
733 by (etac project_guarantees 1); |
753 by (etac project_guarantees 1); |
734 (*the "increasing" guarantee*) |
754 (*the "increasing" guarantee*) |
735 by (asm_simp_tac |
755 by (asm_simp_tac |
736 (simpset() addsimps [project_increasing RS sym]) 2); |
756 (simpset() addsimps [Join_project_increasing RS sym]) 2); |
737 by (stac (project_set_UNIV RS project_extend_Join) 2); |
|
738 by (assume_tac 2); |
|
739 (*the "localTo" requirement*) |
757 (*the "localTo" requirement*) |
740 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
758 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
741 by (asm_simp_tac |
759 by (asm_simp_tac |
742 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
760 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
743 qed "extend_localTo_guar_increasing"; |
761 qed "extend_localTo_guar_increasing"; |