444 \ ==> extending v C h F (Increasing (func o f)) (Increasing func)"; |
444 \ ==> extending v C h F (Increasing (func o f)) (Increasing func)"; |
445 by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1); |
445 by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1); |
446 qed "extending_Increasing"; |
446 qed "extending_Increasing"; |
447 |
447 |
448 |
448 |
449 (** Progress includes safety in the definition of ensures **) |
449 (*** leadsETo in the precondition ***) |
450 |
|
451 (*** Progress for (project h C F) ***) |
|
452 |
450 |
453 (** transient **) |
451 (** transient **) |
454 |
452 |
455 (*Premise is that C includes the domains of all actions that could be the |
|
456 transient one. Could have C=UNIV of course*) |
|
457 Goalw [transient_def] |
453 Goalw [transient_def] |
458 "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \ |
454 "[| G : transient (C Int extend_set h A); G : stable C |] \ |
459 \ Domain act <= C; \ |
455 \ ==> project h C G : transient (project_set h C Int A)"; |
460 \ F : transient (extend_set h A) |] \ |
456 by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
461 \ ==> project h C F : transient A"; |
457 by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1); |
462 by (auto_tac (claset() delrules [ballE], |
458 by (asm_full_simp_tac |
463 simpset() addsimps [Domain_project_act, Int_absorb1])); |
459 (simpset() addsimps [stable_def, constrains_def]) 2); |
464 by (REPEAT (ball_tac 1)); |
460 by (Blast_tac 2); |
465 by (auto_tac (claset(), |
461 (*back to main goal*) |
466 simpset() addsimps [extend_set_def, project_act_def])); |
462 by (thin_tac "?AA <= -C Un ?BB" 1); |
467 by (ALLGOALS Blast_tac); |
463 by (ball_tac 1); |
|
464 by (asm_full_simp_tac |
|
465 (simpset() addsimps [extend_set_def, project_act_def]) 1); |
|
466 by (Blast_tac 1); |
468 qed "transient_extend_set_imp_project_transient"; |
467 qed "transient_extend_set_imp_project_transient"; |
469 |
468 |
470 |
469 (*converse might hold too?*) |
471 (** ensures **) |
470 Goalw [transient_def] |
472 |
471 "project h C (extend h F) : transient (project_set h C Int D) \ |
473 (*For simplicity, the complicated condition on C is eliminated |
472 \ ==> F : transient (project_set h C Int D)"; |
474 NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*) |
473 by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
475 Goal "F : (extend_set h A) ensures (extend_set h B) \ |
474 by (rtac bexI 1); |
476 \ ==> project h UNIV F : A ensures B"; |
475 by (assume_tac 2); |
|
476 by Auto_tac; |
|
477 by (rewtac extend_act_def); |
|
478 by (Blast_tac 1); |
|
479 qed "project_extend_transient_D"; |
|
480 |
|
481 |
|
482 (** ensures -- a primitive combining progress with safety **) |
|
483 |
|
484 (*Used to prove project_leadsETo_I*) |
|
485 Goal "[| extend h F : stable C; G : stable C; \ |
|
486 \ extend h F Join G : A ensures B; A-B = C Int extend_set h D |] \ |
|
487 \ ==> F Join project h C G \ |
|
488 \ : (project_set h C Int project_set h A) ensures (project_set h B)"; |
477 by (asm_full_simp_tac |
489 by (asm_full_simp_tac |
478 (simpset() addsimps [ensures_def, project_constrains, |
490 (simpset() addsimps [ensures_def, Join_constrains, project_constrains, |
479 transient_extend_set_imp_project_transient, |
491 Join_transient, extend_transient]) 1); |
480 extend_set_Un_distrib RS sym, |
492 by (Clarify_tac 1); |
481 extend_set_Diff_distrib RS sym]) 1); |
493 by (REPEAT_FIRST (rtac conjI)); |
482 by (Blast_tac 1); |
494 (*first subgoal*) |
|
495 by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS |
|
496 constrains_Int RS constrains_weaken] |
|
497 addSDs [extend_constrains_project_set] |
|
498 addSDs [equalityD1]) 1); |
|
499 (*2nd subgoal*) |
|
500 by (etac (stableD RS constrains_Int RS constrains_weaken) 1); |
|
501 by (assume_tac 1); |
|
502 by (Blast_tac 3); |
|
503 by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib, |
|
504 extend_set_Un_distrib]) 2); |
|
505 by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2); |
|
506 by (full_simp_tac (simpset() addsimps [extend_set_def]) 1); |
|
507 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
508 (*The transient part*) |
|
509 by Auto_tac; |
|
510 by (force_tac (claset() addSDs [equalityD1] |
|
511 addIs [transient_extend_set_imp_project_transient RS |
|
512 transient_strengthen], |
|
513 simpset()) 2); |
|
514 by (full_simp_tac (simpset() addsimps [Int_Diff]) 1); |
|
515 by (force_tac (claset() addSDs [equalityD1] |
|
516 addIs [transient_extend_set_imp_project_transient RS |
|
517 project_extend_transient_D RS transient_strengthen], |
|
518 simpset()) 1); |
483 qed "ensures_extend_set_imp_project_ensures"; |
519 qed "ensures_extend_set_imp_project_ensures"; |
484 |
520 |
|
521 (*Used to prove project_leadsETo_D*) |
485 Goal "[| project h C G ~: transient (A-B) | A<=B; \ |
522 Goal "[| project h C G ~: transient (A-B) | A<=B; \ |
486 \ extend h F Join G : stable C; \ |
523 \ extend h F Join G : stable C; \ |
487 \ F Join project h C G : A ensures B |] \ |
524 \ F Join project h C G : A ensures B |] \ |
488 \ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"; |
525 \ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"; |
489 by (etac disjE 1); |
526 by (etac disjE 1); |
517 \ extend h F Join G : stable C; \ |
554 \ extend h F Join G : stable C; \ |
518 \ F Join project h C G : (project_set h C Int A) leadsTo B |] \ |
555 \ F Join project h C G : (project_set h C Int A) leadsTo B |] \ |
519 \ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; |
556 \ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; |
520 by (rtac (lemma RS leadsTo_weaken) 1); |
557 by (rtac (lemma RS leadsTo_weaken) 1); |
521 by (auto_tac (claset(), simpset() addsimps [split_extended_all])); |
558 by (auto_tac (claset(), simpset() addsimps [split_extended_all])); |
522 qed "project_leadsTo_lemma"; |
559 qed "project_leadsTo_D_lemma"; |
523 |
560 |
524 Goal "[| C = (reachable (extend h F Join G)); \ |
561 Goal "[| C = (reachable (extend h F Join G)); \ |
525 \ ALL D. project h C G : transient D --> D={}; \ |
562 \ ALL D. project h C G : transient D --> D={}; \ |
526 \ F Join project h C G : A LeadsTo B |] \ |
563 \ F Join project h C G : A LeadsTo B |] \ |
527 \ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"; |
564 \ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"; |
528 by (asm_full_simp_tac |
565 by (asm_full_simp_tac |
529 (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, |
566 (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, |
530 project_set_reachable_extend_eq]) 1); |
567 project_set_reachable_extend_eq]) 1); |
531 qed "Join_project_LeadsTo"; |
568 qed "Join_project_LeadsTo"; |
532 |
569 |
533 |
570 |
534 (*** GUARANTEES and EXTEND ***) |
571 (*** GUARANTEES and EXTEND ***) |