595 in simple cases it may be able to handle goals like |- MyProg --> []Inv. |
595 in simple cases it may be able to handle goals like |- MyProg --> []Inv. |
596 In these simple cases the simplifier seems to be more useful than the |
596 In these simple cases the simplifier seems to be more useful than the |
597 auto-tactic, which applies too much propositional logic and simplifies |
597 auto-tactic, which applies too much propositional logic and simplifies |
598 too late. |
598 too late. |
599 *) |
599 *) |
600 fun auto_inv_tac ss = |
600 fun auto_inv_tac ctxt = |
601 SELECT_GOAL |
601 SELECT_GOAL |
602 (inv_tac (map_simpset (K ss) @{context}) 1 THEN |
602 (inv_tac ctxt 1 THEN |
603 (TRYALL (action_simp_tac |
603 (TRYALL (action_simp_tac |
604 (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}]))); |
604 (simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}]))); |
605 *} |
605 *} |
606 |
606 |
607 method_setup invariant = {* |
607 method_setup invariant = {* |
608 Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac)) |
608 Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac)) |
609 *} "" |
609 *} "" |
610 |
610 |
611 method_setup auto_invariant = {* |
611 method_setup auto_invariant = {* |
612 Method.sections Clasimp.clasimp_modifiers |
612 Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac)) |
613 >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of)) |
|
614 *} "" |
613 *} "" |
615 |
614 |
616 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q" |
615 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q" |
617 apply (unfold dmd_def) |
616 apply (unfold dmd_def) |
618 apply (clarsimp dest!: BoxPrime [temp_use]) |
617 apply (clarsimp dest!: BoxPrime [temp_use]) |