104 by (auto_tac (claset(), |
104 by (auto_tac (claset(), |
105 simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
105 simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
106 extend_stable RS iffD1])); |
106 extend_stable RS iffD1])); |
107 qed "Join_project_increasing"; |
107 qed "Join_project_increasing"; |
108 |
108 |
|
109 (*For using project_guarantees in particular cases*) |
|
110 Goal "extend h F Join G : extend_set h A co extend_set h B \ |
|
111 \ ==> F Join project UNIV h G : A co B"; |
|
112 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
113 by (asm_full_simp_tac |
|
114 (simpset() addsimps [project_constrains, Join_constrains, |
|
115 extend_constrains]) 1); |
|
116 by (fast_tac (claset() addDs [constrains_imp_subset]) 1); |
|
117 qed "project_constrains_I"; |
|
118 |
109 |
119 |
110 (*** Diff, needed for localTo ***) |
120 (*** Diff, needed for localTo ***) |
111 |
121 |
112 (*Opposite direction fails because Diff in the extended state may remove |
122 (*Opposite direction fails because Diff in the extended state may remove |
113 fewer actions, i.e. those that affect other state variables.*) |
123 fewer actions, i.e. those that affect other state variables.*) |
138 by (etac Diff_project_co 1); |
148 by (etac Diff_project_co 1); |
139 by (assume_tac 1); |
149 by (assume_tac 1); |
140 qed "Diff_project_stable"; |
150 qed "Diff_project_stable"; |
141 |
151 |
142 (*Converse appears to fail*) |
152 (*Converse appears to fail*) |
143 Goal "[| UNIV <= project_set h C; (H : (func o f) localTo extend h G) |] \ |
153 Goal "[| UNIV <= project_set h C; H : (func o f) localTo extend h G |] \ |
144 \ ==> (project C h H : func localTo G)"; |
154 \ ==> project C h H : func localTo G"; |
145 by (asm_full_simp_tac |
155 by (asm_full_simp_tac |
146 (simpset() addsimps [localTo_def, |
156 (simpset() addsimps [localTo_def, |
147 project_extend_Join RS sym, |
157 project_extend_Join RS sym, |
148 subset_UNIV RS subset_trans RS Diff_project_stable, |
158 subset_UNIV RS subset_trans RS Diff_project_stable, |
149 Collect_eq_extend_set RS sym]) 1); |
159 Collect_eq_extend_set RS sym]) 1); |
|
160 qed "project_localTo_lemma"; |
|
161 |
|
162 Goal "extend h F Join G : (v o f) localTo extend h H \ |
|
163 \ ==> F Join project UNIV h G : v localTo H"; |
|
164 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
165 by (asm_simp_tac |
|
166 (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1); |
150 qed "project_localTo_I"; |
167 qed "project_localTo_I"; |
151 |
168 |
152 |
169 |
153 (** Reachability and project **) |
170 (** Reachability and project **) |
154 |
171 |
367 by (asm_simp_tac (simpset() delsimps UN_simps |
395 by (asm_simp_tac (simpset() delsimps UN_simps |
368 addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); |
396 addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); |
369 by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, |
397 by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, |
370 leadsTo_Trans]) 2); |
398 leadsTo_Trans]) 2); |
371 by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1); |
399 by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1); |
372 qed "Join_project_leadsTo_I"; |
400 qed "project_leadsTo_lemma"; |
373 |
401 |
374 (*Instance of the previous theorem for STRONG progress*) |
402 (*Instance of the previous theorem for STRONG progress*) |
375 Goal "[| ALL x. project UNIV h G ~: transient {x}; \ |
403 Goal "[| ALL x. project UNIV h G ~: transient {x}; \ |
376 \ F Join project UNIV h G : A leadsTo B |] \ |
404 \ F Join project UNIV h G : A leadsTo B |] \ |
377 \ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
405 \ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
378 by (dtac Join_project_leadsTo_I 1); |
406 by (dtac project_leadsTo_lemma 1); |
379 by Auto_tac; |
407 by Auto_tac; |
380 qed "Join_project_UNIV_leadsTo_I"; |
408 qed "project_UNIV_leadsTo_lemma"; |
381 |
409 |
382 (** Towards the analogous theorem for WEAK progress*) |
410 (** Towards the analogous theorem for WEAK progress*) |
383 |
411 |
384 Goal "[| ALL x. project C h G ~: transient {x}; \ |
412 Goal "[| ALL x. project C h G ~: transient {x}; \ |
385 \ extend h F Join G : stable C; \ |
413 \ extend h F Join G : stable C; \ |
473 by (etac project_guarantees 1); |
501 by (etac project_guarantees 1); |
474 by (rtac (subset_UNIV RS project_Increasing_D) 2); |
502 by (rtac (subset_UNIV RS project_Increasing_D) 2); |
475 by Auto_tac; |
503 by Auto_tac; |
476 qed "extend_guar_Increasing"; |
504 qed "extend_guar_Increasing"; |
477 |
505 |
478 Goal "F : (func localTo G) guarantees increasing func \ |
506 Goal "F : (v localTo G) guarantees increasing func \ |
479 \ ==> extend h F : (func o f) localTo (extend h G) \ |
507 \ ==> extend h F : (v o f) localTo (extend h G) \ |
480 \ guarantees increasing (func o f)"; |
508 \ guarantees increasing (func o f)"; |
481 by (etac project_guarantees 1); |
509 by (etac project_guarantees 1); |
482 (*the "increasing" guarantee*) |
510 (*the "increasing" guarantee*) |
483 by (asm_simp_tac |
511 by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2); |
484 (simpset() addsimps [Join_project_increasing RS sym]) 2); |
512 by (etac project_localTo_I 1); |
485 (*the "localTo" requirement*) |
|
486 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
487 by (asm_simp_tac |
|
488 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
|
489 qed "extend_localTo_guar_increasing"; |
513 qed "extend_localTo_guar_increasing"; |
490 |
514 |
491 Goal "F : (func localTo G) guarantees Increasing func \ |
515 Goal "F : (v localTo G) guarantees Increasing func \ |
492 \ ==> extend h F : (func o f) localTo (extend h G) \ |
516 \ ==> extend h F : (v o f) localTo (extend h G) \ |
493 \ guarantees Increasing (func o f)"; |
517 \ guarantees Increasing (func o f)"; |
494 by (etac project_guarantees 1); |
518 by (etac project_guarantees 1); |
495 (*the "Increasing" guarantee*) |
519 (*the "Increasing" guarantee*) |
496 by (etac (subset_UNIV RS project_Increasing_D) 2); |
520 by (etac (subset_UNIV RS project_Increasing_D) 2); |
497 (*the "localTo" requirement*) |
521 by (etac project_localTo_I 1); |
498 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
499 by (asm_simp_tac |
|
500 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
|
501 qed "extend_localTo_guar_Increasing"; |
522 qed "extend_localTo_guar_Increasing"; |
|
523 |
|
524 Goal "F : Always A guarantees Always B \ |
|
525 \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)"; |
|
526 by (etac project_guarantees 1); |
|
527 by (etac (subset_refl RS project_Always_D) 2); |
|
528 by (etac (subset_refl RS project_Always_I) 1); |
|
529 qed "extend_guar_Always"; |
502 |
530 |
503 |
531 |
504 (** Guarantees with a leadsTo postcondition **) |
532 (** Guarantees with a leadsTo postcondition **) |
505 |
533 |
506 Goal "[| G : f localTo extend h F; \ |
534 Goal "[| G : f localTo extend h F; \ |
507 \ Disjoint (extend h F) G |] ==> project C h G : stable {x}"; |
535 \ Disjoint (extend h F) G |] ==> project C h G : stable {x}"; |
508 by (asm_full_simp_tac |
536 by (asm_full_simp_tac |
509 (simpset() addsimps [localTo_imp_stable, |
537 (simpset() addsimps [localTo_imp_stable, |
510 extend_set_sing, project_stable_I]) 1); |
538 extend_set_sing, project_stable_I]) 1); |
511 qed "localTo_imp_project_stable"; |
539 qed "localTo_imp_project_stable"; |
512 |
|
513 |
540 |
514 Goal "F : stable{s} ==> F ~: transient {s}"; |
541 Goal "F : stable{s} ==> F ~: transient {s}"; |
515 by (auto_tac (claset(), |
542 by (auto_tac (claset(), |
516 simpset() addsimps [FP_def, transient_def, |
543 simpset() addsimps [FP_def, transient_def, |
517 stable_def, constrains_def])); |
544 stable_def, constrains_def])); |
518 qed "stable_sing_imp_not_transient"; |
545 qed "stable_sing_imp_not_transient"; |
519 |
546 |
|
547 Goal "[| F Join project UNIV h G : A leadsTo B; \ |
|
548 \ extend h F Join G : f localTo extend h F; \ |
|
549 \ Disjoint (extend h F) G |] \ |
|
550 \ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
|
551 by (rtac project_UNIV_leadsTo_lemma 1); |
|
552 by Auto_tac; |
|
553 by (asm_full_simp_tac |
|
554 (simpset() addsimps [Join_localTo, self_localTo, |
|
555 localTo_imp_project_stable, |
|
556 stable_sing_imp_not_transient]) 1); |
|
557 qed "project_leadsTo_D"; |
|
558 |
|
559 |
|
560 Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \ |
|
561 \ extend h F Join G : f localTo extend h F; \ |
|
562 \ Disjoint (extend h F) G |] \ |
|
563 \ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"; |
|
564 by (rtac Join_project_LeadsTo 1); |
|
565 by Auto_tac; |
|
566 by (asm_full_simp_tac |
|
567 (simpset() addsimps [Join_localTo, self_localTo, |
|
568 localTo_imp_project_stable, |
|
569 stable_sing_imp_not_transient]) 1); |
|
570 qed "project_LeadsTo_D"; |
|
571 |
|
572 |
520 (*STRONG precondition and postcondition*) |
573 (*STRONG precondition and postcondition*) |
521 Goal "F : (A co A') guarantees (B leadsTo B') \ |
574 Goal "F : (A co A') guarantees (B leadsTo B') \ |
522 \ ==> extend h F : ((extend_set h A) co (extend_set h A')) \ |
575 \ ==> extend h F : ((extend_set h A) co (extend_set h A')) \ |
523 \ Int (f localTo (extend h F)) \ |
576 \ Int (f localTo (extend h F)) \ |
524 \ guarantees ((extend_set h B) leadsTo (extend_set h B'))"; |
577 \ guarantees ((extend_set h B) leadsTo (extend_set h B'))"; |
525 by (etac project_guarantees 1); |
578 by (etac project_guarantees 1); |
526 (*the safety precondition*) |
579 (*the safety precondition*) |
527 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
580 by (fast_tac (claset() addIs [project_constrains_I]) 1); |
528 by (asm_full_simp_tac |
|
529 (simpset() addsimps [project_constrains, Join_constrains, |
|
530 extend_constrains]) 1); |
|
531 by (fast_tac (claset() addDs [constrains_imp_subset]) 1); |
|
532 (*the liveness postcondition*) |
581 (*the liveness postcondition*) |
533 by (rtac Join_project_UNIV_leadsTo_I 1); |
582 by (fast_tac (claset() addIs [project_leadsTo_D]) 1); |
534 by Auto_tac; |
|
535 by (asm_full_simp_tac |
|
536 (simpset() addsimps [Join_localTo, self_localTo, |
|
537 localTo_imp_project_stable, |
|
538 stable_sing_imp_not_transient]) 1); |
|
539 qed "extend_co_guar_leadsTo"; |
583 qed "extend_co_guar_leadsTo"; |
540 |
584 |
541 (*WEAK precondition and postcondition*) |
585 (*WEAK precondition and postcondition*) |
542 Goal "F : (A Co A') guarantees (B LeadsTo B') \ |
586 Goal "F : (A Co A') guarantees (B LeadsTo B') \ |
543 \ ==> extend h F : ((extend_set h A) Co (extend_set h A')) \ |
587 \ ==> extend h F : ((extend_set h A) Co (extend_set h A')) \ |