463 |
463 |
464 text {* The so defined ML tactics are then ``exported'' to be used in |
464 text {* The so defined ML tactics are then ``exported'' to be used in |
465 Isabelle proofs. *} |
465 Isabelle proofs. *} |
466 |
466 |
467 method_setup oghoare = {* |
467 method_setup oghoare = {* |
468 Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *} |
468 Method.no_args (SIMPLE_METHOD' oghoare_tac) *} |
469 "verification condition generator for the oghoare logic" |
469 "verification condition generator for the oghoare logic" |
470 |
470 |
471 method_setup annhoare = {* |
471 method_setup annhoare = {* |
472 Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *} |
472 Method.no_args (SIMPLE_METHOD' annhoare_tac) *} |
473 "verification condition generator for the ann_hoare logic" |
473 "verification condition generator for the ann_hoare logic" |
474 |
474 |
475 method_setup interfree_aux = {* |
475 method_setup interfree_aux = {* |
476 Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *} |
476 Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *} |
477 "verification condition generator for interference freedom tests" |
477 "verification condition generator for interference freedom tests" |
478 |
478 |
479 text {* Tactics useful for dealing with the generated verification conditions: *} |
479 text {* Tactics useful for dealing with the generated verification conditions: *} |
480 |
480 |
481 method_setup conjI_tac = {* |
481 method_setup conjI_tac = {* |
482 Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *} |
482 Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *} |
483 "verification condition generator for interference freedom tests" |
483 "verification condition generator for interference freedom tests" |
484 |
484 |
485 ML {* |
485 ML {* |
486 fun disjE_Tac tac i st = st |> |
486 fun disjE_Tac tac i st = st |> |
487 ( (EVERY [etac disjE i, |
487 ( (EVERY [etac disjE i, |
488 disjE_Tac tac (i+1), |
488 disjE_Tac tac (i+1), |
489 tac i]) ORELSE (tac i) ) |
489 tac i]) ORELSE (tac i) ) |
490 *} |
490 *} |
491 |
491 |
492 method_setup disjE_tac = {* |
492 method_setup disjE_tac = {* |
493 Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *} |
493 Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *} |
494 "verification condition generator for interference freedom tests" |
494 "verification condition generator for interference freedom tests" |
495 |
495 |
496 end |
496 end |