Conversion to use blast_tac (with other improvements)
authorpaulson
Wed May 07 13:01:43 1997 +0200 (1997-05-07)
changeset 3121cbb6c0c1c58a
parent 3120 c58423c20740
child 3122 2fe26ca380a1
Conversion to use blast_tac (with other improvements)
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Wed May 07 12:50:26 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Wed May 07 13:01:43 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
     1.6  by (Blast_tac 1);
     1.7 -qed "keysFor_UN";
     1.8 +qed "keysFor_UN1";
     1.9  
    1.10  (*Monotonicity*)
    1.11  goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    1.12 @@ -67,9 +67,11 @@
    1.13  by (Auto_tac());
    1.14  qed "keysFor_insert_Crypt";
    1.15  
    1.16 -Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    1.17 +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
    1.18            keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    1.19            keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.20 +AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
    1.21 +	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
    1.22  
    1.23  goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.24  by (Blast_tac 1);
    1.25 @@ -173,8 +175,12 @@
    1.26  by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
    1.27  qed "parts_UN1";
    1.28  
    1.29 -(*Added to simplify arguments to parts, analz and synth*)
    1.30 +(*Added to simplify arguments to parts, analz and synth.
    1.31 +  NOTE: the UN versions are no longer used!*)
    1.32  Addsimps [parts_Un, parts_UN, parts_UN1];
    1.33 +AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
    1.34 +	parts_UN RS equalityD1 RS subsetD RS UN_E,
    1.35 +	parts_UN1 RS equalityD1 RS subsetD RS UN1_E];
    1.36  
    1.37  goal thy "insert X (parts H) <= parts(insert X H)";
    1.38  by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
    1.39 @@ -809,6 +815,21 @@
    1.40  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
    1.41  val pushes = pushKeys@pushCrypts;
    1.42  
    1.43 +
    1.44 +(*** Tactics useful for many protocol proofs ***)
    1.45 +
    1.46 +(*Prove base case (subgoal i) and simplify others*)
    1.47 +fun prove_simple_subgoals_tac i = 
    1.48 +    fast_tac (!claset addss (!simpset)) i THEN
    1.49 +    ALLGOALS Asm_simp_tac;
    1.50 +
    1.51 +fun Fake_parts_insert_tac i = 
    1.52 +    blast_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.53 +			      impOfSubs Fake_parts_insert]) i;
    1.54 +
    1.55 +(*Apply rules to break down assumptions of the form
    1.56 +  Y : parts(insert X H)  and  Y : analz(insert X H)
    1.57 +*)
    1.58  val Fake_insert_tac = 
    1.59      dresolve_tac [impOfSubs Fake_analz_insert,
    1.60                    impOfSubs Fake_parts_insert] THEN'
     2.1 --- a/src/HOL/Auth/NS_Public.ML	Wed May 07 12:50:26 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Public.ML	Wed May 07 13:01:43 1997 +0200
     2.3 @@ -12,15 +12,12 @@
     2.4  proof_timing:=true;
     2.5  HOL_quantifiers := false;
     2.6  
     2.7 -val op addss = op unsafe_addss;
     2.8 -
     2.9  AddIffs [Spy_in_lost];
    2.10  
    2.11  (*Replacing the variable by a constant improves search speed by 50%!*)
    2.12  val Says_imp_sees_Spy' = 
    2.13      read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    2.14  
    2.15 -
    2.16  (*A "possibility property": there are traces that reach the end*)
    2.17  goal thy 
    2.18   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    2.19 @@ -42,17 +39,6 @@
    2.20  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    2.21  
    2.22  
    2.23 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    2.24 -fun parts_induct_tac i = SELECT_GOAL
    2.25 -    (DETERM (etac ns_public.induct 1 THEN 
    2.26 -             (*Fake message*)
    2.27 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.28 -                                           impOfSubs Fake_parts_insert]
    2.29 -                                    addss (!simpset)) 2)) THEN
    2.30 -     (*Base case*)
    2.31 -     fast_tac (!claset addss (!simpset)) 1 THEN
    2.32 -     ALLGOALS Asm_simp_tac) i;
    2.33 -
    2.34  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    2.35      sends messages containing X! **)
    2.36  
    2.37 @@ -60,8 +46,9 @@
    2.38  goal thy 
    2.39   "!!evs. evs : ns_public \
    2.40  \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    2.41 -by (parts_induct_tac 1);
    2.42 -by (Auto_tac());
    2.43 +by (etac ns_public.induct 1);
    2.44 +by (prove_simple_subgoals_tac 1);
    2.45 +by (Fake_parts_insert_tac 1);
    2.46  qed "Spy_see_priK";
    2.47  Addsimps [Spy_see_priK];
    2.48  
    2.49 @@ -74,7 +61,7 @@
    2.50  
    2.51  goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
    2.52  \                  evs : ns_public |] ==> A:lost";
    2.53 -by (fast_tac (!claset addDs [Spy_see_priK]) 1);
    2.54 +by (blast_tac (!claset addDs [Spy_see_priK]) 1);
    2.55  qed "Spy_see_priK_D";
    2.56  
    2.57  bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    2.58 @@ -82,7 +69,7 @@
    2.59  
    2.60  
    2.61  fun analz_induct_tac i = 
    2.62 -    etac ns_public.induct i     THEN
    2.63 +    etac ns_public.induct i   THEN
    2.64      ALLGOALS (asm_simp_tac 
    2.65                (!simpset addsimps [not_parts_not_analz]
    2.66                          setloop split_tac [expand_if]));
    2.67 @@ -100,16 +87,15 @@
    2.68  by (etac rev_mp 1);
    2.69  by (analz_induct_tac 1);
    2.70  (*NS3*)
    2.71 -by (fast_tac (!claset addSEs partsEs) 4);
    2.72 +by (blast_tac (!claset addSEs partsEs) 4);
    2.73  (*NS2*)
    2.74 -by (fast_tac (!claset addSEs partsEs) 3);
    2.75 +by (blast_tac (!claset addSEs partsEs) 3);
    2.76  (*Fake*)
    2.77 -by (deepen_tac (!claset addSIs [analz_insertI]
    2.78 +by (blast_tac (!claset addSIs [analz_insertI]
    2.79                          addDs [impOfSubs analz_subset_parts,
    2.80 -			       impOfSubs Fake_parts_insert]
    2.81 -			addss (!simpset)) 0 2);
    2.82 +			       impOfSubs Fake_parts_insert]) 2);
    2.83  (*Base*)
    2.84 -by (fast_tac (!claset addss (!simpset)) 1);
    2.85 +by (Blast_tac 1);
    2.86  qed "no_nonce_NS1_NS2";
    2.87  
    2.88  
    2.89 @@ -124,17 +110,16 @@
    2.90  (*NS1*)
    2.91  by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
    2.92  by (expand_case_tac "NA = ?y" 3 THEN
    2.93 -    REPEAT (fast_tac (!claset addSEs partsEs) 3));
    2.94 +    REPEAT (blast_tac (!claset addSEs partsEs) 3));
    2.95  (*Base*)
    2.96 -by (fast_tac (!claset addss (!simpset)) 1);
    2.97 +by (Blast_tac 1);
    2.98  (*Fake*)
    2.99  by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   2.100  by (step_tac (!claset addSIs [analz_insertI]) 1);
   2.101  by (ex_strip_tac 1);
   2.102 -by (best_tac (!claset delrules [conjI]
   2.103 +by (blast_tac (!claset delrules [conjI]
   2.104                        addSDs [impOfSubs Fake_parts_insert]
   2.105 -                      addDs  [impOfSubs analz_subset_parts]
   2.106 -                      addss (!simpset)) 1);
   2.107 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   2.108  val lemma = result();
   2.109  
   2.110  goal thy 
   2.111 @@ -155,14 +140,14 @@
   2.112  by (etac rev_mp 1);
   2.113  by (analz_induct_tac 1);
   2.114  (*NS3*)
   2.115 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.116 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   2.117 +by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
   2.118 +                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   2.119  (*NS2*)
   2.120 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.121 -                        addSEs [MPair_parts]
   2.122 -			addDs  [parts.Body, unique_NA]) 0 3);
   2.123 +by (blast_tac (!claset addSEs [MPair_parts]
   2.124 +		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   2.125 +			       parts.Body, unique_NA]) 3);
   2.126  (*NS1*)
   2.127 -by (fast_tac (!claset addSEs sees_Spy_partsEs
   2.128 +by (blast_tac (!claset addSEs sees_Spy_partsEs
   2.129                        addIs  [impOfSubs analz_subset_parts]) 2);
   2.130  (*Fake*)
   2.131  by (spy_analz_tac 1);
   2.132 @@ -184,15 +169,11 @@
   2.133  by (etac ns_public.induct 1);
   2.134  by (ALLGOALS Asm_simp_tac);
   2.135  (*NS1*)
   2.136 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.137 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.138  (*Fake*)
   2.139 -by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   2.140 -by (fast_tac (!claset addss (!simpset)) 1);
   2.141 -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   2.142 -by (best_tac (!claset addSIs [disjI2]
   2.143 -                      addSDs [impOfSubs Fake_parts_insert]
   2.144 -                      addDs  [impOfSubs analz_subset_parts]
   2.145 -                      addss (!simpset)) 1);
   2.146 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   2.147 +                       addDs  [Spy_not_see_NA, 
   2.148 +			       impOfSubs analz_subset_parts]) 1);
   2.149  qed "A_trusts_NS2";
   2.150  
   2.151  (*If the encrypted message appears then it originated with Alice in NS1*)
   2.152 @@ -205,13 +186,11 @@
   2.153  by (etac rev_mp 1);
   2.154  by (analz_induct_tac 1);
   2.155  (*Fake*)
   2.156 -by (best_tac (!claset addSIs [disjI2]
   2.157 -                      addSDs [impOfSubs Fake_parts_insert]
   2.158 -                      addIs  [analz_insertI]
   2.159 -                      addDs  [impOfSubs analz_subset_parts]
   2.160 -                      addss (!simpset)) 2);
   2.161 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   2.162 +                       addIs  [analz_insertI]
   2.163 +                       addDs  [impOfSubs analz_subset_parts]) 2);
   2.164  (*Base*)
   2.165 -by (fast_tac (!claset addss (!simpset)) 1);
   2.166 +by (Blast_tac 1);
   2.167  qed "B_trusts_NS1";
   2.168  
   2.169  
   2.170 @@ -231,17 +210,16 @@
   2.171  (*NS2*)
   2.172  by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   2.173  by (expand_case_tac "NB = ?y" 3 THEN
   2.174 -    REPEAT (fast_tac (!claset addSEs partsEs) 3));
   2.175 +    REPEAT (blast_tac (!claset addSEs partsEs) 3));
   2.176  (*Base*)
   2.177 -by (fast_tac (!claset addss (!simpset)) 1);
   2.178 +by (Blast_tac 1);
   2.179  (*Fake*)
   2.180  by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   2.181  by (step_tac (!claset addSIs [analz_insertI]) 1);
   2.182  by (ex_strip_tac 1);
   2.183 -by (best_tac (!claset delrules [conjI]
   2.184 +by (blast_tac (!claset delrules [conjI]
   2.185                        addSDs [impOfSubs Fake_parts_insert]
   2.186 -                      addDs  [impOfSubs analz_subset_parts] 
   2.187 -                      addss (!simpset)) 1);
   2.188 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   2.189  val lemma = result();
   2.190  
   2.191  goal thy 
   2.192 @@ -265,26 +243,21 @@
   2.193  by (etac rev_mp 1);
   2.194  by (analz_induct_tac 1);
   2.195  (*NS3*)
   2.196 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.197 -                      addDs  [unique_NB]) 4);
   2.198 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
   2.199 +			      unique_NB]) 4);
   2.200  (*NS1*)
   2.201 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.202 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.203  (*Fake*)
   2.204  by (spy_analz_tac 1);
   2.205  (*NS2*)
   2.206  by (Step_tac 1);
   2.207 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
   2.208 -by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.209 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   2.210 -by (fast_tac (!claset addIs  [impOfSubs analz_subset_parts]) 1);
   2.211 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   2.212 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.213 +                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   2.214 +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
   2.215  qed "Spy_not_see_NB";
   2.216  
   2.217  
   2.218 -(*Matches only NS2, not NS1 (or NS3)*)
   2.219 -val Says_imp_sees_Spy'' = 
   2.220 -    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
   2.221 -
   2.222 -
   2.223  (*Authentication for B: if he receives message 3 and has used NB
   2.224    in message 2, then A has sent message 3.*)
   2.225  goal thy 
   2.226 @@ -296,28 +269,27 @@
   2.227  by (etac rev_mp 1);
   2.228  (*prepare induction over Crypt (pubK B) NB : parts H*)
   2.229  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
   2.230 -by (etac ns_public.induct 1);
   2.231 -by (ALLGOALS Asm_simp_tac);
   2.232 +by (analz_induct_tac 1);
   2.233  (*NS1*)
   2.234 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.235 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.236  (*Fake*)
   2.237 -by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   2.238 -by (fast_tac (!claset addss (!simpset)) 1);
   2.239 -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   2.240 -by (best_tac (!claset addSIs [disjI2]
   2.241 -                      addSDs [impOfSubs Fake_parts_insert]
   2.242 -                      addDs  [impOfSubs analz_subset_parts] 
   2.243 -                      addss (!simpset)) 1);
   2.244 -(*NS3*)
   2.245 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   2.246 +                       addDs  [Spy_not_see_NB, 
   2.247 +			       impOfSubs analz_subset_parts]) 1);
   2.248 +(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
   2.249  by (Step_tac 1);
   2.250 -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   2.251 -by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   2.252 -                      addDs  [unique_NB]) 1);
   2.253 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
   2.254 +			      Spy_not_see_NB, unique_NB]) 1);
   2.255  qed "B_trusts_NS3";
   2.256  
   2.257  
   2.258  (**** Overall guarantee for B*)
   2.259  
   2.260 +(*Matches only NS2, not NS1 (or NS3)*)
   2.261 +val Says_imp_sees_Spy'' = 
   2.262 +    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
   2.263 +
   2.264 +
   2.265  (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   2.266    NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
   2.267  goal thy 
   2.268 @@ -333,19 +305,18 @@
   2.269  by (ALLGOALS Asm_simp_tac);
   2.270  (*Fake, NS2, NS3*)
   2.271  (*NS1*)
   2.272 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.273 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   2.274  (*Fake*)
   2.275  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   2.276 -by (fast_tac (!claset addss (!simpset)) 1);
   2.277 +by (Blast_tac 1);
   2.278  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   2.279 -by (best_tac (!claset addSIs [disjI2]
   2.280 +by (blast_tac (!claset addSIs [disjI2]
   2.281                        addDs [impOfSubs analz_subset_parts,
   2.282 -                             impOfSubs Fake_parts_insert]
   2.283 -                      addss (!simpset)) 1);
   2.284 +                             impOfSubs Fake_parts_insert]) 1);
   2.285  (*NS3*)
   2.286  by (Step_tac 1);
   2.287  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   2.288 -by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   2.289 -                      addDs  [unique_NB]) 1);
   2.290 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   2.291 +                       addDs  [unique_NB]) 1);
   2.292  qed "B_trusts_protocol";
   2.293  
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Wed May 07 12:50:26 1997 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed May 07 13:01:43 1997 +0200
     3.3 @@ -16,15 +16,12 @@
     3.4  proof_timing:=true;
     3.5  HOL_quantifiers := false;
     3.6  
     3.7 -val op addss = op unsafe_addss;
     3.8 -
     3.9  AddIffs [Spy_in_lost];
    3.10  
    3.11  (*Replacing the variable by a constant improves search speed by 50%!*)
    3.12  val Says_imp_sees_Spy' = 
    3.13      read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    3.14  
    3.15 -
    3.16  (*A "possibility property": there are traces that reach the end*)
    3.17  goal thy 
    3.18   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    3.19 @@ -46,17 +43,6 @@
    3.20  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    3.21  
    3.22  
    3.23 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    3.24 -fun parts_induct_tac i = SELECT_GOAL
    3.25 -    (DETERM (etac ns_public.induct 1 THEN 
    3.26 -             (*Fake message*)
    3.27 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.28 -                                           impOfSubs Fake_parts_insert]
    3.29 -                                    addss (!simpset)) 2)) THEN
    3.30 -     (*Base case*)
    3.31 -     fast_tac (!claset addss (!simpset)) 1 THEN
    3.32 -     ALLGOALS Asm_simp_tac) i;
    3.33 -
    3.34  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    3.35      sends messages containing X! **)
    3.36  
    3.37 @@ -64,8 +50,9 @@
    3.38  goal thy 
    3.39   "!!evs. evs : ns_public \
    3.40  \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    3.41 -by (parts_induct_tac 1);
    3.42 -by (Auto_tac());
    3.43 +by (etac ns_public.induct 1);
    3.44 +by (prove_simple_subgoals_tac 1);
    3.45 +by (Fake_parts_insert_tac 1);
    3.46  qed "Spy_see_priK";
    3.47  Addsimps [Spy_see_priK];
    3.48  
    3.49 @@ -78,7 +65,7 @@
    3.50  
    3.51  goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
    3.52  \                  evs : ns_public |] ==> A:lost";
    3.53 -by (fast_tac (!claset addDs [Spy_see_priK]) 1);
    3.54 +by (blast_tac (!claset addDs [Spy_see_priK]) 1);
    3.55  qed "Spy_see_priK_D";
    3.56  
    3.57  bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    3.58 @@ -86,7 +73,7 @@
    3.59  
    3.60  
    3.61  fun analz_induct_tac i = 
    3.62 -    etac ns_public.induct i     THEN
    3.63 +    etac ns_public.induct i   THEN
    3.64      ALLGOALS (asm_simp_tac 
    3.65                (!simpset addsimps [not_parts_not_analz]
    3.66                          setloop split_tac [expand_if]));
    3.67 @@ -105,16 +92,15 @@
    3.68  by (etac rev_mp 1);
    3.69  by (analz_induct_tac 1);
    3.70  (*NS3*)
    3.71 -by (fast_tac (!claset addSEs partsEs) 4);
    3.72 +by (blast_tac (!claset addSEs partsEs) 4);
    3.73  (*NS2*)
    3.74 -by (fast_tac (!claset addSEs partsEs) 3);
    3.75 +by (blast_tac (!claset addSEs partsEs) 3);
    3.76  (*Fake*)
    3.77 -by (deepen_tac (!claset addSIs [analz_insertI]
    3.78 +by (blast_tac (!claset addSIs [analz_insertI]
    3.79                          addDs [impOfSubs analz_subset_parts,
    3.80 -			       impOfSubs Fake_parts_insert]
    3.81 -			addss (!simpset)) 0 2);
    3.82 +			       impOfSubs Fake_parts_insert]) 2);
    3.83  (*Base*)
    3.84 -by (fast_tac (!claset addss (!simpset)) 1);
    3.85 +by (Blast_tac 1);
    3.86  qed "no_nonce_NS1_NS2";
    3.87  
    3.88  
    3.89 @@ -129,17 +115,16 @@
    3.90  (*NS1*)
    3.91  by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
    3.92  by (expand_case_tac "NA = ?y" 3 THEN
    3.93 -    REPEAT (fast_tac (!claset addSEs partsEs) 3));
    3.94 +    REPEAT (blast_tac (!claset addSEs partsEs) 3));
    3.95  (*Base*)
    3.96 -by (fast_tac (!claset addss (!simpset)) 1);
    3.97 +by (Blast_tac 1);
    3.98  (*Fake*)
    3.99  by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   3.100  by (step_tac (!claset addSIs [analz_insertI]) 1);
   3.101  by (ex_strip_tac 1);
   3.102 -by (best_tac (!claset delrules [conjI]
   3.103 +by (blast_tac (!claset delrules [conjI]
   3.104                        addSDs [impOfSubs Fake_parts_insert]
   3.105 -                      addDs  [impOfSubs analz_subset_parts]
   3.106 -                      addss (!simpset)) 1);
   3.107 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   3.108  val lemma = result();
   3.109  
   3.110  goal thy 
   3.111 @@ -160,15 +145,15 @@
   3.112  by (etac rev_mp 1);
   3.113  by (analz_induct_tac 1);
   3.114  (*NS3*)
   3.115 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.116 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   3.117 +by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
   3.118 +                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   3.119  (*NS2*)
   3.120 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.121 -                        addSEs [MPair_parts]
   3.122 -			addDs  [parts.Body, unique_NA]) 0 3);
   3.123 +by (blast_tac (!claset addSEs [MPair_parts]
   3.124 +		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   3.125 +			       parts.Body, unique_NA]) 3);
   3.126  (*NS1*)
   3.127 -by (fast_tac (!claset addSEs sees_Spy_partsEs
   3.128 -                      addIs  [impOfSubs analz_subset_parts]) 2);
   3.129 +by (blast_tac (!claset addSEs sees_Spy_partsEs
   3.130 +                       addIs  [impOfSubs analz_subset_parts]) 2);
   3.131  (*Fake*)
   3.132  by (spy_analz_tac 1);
   3.133  qed "Spy_not_see_NA";
   3.134 @@ -187,20 +172,15 @@
   3.135  by (etac ns_public.induct 1);
   3.136  by (ALLGOALS Asm_simp_tac);
   3.137  (*NS1*)
   3.138 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.139 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.140  (*Fake*)
   3.141 -by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   3.142 -by (fast_tac (!claset addss (!simpset)) 1);
   3.143 -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   3.144 -by (best_tac (!claset addSIs [disjI2]
   3.145 -                      addSDs [impOfSubs Fake_parts_insert]
   3.146 -                      addDs  [impOfSubs analz_subset_parts]
   3.147 -                      addss (!simpset)) 1);
   3.148 -(*NS2*)
   3.149 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   3.150 +                       addDs  [Spy_not_see_NA, 
   3.151 +			       impOfSubs analz_subset_parts]) 1);
   3.152 +(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
   3.153  by (Step_tac 1);
   3.154 -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   3.155 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.156 -                        addDs  [unique_NA]) 1 1);
   3.157 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
   3.158 +			      Spy_not_see_NA, unique_NA]) 1);
   3.159  qed "A_trusts_NS2";
   3.160  
   3.161  (*If the encrypted message appears then it originated with Alice in NS1*)
   3.162 @@ -213,14 +193,12 @@
   3.163  by (etac rev_mp 1);
   3.164  by (analz_induct_tac 1);
   3.165  (*Fake*)
   3.166 -by (best_tac (!claset addSIs [disjI2]
   3.167 -                      addSDs [impOfSubs Fake_parts_insert]
   3.168 -                      addIs  [analz_insertI]
   3.169 -                      addDs  [impOfSubs analz_subset_parts]
   3.170 -                      addss (!simpset)) 2);
   3.171 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   3.172 +                       addIs  [analz_insertI]
   3.173 +                       addDs  [impOfSubs analz_subset_parts]) 2);
   3.174  (*Base*)
   3.175 -by (fast_tac (!claset addss (!simpset)) 1);
   3.176 -qed_spec_mp "B_trusts_NS1";
   3.177 +by (Blast_tac 1);
   3.178 +qed "B_trusts_NS1";
   3.179  
   3.180  
   3.181  
   3.182 @@ -238,17 +216,16 @@
   3.183  (*NS2*)
   3.184  by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   3.185  by (expand_case_tac "NB = ?y" 3 THEN
   3.186 -    REPEAT (fast_tac (!claset addSEs partsEs) 3));
   3.187 +    REPEAT (blast_tac (!claset addSEs partsEs) 3));
   3.188  (*Base*)
   3.189 -by (fast_tac (!claset addss (!simpset)) 1);
   3.190 +by (Blast_tac 1);
   3.191  (*Fake*)
   3.192  by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   3.193  by (step_tac (!claset addSIs [analz_insertI]) 1);
   3.194  by (ex_strip_tac 1);
   3.195 -by (best_tac (!claset delrules [conjI]
   3.196 +by (blast_tac (!claset delrules [conjI]
   3.197                        addSDs [impOfSubs Fake_parts_insert]
   3.198 -                      addDs  [impOfSubs analz_subset_parts] 
   3.199 -                      addss (!simpset)) 1);
   3.200 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   3.201  val lemma = result();
   3.202  
   3.203  goal thy 
   3.204 @@ -271,22 +248,21 @@
   3.205  by (etac rev_mp 1);
   3.206  by (analz_induct_tac 1);
   3.207  (*NS1*)
   3.208 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.209 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.210  (*Fake*)
   3.211  by (spy_analz_tac 1);
   3.212  (*NS2 and NS3*)
   3.213  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   3.214  by (step_tac (!claset delrules [allI]) 1);
   3.215 -by (Fast_tac 5);
   3.216 -by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
   3.217 +by (Blast_tac 5);
   3.218 +(*NS3*)
   3.219 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
   3.220 +			      Spy_not_see_NB, unique_NB]) 4);
   3.221  (*NS2*)
   3.222 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.223 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.224 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.225 -(*NS3*)
   3.226 -by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
   3.227 -    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
   3.228 -by (Fast_tac 1);
   3.229 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   3.230 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.231 +                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   3.232 +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
   3.233  qed "Spy_not_see_NB";
   3.234  
   3.235  
   3.236 @@ -305,22 +281,15 @@
   3.237  by (analz_induct_tac 1);
   3.238  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   3.239  (*NS1*)
   3.240 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.241 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   3.242  (*Fake*)
   3.243 -by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   3.244 -by (fast_tac (!claset addss (!simpset)) 1);
   3.245 -by (rtac (ccontr RS disjI2) 1);
   3.246 -by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
   3.247 -    THEN Fast_tac 1);
   3.248 -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   3.249 -                      addDs  [impOfSubs analz_subset_parts] 
   3.250 -                      addss (!simpset)) 1);
   3.251 -(*NS3*)
   3.252 +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   3.253 +                       addDs  [Spy_not_see_NB, 
   3.254 +			       impOfSubs analz_subset_parts]) 1);
   3.255 +(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
   3.256  by (Step_tac 1);
   3.257 -by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
   3.258 -    THEN Fast_tac 1);
   3.259 -by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.260 -                      addDs  [unique_NB]) 1);
   3.261 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
   3.262 +			      Spy_not_see_NB, unique_NB]) 1);
   3.263  qed "B_trusts_NS3";
   3.264  
   3.265  
   3.266 @@ -331,18 +300,18 @@
   3.267  \     --> Nonce NB ~: analz (sees lost Spy evs)";
   3.268  by (analz_induct_tac 1);
   3.269  (*NS1*)
   3.270 -by (fast_tac (!claset addSEs partsEs
   3.271 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.272 +by (blast_tac (!claset addSEs partsEs
   3.273 +                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.274  (*Fake*)
   3.275  by (spy_analz_tac 1);
   3.276  (*NS2 and NS3*)
   3.277  by (Step_tac 1);
   3.278 -by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
   3.279 +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
   3.280  (*NS2*)
   3.281 -by (fast_tac (!claset addSEs partsEs
   3.282 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.283 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.284 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.285 +by (blast_tac (!claset addSEs partsEs
   3.286 +                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.287 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.288 +                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.289  (*NS3*)
   3.290  by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
   3.291      THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
     4.1 --- a/src/HOL/Auth/NS_Shared.ML	Wed May 07 12:50:26 1997 +0200
     4.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed May 07 13:01:43 1997 +0200
     4.3 @@ -15,6 +15,9 @@
     4.4  proof_timing:=true;
     4.5  HOL_quantifiers := false;
     4.6  
     4.7 +(*Replacing the variable by a constant improves search speed by 50%!*)
     4.8 +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
     4.9 +
    4.10  
    4.11  (*A "possibility property": there are traces that reach the end*)
    4.12  goal thy 
    4.13 @@ -35,7 +38,7 @@
    4.14  by (rtac subsetI 1);
    4.15  by (etac ns_shared.induct 1);
    4.16  by (REPEAT_FIRST
    4.17 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    4.18 +    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    4.19                                :: ns_shared.intrs))));
    4.20  qed "ns_shared_mono";
    4.21  
    4.22 @@ -51,29 +54,23 @@
    4.23  (*For reasoning about the encrypted portion of message NS3*)
    4.24  goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
    4.25  \                ==> X : parts (sees lost Spy evs)";
    4.26 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.27 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.28  qed "NS3_msg_in_parts_sees_Spy";
    4.29                                
    4.30  goal thy
    4.31      "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
    4.32  \           ==> K : parts (sees lost Spy evs)";
    4.33 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.34 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.35  qed "Oops_parts_sees_Spy";
    4.36  
    4.37 -val parts_Fake_tac = 
    4.38 -    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
    4.39 -    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8;
    4.40 -
    4.41 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    4.42 -fun parts_induct_tac i = SELECT_GOAL
    4.43 -    (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
    4.44 -             (*Fake message*)
    4.45 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    4.46 -                                           impOfSubs Fake_parts_insert]
    4.47 -                                    addss (!simpset)) 2)) THEN
    4.48 -     (*Base case*)
    4.49 -     fast_tac (!claset addss (!simpset)) 1 THEN
    4.50 -     ALLGOALS Asm_simp_tac) i;
    4.51 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    4.52 +  We instantiate the variable to "lost" since leaving it as a Var would
    4.53 +  interfere with simplification.*)
    4.54 +val parts_induct_tac = 
    4.55 +    etac ns_shared.induct 1  THEN 
    4.56 +    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
    4.57 +    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
    4.58 +    prove_simple_subgoals_tac 1;
    4.59  
    4.60  
    4.61  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    4.62 @@ -83,8 +80,9 @@
    4.63  goal thy 
    4.64   "!!evs. evs : ns_shared lost \
    4.65  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    4.66 -by (parts_induct_tac 1);
    4.67 -by (Auto_tac());
    4.68 +by parts_induct_tac;
    4.69 +by (Fake_parts_insert_tac 1);
    4.70 +by (Blast_tac 1);
    4.71  qed "Spy_see_shrK";
    4.72  Addsimps [Spy_see_shrK];
    4.73  
    4.74 @@ -97,7 +95,7 @@
    4.75  
    4.76  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    4.77  \                  evs : ns_shared lost |] ==> A:lost";
    4.78 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    4.79 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    4.80  qed "Spy_see_shrK_D";
    4.81  
    4.82  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    4.83 @@ -107,15 +105,15 @@
    4.84  (*Nobody can have used non-existent keys!*)
    4.85  goal thy "!!evs. evs : ns_shared lost ==>      \
    4.86  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    4.87 -by (parts_induct_tac 1);
    4.88 +by parts_induct_tac;
    4.89  (*Fake*)
    4.90  by (best_tac
    4.91        (!claset addIs [impOfSubs analz_subset_parts]
    4.92                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    4.93                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    4.94 -               unsafe_addss (!simpset)) 1);
    4.95 +               addss (!simpset)) 1);
    4.96  (*NS2, NS4, NS5*)
    4.97 -by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
    4.98 +by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
    4.99  qed_spec_mp "new_keys_not_used";
   4.100  
   4.101  bind_thm ("new_keys_not_analzd",
   4.102 @@ -152,7 +150,8 @@
   4.103  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   4.104  \             : set_of_list evs";
   4.105  by (etac rev_mp 1);
   4.106 -by (parts_induct_tac 1);
   4.107 +by parts_induct_tac;
   4.108 +by (Fake_parts_insert_tac 1);
   4.109  by (Auto_tac());
   4.110  qed "A_trusts_NS2";
   4.111  
   4.112 @@ -163,20 +162,19 @@
   4.113  goal thy 
   4.114   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
   4.115  \            : set_of_list evs;  evs : ns_shared lost |]                   \
   4.116 -\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))  \
   4.117 +\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
   4.118  \            | X : analz (sees lost Spy evs)";
   4.119  by (case_tac "A : lost" 1);
   4.120 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   4.121 -                      unsafe_addss (!simpset)) 1);
   4.122 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
   4.123 +                      addss (!simpset)) 1);
   4.124  by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
   4.125 -by (fast_tac (!claset addEs  partsEs
   4.126 -                      addSDs [A_trusts_NS2, Says_Server_message_form]
   4.127 -                      addss (!simpset)) 1);
   4.128 +by (blast_tac (!claset addEs  partsEs
   4.129 +                      addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
   4.130  qed "Says_S_message_form";
   4.131  
   4.132  
   4.133  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   4.134 -val analz_Fake_tac = 
   4.135 +val analz_sees_tac = 
   4.136      forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
   4.137      forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
   4.138      REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   4.139 @@ -200,15 +198,12 @@
   4.140   "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
   4.141  \        (Crypt KAB X) : parts (sees lost Spy evs) & \
   4.142  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   4.143 -by (etac ns_shared.induct 1);
   4.144 -by parts_Fake_tac;
   4.145 -by (ALLGOALS Asm_simp_tac);
   4.146 +by parts_induct_tac;
   4.147  (*Deals with Faked messages*)
   4.148 -by (best_tac (!claset addSEs partsEs
   4.149 -                      addDs [impOfSubs parts_insert_subset_Un]
   4.150 -                      addss (!simpset)) 2);
   4.151 +by (blast_tac (!claset addSEs partsEs
   4.152 +                       addDs [impOfSubs parts_insert_subset_Un]) 1);
   4.153  (*Base, NS4 and NS5*)
   4.154 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   4.155 +by (Auto_tac());
   4.156  result();
   4.157  
   4.158  
   4.159 @@ -221,7 +216,7 @@
   4.160  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   4.161  \            (K : KK | Key K : analz (sees lost Spy evs))";
   4.162  by (etac ns_shared.induct 1);
   4.163 -by analz_Fake_tac;
   4.164 +by analz_sees_tac;
   4.165  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   4.166  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   4.167  (*Takes 24 secs*)
   4.168 @@ -229,7 +224,7 @@
   4.169  (*NS4, Fake*) 
   4.170  by (EVERY (map spy_analz_tac [3,2]));
   4.171  (*Base*)
   4.172 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   4.173 +by (Blast_tac 1);
   4.174  qed_spec_mp "analz_image_freshK";
   4.175  
   4.176  
   4.177 @@ -253,13 +248,12 @@
   4.178  by (Step_tac 1);
   4.179  (*NS3*)
   4.180  by (ex_strip_tac 2);
   4.181 -by (Fast_tac 2);
   4.182 +by (Blast_tac 2);
   4.183  (*NS2: it can't be a new key*)
   4.184  by (expand_case_tac "K = ?y" 1);
   4.185  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   4.186 -by (fast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   4.187 -                      addSEs sees_Spy_partsEs
   4.188 -                      addss (!simpset addsimps [parts_insertI])) 1);
   4.189 +by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   4.190 +                      addSEs sees_Spy_partsEs) 1);
   4.191  val lemma = result();
   4.192  
   4.193  (*In messages of this form, the session key uniquely identifies the rest*)
   4.194 @@ -286,7 +280,7 @@
   4.195  \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
   4.196  \        Key K ~: analz (sees lost Spy evs)";
   4.197  by (etac ns_shared.induct 1);
   4.198 -by analz_Fake_tac;
   4.199 +by analz_sees_tac;
   4.200  by (ALLGOALS 
   4.201      (asm_simp_tac 
   4.202       (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
   4.203 @@ -294,17 +288,16 @@
   4.204  (*NS4, Fake*) 
   4.205  by (EVERY (map spy_analz_tac [4,1]));
   4.206  (*NS2*)
   4.207 -by (fast_tac (!claset addSEs sees_Spy_partsEs
   4.208 -                      addIs [parts_insertI, impOfSubs analz_subset_parts]
   4.209 -                      addss (!simpset)) 1);
   4.210 +by (blast_tac (!claset addSEs sees_Spy_partsEs
   4.211 +                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
   4.212  (*Oops*)
   4.213 -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
   4.214 +by (blast_tac (!claset addDs [unique_session_keys]) 2);
   4.215  (*NS3*) (**LEVEL 6 **)
   4.216  by (step_tac (!claset delrules [impCE]) 1);
   4.217 -by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
   4.218 +by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
   4.219  by (assume_tac 2);
   4.220 -by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
   4.221 -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   4.222 +by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1);
   4.223 +by (blast_tac (!claset addDs [unique_session_keys]) 1);
   4.224  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   4.225  
   4.226  
   4.227 @@ -316,7 +309,7 @@
   4.228  \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   4.229  \        |] ==> Key K ~: analz (sees lost Spy evs)";
   4.230  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   4.231 -by (fast_tac (!claset addSEs [lemma]) 1);
   4.232 +by (blast_tac (!claset addSDs [lemma]) 1);
   4.233  qed "Spy_not_see_encrypted_key";
   4.234  
   4.235  
   4.236 @@ -330,7 +323,7 @@
   4.237  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   4.238  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   4.239  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   4.240 -by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   4.241 +by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   4.242  qed "Agent_not_see_encrypted_key";
   4.243  
   4.244  
   4.245 @@ -349,13 +342,10 @@
   4.246  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   4.247  \             : set_of_list evs";
   4.248  by (etac rev_mp 1);
   4.249 -by (etac ns_shared.induct 1);
   4.250 -by parts_Fake_tac;
   4.251 +by parts_induct_tac;
   4.252 +by (Fake_parts_insert_tac 1);
   4.253  (*Fake case*)
   4.254 -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   4.255 -                      addDs  [impOfSubs analz_subset_parts]
   4.256 -                      addss  (!simpset)) 2);
   4.257 -by (Auto_tac());
   4.258 +by (ALLGOALS Blast_tac);
   4.259  qed "B_trusts_NS3";
   4.260  
   4.261  
   4.262 @@ -368,28 +358,28 @@
   4.263  \            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   4.264  by (etac ns_shared.induct 1);
   4.265  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   4.266 -by parts_Fake_tac;
   4.267 +by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
   4.268 +by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
   4.269  by (TRYALL (rtac impI));
   4.270  by (REPEAT_FIRST
   4.271      (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   4.272  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   4.273 -(**LEVEL 6**)
   4.274 -by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   4.275 -                      addDs [impOfSubs analz_subset_parts]) 1);
   4.276 -by (Fast_tac 2);
   4.277 +(**LEVEL 7**)
   4.278 +by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   4.279 +                       addDs [impOfSubs analz_subset_parts]) 1);
   4.280 +by (Blast_tac 2);
   4.281  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   4.282  (*Subgoal 1: contradiction from the assumptions  
   4.283    Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
   4.284  by (dtac Crypt_imp_invKey_keysFor 1);
   4.285 -(**LEVEL 10**)
   4.286 +(**LEVEL 11**)
   4.287  by (Asm_full_simp_tac 1);
   4.288  by (rtac disjI1 1);
   4.289  by (thin_tac "?PP-->?QQ" 1);
   4.290  by (case_tac "Ba : lost" 1);
   4.291 -by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
   4.292 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN 
   4.293 -    REPEAT (assume_tac 1));
   4.294 -by (best_tac (!claset addDs [unique_session_keys]) 1);
   4.295 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
   4.296 +			      unique_session_keys]) 2);
   4.297 +by (blast_tac (!claset addDs [Says_Crypt_lost]) 1);
   4.298  val lemma = result();
   4.299  
   4.300  goal thy
   4.301 @@ -399,6 +389,6 @@
   4.302  \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   4.303  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   4.304  \        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   4.305 -by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   4.306 -                      addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
   4.307 +by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   4.308 +                       addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   4.309  qed "A_trusts_NS4";
     5.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed May 07 12:50:26 1997 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed May 07 13:01:43 1997 +0200
     5.3 @@ -18,8 +18,7 @@
     5.4  HOL_quantifiers := false;
     5.5  
     5.6  (*Replacing the variable by a constant improves search speed by 50%!*)
     5.7 -val Says_imp_sees_Spy' = 
     5.8 -    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
     5.9 +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
    5.10  
    5.11  
    5.12  (*A "possibility property": there are traces that reach the end*)
    5.13 @@ -81,35 +80,30 @@
    5.14  bind_thm ("OR4_parts_sees_Spy",
    5.15            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    5.16  
    5.17 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    5.18 -  harder to complete, since simplification does less for us.*)
    5.19 -val parts_Fake_tac = 
    5.20 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    5.21 +  We instantiate the variable to "lost" since leaving it as a Var would
    5.22 +  interfere with simplification.*)
    5.23 +val parts_induct_tac = 
    5.24      let val tac = forw_inst_tac [("lost","lost")] 
    5.25 -    in  tac OR2_parts_sees_Spy     4 THEN 
    5.26 +    in  etac otway.induct	   1 THEN 
    5.27 +	tac OR2_parts_sees_Spy     4 THEN 
    5.28          tac OR4_parts_sees_Spy     6 THEN
    5.29 -        tac Oops_parts_sees_Spy    7
    5.30 +        tac Oops_parts_sees_Spy    7 THEN
    5.31 +	prove_simple_subgoals_tac  1
    5.32      end;
    5.33  
    5.34 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    5.35 -fun parts_induct_tac i = SELECT_GOAL
    5.36 -    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    5.37 -             (*Fake message*)
    5.38 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    5.39 -                                           impOfSubs Fake_parts_insert]
    5.40 -                            unsafe_addss (!simpset)) 2)) THEN
    5.41 -     (*Base case*)
    5.42 -     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
    5.43 -     ALLGOALS Asm_simp_tac) i;
    5.44  
    5.45  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    5.46      sends messages containing X! **)
    5.47  
    5.48 +
    5.49  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    5.50  goal thy 
    5.51   "!!evs. evs : otway lost \
    5.52  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    5.53 -by (parts_induct_tac 1);
    5.54 -by (Auto_tac());
    5.55 +by parts_induct_tac;
    5.56 +by (Fake_parts_insert_tac 1);
    5.57 +by (Blast_tac 1);
    5.58  qed "Spy_see_shrK";
    5.59  Addsimps [Spy_see_shrK];
    5.60  
    5.61 @@ -132,7 +126,7 @@
    5.62  (*Nobody can have used non-existent keys!*)
    5.63  goal thy "!!evs. evs : otway lost ==>          \
    5.64  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    5.65 -by (parts_induct_tac 1);
    5.66 +by parts_induct_tac;
    5.67  (*Fake*)
    5.68  by (best_tac
    5.69        (!claset addIs [impOfSubs analz_subset_parts]
    5.70 @@ -167,7 +161,7 @@
    5.71  
    5.72  
    5.73  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
    5.74 -val analz_Fake_tac = 
    5.75 +val analz_sees_tac = 
    5.76      dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
    5.77      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    5.78      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    5.79 @@ -194,7 +188,7 @@
    5.80  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    5.81  \            (K : KK | Key K : analz (sees lost Spy evs))";
    5.82  by (etac otway.induct 1);
    5.83 -by analz_Fake_tac;
    5.84 +by analz_sees_tac;
    5.85  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    5.86  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    5.87  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    5.88 @@ -254,7 +248,8 @@
    5.89  \            Says A B {|NA, Agent A, Agent B,                      \
    5.90  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    5.91  \             : set_of_list evs";
    5.92 -by (parts_induct_tac 1);
    5.93 +by parts_induct_tac;
    5.94 +by (Fake_parts_insert_tac 1);
    5.95  qed_spec_mp "Crypt_imp_OR1";
    5.96  
    5.97  
    5.98 @@ -265,7 +260,8 @@
    5.99  \ ==> EX B'. ALL B.    \
   5.100  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   5.101  \        --> B = B'";
   5.102 -by (parts_induct_tac 1);
   5.103 +by parts_induct_tac;
   5.104 +by (Fake_parts_insert_tac 1);
   5.105  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   5.106  (*OR1: creation of new Nonce.  Move assertion into global context*)
   5.107  by (expand_case_tac "NA = ?y" 1);
   5.108 @@ -290,7 +286,8 @@
   5.109  \             : parts (sees lost Spy evs) -->                    \
   5.110  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   5.111  \             ~: parts (sees lost Spy evs)";
   5.112 -by (parts_induct_tac 1);
   5.113 +by parts_induct_tac;
   5.114 +by (Fake_parts_insert_tac 1);
   5.115  by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   5.116                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   5.117  qed_spec_mp"no_nonce_OR1_OR2";
   5.118 @@ -309,7 +306,8 @@
   5.119  \                   Crypt (shrK A) {|NA, Key K|},                      \
   5.120  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   5.121  \                   : set_of_list evs)";
   5.122 -by (parts_induct_tac 1);
   5.123 +by parts_induct_tac;
   5.124 +by (Fake_parts_insert_tac 1);
   5.125  (*OR1: it cannot be a new Nonce, contradiction.*)
   5.126  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   5.127  (*OR3 and OR4*) 
   5.128 @@ -364,7 +362,7 @@
   5.129  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   5.130  \            Key K ~: analz (sees lost Spy evs)";
   5.131  by (etac otway.induct 1);
   5.132 -by analz_Fake_tac;
   5.133 +by analz_sees_tac;
   5.134  by (ALLGOALS
   5.135      (asm_simp_tac (!simpset addcongs [conj_cong] 
   5.136                              addsimps [not_parts_not_analz, analz_insert_freshK]
   5.137 @@ -418,7 +416,8 @@
   5.138  \             {|NA, Agent A, Agent B, X,                       \
   5.139  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   5.140  \             : set_of_list evs)";
   5.141 -by (parts_induct_tac 1);
   5.142 +by parts_induct_tac;
   5.143 +by (Fake_parts_insert_tac 1);
   5.144  by (ALLGOALS Blast_tac);
   5.145  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   5.146  
   5.147 @@ -430,7 +429,8 @@
   5.148  \ ==> EX NA' A'. ALL NA A.                               \
   5.149  \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   5.150  \      --> NA = NA' & A = A'";
   5.151 -by (parts_induct_tac 1);
   5.152 +by parts_induct_tac;
   5.153 +by (Fake_parts_insert_tac 1);
   5.154  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   5.155  (*OR2: creation of new Nonce.  Move assertion into global context*)
   5.156  by (expand_case_tac "NB = ?y" 1);
   5.157 @@ -461,7 +461,8 @@
   5.158  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   5.159  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   5.160  \                   : set_of_list evs)";
   5.161 -by (parts_induct_tac 1);
   5.162 +by parts_induct_tac;
   5.163 +by (Fake_parts_insert_tac 1);
   5.164  (*OR1: it cannot be a new Nonce, contradiction.*)
   5.165  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   5.166  (*OR4*)
     6.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed May 07 12:50:26 1997 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed May 07 13:01:43 1997 +0200
     6.3 @@ -69,22 +69,17 @@
     6.4  bind_thm ("OR4_parts_sees_Spy",
     6.5            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
     6.6  
     6.7 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
     6.8 -  harder to complete, since simplification does less for us.*)
     6.9 -val parts_Fake_tac = 
    6.10 -    forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    6.11 -    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
    6.12 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    6.13 +  We instantiate the variable to "lost" since leaving it as a Var would
    6.14 +  interfere with simplification.*)
    6.15 +val parts_induct_tac = 
    6.16 +    let val tac = forw_inst_tac [("lost","lost")] 
    6.17 +    in  etac otway.induct	   1 THEN 
    6.18 +        tac OR4_parts_sees_Spy     6 THEN
    6.19 +        tac Oops_parts_sees_Spy    7 THEN
    6.20 +	prove_simple_subgoals_tac  1
    6.21 +    end;
    6.22  
    6.23 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    6.24 -fun parts_induct_tac i = SELECT_GOAL
    6.25 -    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    6.26 -             (*Fake message*)
    6.27 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    6.28 -                                           impOfSubs Fake_parts_insert]
    6.29 -                                    addss (!simpset)) 2)) THEN
    6.30 -     (*Base case*)
    6.31 -     fast_tac (!claset addss (!simpset)) 1 THEN
    6.32 -     ALLGOALS Asm_simp_tac) i;
    6.33  
    6.34  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    6.35      sends messages containing X! **)
    6.36 @@ -93,8 +88,9 @@
    6.37  goal thy 
    6.38   "!!evs. evs : otway lost \
    6.39  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    6.40 -by (parts_induct_tac 1);
    6.41 -by (Auto_tac());
    6.42 +by parts_induct_tac;
    6.43 +by (Fake_parts_insert_tac 1);
    6.44 +by (Blast_tac 1);
    6.45  qed "Spy_see_shrK";
    6.46  Addsimps [Spy_see_shrK];
    6.47  
    6.48 @@ -117,7 +113,7 @@
    6.49  (*Nobody can have used non-existent keys!*)
    6.50  goal thy "!!evs. evs : otway lost ==>          \
    6.51  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    6.52 -by (parts_induct_tac 1);
    6.53 +by parts_induct_tac;
    6.54  (*Fake*)
    6.55  by (best_tac
    6.56        (!claset addIs [impOfSubs analz_subset_parts]
    6.57 @@ -154,7 +150,7 @@
    6.58  
    6.59  
    6.60  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
    6.61 -val analz_Fake_tac = 
    6.62 +val analz_sees_tac = 
    6.63      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    6.64      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    6.65      assume_tac 7 THEN
    6.66 @@ -180,7 +176,7 @@
    6.67  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    6.68  \            (K : KK | Key K : analz (sees lost Spy evs))";
    6.69  by (etac otway.induct 1);
    6.70 -by analz_Fake_tac;
    6.71 +by analz_sees_tac;
    6.72  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    6.73  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    6.74  (*14 seconds*)
    6.75 @@ -250,7 +246,8 @@
    6.76  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    6.77  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    6.78  \                  : set_of_list evs)";
    6.79 -by (parts_induct_tac 1);
    6.80 +by parts_induct_tac;
    6.81 +by (Fake_parts_insert_tac 1);
    6.82  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    6.83  (*OR3*)
    6.84  by (Blast_tac 1);
    6.85 @@ -285,7 +282,7 @@
    6.86  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
    6.87  \            Key K ~: analz (sees lost Spy evs)";
    6.88  by (etac otway.induct 1);
    6.89 -by analz_Fake_tac;
    6.90 +by analz_sees_tac;
    6.91  by (ALLGOALS
    6.92      (asm_simp_tac (!simpset addcongs [conj_cong] 
    6.93                              addsimps [not_parts_not_analz,
    6.94 @@ -340,7 +337,8 @@
    6.95  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    6.96  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    6.97  \                     : set_of_list evs)";
    6.98 -by (parts_induct_tac 1);
    6.99 +by parts_induct_tac;
   6.100 +by (Fake_parts_insert_tac 1);
   6.101  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   6.102  (*OR3*)
   6.103  by (Blast_tac 1);
     7.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed May 07 12:50:26 1997 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed May 07 13:01:43 1997 +0200
     7.3 @@ -20,9 +20,11 @@
     7.4  proof_timing:=true;
     7.5  HOL_quantifiers := false;
     7.6  
     7.7 -(*No need to declare Says_imp_sees_Spy' because "lost" is a CONSTANT*)
     7.8 +(*Replacing the variable by a constant improves search speed by 50%!*)
     7.9 +val Says_imp_sees_Spy' = 
    7.10 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    7.11  
    7.12 -(*Weak liveness: there are traces that reach the end*)
    7.13 +(*A "possibility property": there are traces that reach the end*)
    7.14  goal thy 
    7.15   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    7.16  \        ==> EX K. EX NA. EX evs: otway.          \
    7.17 @@ -49,12 +51,12 @@
    7.18  
    7.19  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    7.20  \                X : analz (sees lost Spy evs)";
    7.21 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    7.22 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    7.23  qed "OR2_analz_sees_Spy";
    7.24  
    7.25  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
    7.26  \                X : analz (sees lost Spy evs)";
    7.27 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    7.28 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    7.29  qed "OR4_analz_sees_Spy";
    7.30  
    7.31  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    7.32 @@ -72,21 +74,13 @@
    7.33  bind_thm ("OR4_parts_sees_Spy",
    7.34            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    7.35  
    7.36 -val parts_Fake_tac = 
    7.37 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    7.38 +val parts_induct_tac = 
    7.39 +    etac otway.induct 1 THEN 
    7.40      forward_tac [OR2_parts_sees_Spy] 4 THEN 
    7.41      forward_tac [OR4_parts_sees_Spy] 6 THEN
    7.42 -    forward_tac [Oops_parts_sees_Spy] 7;
    7.43 -
    7.44 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    7.45 -fun parts_induct_tac i = SELECT_GOAL
    7.46 -    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    7.47 -             (*Fake message*)
    7.48 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    7.49 -                                           impOfSubs Fake_parts_insert]
    7.50 -                                    addss (!simpset)) 2)) THEN
    7.51 -     (*Base case*)
    7.52 -     fast_tac (!claset addss (!simpset)) 1 THEN
    7.53 -     ALLGOALS Asm_simp_tac) i;
    7.54 +    forward_tac [Oops_parts_sees_Spy] 7 THEN
    7.55 +    prove_simple_subgoals_tac 1;
    7.56  
    7.57  
    7.58  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    7.59 @@ -96,8 +90,9 @@
    7.60  goal thy 
    7.61   "!!evs. evs : otway \
    7.62  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    7.63 -by (parts_induct_tac 1);
    7.64 -by (Auto_tac());
    7.65 +by parts_induct_tac;
    7.66 +by (Fake_parts_insert_tac 1);
    7.67 +by (Blast_tac 1);
    7.68  qed "Spy_see_shrK";
    7.69  Addsimps [Spy_see_shrK];
    7.70  
    7.71 @@ -120,7 +115,7 @@
    7.72  (*Nobody can have used non-existent keys!*)
    7.73  goal thy "!!evs. evs : otway ==>          \
    7.74  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    7.75 -by (parts_induct_tac 1);
    7.76 +by parts_induct_tac;
    7.77  (*Fake*)
    7.78  by (best_tac
    7.79        (!claset addIs [impOfSubs analz_subset_parts]
    7.80 @@ -128,7 +123,7 @@
    7.81                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    7.82                 unsafe_addss (!simpset)) 1);
    7.83  (*OR1-3*)
    7.84 -by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    7.85 +by (ALLGOALS Blast_tac);
    7.86  qed_spec_mp "new_keys_not_used";
    7.87  
    7.88  bind_thm ("new_keys_not_analzd",
    7.89 @@ -150,12 +145,13 @@
    7.90  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    7.91  by (etac rev_mp 1);
    7.92  by (etac otway.induct 1);
    7.93 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    7.94 +by (prove_simple_subgoals_tac 1);
    7.95 +by (Blast_tac 1); 
    7.96  qed "Says_Server_message_form";
    7.97  
    7.98  
    7.99  (*For proofs involving analz.*)
   7.100 -val analz_Fake_tac = 
   7.101 +val analz_sees_tac = 
   7.102      dtac OR2_analz_sees_Spy 4 THEN 
   7.103      dtac OR4_analz_sees_Spy 6 THEN
   7.104      forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
   7.105 @@ -181,12 +177,12 @@
   7.106  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   7.107  \            (K : KK | Key K : analz (sees lost Spy evs))";
   7.108  by (etac otway.induct 1);
   7.109 -by analz_Fake_tac;
   7.110 +by analz_sees_tac;
   7.111  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   7.112  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   7.113  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   7.114  (*Base*)
   7.115 -by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   7.116 +by (Blast_tac 1);
   7.117  (*Fake, OR2, OR4*) 
   7.118  by (REPEAT (spy_analz_tac 1));
   7.119  qed_spec_mp "analz_image_freshK";
   7.120 @@ -217,8 +213,7 @@
   7.121  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   7.122  (*...we assume X is a recent message, and handle this case by contradiction*)
   7.123  by (blast_tac (!claset addSEs sees_Spy_partsEs
   7.124 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   7.125 -                      addss (!simpset addsimps [parts_insertI])) 1);
   7.126 +                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   7.127  val lemma = result();
   7.128  
   7.129  goal thy 
   7.130 @@ -240,7 +235,7 @@
   7.131  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
   7.132  \            Key K ~: analz (sees lost Spy evs)";
   7.133  by (etac otway.induct 1);
   7.134 -by analz_Fake_tac;
   7.135 +by analz_sees_tac;
   7.136  by (ALLGOALS
   7.137      (asm_simp_tac (!simpset addcongs [conj_cong] 
   7.138                              addsimps [not_parts_not_analz, analz_insert_freshK]
   7.139 @@ -280,7 +275,8 @@
   7.140  \            Says A B {|NA, Agent A, Agent B,                  \
   7.141  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   7.142  \             : set_of_list evs";
   7.143 -by (parts_induct_tac 1);
   7.144 +by parts_induct_tac;
   7.145 +by (Fake_parts_insert_tac 1);
   7.146  by (Blast_tac 1);
   7.147  qed_spec_mp "Crypt_imp_OR1";
   7.148  
   7.149 @@ -300,7 +296,8 @@
   7.150  \                   Crypt (shrK A) {|NA, Key K|},              \
   7.151  \                   Crypt (shrK B) {|NB, Key K|}|}             \
   7.152  \                   : set_of_list evs)";
   7.153 -by (parts_induct_tac 1);
   7.154 +by parts_induct_tac;
   7.155 +by (Fake_parts_insert_tac 1);
   7.156  (*OR1: it cannot be a new Nonce, contradiction.*)
   7.157  by (blast_tac (!claset addSIs [parts_insertI]
   7.158                        addSEs sees_Spy_partsEs) 1);
     8.1 --- a/src/HOL/Auth/Public.ML	Wed May 07 12:50:26 1997 +0200
     8.2 +++ b/src/HOL/Auth/Public.ML	Wed May 07 13:01:43 1997 +0200
     8.3 @@ -80,7 +80,7 @@
     8.4  (*Added for Yahalom/lost_tac*)
     8.5  goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
     8.6  \              ==> X : analz (sees lost Spy evs)";
     8.7 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
     8.8 +by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
     8.9  qed "Crypt_Spy_analz_lost";
    8.10  
    8.11  (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
    8.12 @@ -120,8 +120,8 @@
    8.13  by (Step_tac 1);
    8.14  by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
    8.15  by (ALLGOALS
    8.16 -    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
    8.17 -                       setloop split_tac [expand_if]))));
    8.18 +    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
    8.19 +				            setloop split_tac [expand_if]))));
    8.20  qed "UN_parts_sees_Says";
    8.21  
    8.22  goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
    8.23 @@ -136,16 +136,14 @@
    8.24  goal thy  
    8.25   "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
    8.26  \        ==> X : analz (sees lost Spy evs)";
    8.27 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    8.28 -                      addss (!simpset)) 1);
    8.29 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    8.30  qed "Says_Crypt_lost";
    8.31  
    8.32  goal thy  
    8.33   "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;        \
    8.34  \           X ~: analz (sees lost Spy evs) |]                     \
    8.35  \        ==> C ~: lost";
    8.36 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    8.37 -                      addss (!simpset)) 1);
    8.38 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    8.39  qed "Says_Crypt_not_lost";
    8.40  
    8.41  Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
     9.1 --- a/src/HOL/Auth/ROOT.ML	Wed May 07 12:50:26 1997 +0200
     9.2 +++ b/src/HOL/Auth/ROOT.ML	Wed May 07 13:01:43 1997 +0200
     9.3 @@ -12,6 +12,9 @@
     9.4  proof_timing := true;
     9.5  goals_limit := 1;
     9.6  
     9.7 +(*New version of addss isn't ready--too slow*)
     9.8 +val op addss = op unsafe_addss;
     9.9 +
    9.10  (*Shared-key protocols*)
    9.11  time_use_thy "NS_Shared";
    9.12  time_use_thy "OtwayRees";
    10.1 --- a/src/HOL/Auth/Recur.ML	Wed May 07 12:50:26 1997 +0200
    10.2 +++ b/src/HOL/Auth/Recur.ML	Wed May 07 13:01:43 1997 +0200
    10.3 @@ -82,7 +82,7 @@
    10.4  by (rtac subsetI 1);
    10.5  by (etac recur.induct 1);
    10.6  by (REPEAT_FIRST
    10.7 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    10.8 +    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    10.9                                :: recur.intrs))));
   10.10  qed "recur_mono";
   10.11  
   10.12 @@ -128,7 +128,7 @@
   10.13  
   10.14  goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
   10.15  \                ==> RA : analz (sees lost Spy evs)";
   10.16 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   10.17 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   10.18  qed "RA4_analz_sees_Spy";
   10.19  
   10.20  (*RA2_analz... and RA4_analz... let us treat those cases using the same 
   10.21 @@ -141,26 +141,19 @@
   10.22  bind_thm ("RA4_parts_sees_Spy",
   10.23            RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   10.24  
   10.25 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   10.26 -  harder to complete, since simplification does less for us.*)
   10.27 -val parts_Fake_tac = 
   10.28 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
   10.29 +  We instantiate the variable to "lost" since leaving it as a Var would
   10.30 +  interfere with simplification.*)
   10.31 +val parts_induct_tac = 
   10.32      let val tac = forw_inst_tac [("lost","lost")] 
   10.33 -    in  tac RA2_parts_sees_Spy 4              THEN
   10.34 +    in  etac recur.induct      1	      THEN
   10.35 +	tac RA2_parts_sees_Spy 4              THEN
   10.36          etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
   10.37          forward_tac [respond_imp_responses] 5 THEN
   10.38 -        tac RA4_parts_sees_Spy 6
   10.39 +        tac RA4_parts_sees_Spy 6	      THEN
   10.40 +	prove_simple_subgoals_tac 1
   10.41      end;
   10.42  
   10.43 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   10.44 -fun parts_induct_tac i = SELECT_GOAL
   10.45 -    (DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN
   10.46 -             (*Fake message*)
   10.47 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   10.48 -                                           impOfSubs Fake_parts_insert]
   10.49 -                            unsafe_addss (!simpset)) 2)) THEN
   10.50 -     (*Base case*)
   10.51 -     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
   10.52 -     ALLGOALS Asm_simp_tac) i;
   10.53  
   10.54  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   10.55      sends messages containing X! **)
   10.56 @@ -171,14 +164,14 @@
   10.57  goal thy 
   10.58   "!!evs. evs : recur lost \
   10.59  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   10.60 -by (parts_induct_tac 1);
   10.61 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   10.62 +by parts_induct_tac;
   10.63 +by (Fake_parts_insert_tac 1);
   10.64 +by (ALLGOALS 
   10.65 +    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
   10.66  (*RA3*)
   10.67 -by (fast_tac (!claset addDs [Key_in_parts_respond]
   10.68 -                      addss (!simpset addsimps [parts_insert_sees])) 2);
   10.69 +by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
   10.70  (*RA2*)
   10.71 -by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
   10.72 -                      unsafe_addss (!simpset)) 1);
   10.73 +by (blast_tac (!claset addSEs partsEs  addDs [parts_cut]) 1);
   10.74  qed "Spy_see_shrK";
   10.75  Addsimps [Spy_see_shrK];
   10.76  
   10.77 @@ -191,7 +184,7 @@
   10.78  
   10.79  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   10.80  \                  evs : recur lost |] ==> A:lost";
   10.81 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   10.82 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   10.83  qed "Spy_see_shrK_D";
   10.84  
   10.85  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   10.86 @@ -212,10 +205,10 @@
   10.87  
   10.88  goal thy "!!evs. evs : recur lost ==>          \
   10.89  \       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   10.90 -by (parts_induct_tac 1);
   10.91 +by parts_induct_tac;
   10.92  (*RA3*)
   10.93  by (best_tac (!claset addDs  [Key_in_keysFor_parts]
   10.94 -                      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
   10.95 +	      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
   10.96  (*Fake*)
   10.97  by (best_tac
   10.98        (!claset addIs [impOfSubs analz_subset_parts]
   10.99 @@ -236,7 +229,7 @@
  10.100  (*** Proofs involving analz ***)
  10.101  
  10.102  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
  10.103 -val analz_Fake_tac = 
  10.104 +val analz_sees_tac = 
  10.105      etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
  10.106      dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
  10.107      forward_tac [respond_imp_responses] 5                THEN
  10.108 @@ -267,14 +260,14 @@
  10.109  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  10.110  \            (K : KK | Key K : analz (sees lost Spy evs))";
  10.111  by (etac recur.induct 1);
  10.112 -by analz_Fake_tac;
  10.113 +by analz_sees_tac;
  10.114  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  10.115  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  10.116  by (ALLGOALS 
  10.117      (asm_simp_tac
  10.118       (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
  10.119  (*Base*)
  10.120 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  10.121 +by (Blast_tac 1);
  10.122  (*RA4, RA2, Fake*) 
  10.123  by (REPEAT (spy_analz_tac 1));
  10.124  val raw_analz_image_freshK = result();
  10.125 @@ -304,17 +297,13 @@
  10.126  \                   evs : recur lost;  A ~: lost |]                       \
  10.127  \                ==> X : parts (sees lost Spy evs)";
  10.128  by (etac rev_mp 1);
  10.129 -by (etac recur.induct 1);
  10.130 -by parts_Fake_tac;
  10.131 +by parts_induct_tac;
  10.132  (*RA3 requires a further induction*)
  10.133 -by (etac responses.induct 5);
  10.134 +by (etac responses.induct 2);
  10.135  by (ALLGOALS Asm_simp_tac);
  10.136  (*Fake*)
  10.137 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
  10.138 -                             impOfSubs Fake_parts_insert]
  10.139 -                      addss (!simpset addsimps [parts_insert_sees])) 2);
  10.140 -(*Two others*)
  10.141 -by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
  10.142 +by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
  10.143 +by (Fake_parts_insert_tac 1);
  10.144  qed "Hash_imp_body";
  10.145  
  10.146  
  10.147 @@ -329,14 +318,15 @@
  10.148  \ ==> EX B' P'. ALL B P.                                     \
  10.149  \        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
  10.150  \          -->  B=B' & P=P'";
  10.151 -by (parts_induct_tac 1);
  10.152 +by parts_induct_tac;
  10.153 +by (Fake_parts_insert_tac 1);
  10.154  by (etac responses.induct 3);
  10.155  by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
  10.156  by (step_tac (!claset addSEs partsEs) 1);
  10.157  (*RA1,2: creation of new Nonce.  Move assertion into global context*)
  10.158  by (ALLGOALS (expand_case_tac "NA = ?y"));
  10.159  by (REPEAT_FIRST (ares_tac [exI]));
  10.160 -by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
  10.161 +by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
  10.162                                addSEs sees_Spy_partsEs) 1));
  10.163  val lemma = result();
  10.164  
  10.165 @@ -379,7 +369,7 @@
  10.166       (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
  10.167  (*Simplification using two distinct treatments of "image"*)
  10.168  by (simp_tac (!simpset addsimps [parts_insert2]) 1);
  10.169 -by (fast_tac (!claset delrules [allE]) 1);
  10.170 +by (blast_tac (!claset delrules [allE]) 1);
  10.171  qed "resp_analz_insert_lemma";
  10.172  
  10.173  bind_thm ("resp_analz_insert",
  10.174 @@ -417,11 +407,11 @@
  10.175  by (etac respond.induct 1);
  10.176  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
  10.177  (*Base case*)
  10.178 -by (Fast_tac 1);
  10.179 +by (Blast_tac 1);
  10.180  by (Step_tac 1);
  10.181  by (expand_case_tac "K = KBC" 1);
  10.182  by (dtac respond_Key_in_parts 1);
  10.183 -by (best_tac (!claset addSIs [exI]
  10.184 +by (blast_tac (!claset addSIs [exI]
  10.185                        addSEs partsEs
  10.186                        addDs [Key_in_parts_respond]) 1);
  10.187  by (expand_case_tac "K = KAB" 1);
  10.188 @@ -457,19 +447,18 @@
  10.189       (analz_image_freshK_ss addsimps 
  10.190         [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
  10.191  by (ALLGOALS Simp_tac);
  10.192 -by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
  10.193 +by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
  10.194  by (step_tac (!claset addSEs [MPair_parts]) 1);
  10.195  (** LEVEL 7 **)
  10.196 -by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
  10.197 +by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
  10.198                        addDs  [impOfSubs analz_subset_parts]) 4);
  10.199 -by (fast_tac (!claset addSDs [respond_certificate]) 3);
  10.200 -by (best_tac (!claset addSEs partsEs
  10.201 -                      addDs [Key_in_parts_respond]
  10.202 -                      addss (!simpset)) 2);
  10.203 +by (blast_tac (!claset addSDs [respond_certificate]) 3);
  10.204 +by (blast_tac (!claset addSEs partsEs
  10.205 +                       addDs [Key_in_parts_respond]) 2);
  10.206  by (dtac unique_session_keys 1);
  10.207  by (etac respond_certificate 1);
  10.208  by (assume_tac 1);
  10.209 -by (Fast_tac 1);
  10.210 +by (Blast_tac 1);
  10.211  qed_spec_mp "respond_Spy_not_see_session_key";
  10.212  
  10.213  
  10.214 @@ -480,7 +469,7 @@
  10.215  \        ==> Key K ~: analz (sees lost Spy evs)";
  10.216  by (etac rev_mp 1);
  10.217  by (etac recur.induct 1);
  10.218 -by analz_Fake_tac;
  10.219 +by analz_sees_tac;
  10.220  by (ALLGOALS
  10.221      (asm_simp_tac
  10.222       (!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
  10.223 @@ -492,17 +481,16 @@
  10.224  (*Fake*)
  10.225  by (spy_analz_tac 2);
  10.226  (*Base*)
  10.227 -by (fast_tac (!claset addss (!simpset)) 1);
  10.228 +by (Blast_tac 1);
  10.229  (*RA3 remains*)
  10.230  by (step_tac (!claset delrules [impCE]) 1);
  10.231  (*RA3, case 2: K is an old key*)
  10.232 -by (best_tac (!claset addSDs [resp_analz_insert]
  10.233 -                      addSEs partsEs
  10.234 -                      addDs [Key_in_parts_respond]
  10.235 -                      addss (!simpset)) 2);
  10.236 +by (blast_tac (!claset addSDs [resp_analz_insert]
  10.237 +                       addSEs partsEs
  10.238 +                       addDs [Key_in_parts_respond]) 2);
  10.239  (*RA3, case 1: use lemma previously proved by induction*)
  10.240 -by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
  10.241 -                              (2,rev_notE)]) 1);
  10.242 +by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
  10.243 +			       (2,rev_notE)]) 1);
  10.244  qed "Spy_not_see_session_key";
  10.245  
  10.246  
  10.247 @@ -516,8 +504,8 @@
  10.248  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  10.249  by (FIRSTGOAL (rtac Spy_not_see_session_key));
  10.250  by (REPEAT_FIRST
  10.251 -    (deepen_tac
  10.252 -     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])) 0));
  10.253 +    (blast_tac
  10.254 +     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
  10.255  qed "Agent_not_see_session_key";
  10.256  
  10.257  
  10.258 @@ -544,9 +532,10 @@
  10.259  \        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
  10.260  \             : set_of_list evs";
  10.261  by (etac rev_mp 1);
  10.262 -by (parts_induct_tac 1);
  10.263 +by parts_induct_tac;
  10.264 +by (Fake_parts_insert_tac 1);
  10.265  (*RA3*)
  10.266 -by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
  10.267 +by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
  10.268  qed_spec_mp "Hash_auth_sender";
  10.269  
  10.270  (** These two results subsume (for all agents) the guarantees proved
  10.271 @@ -561,18 +550,15 @@
  10.272  \        ==> EX C RC. Says Server C RC : set_of_list evs &   \
  10.273  \                     Crypt (shrK A) Y : parts {RC}";
  10.274  by (etac rev_mp 1);
  10.275 -by (parts_induct_tac 1);
  10.276 +by parts_induct_tac;
  10.277 +by (Fake_parts_insert_tac 1);
  10.278  (*RA4*)
  10.279 -by (Fast_tac 4);
  10.280 +by (Blast_tac 4);
  10.281  (*RA3*)
  10.282  by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
  10.283 -    THEN Fast_tac 3);
  10.284 +    THEN Blast_tac 3);
  10.285  (*RA1*)
  10.286 -by (Fast_tac 1);
  10.287 +by (Blast_tac 1);
  10.288  (*RA2: it cannot be a new Nonce, contradiction.*)
  10.289 -by (deepen_tac (!claset delrules [impCE]
  10.290 -                      addSIs [disjI2]
  10.291 -                      addSEs [MPair_parts]
  10.292 -                      addDs  [parts.Body]
  10.293 -                      unsafe_addss  (!simpset)) 0 1);
  10.294 +by (Blast_tac 1);
  10.295  qed "Cert_imp_Server_msg";
    11.1 --- a/src/HOL/Auth/Shared.ML	Wed May 07 12:50:26 1997 +0200
    11.2 +++ b/src/HOL/Auth/Shared.ML	Wed May 07 13:01:43 1997 +0200
    11.3 @@ -56,7 +56,7 @@
    11.4  
    11.5  goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
    11.6  by (agent.induct_tac "C" 1);
    11.7 -by (auto_tac (!claset addIs [range_eqI], !simpset));
    11.8 +by (Auto_tac ());
    11.9  qed "keysFor_parts_initState";
   11.10  Addsimps [keysFor_parts_initState];
   11.11  
   11.12 @@ -210,14 +210,14 @@
   11.13  (** Fresh keys never clash with long-term shared keys **)
   11.14  
   11.15  goal thy "Key (shrK A) : used evs";
   11.16 -by (Best_tac 1);
   11.17 +by (Blast_tac 1);
   11.18  qed "shrK_in_used";
   11.19  AddIffs [shrK_in_used];
   11.20  
   11.21 -(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
   11.22 +(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   11.23    from long-term shared keys*)
   11.24  goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
   11.25 -by (Best_tac 1);
   11.26 +by (Blast_tac 1);
   11.27  qed "Key_not_used";
   11.28  
   11.29  (*A session key cannot clash with a long-term shared key*)
   11.30 @@ -237,7 +237,7 @@
   11.31  by (list.induct_tac "l" 1);
   11.32  by (event.induct_tac "a" 2);
   11.33  by (ALLGOALS Asm_simp_tac);
   11.34 -by (Best_tac 1);
   11.35 +by (Blast_tac 1);
   11.36  qed "used_nil_subset";
   11.37  
   11.38  goal thy "used l <= used (l@l')";
   11.39 @@ -245,7 +245,7 @@
   11.40  by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
   11.41  by (event.induct_tac "a" 1);
   11.42  by (Asm_simp_tac 1);
   11.43 -by (Best_tac 1);
   11.44 +by (Blast_tac 1);
   11.45  qed "used_subset_append";
   11.46  
   11.47  
   11.48 @@ -372,8 +372,8 @@
   11.49  goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
   11.50  by (list.induct_tac "evs" 1);
   11.51  by (event.induct_tac "a" 2);
   11.52 -by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   11.53 -                                addss (!simpset))));
   11.54 +by (ALLGOALS Asm_simp_tac);
   11.55 +by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
   11.56  qed "sees_agent_subset_sees_Spy";
   11.57  
   11.58  (*The Spy can see more than anybody else who's lost their key!*)
   11.59 @@ -381,7 +381,8 @@
   11.60  by (list.induct_tac "evs" 1);
   11.61  by (event.induct_tac "a" 2);
   11.62  by (agent.induct_tac "A" 1);
   11.63 -by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
   11.64 +by (ALLGOALS Asm_simp_tac);
   11.65 +by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
   11.66  qed_spec_mp "sees_lost_agent_subset_sees_Spy";
   11.67  
   11.68  
    12.1 --- a/src/HOL/Auth/WooLam.ML	Wed May 07 12:50:26 1997 +0200
    12.2 +++ b/src/HOL/Auth/WooLam.ML	Wed May 07 13:01:43 1997 +0200
    12.3 @@ -28,8 +28,7 @@
    12.4            woolam.WL4 RS woolam.WL5) 2);
    12.5  by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
    12.6  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    12.7 -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    12.8 -                                    addss (!simpset setSolver safe_solver))));
    12.9 +by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE])));
   12.10  result();
   12.11  
   12.12  
   12.13 @@ -54,18 +53,12 @@
   12.14  bind_thm ("WL4_parts_sees_Spy",
   12.15            WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   12.16  
   12.17 -val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
   12.18 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   12.19 +val parts_induct_tac = 
   12.20 +    etac woolam.induct 1  THEN 
   12.21 +    forward_tac [WL4_parts_sees_Spy] 6  THEN
   12.22 +    prove_simple_subgoals_tac  1;
   12.23  
   12.24 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   12.25 -fun parts_induct_tac i = SELECT_GOAL
   12.26 -    (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
   12.27 -             (*Fake message*)
   12.28 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   12.29 -                                           impOfSubs Fake_parts_insert]
   12.30 -                                    addss (!simpset)) 2)) THEN
   12.31 -     (*Base case*)
   12.32 -     fast_tac (!claset addss (!simpset)) 1 THEN
   12.33 -     ALLGOALS Asm_simp_tac) i;
   12.34  
   12.35  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   12.36      sends messages containing X! **)
   12.37 @@ -74,8 +67,8 @@
   12.38  goal thy 
   12.39   "!!evs. evs : woolam \
   12.40  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   12.41 -by (parts_induct_tac 1);
   12.42 -by (Auto_tac());
   12.43 +by parts_induct_tac;
   12.44 +by (Fake_parts_insert_tac 1);
   12.45  qed "Spy_see_shrK";
   12.46  Addsimps [Spy_see_shrK];
   12.47  
   12.48 @@ -88,7 +81,7 @@
   12.49  
   12.50  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   12.51  \                  evs : woolam |] ==> A:lost";
   12.52 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   12.53 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   12.54  qed "Spy_see_shrK_D";
   12.55  
   12.56  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   12.57 @@ -105,8 +98,9 @@
   12.58   "!!evs. [| A ~: lost;  evs : woolam |]                   \
   12.59  \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
   12.60  \        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
   12.61 -by (parts_induct_tac 1);
   12.62 -by (Fast_tac 1);
   12.63 +by parts_induct_tac;
   12.64 +by (Fake_parts_insert_tac 1);
   12.65 +by (Blast_tac 1);
   12.66  qed_spec_mp "NB_Crypt_imp_Alice_msg";
   12.67  
   12.68  (*Guarantee for Server: if it gets a message containing a certificate from 
   12.69 @@ -117,7 +111,7 @@
   12.70  \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   12.71  \            : set_of_list evs |]                                  \
   12.72  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   12.73 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   12.74 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   12.75                        addSEs [MPair_parts]
   12.76                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   12.77  qed "Server_trusts_WL4";
   12.78 @@ -131,8 +125,9 @@
   12.79  \        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
   12.80  \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   12.81  \               : set_of_list evs)";
   12.82 -by (parts_induct_tac 1);
   12.83 -by (ALLGOALS Fast_tac);
   12.84 +by parts_induct_tac;
   12.85 +by (Fake_parts_insert_tac 1);
   12.86 +by (ALLGOALS Blast_tac);
   12.87  bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
   12.88  
   12.89  
   12.90 @@ -141,7 +136,8 @@
   12.91   "!!evs. [| B ~: lost;  evs : woolam |]                   \
   12.92  \    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   12.93  \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   12.94 -by (parts_induct_tac 1);
   12.95 +by parts_induct_tac;
   12.96 +by (Fake_parts_insert_tac 1);
   12.97  qed_spec_mp "NB_Crypt_imp_Server_msg";
   12.98  
   12.99  (*Partial guarantee for B: if it gets a message of correct form then the Server
  12.100 @@ -150,7 +146,7 @@
  12.101   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
  12.102  \           B ~: lost;  evs : woolam |]                                  \
  12.103  \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
  12.104 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  12.105 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  12.106                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
  12.107  qed "B_got_WL5";
  12.108  
  12.109 @@ -162,7 +158,7 @@
  12.110   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
  12.111  \           A ~: lost;  B ~: lost;  evs : woolam  |] \
  12.112  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
  12.113 -by (fast_tac (!claset addIs  [Server_trusts_WL4]
  12.114 +by (blast_tac (!claset addIs  [Server_trusts_WL4]
  12.115                        addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
  12.116  qed "B_trusts_WL5";
  12.117  
  12.118 @@ -172,8 +168,9 @@
  12.119   "!!evs. [| B ~= Spy;  evs : woolam |]                   \
  12.120  \    ==> Says B A (Nonce NB) : set_of_list evs        \
  12.121  \        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
  12.122 -by (parts_induct_tac 1);
  12.123 -by (ALLGOALS Fast_tac);
  12.124 +by parts_induct_tac;
  12.125 +by (Fake_parts_insert_tac 1);
  12.126 +by (ALLGOALS Blast_tac);
  12.127  bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
  12.128  
  12.129  
  12.130 @@ -183,7 +180,8 @@
  12.131  \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
  12.132  \        Says B A (Nonce NB) : set_of_list evs        \
  12.133  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
  12.134 -by (parts_induct_tac 1);
  12.135 +by parts_induct_tac;
  12.136 +by (Fake_parts_insert_tac 1);
  12.137  by (Step_tac 1);
  12.138 -by (best_tac (!claset addSEs partsEs) 1);
  12.139 +by (blast_tac (!claset addSEs partsEs) 1);
  12.140  **)
    13.1 --- a/src/HOL/Auth/Yahalom.ML	Wed May 07 12:50:26 1997 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed May 07 13:01:43 1997 +0200
    13.3 @@ -16,7 +16,8 @@
    13.4  HOL_quantifiers := false;
    13.5  Pretty.setdepth 25;
    13.6  
    13.7 -val op addss = op unsafe_addss;
    13.8 +(*Replacing the variable by a constant improves speed*)
    13.9 +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
   13.10  
   13.11  
   13.12  (*A "possibility property": there are traces that reach the end*)
   13.13 @@ -38,7 +39,7 @@
   13.14  by (rtac subsetI 1);
   13.15  by (etac yahalom.induct 1);
   13.16  by (REPEAT_FIRST
   13.17 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
   13.18 +    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
   13.19                                :: yahalom.intrs))));
   13.20  qed "yahalom_mono";
   13.21  
   13.22 @@ -57,7 +58,7 @@
   13.23  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   13.24  goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   13.25  \                X : analz (sees lost Spy evs)";
   13.26 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   13.27 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
   13.28  qed "YM4_analz_sees_Spy";
   13.29  
   13.30  bind_thm ("YM4_parts_sees_Spy",
   13.31 @@ -67,26 +68,20 @@
   13.32  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
   13.33  \                  : set_of_list evs ==> \
   13.34  \                K : parts (sees lost Spy evs)";
   13.35 -by (fast_tac (!claset addSEs partsEs
   13.36 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   13.37 +by (blast_tac (!claset addSEs partsEs
   13.38 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   13.39  qed "YM4_Key_parts_sees_Spy";
   13.40  
   13.41 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   13.42 -  harder: the simplifier does less.*)
   13.43 -val parts_Fake_tac = 
   13.44 -    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
   13.45 -    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
   13.46 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
   13.47 +  We instantiate the variable to "lost" since leaving it as a Var would
   13.48 +  interfere with simplification.*)
   13.49 +val parts_sees_tac = 
   13.50 +    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
   13.51 +    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
   13.52 +    prove_simple_subgoals_tac  1;
   13.53  
   13.54 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   13.55 -fun parts_induct_tac i = SELECT_GOAL
   13.56 -    (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
   13.57 -             (*Fake message*)
   13.58 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   13.59 -                                           impOfSubs Fake_parts_insert]
   13.60 -                                    addss (!simpset)) 2)) THEN
   13.61 -     (*Base case*)
   13.62 -     fast_tac (!claset addss (!simpset)) 1 THEN
   13.63 -     ALLGOALS Asm_simp_tac) i;
   13.64 +val parts_induct_tac = 
   13.65 +    etac yahalom.induct 1 THEN parts_sees_tac;
   13.66  
   13.67  
   13.68  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   13.69 @@ -96,8 +91,9 @@
   13.70  goal thy 
   13.71   "!!evs. evs : yahalom lost \
   13.72  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   13.73 -by (parts_induct_tac 1);
   13.74 -by (Auto_tac());
   13.75 +by parts_induct_tac;
   13.76 +by (Fake_parts_insert_tac 1);
   13.77 +by (Blast_tac 1);
   13.78  qed "Spy_see_shrK";
   13.79  Addsimps [Spy_see_shrK];
   13.80  
   13.81 @@ -110,7 +106,7 @@
   13.82  
   13.83  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   13.84  \                  evs : yahalom lost |] ==> A:lost";
   13.85 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   13.86 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   13.87  qed "Spy_see_shrK_D";
   13.88  
   13.89  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   13.90 @@ -120,11 +116,11 @@
   13.91  (*Nobody can have used non-existent keys!*)
   13.92  goal thy "!!evs. evs : yahalom lost ==>          \
   13.93  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   13.94 -by (parts_induct_tac 1);
   13.95 +by parts_induct_tac;
   13.96  (*YM4: Key K is not fresh!*)
   13.97 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
   13.98 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   13.99  (*YM3*)
  13.100 -by (fast_tac (!claset addss (!simpset)) 2);
  13.101 +by (Blast_tac 2);
  13.102  (*Fake*)
  13.103  by (best_tac
  13.104        (!claset addIs [impOfSubs analz_subset_parts]
  13.105 @@ -149,12 +145,13 @@
  13.106  \        ==> K ~: range shrK";
  13.107  by (etac rev_mp 1);
  13.108  by (etac yahalom.induct 1);
  13.109 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  13.110 +by (ALLGOALS Asm_simp_tac);
  13.111 +by (Blast_tac 1);
  13.112  qed "Says_Server_message_form";
  13.113  
  13.114  
  13.115  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
  13.116 -val analz_Fake_tac = 
  13.117 +val analz_sees_tac = 
  13.118      forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
  13.119      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
  13.120      assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
  13.121 @@ -177,12 +174,12 @@
  13.122  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  13.123  \            (K : KK | Key K : analz (sees lost Spy evs))";
  13.124  by (etac yahalom.induct 1);
  13.125 -by analz_Fake_tac;
  13.126 +by analz_sees_tac;
  13.127  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  13.128  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  13.129  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  13.130  (*Base*)
  13.131 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  13.132 +by (Blast_tac 1);
  13.133  (*YM4, Fake*) 
  13.134  by (REPEAT (spy_analz_tac 1));
  13.135  qed_spec_mp "analz_image_freshK";
  13.136 @@ -207,14 +204,13 @@
  13.137  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
  13.138  by (Step_tac 1);
  13.139  by (ex_strip_tac 2);
  13.140 -by (Fast_tac 2);
  13.141 +by (Blast_tac 2);
  13.142  (*Remaining case: YM3*)
  13.143  by (expand_case_tac "K = ?y" 1);
  13.144  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  13.145  (*...we assume X is a recent message and handle this case by contradiction*)
  13.146 -by (fast_tac (!claset addSEs sees_Spy_partsEs
  13.147 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
  13.148 -                      addss (!simpset addsimps [parts_insertI])) 1);
  13.149 +by (blast_tac (!claset addSEs sees_Spy_partsEs
  13.150 +                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
  13.151  val lemma = result();
  13.152  
  13.153  goal thy 
  13.154 @@ -240,7 +236,8 @@
  13.155  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
  13.156  \             : set_of_list evs";
  13.157  by (etac rev_mp 1);
  13.158 -by (parts_induct_tac 1);
  13.159 +by parts_induct_tac;
  13.160 +by (Fake_parts_insert_tac 1);
  13.161  qed "A_trusts_YM3";
  13.162  
  13.163  
  13.164 @@ -255,22 +252,19 @@
  13.165  \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
  13.166  \            Key K ~: analz (sees lost Spy evs)";
  13.167  by (etac yahalom.induct 1);
  13.168 -by analz_Fake_tac;
  13.169 +by analz_sees_tac;
  13.170  by (ALLGOALS
  13.171      (asm_simp_tac 
  13.172       (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
  13.173                 setloop split_tac [expand_if])));
  13.174  (*YM3*)
  13.175 -by (fast_tac (!claset delrules [impCE]
  13.176 -                      addSEs sees_Spy_partsEs
  13.177 -                      addIs [impOfSubs analz_subset_parts]
  13.178 -                      addss (!simpset addsimps [parts_insert2])) 2);
  13.179 +by (blast_tac (!claset delrules [impCE]
  13.180 +                       addSEs sees_Spy_partsEs
  13.181 +                       addIs [impOfSubs analz_subset_parts]) 2);
  13.182  (*OR4, Fake*) 
  13.183  by (REPEAT_FIRST spy_analz_tac);
  13.184  (*Oops*)
  13.185 -by (fast_tac (!claset delrules [disjE] 
  13.186 -                      addDs [unique_session_keys]
  13.187 -                      addss (!simpset)) 1);
  13.188 +by (blast_tac (!claset addDs [unique_session_keys]) 1);
  13.189  val lemma = result() RS mp RS mp RSN(2,rev_notE);
  13.190  
  13.191  
  13.192 @@ -284,7 +278,7 @@
  13.193  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  13.194  \        ==> Key K ~: analz (sees lost Spy evs)";
  13.195  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  13.196 -by (fast_tac (!claset addSEs [lemma]) 1);
  13.197 +by (blast_tac (!claset addSEs [lemma]) 1);
  13.198  qed "Spy_not_see_encrypted_key";
  13.199  
  13.200  
  13.201 @@ -300,7 +294,7 @@
  13.202  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  13.203  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  13.204  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
  13.205 -by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
  13.206 +by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
  13.207  qed "Agent_not_see_encrypted_key";
  13.208  
  13.209  
  13.210 @@ -317,9 +311,10 @@
  13.211  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  13.212  \                       : set_of_list evs";
  13.213  by (etac rev_mp 1);
  13.214 -by (parts_induct_tac 1);
  13.215 +by parts_induct_tac;
  13.216 +by (Fake_parts_insert_tac 1);
  13.217  (*YM3*)
  13.218 -by (Fast_tac 1);
  13.219 +by (Blast_tac 1);
  13.220  qed "B_trusts_YM4_shrK";
  13.221  
  13.222  
  13.223 @@ -330,19 +325,15 @@
  13.224  \   EX NA' A' B'. ALL NA A B. \
  13.225  \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
  13.226  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
  13.227 -by (etac yahalom.induct 1 THEN parts_Fake_tac);
  13.228 -(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
  13.229 -by (REPEAT (etac exE 2) THEN 
  13.230 -    best_tac (!claset addSIs [exI]
  13.231 -                      addDs [impOfSubs Fake_parts_insert]
  13.232 -                      addss (!simpset)) 2);
  13.233 -(*Base case*)
  13.234 -by (fast_tac (!claset addss (!simpset)) 1);
  13.235 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
  13.236 +by parts_induct_tac;
  13.237 +(*Fake*)
  13.238 +by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
  13.239 +    THEN Fake_parts_insert_tac 1);
  13.240 +by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
  13.241  (*YM2: creation of new Nonce.  Move assertion into global context*)
  13.242  by (expand_case_tac "NB = ?y" 1);
  13.243  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
  13.244 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
  13.245 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  13.246  val lemma = result();
  13.247  
  13.248  goal thy 
  13.249 @@ -358,7 +349,7 @@
  13.250  fun lost_tac s =
  13.251      case_tac ("(" ^ s ^ ") : lost") THEN'
  13.252      SELECT_GOAL 
  13.253 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
  13.254 +      (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN
  13.255         REPEAT_DETERM (etac MPair_analz 1) THEN
  13.256         THEN_BEST_FIRST 
  13.257           (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
  13.258 @@ -376,31 +367,34 @@
  13.259  \          evs : yahalom lost |]  \
  13.260  \        ==> NA' = NA & A' = A & B' = B";
  13.261  by (lost_tac "B'" 1);
  13.262 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  13.263 -                      addSEs [MPair_parts]
  13.264 -                      addDs  [unique_NB]) 1);
  13.265 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
  13.266 +                       addSEs [MPair_parts]
  13.267 +                       addDs  [unique_NB]) 1);
  13.268  qed "Says_unique_NB";
  13.269  
  13.270 +(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
  13.271 +  It simplifies the proof by discarding needless information about
  13.272 +	analz (insert X (sees lost Spy evs)) 
  13.273 +*)
  13.274 +val analz_mono_parts_induct_tac = 
  13.275 +    etac yahalom.induct 1 
  13.276 +    THEN 
  13.277 +    REPEAT_FIRST  
  13.278 +      (rtac impI THEN' 
  13.279 +       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
  13.280 +       mp_tac)  
  13.281 +    THEN  parts_sees_tac;
  13.282 +
  13.283  goal thy 
  13.284   "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
  13.285 -\ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
  13.286 -\      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
  13.287 -\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
  13.288 -by (etac yahalom.induct 1);
  13.289 -by parts_Fake_tac;
  13.290 -by (REPEAT_FIRST 
  13.291 -    (rtac impI THEN' 
  13.292 -     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
  13.293 -     mp_tac));
  13.294 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
  13.295 -                             impOfSubs Fake_parts_insert]
  13.296 -                      addss (!simpset)) 2);
  13.297 -by (ALLGOALS Asm_simp_tac);
  13.298 -by (fast_tac (!claset addss (!simpset)) 1);
  13.299 -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
  13.300 -                      addSIs [parts_insertI]
  13.301 -                      addSEs partsEs
  13.302 -                      addss (!simpset)) 1);
  13.303 +\ ==> Nonce NB ~: analz (sees lost Spy evs) -->  \
  13.304 +\     Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
  13.305 +\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
  13.306 +by analz_mono_parts_induct_tac;
  13.307 +by (Fake_parts_insert_tac 1);
  13.308 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
  13.309 +                       addSIs [parts_insertI]
  13.310 +                       addSEs partsEs) 1);
  13.311  val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
  13.312  
  13.313  
  13.314 @@ -419,23 +413,15 @@
  13.315  \                                  Nonce NA, Nonce NB|},                \
  13.316  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  13.317  \                       : set_of_list evs)";
  13.318 -by (etac yahalom.induct 1);
  13.319 -by parts_Fake_tac;
  13.320 -by (fast_tac (!claset addss (!simpset)) 1);
  13.321 -by (REPEAT_FIRST
  13.322 -    (rtac impI THEN'
  13.323 -     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
  13.324 -by (ALLGOALS Asm_simp_tac);
  13.325 -(*Fake, YM3, YM4*)
  13.326 -by (Fast_tac 2);
  13.327 -by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
  13.328 -                      addDs [impOfSubs analz_subset_parts]
  13.329 -                      addss (!simpset)) 1);
  13.330 -(*YM4*)
  13.331 +by analz_mono_parts_induct_tac;
  13.332 +(*YM4 & Fake*)
  13.333 +by (Blast_tac 2);
  13.334 +by (Fake_parts_insert_tac 1);
  13.335 +(*YM3*)
  13.336  by (Step_tac 1);
  13.337  by (lost_tac "A" 1);
  13.338 -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
  13.339 -                             A_trusts_YM3]) 1);
  13.340 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
  13.341 +			      A_trusts_YM3]) 1);
  13.342  val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
  13.343  
  13.344  
  13.345 @@ -448,26 +434,19 @@
  13.346  \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
  13.347  \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
  13.348  \            (EX A B NA. Says Server A                                  \
  13.349 -\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  13.350 -\                                  Nonce NA, Nonce NB|},       \
  13.351 +\                        {|Crypt (shrK A) {|Agent B, Key K,             \
  13.352 +\                                  Nonce NA, Nonce NB|},                \
  13.353  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  13.354  \                       : set_of_list evs)";
  13.355 -by (etac yahalom.induct 1);
  13.356 -by parts_Fake_tac;
  13.357 -by (fast_tac (!claset addss (!simpset)) 1);
  13.358 -by (TRYALL (rtac impI));
  13.359 -by (REPEAT_FIRST
  13.360 -    (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
  13.361 -by (ALLGOALS Asm_simp_tac);
  13.362 -(*Fake, YM3, YM4*)
  13.363 -by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
  13.364 -                      addDs  [impOfSubs analz_subset_parts]) 1);
  13.365 -by (Fast_tac 1);
  13.366 -(*YM4*)
  13.367 +by analz_mono_parts_induct_tac;
  13.368 +(*YM4 & Fake*)
  13.369 +by (Blast_tac 2);
  13.370 +by (Fake_parts_insert_tac 1);
  13.371 +(*YM3*)
  13.372  by (Step_tac 1);
  13.373  by (lost_tac "A" 1);
  13.374 -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
  13.375 -                             A_trusts_YM3]) 1);
  13.376 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
  13.377 +			      A_trusts_YM3]) 1);
  13.378  result() RS mp RSN (2, rev_mp);
  13.379  
  13.380  
  13.381 @@ -482,7 +461,7 @@
  13.382  by (etac rev_mp 1);
  13.383  by (etac yahalom.induct 1);
  13.384  by (ALLGOALS Asm_simp_tac);
  13.385 -by (ALLGOALS Fast_tac);
  13.386 +by (ALLGOALS Blast_tac);
  13.387  qed "Says_Server_imp_YM2";
  13.388  
  13.389  
  13.390 @@ -491,9 +470,9 @@
  13.391  val no_nonce_tac = SELECT_GOAL
  13.392     (REPEAT (resolve_tac [impI, notI] 1) THEN
  13.393      REPEAT (hyp_subst_tac 1) THEN
  13.394 -    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
  13.395 +    etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
  13.396      THEN
  13.397 -    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
  13.398 +    etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd) 4
  13.399      THEN 
  13.400      REPEAT_FIRST assume_tac);
  13.401  
  13.402 @@ -509,30 +488,30 @@
  13.403  goal thy  
  13.404   "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
  13.405  \        P --> (X : analz (G Un H)) = (X : analz H)";
  13.406 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
  13.407 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
  13.408  qed "Nonce_secrecy_lemma";
  13.409  
  13.410  goal thy 
  13.411 - "!!evs. evs : yahalom lost ==>                                          \
  13.412 + "!!evs. evs : yahalom lost ==>                                              \
  13.413  \        (ALL KK. KK <= Compl (range shrK) -->                               \
  13.414 -\             (ALL K: KK. ALL A B na X.                                       \
  13.415 +\             (ALL K: KK. ALL A B na X.                                      \
  13.416  \                 Says Server A                                              \
  13.417  \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  13.418 -\                 ~: set_of_list evs)   -->  \
  13.419 -\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =      \
  13.420 +\                 ~: set_of_list evs)   -->                                  \
  13.421 +\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =          \
  13.422  \             (Nonce NB : analz (sees lost Spy evs)))";
  13.423  by (etac yahalom.induct 1);
  13.424 -by analz_Fake_tac;
  13.425 +by analz_sees_tac;
  13.426  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
  13.427  by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
  13.428  by (rtac ccontr 7);
  13.429 -by (subgoal_tac "ALL A B na X.                                       \
  13.430 +by (subgoal_tac "ALL A B na X.                                               \
  13.431  \                 Says Server A                                              \
  13.432  \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  13.433  \                 ~: set_of_list evsa" 7);
  13.434  by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
  13.435 -by (subgoal_tac "ALL A B na X.                                       \
  13.436 -\                 Says Server A                                              \
  13.437 +by (subgoal_tac "ALL A B na X.                                                \
  13.438 +\                 Says Server A                                               \
  13.439  \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
  13.440  \                 ~: set_of_list evsa" 5);
  13.441  by (ALLGOALS  (*22 seconds*)
  13.442 @@ -542,15 +521,14 @@
  13.443                 not_parts_not_analz, analz_image_freshK]
  13.444                @ pushes @ ball_simps))));
  13.445  (*Base*)
  13.446 -by (fast_tac (!claset addss (!simpset)) 1);
  13.447 +by (Blast_tac 1);
  13.448  (*Fake*) (** LEVEL 10 **)
  13.449  by (spy_analz_tac 1);
  13.450  (*YM3*)
  13.451 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
  13.452 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  13.453  (*Oops*)
  13.454 -(*20 secs*)
  13.455 -by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
  13.456 -                      addss (!simpset)) 2);
  13.457 +by (Asm_full_simp_tac 2); 
  13.458 +by (blast_tac (!claset addDs [unique_session_keys]) 2);
  13.459  (*YM4*)
  13.460  (** LEVEL 13 **)
  13.461  by (REPEAT (resolve_tac [impI, allI] 1));
  13.462 @@ -562,10 +540,10 @@
  13.463  by (step_tac (!claset addSDs [not_analz_insert]) 1);
  13.464  by (lost_tac "A" 1);
  13.465  (** LEVEL 20 **)
  13.466 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
  13.467 +by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
  13.468      THEN REPEAT (assume_tac 1));
  13.469  by (thin_tac "All ?PP" 1);
  13.470 -by (Fast_tac 1);
  13.471 +by (Blast_tac 1);
  13.472  qed_spec_mp "Nonce_secrecy";
  13.473  
  13.474  
  13.475 @@ -581,8 +559,8 @@
  13.476  \           KAB ~: range shrK;  evs : yahalom lost |]                  \
  13.477  \        ==>  NB = NB'";
  13.478  by (rtac ccontr 1);
  13.479 -by (subgoal_tac "ALL A B na X.                                       \
  13.480 -\                 Says Server A                                              \
  13.481 +by (subgoal_tac "ALL A B na X.                                                \
  13.482 +\                 Says Server A                                               \
  13.483  \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
  13.484  \                 ~: set_of_list evs" 1);
  13.485  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
  13.486 @@ -592,6 +570,8 @@
  13.487  qed "single_Nonce_secrecy";
  13.488  
  13.489  
  13.490 +val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
  13.491 +
  13.492  goal thy 
  13.493   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
  13.494  \ ==> Says B Server                                                    \
  13.495 @@ -600,55 +580,53 @@
  13.496  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
  13.497  \     Nonce NB ~: analz (sees lost Spy evs)";
  13.498  by (etac yahalom.induct 1);
  13.499 -by analz_Fake_tac;
  13.500 +by analz_sees_tac;
  13.501  by (ALLGOALS
  13.502      (asm_simp_tac 
  13.503       (!simpset addsimps ([not_parts_not_analz,
  13.504                            analz_insert_freshK] @ pushes)
  13.505                 setloop split_tac [expand_if])));
  13.506 -by (fast_tac (!claset addSIs [parts_insertI]
  13.507 -                      addSEs sees_Spy_partsEs
  13.508 -                      addss (!simpset)) 2);
  13.509 +by (blast_tac (!claset addSIs [parts_insertI]
  13.510 +                       addSEs sees_Spy_partsEs) 2);
  13.511  (*Proof of YM2*) (** LEVEL 4 **)
  13.512 -by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
  13.513 -                               impOfSubs analz_subset_parts]
  13.514 -                        addSEs partsEs) 3 2);
  13.515 +by (blast_tac (!claset addSEs partsEs
  13.516 +		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
  13.517 +			       impOfSubs analz_subset_parts]) 2);
  13.518  (*Prove YM3 by showing that no NB can also be an NA*)
  13.519  by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
  13.520 -by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
  13.521 +by (blast_tac (!claset addDs [Says_unique_NB']) 2 THEN flexflex_tac);
  13.522  (*Fake*)
  13.523  by (spy_analz_tac 1);
  13.524  (*YM4*) (** LEVEL 8 **)
  13.525  by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
  13.526  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
  13.527 -(*43 secs??*)
  13.528 +(*  SLOW: 13s*)
  13.529  by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
  13.530  by (lost_tac "Aa" 1);
  13.531 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
  13.532 +by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
  13.533  by (forward_tac [Says_Server_message_form] 3);
  13.534  by (forward_tac [Says_Server_imp_YM2] 4);
  13.535 -(** LEVEL 15 **)
  13.536 -by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
  13.537 +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
  13.538 +(** LEVEL 16 **)
  13.539 +(*  use unique_NB to identify message components  *)
  13.540  by (lost_tac "Ba" 1);
  13.541 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
  13.542 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  13.543 -                      addSEs [MPair_parts]) 1);
  13.544 -by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
  13.545 +by (subgoal_tac "Aa=A & Ba=B & NAa=NA" 1);
  13.546 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
  13.547 +                       addSEs [MPair_parts] addDs [unique_NB]) 2);
  13.548 +by (blast_tac (!claset addDs [Spy_not_see_encrypted_key,
  13.549 +			      impOfSubs Fake_analz_insert]
  13.550 +		       addIs [impOfSubs analz_mono]) 1);
  13.551  (** LEVEL 20 **)
  13.552 -by (dtac Spy_not_see_encrypted_key 1);
  13.553 -by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
  13.554 -by (spy_analz_tac 1);
  13.555 -(*Oops case*) (** LEVEL 23 **)
  13.556 +(*Oops case*)
  13.557  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
  13.558  by (step_tac (!claset delrules [disjE, conjI]) 1);
  13.559  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
  13.560  by (expand_case_tac "NB = NBa" 1);
  13.561 -by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
  13.562 +by (blast_tac (!claset addDs [Says_unique_NB']) 1);
  13.563  by (rtac conjI 1);
  13.564  by (no_nonce_tac 1);
  13.565  (** LEVEL 30 **)
  13.566 -by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
  13.567 -by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
  13.568 +by (blast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
  13.569  val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
  13.570  
  13.571  
  13.572 @@ -671,11 +649,11 @@
  13.573  \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
  13.574  \                   : set_of_list evs";
  13.575  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
  13.576 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
  13.577 +by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
  13.578      dtac B_trusts_YM4_shrK 1);
  13.579  by (dtac B_trusts_YM4_newK 3);
  13.580  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
  13.581  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
  13.582  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
  13.583 -by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
  13.584 +by (blast_tac (!claset addDs [Says_unique_NB']) 1);
  13.585  qed "B_trusts_YM4";
    14.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed May 07 12:50:26 1997 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed May 07 13:01:43 1997 +0200
    14.3 @@ -17,8 +17,6 @@
    14.4  proof_timing:=true;
    14.5  HOL_quantifiers := false;
    14.6  
    14.7 -val op addss = op unsafe_addss;
    14.8 -
    14.9  (*A "possibility property": there are traces that reach the end*)
   14.10  goal thy 
   14.11   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   14.12 @@ -38,7 +36,7 @@
   14.13  by (rtac subsetI 1);
   14.14  by (etac yahalom.induct 1);
   14.15  by (REPEAT_FIRST
   14.16 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
   14.17 +    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
   14.18                                :: yahalom.intrs))));
   14.19  qed "yahalom_mono";
   14.20  
   14.21 @@ -57,7 +55,7 @@
   14.22  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   14.23  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   14.24  \                X : analz (sees lost Spy evs)";
   14.25 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   14.26 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   14.27  qed "YM4_analz_sees_Spy";
   14.28  
   14.29  bind_thm ("YM4_parts_sees_Spy",
   14.30 @@ -67,26 +65,18 @@
   14.31  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
   14.32  \                  : set_of_list evs ==> \
   14.33  \                K : parts (sees lost Spy evs)";
   14.34 -by (fast_tac (!claset addSEs partsEs
   14.35 +by (blast_tac (!claset addSEs partsEs
   14.36                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   14.37  qed "YM4_Key_parts_sees_Spy";
   14.38  
   14.39 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   14.40 -  harder: the simplifier does less.*)
   14.41 -val parts_Fake_tac = 
   14.42 -    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
   14.43 -    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
   14.44 -
   14.45 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   14.46 -fun parts_induct_tac i = SELECT_GOAL
   14.47 -    (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
   14.48 -             (*Fake message*)
   14.49 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   14.50 -                                           impOfSubs Fake_parts_insert]
   14.51 -                                    addss (!simpset)) 2)) THEN
   14.52 -     (*Base case*)
   14.53 -     fast_tac (!claset addss (!simpset)) 1 THEN
   14.54 -     ALLGOALS Asm_simp_tac) i;
   14.55 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
   14.56 +  We instantiate the variable to "lost" since leaving it as a Var would
   14.57 +  interfere with simplification.*)
   14.58 +val parts_induct_tac = 
   14.59 +    etac yahalom.induct 1 THEN 
   14.60 +    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
   14.61 +    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
   14.62 +    prove_simple_subgoals_tac  1;
   14.63  
   14.64  
   14.65  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   14.66 @@ -96,8 +86,9 @@
   14.67  goal thy 
   14.68   "!!evs. evs : yahalom lost \
   14.69  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   14.70 -by (parts_induct_tac 1);
   14.71 -by (Auto_tac());
   14.72 +by parts_induct_tac;
   14.73 +by (Fake_parts_insert_tac 1);
   14.74 +by (Blast_tac 1);
   14.75  qed "Spy_see_shrK";
   14.76  Addsimps [Spy_see_shrK];
   14.77  
   14.78 @@ -110,7 +101,7 @@
   14.79  
   14.80  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   14.81  \                  evs : yahalom lost |] ==> A:lost";
   14.82 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   14.83 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   14.84  qed "Spy_see_shrK_D";
   14.85  
   14.86  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   14.87 @@ -120,11 +111,11 @@
   14.88  (*Nobody can have used non-existent keys!*)
   14.89  goal thy "!!evs. evs : yahalom lost ==>          \
   14.90  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   14.91 -by (parts_induct_tac 1);
   14.92 +by parts_induct_tac;
   14.93  (*YM4: Key K is not fresh!*)
   14.94 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
   14.95 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   14.96  (*YM3*)
   14.97 -by (fast_tac (!claset addss (!simpset)) 2);
   14.98 +by (blast_tac (!claset addss (!simpset)) 2);
   14.99  (*Fake*)
  14.100  by (best_tac
  14.101        (!claset addIs [impOfSubs analz_subset_parts]
  14.102 @@ -149,12 +140,12 @@
  14.103  \        ==> K ~: range shrK & A ~= B";
  14.104  by (etac rev_mp 1);
  14.105  by (etac yahalom.induct 1);
  14.106 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  14.107 +by (ALLGOALS Asm_simp_tac);
  14.108  qed "Says_Server_message_form";
  14.109  
  14.110  
  14.111  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
  14.112 -val analz_Fake_tac = 
  14.113 +val analz_sees_tac = 
  14.114      dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
  14.115      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
  14.116      assume_tac 7 THEN
  14.117 @@ -179,12 +170,12 @@
  14.118  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  14.119  \            (K : KK | Key K : analz (sees lost Spy evs))";
  14.120  by (etac yahalom.induct 1);
  14.121 -by analz_Fake_tac;
  14.122 +by analz_sees_tac;
  14.123  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  14.124  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  14.125  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  14.126  (*Base*)
  14.127 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  14.128 +by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  14.129  (*YM4, Fake*) 
  14.130  by (REPEAT (spy_analz_tac 1));
  14.131  qed_spec_mp "analz_image_freshK";
  14.132 @@ -212,7 +203,7 @@
  14.133  by (expand_case_tac "K = ?y" 1);
  14.134  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  14.135  (*...we assume X is a recent message and handle this case by contradiction*)
  14.136 -by (fast_tac (!claset addSEs sees_Spy_partsEs
  14.137 +by (blast_tac (!claset addSEs sees_Spy_partsEs
  14.138                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
  14.139                        addss (!simpset addsimps [parts_insertI])) 1);
  14.140  val lemma = result();
  14.141 @@ -234,30 +225,28 @@
  14.142  
  14.143  goal thy 
  14.144   "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
  14.145 -\           evs : yahalom lost |]            \
  14.146 +\           evs : yahalom lost |]                                    \
  14.147  \        ==> Says Server A                                           \
  14.148 -\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},           \
  14.149 -\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}          \
  14.150 -\             : set_of_list evs -->                               \
  14.151 -\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
  14.152 +\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},          \
  14.153 +\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}         \
  14.154 +\             : set_of_list evs -->                                  \
  14.155 +\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->     \
  14.156  \            Key K ~: analz (sees lost Spy evs)";
  14.157  by (etac yahalom.induct 1);
  14.158 -by analz_Fake_tac;
  14.159 +by analz_sees_tac;
  14.160  by (ALLGOALS
  14.161      (asm_simp_tac 
  14.162       (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
  14.163                 setloop split_tac [expand_if])));
  14.164  (*YM3*)
  14.165 -by (fast_tac (!claset delrules [impCE]
  14.166 +by (blast_tac (!claset delrules [impCE]
  14.167                        addSEs sees_Spy_partsEs
  14.168                        addIs [impOfSubs analz_subset_parts]
  14.169                        addss (!simpset addsimps [parts_insert2])) 2);
  14.170  (*OR4, Fake*) 
  14.171  by (REPEAT_FIRST spy_analz_tac);
  14.172  (*Oops*)
  14.173 -by (fast_tac (!claset delrules [disjE] 
  14.174 -                      addDs [unique_session_keys]
  14.175 -                      addss (!simpset)) 1);
  14.176 +by (blast_tac (!claset addDs [unique_session_keys]) 1);
  14.177  val lemma = result() RS mp RS mp RSN(2,rev_notE);
  14.178  
  14.179  
  14.180 @@ -271,7 +260,7 @@
  14.181  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  14.182  \        ==> Key K ~: analz (sees lost Spy evs)";
  14.183  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  14.184 -by (fast_tac (!claset addSEs [lemma]) 1);
  14.185 +by (blast_tac (!claset addSEs [lemma]) 1);
  14.186  qed "Spy_not_see_encrypted_key";
  14.187  
  14.188  
  14.189 @@ -287,7 +276,7 @@
  14.190  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  14.191  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  14.192  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
  14.193 -by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
  14.194 +by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
  14.195  qed "Agent_not_see_encrypted_key";
  14.196  
  14.197  
  14.198 @@ -303,9 +292,9 @@
  14.199  \                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
  14.200  \                    : set_of_list evs";
  14.201  by (etac rev_mp 1);
  14.202 -by (parts_induct_tac 1);
  14.203 -(*The nested conjunctions are entirely useless*)
  14.204 -by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
  14.205 +by parts_induct_tac;
  14.206 +by (Fake_parts_insert_tac 1);
  14.207 +by (Blast_tac 1);
  14.208  qed "A_trusts_YM3";
  14.209  
  14.210  
  14.211 @@ -321,9 +310,10 @@
  14.212  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
  14.213  \                       : set_of_list evs";
  14.214  by (etac rev_mp 1);
  14.215 -by (parts_induct_tac 1);
  14.216 +by parts_induct_tac;
  14.217 +by (Fake_parts_insert_tac 1);
  14.218  (*YM3*)
  14.219 -by (Fast_tac 1);
  14.220 +by (Blast_tac 1);
  14.221  qed "B_trusts_YM4_shrK";
  14.222  
  14.223  (*With this variant we don't bother to use the 2nd part of YM4 at all, since
  14.224 @@ -342,5 +332,5 @@
  14.225  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
  14.226  \                   : set_of_list evs";
  14.227  by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
  14.228 -by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
  14.229 +by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
  14.230  qed "B_trusts_YM4";