--- a/src/HOL/TLA/Inc/Inc.thy Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Thu May 12 22:07:30 2011 +0200
@@ -112,7 +112,7 @@
by (auto simp: PsiInv_defs)
lemma PsiInv: "|- Psi --> []PsiInv"
- apply (tactic {* inv_tac (@{clasimpset} addsimps2 [@{thm Psi_def}]) 1 *})
+ apply (invariant simp: Psi_def)
apply (force simp: PsiInv_Init [try_rewrite] Init_def)
apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
@@ -125,7 +125,7 @@
*)
lemma "|- Psi --> []PsiInv"
- by (tactic {* auto_inv_tac (@{simpset} addsimps (@{thms PsiInv_defs} @ @{thms Psi_defs})) 1 *})
+ by (auto_invariant simp: PsiInv_defs Psi_defs)
(**** Step simulation ****)
--- a/src/HOL/TLA/Memory/Memory.thy Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Thu May 12 22:07:30 2011 +0200
@@ -147,8 +147,7 @@
(* The memory spec implies the memory invariant *)
lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
- by (tactic {* auto_inv_tac
- (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
+ by (auto_invariant simp: RM_temp_defs RM_action_defs)
(* The invariant is trivial for non-locations *)
lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
--- a/src/HOL/TLA/TLA.thy Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Thu May 12 22:07:30 2011 +0200
@@ -607,6 +607,16 @@
(ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
+method_setup invariant = {*
+ Method.sections Clasimp.clasimp_modifiers
+ >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
+*} ""
+
+method_setup auto_invariant = {*
+ Method.sections Clasimp.clasimp_modifiers
+ >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of))
+*} ""
+
lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
apply (unfold dmd_def)
apply (clarsimp dest!: BoxPrime [temp_use])