equal
deleted
inserted
replaced
531 |
531 |
532 (*Combines a list of invariance THEOREMS into one.*) |
532 (*Combines a list of invariance THEOREMS into one.*) |
533 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I); |
533 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I); |
534 |
534 |
535 (*To allow expansion of the program's definition when appropriate*) |
535 (*To allow expansion of the program's definition when appropriate*) |
536 val program_defs_ref = ref ([]: thm list); |
536 structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions"); |
537 |
537 |
538 (*proves "co" properties when the program is specified*) |
538 (*proves "co" properties when the program is specified*) |
539 |
539 |
540 fun constrains_tac ctxt = |
540 fun constrains_tac ctxt = |
541 let val css as (cs, ss) = local_clasimpset_of ctxt in |
541 let val css as (cs, ss) = local_clasimpset_of ctxt in |
547 constrains_imp_Constrains] 1), |
547 constrains_imp_Constrains] 1), |
548 rtac constrainsI 1, |
548 rtac constrainsI 1, |
549 (* Three subgoals *) |
549 (* Three subgoals *) |
550 rewrite_goal_tac [st_set_def] 3, |
550 rewrite_goal_tac [st_set_def] 3, |
551 REPEAT (force_tac css 2), |
551 REPEAT (force_tac css 2), |
552 full_simp_tac (ss addsimps !program_defs_ref) 1, |
552 full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1, |
553 ALLGOALS (clarify_tac cs), |
553 ALLGOALS (clarify_tac cs), |
554 REPEAT (FIRSTGOAL (etac disjE)), |
554 REPEAT (FIRSTGOAL (etac disjE)), |
555 ALLGOALS (clarify_tac cs), |
555 ALLGOALS (clarify_tac cs), |
556 REPEAT (FIRSTGOAL (etac disjE)), |
556 REPEAT (FIRSTGOAL (etac disjE)), |
557 ALLGOALS (clarify_tac cs), |
557 ALLGOALS (clarify_tac cs), |
562 (*For proving invariants*) |
562 (*For proving invariants*) |
563 fun always_tac ctxt i = |
563 fun always_tac ctxt i = |
564 rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i; |
564 rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i; |
565 *} |
565 *} |
566 |
566 |
|
567 setup ProgramDefs.setup |
|
568 |
567 method_setup safety = {* |
569 method_setup safety = {* |
568 Method.ctxt_args (fn ctxt => |
570 Method.ctxt_args (fn ctxt => |
569 Method.SIMPLE_METHOD' (constrains_tac ctxt)) *} |
571 Method.SIMPLE_METHOD' (constrains_tac ctxt)) *} |
570 "for proving safety properties" |
572 "for proving safety properties" |
571 |
573 |