469 ); |
469 ); |
470 |
470 |
471 (*proves "co" properties when the program is specified*) |
471 (*proves "co" properties when the program is specified*) |
472 |
472 |
473 fun constrains_tac ctxt = |
473 fun constrains_tac ctxt = |
474 let val ss = simpset_of ctxt in |
|
475 SELECT_GOAL |
474 SELECT_GOAL |
476 (EVERY [REPEAT (Always_Int_tac 1), |
475 (EVERY [REPEAT (Always_Int_tac 1), |
477 REPEAT (etac @{thm Always_ConstrainsI} 1 |
476 REPEAT (etac @{thm Always_ConstrainsI} 1 |
478 ORELSE |
477 ORELSE |
479 resolve_tac [@{thm StableI}, @{thm stableI}, |
478 resolve_tac [@{thm StableI}, @{thm stableI}, |
480 @{thm constrains_imp_Constrains}] 1), |
479 @{thm constrains_imp_Constrains}] 1), |
481 rtac @{thm constrainsI} 1, |
480 rtac @{thm constrainsI} 1, |
482 (* Three subgoals *) |
481 (* Three subgoals *) |
483 rewrite_goal_tac [@{thm st_set_def}] 3, |
482 rewrite_goal_tac [@{thm st_set_def}] 3, |
484 REPEAT (force_tac ctxt 2), |
483 REPEAT (force_tac ctxt 2), |
485 full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1, |
484 full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1, |
486 ALLGOALS (clarify_tac ctxt), |
485 ALLGOALS (clarify_tac ctxt), |
487 REPEAT (FIRSTGOAL (etac @{thm disjE})), |
486 REPEAT (FIRSTGOAL (etac @{thm disjE})), |
488 ALLGOALS (clarify_tac ctxt), |
487 ALLGOALS (clarify_tac ctxt), |
489 REPEAT (FIRSTGOAL (etac @{thm disjE})), |
488 REPEAT (FIRSTGOAL (etac @{thm disjE})), |
490 ALLGOALS (clarify_tac ctxt), |
489 ALLGOALS (clarify_tac ctxt), |
491 ALLGOALS (asm_full_simp_tac ss), |
490 ALLGOALS (asm_full_simp_tac ctxt), |
492 ALLGOALS (clarify_tac ctxt)]) |
491 ALLGOALS (clarify_tac ctxt)]); |
493 end; |
|
494 |
492 |
495 (*For proving invariants*) |
493 (*For proving invariants*) |
496 fun always_tac ctxt i = |
494 fun always_tac ctxt i = |
497 rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i; |
495 rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i; |
498 *} |
496 *} |