src/HOL/Auth/Smartcard/Smartcard.thy
changeset 23894 1a4167d761ac
parent 22265 3c5c6bdf61de
child 24122 fc7f857d33c8
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 21 23:25:00 2007 +0200
@@ -359,23 +359,20 @@
 {*
 (*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,
                          used_Inputs, used_C_Gets, used_Outpts, used_A_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]))
 *}
@@ -426,8 +423,8 @@
 val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
 
 val analz_image_freshK_ss = 
-     simpset() delsimps [image_insert, image_Un]
-	       delsimps [imp_disjL]    (*reduces blow-up*)
+     @{simpset} delsimps [image_insert, image_Un]
+	       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
 	       addsimps thms "analz_image_freshK_simps"
 *}
 
@@ -450,11 +447,16 @@
 
 method_setup possibility = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (gen_possibility_tac (Simplifier.get_local_simpset 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 \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (induct e) (auto simp: knows_Cons)
 
 (*Needed for actual protocols that will follow*)
 declare shrK_disj_crdK[THEN not_sym, iff]
@@ -466,8 +468,4 @@
 
 declare legalUse_def [iff] illegalUse_def [iff]
 
-
-
-
-
 end