--- a/src/HOL/Auth/Shared.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Shared.thy Sat Jul 21 23:25:00 2007 +0200
@@ -195,22 +195,19 @@
{*
(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
-fun gen_possibility_tac ss state = state |>
+fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets]
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets]
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply])))
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state
-
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
-fun basic_possibility_tac st = st |>
+fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
*}
@@ -273,10 +270,15 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
+ Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
+ "for proving possibility theorems"
+
+method_setup basic_possibility = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (induct e) (auto simp: knows_Cons)
end