tuned ML bindings (for multithreading);
authorwenzelm
Wed Aug 01 20:25:16 2007 +0200 (2007-08-01)
changeset 24122fc7f857d33c8
parent 24121 a93b0f4df838
child 24123 a0fc58900606
tuned ML bindings (for multithreading);
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Aug 01 19:59:12 2007 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Aug 01 20:25:16 2007 +0200
     1.3 @@ -258,18 +258,6 @@
     1.4         knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
     1.5         knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 -val analz_mono_contra_tac = 
    1.10 -  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.11 -  in
    1.12 -    rtac analz_impI THEN' 
    1.13 -    REPEAT1 o 
    1.14 -      (dresolve_tac (thms"analz_mono_contra"))
    1.15 -    THEN' mp_tac
    1.16 -  end
    1.17 -*}
    1.18 -
    1.19  
    1.20  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    1.21  by (induct e, auto simp: knows_Cons)
    1.22 @@ -289,6 +277,19 @@
    1.23             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.24      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
    1.25  
    1.26 +
    1.27 +ML
    1.28 +{*
    1.29 +val analz_mono_contra_tac = 
    1.30 +  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.31 +  in
    1.32 +    rtac analz_impI THEN' 
    1.33 +    REPEAT1 o 
    1.34 +      (dresolve_tac @{thms analz_mono_contra})
    1.35 +    THEN' mp_tac
    1.36 +  end
    1.37 +*}
    1.38 +
    1.39  method_setup analz_mono_contra = {*
    1.40      Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    1.41      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.42 @@ -297,51 +298,15 @@
    1.43  
    1.44  ML
    1.45  {*
    1.46 -val knows_Cons     = thm "knows_Cons"
    1.47 -val used_Nil       = thm "used_Nil"
    1.48 -val used_Cons      = thm "used_Cons"
    1.49 -
    1.50 -val Notes_imp_used = thm "Notes_imp_used";
    1.51 -val Says_imp_used = thm "Says_imp_used";
    1.52 -val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
    1.53 -val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
    1.54 -val knows_Spy_partsEs = thms "knows_Spy_partsEs";
    1.55 -val spies_partsEs = thms "spies_partsEs";
    1.56 -val Says_imp_spies = thm "Says_imp_spies";
    1.57 -val parts_insert_spies = thm "parts_insert_spies";
    1.58 -val Says_imp_knows = thm "Says_imp_knows";
    1.59 -val Notes_imp_knows = thm "Notes_imp_knows";
    1.60 -val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
    1.61 -val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
    1.62 -val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
    1.63 -val usedI = thm "usedI";
    1.64 -val initState_into_used = thm "initState_into_used";
    1.65 -val used_Says = thm "used_Says";
    1.66 -val used_Notes = thm "used_Notes";
    1.67 -val used_Gets = thm "used_Gets";
    1.68 -val used_nil_subset = thm "used_nil_subset";
    1.69 -val analz_mono_contra = thms "analz_mono_contra";
    1.70 -val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
    1.71 -val initState_subset_knows = thm "initState_subset_knows";
    1.72 -val keysFor_parts_insert = thm "keysFor_parts_insert";
    1.73 -
    1.74 -
    1.75 -val synth_analz_mono = thm "synth_analz_mono";
    1.76 -
    1.77 -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
    1.78 -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
    1.79 -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
    1.80 -
    1.81 -
    1.82  val synth_analz_mono_contra_tac = 
    1.83    let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.84    in
    1.85      rtac syan_impI THEN' 
    1.86      REPEAT1 o 
    1.87        (dresolve_tac 
    1.88 -       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
    1.89 -        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
    1.90 -	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
    1.91 +       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.92 +       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.93 +       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.94      THEN'
    1.95      mp_tac
    1.96    end;
     2.1 --- a/src/HOL/Auth/Message.thy	Wed Aug 01 19:59:12 2007 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Wed Aug 01 20:25:16 2007 +0200
     2.3 @@ -840,21 +840,8 @@
     2.4  subsection{*Tactics useful for many protocol proofs*}
     2.5  ML
     2.6  {*
     2.7 -val invKey = thm "invKey"
     2.8 -val keysFor_def = thm "keysFor_def"
     2.9 -val HPair_def = thm "HPair_def"
    2.10 -val symKeys_def = thm "symKeys_def"
    2.11 -val parts_mono = thm "parts_mono";
    2.12 -val analz_mono = thm "analz_mono";
    2.13 -val synth_mono = thm "synth_mono";
    2.14 -val analz_increasing = thm "analz_increasing";
    2.15 -
    2.16 -val analz_insertI = thm "analz_insertI";
    2.17 -val analz_subset_parts = thm "analz_subset_parts";
    2.18 -val Fake_parts_insert = thm "Fake_parts_insert";
    2.19 -val Fake_analz_insert = thm "Fake_analz_insert";
    2.20 -val pushes = thms "pushes";
    2.21 -
    2.22 +structure Message =
    2.23 +struct
    2.24  
    2.25  (*Prove base case (subgoal i) and simplify others.  A typical base case
    2.26    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    2.27 @@ -872,9 +859,9 @@
    2.28    Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
    2.29  *)
    2.30  val Fake_insert_tac = 
    2.31 -    dresolve_tac [impOfSubs Fake_analz_insert,
    2.32 -                  impOfSubs Fake_parts_insert] THEN'
    2.33 -    eresolve_tac [asm_rl, thm"synth.Inj"];
    2.34 +    dresolve_tac [impOfSubs @{thm Fake_analz_insert},
    2.35 +                  impOfSubs @{thm Fake_parts_insert}] THEN'
    2.36 +    eresolve_tac [asm_rl, @{thm synth.Inj}];
    2.37  
    2.38  fun Fake_insert_simp_tac ss i = 
    2.39      REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
    2.40 @@ -883,8 +870,8 @@
    2.41      (Fake_insert_simp_tac ss 1
    2.42       THEN
    2.43       IF_UNSOLVED (Blast.depth_tac
    2.44 -		  (cs addIs [analz_insertI,
    2.45 -				   impOfSubs analz_subset_parts]) 4 1))
    2.46 +		  (cs addIs [@{thm analz_insertI},
    2.47 +				   impOfSubs @{thm analz_subset_parts}]) 4 1))
    2.48  
    2.49  (*The explicit claset and simpset arguments help it work with Isar*)
    2.50  fun gen_spy_analz_tac (cs,ss) i =
    2.51 @@ -900,6 +887,8 @@
    2.52         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    2.53  
    2.54  fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    2.55 +
    2.56 +end
    2.57  *}
    2.58  
    2.59  text{*By default only @{text o_apply} is built-in.  But in the presence of
    2.60 @@ -951,18 +940,17 @@
    2.61  
    2.62  method_setup spy_analz = {*
    2.63      Method.ctxt_args (fn ctxt =>
    2.64 -        Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    2.65 +        Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    2.66      "for proving the Fake case when analz is involved"
    2.67  
    2.68  method_setup atomic_spy_analz = {*
    2.69      Method.ctxt_args (fn ctxt =>
    2.70 -        Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    2.71 +        Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    2.72      "for debugging spy_analz"
    2.73  
    2.74  method_setup Fake_insert_simp = {*
    2.75      Method.ctxt_args (fn ctxt =>
    2.76 -        Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    2.77 +        Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    2.78      "for debugging spy_analz"
    2.79  
    2.80 -
    2.81  end
     3.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Wed Aug 01 19:59:12 2007 +0200
     3.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Wed Aug 01 20:25:16 2007 +0200
     3.3 @@ -130,14 +130,10 @@
     3.4  
     3.5  ML
     3.6  {*
     3.7 -val Oops_parts_knows_Spy = thm "Oops_parts_knows_Spy"
     3.8 -val OR4_parts_knows_Spy = thm "OR4_parts_knows_Spy"
     3.9 -val OR2_parts_knows_Spy = thm "OR2_parts_knows_Spy"
    3.10 -
    3.11  fun parts_explicit_tac i = 
    3.12 -    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
    3.13 -    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
    3.14 -    forward_tac [OR2_parts_knows_Spy]  (i+4)
    3.15 +    forward_tac [@{thm Oops_parts_knows_Spy}] (i+7) THEN
    3.16 +    forward_tac [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
    3.17 +    forward_tac [@{thm OR2_parts_knows_Spy}]  (i+4)
    3.18  *}
    3.19   
    3.20  method_setup parts_explicit = {*
    3.21 @@ -249,21 +245,24 @@
    3.22  
    3.23  ML
    3.24  {*
    3.25 -val analz_image_freshCryptK_lemma = thm "analz_image_freshCryptK_lemma";
    3.26 -val analz_image_freshK_simps = thms "analz_image_freshK_simps";
    3.27 +structure OtwayReesBella =
    3.28 +struct
    3.29  
    3.30  val analz_image_freshK_ss = 
    3.31 -     simpset() delsimps [image_insert, image_Un]
    3.32 -	       delsimps [imp_disjL]    (*reduces blow-up*)
    3.33 -	       addsimps thms "analz_image_freshK_simps"
    3.34 +  @{simpset} delsimps [image_insert, image_Un]
    3.35 +      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
    3.36 +      addsimps @{thms analz_image_freshK_simps}
    3.37 +
    3.38 +end
    3.39  *}
    3.40  
    3.41  method_setup analz_freshCryptK = {*
    3.42      Method.ctxt_args (fn ctxt =>
    3.43       (Method.SIMPLE_METHOD
    3.44        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    3.45 -                          REPEAT_FIRST (rtac analz_image_freshCryptK_lemma),
    3.46 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
    3.47 +          REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
    3.48 +          ALLGOALS (asm_simp_tac
    3.49 +            (Simplifier.context ctxt OtwayReesBella.analz_image_freshK_ss))]))) *}
    3.50    "for proving useful rewrite rule"
    3.51  
    3.52  
     4.1 --- a/src/HOL/Auth/Public.thy	Wed Aug 01 19:59:12 2007 +0200
     4.2 +++ b/src/HOL/Auth/Public.thy	Wed Aug 01 20:25:16 2007 +0200
     4.3 @@ -377,13 +377,6 @@
     4.4  lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
     4.5  by blast
     4.6  
     4.7 -ML
     4.8 -{*
     4.9 -val Key_not_used = thm "Key_not_used";
    4.10 -val insert_Key_singleton = thm "insert_Key_singleton";
    4.11 -val insert_Key_image = thm "insert_Key_image";
    4.12 -*}
    4.13 -
    4.14  
    4.15  lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
    4.16  by (drule Crypt_imp_invKey_keysFor, simp)
    4.17 @@ -404,31 +397,17 @@
    4.18         Key_not_used insert_Key_image Un_assoc [THEN sym]
    4.19  
    4.20  ML {*
    4.21 -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
    4.22 -val analz_image_freshK_simps = thms "analz_image_freshK_simps";
    4.23 -val imp_disjL = thm "imp_disjL";
    4.24 -
    4.25 -val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un]
    4.26 -  delsimps [imp_disjL]    (*reduces blow-up*)
    4.27 -  addsimps thms "analz_image_freshK_simps"
    4.28 -*}
    4.29 +structure Public =
    4.30 +struct
    4.31  
    4.32 -method_setup analz_freshK = {*
    4.33 -    Method.ctxt_args (fn ctxt =>
    4.34 -     (Method.SIMPLE_METHOD
    4.35 -      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    4.36 -                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
    4.37 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
    4.38 -    "for proving the Session Key Compromise theorem"
    4.39 +val analz_image_freshK_ss = @{simpset} delsimps [image_insert, image_Un]
    4.40 +  delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
    4.41 +  addsimps @{thms analz_image_freshK_simps}
    4.42  
    4.43 -subsection{*Specialized Methods for Possibility Theorems*}
    4.44 -
    4.45 -ML
    4.46 -{*
    4.47  (*Tactic for possibility theorems*)
    4.48  fun possibility_tac ctxt =
    4.49      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    4.50 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
    4.51 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}]))
    4.52       THEN
    4.53       REPEAT_FIRST (eq_assume_tac ORELSE' 
    4.54                     resolve_tac [refl, conjI, @{thm Nonce_supply}]))
    4.55 @@ -440,16 +419,29 @@
    4.56      (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    4.57       THEN
    4.58       REPEAT_FIRST (resolve_tac [refl, conjI]))
    4.59 +
    4.60 +end
    4.61  *}
    4.62  
    4.63 +method_setup analz_freshK = {*
    4.64 +    Method.ctxt_args (fn ctxt =>
    4.65 +     (Method.SIMPLE_METHOD
    4.66 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    4.67 +          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    4.68 +          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
    4.69 +    "for proving the Session Key Compromise theorem"
    4.70 +
    4.71 +
    4.72 +subsection{*Specialized Methods for Possibility Theorems*}
    4.73 +
    4.74  method_setup possibility = {*
    4.75      Method.ctxt_args (fn ctxt =>
    4.76 -        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
    4.77 +        Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *}
    4.78      "for proving possibility theorems"
    4.79  
    4.80  method_setup basic_possibility = {*
    4.81      Method.ctxt_args (fn ctxt =>
    4.82 -        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
    4.83 +        Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *}
    4.84      "for proving possibility theorems"
    4.85  
    4.86  end
     5.1 --- a/src/HOL/Auth/Recur.thy	Wed Aug 01 19:59:12 2007 +0200
     5.2 +++ b/src/HOL/Auth/Recur.thy	Wed Aug 01 20:25:16 2007 +0200
     5.3 @@ -95,7 +95,7 @@
     5.4     (*No "oops" message can easily be expressed.  Each session key is
     5.5       associated--in two separate messages--with two nonces.  This is
     5.6       one try, but it isn't that useful.  Re domino attack, note that
     5.7 -     Recur.ML proves that each session key is secure provided the two
     5.8 +     Recur.thy proves that each session key is secure provided the two
     5.9       peers are, even if there are compromised agents elsewhere in
    5.10       the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
    5.11       etc.
     6.1 --- a/src/HOL/Auth/Shared.thy	Wed Aug 01 19:59:12 2007 +0200
     6.2 +++ b/src/HOL/Auth/Shared.thy	Wed Aug 01 20:25:16 2007 +0200
     6.3 @@ -163,55 +163,6 @@
     6.4      possibility theorems must assume the existence of a few keys.*}
     6.5  
     6.6  
     6.7 -subsection{*Tactics for possibility theorems*}
     6.8 -
     6.9 -ML
    6.10 -{*
    6.11 -val inj_shrK      = thm "inj_shrK";
    6.12 -val isSym_keys    = thm "isSym_keys";
    6.13 -val Nonce_supply = thm "Nonce_supply";
    6.14 -val invKey_K = thm "invKey_K";
    6.15 -val analz_Decrypt' = thm "analz_Decrypt'";
    6.16 -val keysFor_parts_initState = thm "keysFor_parts_initState";
    6.17 -val keysFor_parts_insert = thm "keysFor_parts_insert";
    6.18 -val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
    6.19 -val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
    6.20 -val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
    6.21 -val shrK_in_initState = thm "shrK_in_initState";
    6.22 -val shrK_in_used = thm "shrK_in_used";
    6.23 -val Key_not_used = thm "Key_not_used";
    6.24 -val shrK_neq = thm "shrK_neq";
    6.25 -val Nonce_notin_initState = thm "Nonce_notin_initState";
    6.26 -val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
    6.27 -val Nonce_supply_lemma = thm "Nonce_supply_lemma";
    6.28 -val Nonce_supply1 = thm "Nonce_supply1";
    6.29 -val Nonce_supply2 = thm "Nonce_supply2";
    6.30 -val Nonce_supply3 = thm "Nonce_supply3";
    6.31 -val Nonce_supply = thm "Nonce_supply";
    6.32 -*}
    6.33 -
    6.34 -
    6.35 -ML
    6.36 -{*
    6.37 -(*Omitting used_Says makes the tactic much faster: it leaves expressions
    6.38 -    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    6.39 -fun possibility_tac ctxt =
    6.40 -   (REPEAT 
    6.41 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets] 
    6.42 -                         setSolver safe_solver))
    6.43 -     THEN
    6.44 -     REPEAT_FIRST (eq_assume_tac ORELSE' 
    6.45 -                   resolve_tac [refl, conjI, Nonce_supply])))
    6.46 -
    6.47 -(*For harder protocols (such as Recur) where we have to set up some
    6.48 -  nonces and keys initially*)
    6.49 -fun basic_possibility_tac ctxt =
    6.50 -    REPEAT 
    6.51 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    6.52 -     THEN
    6.53 -     REPEAT_FIRST (resolve_tac [refl, conjI]))
    6.54 -*}
    6.55 -
    6.56  subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
    6.57  
    6.58  lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
    6.59 @@ -241,14 +192,40 @@
    6.60           (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
    6.61  by (blast intro: analz_mono [THEN [2] rev_subsetD])
    6.62  
    6.63 +
    6.64 +subsection{*Tactics for possibility theorems*}
    6.65 +
    6.66  ML
    6.67  {*
    6.68 -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
    6.69 +structure Shared =
    6.70 +struct
    6.71 +
    6.72 +(*Omitting used_Says makes the tactic much faster: it leaves expressions
    6.73 +    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    6.74 +fun possibility_tac ctxt =
    6.75 +   (REPEAT 
    6.76 +    (ALLGOALS (simp_tac (local_simpset_of ctxt
    6.77 +          delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] 
    6.78 +          setSolver safe_solver))
    6.79 +     THEN
    6.80 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
    6.81 +                   resolve_tac [refl, conjI, @{thm Nonce_supply}])))
    6.82  
    6.83 -val analz_image_freshK_ss = 
    6.84 -     simpset() delsimps [image_insert, image_Un]
    6.85 -	       delsimps [imp_disjL]    (*reduces blow-up*)
    6.86 -	       addsimps thms "analz_image_freshK_simps"
    6.87 +(*For harder protocols (such as Recur) where we have to set up some
    6.88 +  nonces and keys initially*)
    6.89 +fun basic_possibility_tac ctxt =
    6.90 +    REPEAT 
    6.91 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    6.92 +     THEN
    6.93 +     REPEAT_FIRST (resolve_tac [refl, conjI]))
    6.94 +
    6.95 +
    6.96 +val analz_image_freshK_ss =
    6.97 +  @{simpset} delsimps [image_insert, image_Un]
    6.98 +      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
    6.99 +      addsimps @{thms analz_image_freshK_simps}
   6.100 +
   6.101 +end
   6.102  *}
   6.103  
   6.104  
   6.105 @@ -264,18 +241,18 @@
   6.106      Method.ctxt_args (fn ctxt =>
   6.107       (Method.SIMPLE_METHOD
   6.108        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   6.109 -                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
   6.110 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
   6.111 +          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   6.112 +          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
   6.113      "for proving the Session Key Compromise theorem"
   6.114  
   6.115  method_setup possibility = {*
   6.116      Method.ctxt_args (fn ctxt =>
   6.117 -        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
   6.118 +        Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
   6.119      "for proving possibility theorems"
   6.120  
   6.121  method_setup basic_possibility = {*
   6.122      Method.ctxt_args (fn ctxt =>
   6.123 -        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
   6.124 +        Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
   6.125      "for proving possibility theorems"
   6.126  
   6.127  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
     7.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Aug 01 19:59:12 2007 +0200
     7.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Aug 01 20:25:16 2007 +0200
     7.3 @@ -272,7 +272,7 @@
     7.4  
     7.5  
     7.6  
     7.7 -(*Begin lemmas on secure means, from Event.ML, proved for shouprubin. They help
     7.8 +(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help
     7.9    the simplifier, especially in analz_image_freshK*)
    7.10  
    7.11  
    7.12 @@ -741,47 +741,43 @@
    7.13  
    7.14  ML
    7.15  {*
    7.16 -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
    7.17 -val Outpts_A_Card_form_4 = thm "Outpts_A_Card_form_4"
    7.18 -val Outpts_A_Card_form_10 = thm "Outpts_A_Card_form_10"
    7.19 -val Gets_imp_knows_Spy = thm "Gets_imp_knows_Spy"
    7.20 -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
    7.21 -val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd"
    7.22 -val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd"
    7.23 +structure ShoupRubin =
    7.24 +struct
    7.25  
    7.26  val prepare_tac = 
    7.27 - (*SR8*)   forward_tac [Outpts_B_Card_form_7] 14 THEN
    7.28 + (*SR8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
    7.29             eresolve_tac [exE] 15 THEN eresolve_tac [exE] 15 THEN 
    7.30 - (*SR9*)   forward_tac [Outpts_A_Card_form_4] 16 THEN 
    7.31 - (*SR11*)  forward_tac [Outpts_A_Card_form_10] 21 THEN
    7.32 + (*SR9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
    7.33 + (*SR11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 THEN
    7.34             eresolve_tac [exE] 22 THEN eresolve_tac [exE] 22
    7.35  
    7.36  fun parts_prepare_tac ctxt = 
    7.37             prepare_tac THEN
    7.38 - (*SR9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN 
    7.39 - (*SR9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN 
    7.40 - (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25    THEN               
    7.41 - (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN                
    7.42 + (*SR9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
    7.43 + (*SR9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
    7.44 + (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
    7.45 + (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
    7.46   (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
    7.47  
    7.48  val analz_prepare_tac = 
    7.49           prepare_tac THEN
    7.50 -         dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN 
    7.51 - (*SR9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN 
    7.52 +         dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN 
    7.53 + (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN 
    7.54           REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
    7.55  
    7.56 +end
    7.57  *}
    7.58  
    7.59  method_setup prepare = {*
    7.60 -    Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
    7.61 +    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *}
    7.62    "to launch a few simple facts that'll help the simplifier"
    7.63  
    7.64  method_setup parts_prepare = {*
    7.65 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
    7.66 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
    7.67    "additional facts to reason about parts"
    7.68  
    7.69  method_setup analz_prepare = {*
    7.70 -    Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
    7.71 +    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
    7.72    "additional facts to reason about analz"
    7.73  
    7.74  
    7.75 @@ -825,24 +821,17 @@
    7.76  apply auto
    7.77  done
    7.78  
    7.79 -ML
    7.80 -{*
    7.81 -val knows_Spy_Inputs_secureM_sr_Spy = thm "knows_Spy_Inputs_secureM_sr_Spy"
    7.82 -val knows_Spy_Outpts_secureM_sr_Spy = thm "knows_Spy_Outpts_secureM_sr_Spy"
    7.83 -val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans"
    7.84 -val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce"
    7.85 -*}
    7.86 -
    7.87  method_setup sc_analz_freshK = {*
    7.88      Method.ctxt_args (fn ctxt =>
    7.89       (Method.SIMPLE_METHOD
    7.90 -      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    7.91 -                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
    7.92 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
    7.93 -                                    addsimps [knows_Spy_Inputs_secureM_sr_Spy,
    7.94 -                                              knows_Spy_Outpts_secureM_sr_Spy,
    7.95 -                                              shouprubin_assumes_securemeans, 
    7.96 -                                              analz_image_Key_Un_Nonce]))]))) *}
    7.97 +      (EVERY [REPEAT_FIRST
    7.98 +       (resolve_tac [allI, ballI, impI]),
    7.99 +        REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   7.100 +        ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
   7.101 +          addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
   7.102 +                    @{thm knows_Spy_Outpts_secureM_sr_Spy},
   7.103 +                    @{thm shouprubin_assumes_securemeans}, 
   7.104 +                    @{thm analz_image_Key_Un_Nonce}]))]))) *}
   7.105      "for proving the Session Key Compromise theorem for smartcard protocols"
   7.106  
   7.107  
     8.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Aug 01 19:59:12 2007 +0200
     8.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Aug 01 20:25:16 2007 +0200
     8.3 @@ -277,7 +277,7 @@
     8.4  
     8.5  
     8.6  
     8.7 -(*Begin lemmas on secure means, from Event.ML, proved for shouprubin. They help
     8.8 +(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help
     8.9    the simplifier, especially in analz_image_freshK*)
    8.10  
    8.11  
    8.12 @@ -750,46 +750,42 @@
    8.13  
    8.14  ML
    8.15  {*
    8.16 -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
    8.17 -val Outpts_A_Card_form_4 = thm "Outpts_A_Card_form_4"
    8.18 -val Outpts_A_Card_form_10 = thm "Outpts_A_Card_form_10"
    8.19 -val Gets_imp_knows_Spy = thm "Gets_imp_knows_Spy"
    8.20 -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
    8.21 -val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd"
    8.22 -val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd"
    8.23 +structure ShoupRubinBella =
    8.24 +struct
    8.25  
    8.26  fun prepare_tac ctxt = 
    8.27 - (*SR_U8*)   forward_tac [Outpts_B_Card_form_7] 14 THEN
    8.28 + (*SR_U8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
    8.29   (*SR_U8*)   clarify_tac (local_claset_of ctxt) 15 THEN
    8.30 - (*SR_U9*)   forward_tac [Outpts_A_Card_form_4] 16 THEN 
    8.31 - (*SR_U11*)  forward_tac [Outpts_A_Card_form_10] 21 
    8.32 + (*SR_U9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
    8.33 + (*SR_U11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 
    8.34  
    8.35  fun parts_prepare_tac ctxt = 
    8.36             prepare_tac ctxt THEN
    8.37 - (*SR_U9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN 
    8.38 - (*SR_U9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN 
    8.39 - (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25    THEN               
    8.40 - (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN                
    8.41 + (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
    8.42 + (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
    8.43 + (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
    8.44 + (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
    8.45   (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
    8.46  
    8.47  fun analz_prepare_tac ctxt = 
    8.48           prepare_tac ctxt THEN
    8.49 -         dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN 
    8.50 - (*SR_U9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN 
    8.51 +         dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
    8.52 + (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
    8.53           REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
    8.54  
    8.55 +end
    8.56  *}
    8.57  
    8.58  method_setup prepare = {*
    8.59 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (prepare_tac ctxt)) *}
    8.60 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
    8.61    "to launch a few simple facts that'll help the simplifier"
    8.62  
    8.63  method_setup parts_prepare = {*
    8.64 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
    8.65 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
    8.66    "additional facts to reason about parts"
    8.67  
    8.68  method_setup analz_prepare = {*
    8.69 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (analz_prepare_tac ctxt)) *}
    8.70 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
    8.71    "additional facts to reason about analz"
    8.72  
    8.73  
    8.74 @@ -834,24 +830,16 @@
    8.75  apply auto
    8.76  done
    8.77  
    8.78 -ML
    8.79 -{*
    8.80 -val knows_Spy_Inputs_secureM_srb_Spy = thm "knows_Spy_Inputs_secureM_srb_Spy"
    8.81 -val knows_Spy_Outpts_secureM_srb_Spy = thm "knows_Spy_Outpts_secureM_srb_Spy"
    8.82 -val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans"
    8.83 -val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce"
    8.84 -*}
    8.85 -
    8.86  method_setup sc_analz_freshK = {*
    8.87      Method.ctxt_args (fn ctxt =>
    8.88       (Method.SIMPLE_METHOD
    8.89        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    8.90 -                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
    8.91 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
    8.92 -                                    addsimps [knows_Spy_Inputs_secureM_srb_Spy,
    8.93 -                                              knows_Spy_Outpts_secureM_srb_Spy,
    8.94 -                                              shouprubin_assumes_securemeans, 
    8.95 -                                              analz_image_Key_Un_Nonce]))]))) *}
    8.96 +          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    8.97 +          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
    8.98 +              addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
    8.99 +                  @{thm knows_Spy_Outpts_secureM_srb_Spy},
   8.100 +                  @{thm shouprubin_assumes_securemeans},
   8.101 +                  @{thm analz_image_Key_Un_Nonce}]))]))) *}
   8.102      "for proving the Session Key Compromise theorem for smartcard protocols"
   8.103  
   8.104  
     9.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Aug 01 19:59:12 2007 +0200
     9.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Aug 01 20:25:16 2007 +0200
     9.3 @@ -322,61 +322,6 @@
     9.4      possibility theorems must assume the existence of a few keys.*}
     9.5  
     9.6  
     9.7 -subsection{*Tactics for possibility theorems*}
     9.8 -
     9.9 -ML
    9.10 -{*
    9.11 -val inj_shrK      = thm "inj_shrK";
    9.12 -val isSym_keys    = thm "isSym_keys";
    9.13 -val Nonce_supply = thm "Nonce_supply";
    9.14 -val invKey_K = thm "invKey_K";
    9.15 -val analz_Decrypt' = thm "analz_Decrypt'";
    9.16 -val keysFor_parts_initState = thm "keysFor_parts_initState";
    9.17 -val keysFor_parts_insert = thm "keysFor_parts_insert";
    9.18 -val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
    9.19 -val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
    9.20 -val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
    9.21 -val shrK_in_initState = thm "shrK_in_initState";
    9.22 -val shrK_in_used = thm "shrK_in_used";
    9.23 -val Key_not_used = thm "Key_not_used";
    9.24 -val shrK_neq = thm "shrK_neq";
    9.25 -val Nonce_notin_initState = thm "Nonce_notin_initState";
    9.26 -val Nonce_supply1 = thm "Nonce_supply1";
    9.27 -val Nonce_supply2 = thm "Nonce_supply2";
    9.28 -val Nonce_supply3 = thm "Nonce_supply3";
    9.29 -val Nonce_supply = thm "Nonce_supply";
    9.30 -val used_Says = thm "used_Says";
    9.31 -val used_Gets = thm "used_Gets";
    9.32 -val used_Notes = thm "used_Notes";
    9.33 -val used_Inputs = thm "used_Inputs";
    9.34 -val used_C_Gets = thm "used_C_Gets";
    9.35 -val used_Outpts = thm "used_Outpts";
    9.36 -val used_A_Gets = thm "used_A_Gets";
    9.37 -*}
    9.38 -
    9.39 -
    9.40 -ML
    9.41 -{*
    9.42 -(*Omitting used_Says makes the tactic much faster: it leaves expressions
    9.43 -    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    9.44 -fun possibility_tac ctxt =
    9.45 -   (REPEAT 
    9.46 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets,
    9.47 -                         used_Inputs, used_C_Gets, used_Outpts, used_A_Gets] 
    9.48 -                         setSolver safe_solver))
    9.49 -     THEN
    9.50 -     REPEAT_FIRST (eq_assume_tac ORELSE' 
    9.51 -                   resolve_tac [refl, conjI, Nonce_supply])))
    9.52 -
    9.53 -(*For harder protocols (such as Recur) where we have to set up some
    9.54 -  nonces and keys initially*)
    9.55 -fun basic_possibility_tac ctxt =
    9.56 -    REPEAT 
    9.57 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    9.58 -     THEN
    9.59 -     REPEAT_FIRST (resolve_tac [refl, conjI]))
    9.60 -*}
    9.61 -
    9.62  subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
    9.63  
    9.64  lemma subset_Compl_range_shrK: "A \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A"
    9.65 @@ -418,18 +363,42 @@
    9.66           (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
    9.67  by (blast intro: analz_mono [THEN [2] rev_subsetD])
    9.68  
    9.69 +
    9.70 +subsection{*Tactics for possibility theorems*}
    9.71 +
    9.72  ML
    9.73  {*
    9.74 -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
    9.75 +structure Smartcard =
    9.76 +struct
    9.77 +
    9.78 +(*Omitting used_Says makes the tactic much faster: it leaves expressions
    9.79 +    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    9.80 +fun possibility_tac ctxt =
    9.81 +   (REPEAT 
    9.82 +    (ALLGOALS (simp_tac (local_simpset_of ctxt
    9.83 +      delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
    9.84 +        @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] 
    9.85 +      setSolver safe_solver))
    9.86 +     THEN
    9.87 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
    9.88 +                   resolve_tac [refl, conjI, @{thm Nonce_supply}])))
    9.89 +
    9.90 +(*For harder protocols (such as Recur) where we have to set up some
    9.91 +  nonces and keys initially*)
    9.92 +fun basic_possibility_tac ctxt =
    9.93 +    REPEAT 
    9.94 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    9.95 +     THEN
    9.96 +     REPEAT_FIRST (resolve_tac [refl, conjI]))
    9.97  
    9.98  val analz_image_freshK_ss = 
    9.99       @{simpset} delsimps [image_insert, image_Un]
   9.100  	       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
   9.101 -	       addsimps thms "analz_image_freshK_simps"
   9.102 +	       addsimps @{thms analz_image_freshK_simps}
   9.103 +end
   9.104  *}
   9.105  
   9.106  
   9.107 -
   9.108  (*Lets blast_tac perform this step without needing the simplifier*)
   9.109  lemma invKey_shrK_iff [iff]:
   9.110       "(Key (invKey K) \<in> X) = (Key K \<in> X)"
   9.111 @@ -441,18 +410,18 @@
   9.112      Method.ctxt_args (fn ctxt =>
   9.113       (Method.SIMPLE_METHOD
   9.114        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   9.115 -                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
   9.116 -                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
   9.117 +          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   9.118 +          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
   9.119      "for proving the Session Key Compromise theorem"
   9.120  
   9.121  method_setup possibility = {*
   9.122      Method.ctxt_args (fn ctxt =>
   9.123 -        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
   9.124 +        Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
   9.125      "for proving possibility theorems"
   9.126  
   9.127  method_setup basic_possibility = {*
   9.128      Method.ctxt_args (fn ctxt =>
   9.129 -        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
   9.130 +        Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
   9.131      "for proving possibility theorems"
   9.132  
   9.133  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"