Some blast_tac calls; more needed
authorpaulson
Mon May 05 12:15:53 1997 +0200 (1997-05-05)
changeset 31024d01cdc119d2
parent 3101 e8a92f497295
child 3103 98af809fee46
Some blast_tac calls; more needed
src/HOL/Auth/Message.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Mon May 05 12:15:20 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Mon May 05 12:15:53 1997 +0200
     1.3 @@ -43,23 +43,23 @@
     1.4  qed "keysFor_mono";
     1.5  
     1.6  goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
     1.7 -by (fast_tac (!claset addss (!simpset)) 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "keysFor_insert_Agent";
    1.10  
    1.11  goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    1.12 -by (fast_tac (!claset addss (!simpset)) 1);
    1.13 +by (Blast_tac 1);
    1.14  qed "keysFor_insert_Nonce";
    1.15  
    1.16  goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    1.17 -by (fast_tac (!claset addss (!simpset)) 1);
    1.18 +by (Blast_tac 1);
    1.19  qed "keysFor_insert_Key";
    1.20  
    1.21  goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    1.22 -by (fast_tac (!claset addss (!simpset)) 1);
    1.23 +by (Blast_tac 1);
    1.24  qed "keysFor_insert_Hash";
    1.25  
    1.26  goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    1.27 -by (fast_tac (!claset addss (!simpset)) 1);
    1.28 +by (Blast_tac 1);
    1.29  qed "keysFor_insert_MPair";
    1.30  
    1.31  goalw thy [keysFor_def]
    1.32 @@ -219,7 +219,7 @@
    1.33  fun parts_tac i =
    1.34    EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
    1.35           etac parts.induct i,
    1.36 -         REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.37 +         REPEAT (Blast_tac i)];
    1.38  
    1.39  goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
    1.40  by (parts_tac 1);
    1.41 @@ -347,7 +347,7 @@
    1.42  fun analz_tac i =
    1.43    EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
    1.44           etac analz.induct i,
    1.45 -         REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.46 +         REPEAT (Blast_tac i)];
    1.47  
    1.48  goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
    1.49  by (analz_tac 1);
    1.50 @@ -390,7 +390,7 @@
    1.51  \              insert (Crypt K X) (analz (insert X H))";
    1.52  by (rtac subsetI 1);
    1.53  by (eres_inst_tac [("za","x")] analz.induct 1);
    1.54 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.55 +by (ALLGOALS (Blast_tac));
    1.56  val lemma1 = result();
    1.57  
    1.58  goal thy "!!H. Key (invKey K) : analz H ==>  \
    1.59 @@ -670,8 +670,7 @@
    1.60  \          ==> Crypt K Y : parts G Un parts H";
    1.61  by (dtac (impOfSubs Fake_parts_insert) 1);
    1.62  by (assume_tac 1);
    1.63 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
    1.64 -                      addss (!simpset)) 1);
    1.65 +by (blast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
    1.66  qed "Crypt_Fake_parts_insert";
    1.67  
    1.68  goal thy "!!H. X: synth (analz G) ==> \
    1.69 @@ -831,8 +830,9 @@
    1.70         DEPTH_SOLVE 
    1.71           (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
    1.72            THEN
    1.73 -          IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
    1.74 -                                                 impOfSubs analz_subset_parts]) 2 1))
    1.75 +          IF_UNSOLVED (Blast.depth_tac
    1.76 +		       (!claset addIs [impOfSubs analz_mono,
    1.77 +				       impOfSubs analz_subset_parts]) 2 1))
    1.78         ]) i);
    1.79  
    1.80  (** Useful in many uniqueness proofs **)
    1.81 @@ -846,7 +846,7 @@
    1.82            REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
    1.83            (*Duplicate the assumption*)
    1.84            forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
    1.85 -          depth_tac (!claset addSDs [spec]) 0];
    1.86 +          Blast.depth_tac (!claset addSDs [spec]) 0];
    1.87  
    1.88  
    1.89  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon May 05 12:15:20 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon May 05 12:15:53 1997 +0200
     2.3 @@ -17,6 +17,10 @@
     2.4  proof_timing:=true;
     2.5  HOL_quantifiers := false;
     2.6  
     2.7 +(*Replacing the variable by a constant improves search speed by 50%!*)
     2.8 +val Says_imp_sees_Spy' = 
     2.9 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    2.10 +
    2.11  
    2.12  (*A "possibility property": there are traces that reach the end*)
    2.13  goal thy 
    2.14 @@ -36,8 +40,8 @@
    2.15  goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    2.16  by (rtac subsetI 1);
    2.17  by (etac otway.induct 1);
    2.18 -by (REPEAT_FIRST
    2.19 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    2.20 +by (ALLGOALS
    2.21 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    2.22                                :: otway.intrs))));
    2.23  qed "otway_mono";
    2.24  
    2.25 @@ -54,17 +58,17 @@
    2.26  
    2.27  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    2.28  \                ==> X : analz (sees lost Spy evs)";
    2.29 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    2.30 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    2.31  qed "OR2_analz_sees_Spy";
    2.32  
    2.33  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    2.34  \                ==> X : analz (sees lost Spy evs)";
    2.35 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    2.36 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    2.37  qed "OR4_analz_sees_Spy";
    2.38  
    2.39  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    2.40  \                 ==> K : parts (sees lost Spy evs)";
    2.41 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    2.42 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    2.43  qed "Oops_parts_sees_Spy";
    2.44  
    2.45  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    2.46 @@ -118,7 +122,7 @@
    2.47  
    2.48  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    2.49  \                  evs : otway lost |] ==> A:lost";
    2.50 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    2.51 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    2.52  qed "Spy_see_shrK_D";
    2.53  
    2.54  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    2.55 @@ -135,8 +139,7 @@
    2.56                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    2.57                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    2.58                 unsafe_addss (!simpset)) 1);
    2.59 -(*OR1-3*)
    2.60 -by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    2.61 +by (ALLGOALS Blast_tac);
    2.62  qed_spec_mp "new_keys_not_used";
    2.63  
    2.64  bind_thm ("new_keys_not_analzd",
    2.65 @@ -158,7 +161,8 @@
    2.66  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    2.67  by (etac rev_mp 1);
    2.68  by (etac otway.induct 1);
    2.69 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    2.70 +by (ALLGOALS Simp_tac);
    2.71 +by (ALLGOALS Blast_tac);
    2.72  qed "Says_Server_message_form";
    2.73  
    2.74  
    2.75 @@ -195,7 +199,7 @@
    2.76  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    2.77  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    2.78  (*Base*)
    2.79 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    2.80 +by (Blast_tac 1);
    2.81  (*Fake, OR2, OR4*) 
    2.82  by (REPEAT (spy_analz_tac 1));
    2.83  qed_spec_mp "analz_image_freshK";
    2.84 @@ -221,13 +225,12 @@
    2.85  by (Step_tac 1);
    2.86  (*Remaining cases: OR3 and OR4*)
    2.87  by (ex_strip_tac 2);
    2.88 -by (Fast_tac 2);
    2.89 +by (Best_tac 2);
    2.90  by (expand_case_tac "K = ?y" 1);
    2.91  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    2.92  (*...we assume X is a recent message, and handle this case by contradiction*)
    2.93 -by (fast_tac (!claset addSEs sees_Spy_partsEs
    2.94 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
    2.95 -                      addss (!simpset addsimps [parts_insertI])) 1);
    2.96 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    2.97 +                       delrules [conjI] (*no split-up into 4 subgoals*)) 1);
    2.98  val lemma = result();
    2.99  
   2.100  goal thy 
   2.101 @@ -266,7 +269,7 @@
   2.102  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   2.103  (*OR1: creation of new Nonce.  Move assertion into global context*)
   2.104  by (expand_case_tac "NA = ?y" 1);
   2.105 -by (best_tac (!claset addSEs sees_Spy_partsEs) 1);
   2.106 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   2.107  val lemma = result();
   2.108  
   2.109  goal thy 
   2.110 @@ -288,9 +291,8 @@
   2.111  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   2.112  \             ~: parts (sees lost Spy evs)";
   2.113  by (parts_induct_tac 1);
   2.114 -by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs
   2.115 -                              addSDs  [impOfSubs parts_insert_subset_Un]
   2.116 -                              addss (!simpset)) 1));
   2.117 +by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   2.118 +                               addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   2.119  qed_spec_mp"no_nonce_OR1_OR2";
   2.120  
   2.121  
   2.122 @@ -309,25 +311,23 @@
   2.123  \                   : set_of_list evs)";
   2.124  by (parts_induct_tac 1);
   2.125  (*OR1: it cannot be a new Nonce, contradiction.*)
   2.126 -by (fast_tac (!claset addSIs [parts_insertI]
   2.127 -                      addSEs sees_Spy_partsEs
   2.128 -                      addss (!simpset)) 1);
   2.129 +by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   2.130  (*OR3 and OR4*) 
   2.131  (*OR4*)
   2.132  by (REPEAT (Safe_step_tac 2));
   2.133 -by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   2.134 +by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   2.135  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   2.136                        addEs  sees_Spy_partsEs) 2);
   2.137  (*OR3*)  (** LEVEL 5 **)
   2.138  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   2.139  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   2.140 -by (fast_tac (!claset addSEs [MPair_parts]
   2.141 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   2.142 +by (blast_tac (!claset addSEs [MPair_parts]
   2.143 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.144                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   2.145                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   2.146 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   2.147 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.148                        addSEs [MPair_parts]
   2.149 -                      addEs  [unique_NA]) 1);
   2.150 +                      addIs  [unique_NA]) 1);
   2.151  qed_spec_mp "NA_Crypt_imp_Server_msg";
   2.152  
   2.153  
   2.154 @@ -347,8 +347,8 @@
   2.155  \                       Crypt (shrK A) {|NA, Key K|},              \
   2.156  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   2.157  \                       : set_of_list evs";
   2.158 -by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   2.159 -                      addEs  sees_Spy_partsEs) 1);
   2.160 +by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   2.161 +                       addEs  sees_Spy_partsEs) 1);
   2.162  qed "A_trusts_OR4";
   2.163  
   2.164  
   2.165 @@ -370,15 +370,13 @@
   2.166                              addsimps [not_parts_not_analz, analz_insert_freshK]
   2.167                              setloop split_tac [expand_if])));
   2.168  (*OR3*)
   2.169 -by (fast_tac (!claset delrules [impCE]
   2.170 -                      addSEs sees_Spy_partsEs
   2.171 -                      addIs [impOfSubs analz_subset_parts]
   2.172 -                      addss (!simpset addsimps [parts_insert2])) 3);
   2.173 +by (blast_tac (!claset delrules [impCE]
   2.174 +                       addSEs sees_Spy_partsEs
   2.175 +                       addIs [impOfSubs analz_subset_parts]) 3);
   2.176  (*OR4, OR2, Fake*) 
   2.177  by (REPEAT_FIRST spy_analz_tac);
   2.178  (*Oops*) (** LEVEL 5 **)
   2.179 -by (fast_tac (!claset delrules [disjE]
   2.180 -                      addDs [unique_session_keys] addss (!simpset)) 1);
   2.181 +by (blast_tac (!claset addSDs [unique_session_keys]) 1);
   2.182  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   2.183  
   2.184  goal thy 
   2.185 @@ -389,7 +387,7 @@
   2.186  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   2.187  \        ==> Key K ~: analz (sees lost Spy evs)";
   2.188  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   2.189 -by (fast_tac (!claset addSEs [lemma]) 1);
   2.190 +by (blast_tac (!claset addSEs [lemma]) 1);
   2.191  qed "Spy_not_see_encrypted_key";
   2.192  
   2.193  
   2.194 @@ -404,7 +402,7 @@
   2.195  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   2.196  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   2.197  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   2.198 -by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   2.199 +by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   2.200  qed "Agent_not_see_encrypted_key";
   2.201  
   2.202  
   2.203 @@ -421,7 +419,7 @@
   2.204  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   2.205  \             : set_of_list evs)";
   2.206  by (parts_induct_tac 1);
   2.207 -by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   2.208 +by (ALLGOALS Blast_tac);
   2.209  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   2.210  
   2.211  
   2.212 @@ -436,7 +434,7 @@
   2.213  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   2.214  (*OR2: creation of new Nonce.  Move assertion into global context*)
   2.215  by (expand_case_tac "NB = ?y" 1);
   2.216 -by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1);
   2.217 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   2.218  val lemma = result();
   2.219  
   2.220  goal thy 
   2.221 @@ -465,21 +463,18 @@
   2.222  \                   : set_of_list evs)";
   2.223  by (parts_induct_tac 1);
   2.224  (*OR1: it cannot be a new Nonce, contradiction.*)
   2.225 -by (fast_tac (!claset addSIs [parts_insertI]
   2.226 -                      addSEs sees_Spy_partsEs
   2.227 -                      addss (!simpset)) 1);
   2.228 +by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   2.229  (*OR4*)
   2.230 -by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   2.231 +by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   2.232  (*OR3*)
   2.233  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   2.234 -by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   2.235 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   2.236 -                      addSEs [MPair_parts]
   2.237 -                      addDs  [unique_NB]) 2);
   2.238 -by (fast_tac (!claset addSEs [MPair_parts]
   2.239 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   2.240 -                      addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   2.241 -                      delrules [conjI, impCE] (*stop split-up*)) 1);
   2.242 +by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   2.243 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.244 +                       addSEs [MPair_parts]
   2.245 +                       addDs  [unique_NB]) 2);
   2.246 +by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   2.247 +                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
   2.248 +                       delrules [conjI, impCE] (*stop split-up*)) 1);
   2.249  qed_spec_mp "NB_Crypt_imp_Server_msg";
   2.250  
   2.251  
   2.252 @@ -497,8 +492,8 @@
   2.253  \                   Crypt (shrK A) {|NA, Key K|},                  \
   2.254  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   2.255  \                   : set_of_list evs";
   2.256 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   2.257 -                      addEs  sees_Spy_partsEs) 1);
   2.258 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   2.259 +                       addSEs sees_Spy_partsEs) 1);
   2.260  qed "B_trusts_OR3";
   2.261  
   2.262  
   2.263 @@ -514,9 +509,10 @@
   2.264  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   2.265  \            : set_of_list evs)";
   2.266  by (etac otway.induct 1);
   2.267 -by (Auto_tac());
   2.268 -by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   2.269 -by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   2.270 +by (ALLGOALS Asm_simp_tac);
   2.271 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   2.272 +		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   2.273 +by (ALLGOALS Blast_tac);
   2.274  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   2.275  
   2.276  
   2.277 @@ -533,6 +529,6 @@
   2.278  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   2.279  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   2.280  \            : set_of_list evs";
   2.281 -by (fast_tac (!claset addSDs  [A_trusts_OR4]
   2.282 -                      addSEs [OR3_imp_OR2]) 1);
   2.283 +by (blast_tac (!claset addSDs  [A_trusts_OR4]
   2.284 +                       addSEs [OR3_imp_OR2]) 1);
   2.285  qed "A_auths_B";
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon May 05 12:15:20 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon May 05 12:15:53 1997 +0200
     3.3 @@ -54,12 +54,12 @@
     3.4  
     3.5  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
     3.6  \                X : analz (sees lost Spy evs)";
     3.7 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     3.8 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     3.9  qed "OR4_analz_sees_Spy";
    3.10  
    3.11  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    3.12  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    3.13 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    3.14 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    3.15  qed "Oops_parts_sees_Spy";
    3.16  
    3.17  (*OR4_analz_sees_Spy lets us treat those cases using the same 
    3.18 @@ -107,7 +107,7 @@
    3.19  
    3.20  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    3.21  \                  evs : otway lost |] ==> A:lost";
    3.22 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    3.23 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    3.24  qed "Spy_see_shrK_D";
    3.25  
    3.26  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    3.27 @@ -125,7 +125,7 @@
    3.28                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    3.29                 unsafe_addss (!simpset)) 1);
    3.30  (*OR3*)
    3.31 -by (fast_tac (!claset addss (!simpset)) 1);
    3.32 +by (Blast_tac 1);
    3.33  qed_spec_mp "new_keys_not_used";
    3.34  
    3.35  bind_thm ("new_keys_not_analzd",
    3.36 @@ -148,7 +148,8 @@
    3.37  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    3.38  by (etac rev_mp 1);
    3.39  by (etac otway.induct 1);
    3.40 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.41 +by (ALLGOALS Asm_simp_tac);
    3.42 +by (Blast_tac 1);
    3.43  qed "Says_Server_message_form";
    3.44  
    3.45  
    3.46 @@ -187,7 +188,7 @@
    3.47  (*OR4, Fake*) 
    3.48  by (EVERY (map spy_analz_tac [3,2]));
    3.49  (*Base*)
    3.50 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    3.51 +by (Blast_tac 1);
    3.52  qed_spec_mp "analz_image_freshK";
    3.53  
    3.54  
    3.55 @@ -213,13 +214,12 @@
    3.56  by (Step_tac 1);
    3.57  (*Remaining cases: OR3 and OR4*)
    3.58  by (ex_strip_tac 2);
    3.59 -by (Fast_tac 2);
    3.60 +by (Blast_tac 2);
    3.61  by (expand_case_tac "K = ?y" 1);
    3.62  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    3.63  (*...we assume X is a recent message and handle this case by contradiction*)
    3.64 -by (fast_tac (!claset addSEs sees_Spy_partsEs
    3.65 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
    3.66 -                      addss (!simpset addsimps [parts_insertI])) 1);
    3.67 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    3.68 +                       delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
    3.69  val lemma = result();
    3.70  
    3.71  
    3.72 @@ -253,7 +253,7 @@
    3.73  by (parts_induct_tac 1);
    3.74  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    3.75  (*OR3*)
    3.76 -by (Fast_tac 1);
    3.77 +by (Blast_tac 1);
    3.78  qed_spec_mp "NA_Crypt_imp_Server_msg";
    3.79  
    3.80  
    3.81 @@ -267,7 +267,7 @@
    3.82  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    3.83  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    3.84  \                   : set_of_list evs";
    3.85 -by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    3.86 +by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    3.87                        addEs  sees_Spy_partsEs) 1);
    3.88  qed "A_trusts_OR4";
    3.89  
    3.90 @@ -292,12 +292,10 @@
    3.91                                        analz_insert_freshK]
    3.92                              setloop split_tac [expand_if])));
    3.93  (*OR3*)
    3.94 -by (fast_tac (!claset delrules [impCE]
    3.95 -                      addSEs sees_Spy_partsEs
    3.96 -                      addIs [impOfSubs analz_subset_parts]
    3.97 -                      addss (!simpset addsimps [parts_insert2])) 2);
    3.98 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    3.99 +                       addIs [impOfSubs analz_subset_parts]) 2);
   3.100  (*Oops*) 
   3.101 -by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
   3.102 +by (blast_tac (!claset addDs [unique_session_keys]) 3);
   3.103  (*OR4, Fake*) 
   3.104  by (REPEAT_FIRST spy_analz_tac);
   3.105  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   3.106 @@ -345,7 +343,7 @@
   3.107  by (parts_induct_tac 1);
   3.108  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   3.109  (*OR3*)
   3.110 -by (Fast_tac 1);
   3.111 +by (Blast_tac 1);
   3.112  qed_spec_mp "NB_Crypt_imp_Server_msg";
   3.113  
   3.114  
   3.115 @@ -359,6 +357,6 @@
   3.116  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   3.117  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   3.118  \                     : set_of_list evs";
   3.119 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   3.120 -                      addEs  sees_Spy_partsEs) 1);
   3.121 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   3.122 +                       addEs  sees_Spy_partsEs) 1);
   3.123  qed "B_trusts_OR3";
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon May 05 12:15:20 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon May 05 12:15:53 1997 +0200
     4.3 @@ -20,6 +20,7 @@
     4.4  proof_timing:=true;
     4.5  HOL_quantifiers := false;
     4.6  
     4.7 +(*No need to declare Says_imp_sees_Spy' because "lost" is a CONSTANT*)
     4.8  
     4.9  (*Weak liveness: there are traces that reach the end*)
    4.10  goal thy 
    4.11 @@ -48,17 +49,17 @@
    4.12  
    4.13  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    4.14  \                X : analz (sees lost Spy evs)";
    4.15 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    4.16 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    4.17  qed "OR2_analz_sees_Spy";
    4.18  
    4.19  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
    4.20  \                X : analz (sees lost Spy evs)";
    4.21 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    4.22 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    4.23  qed "OR4_analz_sees_Spy";
    4.24  
    4.25  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    4.26  \                 ==> K : parts (sees lost Spy evs)";
    4.27 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.28 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    4.29  qed "Oops_parts_sees_Spy";
    4.30  
    4.31  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    4.32 @@ -109,7 +110,7 @@
    4.33  
    4.34  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    4.35  \                  evs : otway |] ==> A:lost";
    4.36 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    4.37 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    4.38  qed "Spy_see_shrK_D";
    4.39  
    4.40  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    4.41 @@ -185,7 +186,7 @@
    4.42  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    4.43  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    4.44  (*Base*)
    4.45 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    4.46 +by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    4.47  (*Fake, OR2, OR4*) 
    4.48  by (REPEAT (spy_analz_tac 1));
    4.49  qed_spec_mp "analz_image_freshK";
    4.50 @@ -211,11 +212,11 @@
    4.51  by (Step_tac 1);
    4.52  (*Remaining cases: OR3 and OR4*)
    4.53  by (ex_strip_tac 2);
    4.54 -by (Fast_tac 2);
    4.55 +by (Blast_tac 2);
    4.56  by (expand_case_tac "K = ?y" 1);
    4.57  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    4.58  (*...we assume X is a recent message, and handle this case by contradiction*)
    4.59 -by (fast_tac (!claset addSEs sees_Spy_partsEs
    4.60 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    4.61                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
    4.62                        addss (!simpset addsimps [parts_insertI])) 1);
    4.63  val lemma = result();
    4.64 @@ -245,15 +246,13 @@
    4.65                              addsimps [not_parts_not_analz, analz_insert_freshK]
    4.66                              setloop split_tac [expand_if])));
    4.67  (*OR3*)
    4.68 -by (fast_tac (!claset delrules [impCE]
    4.69 +by (blast_tac (!claset delrules [impCE]
    4.70                        addSEs sees_Spy_partsEs
    4.71 -                      addIs [impOfSubs analz_subset_parts]
    4.72 -                      addss (!simpset addsimps [parts_insert2])) 3);
    4.73 +                      addIs [impOfSubs analz_subset_parts]) 3);
    4.74  (*OR4, OR2, Fake*) 
    4.75  by (REPEAT_FIRST spy_analz_tac);
    4.76  (*Oops*) (** LEVEL 5 **)
    4.77 -by (fast_tac (!claset delrules [disjE]
    4.78 -                      addDs [unique_session_keys] addss (!simpset)) 1);
    4.79 +by (blast_tac (!claset addSDs [unique_session_keys]) 1);
    4.80  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    4.81  
    4.82  goal thy 
    4.83 @@ -264,7 +263,7 @@
    4.84  \           A ~: lost;  B ~: lost;  evs : otway |]                \
    4.85  \        ==> Key K ~: analz (sees lost Spy evs)";
    4.86  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    4.87 -by (fast_tac (!claset addSEs [lemma]) 1);
    4.88 +by (blast_tac (!claset addSEs [lemma]) 1);
    4.89  qed "Spy_not_see_encrypted_key";
    4.90  
    4.91  
    4.92 @@ -282,7 +281,7 @@
    4.93  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    4.94  \             : set_of_list evs";
    4.95  by (parts_induct_tac 1);
    4.96 -by (Fast_tac 1);
    4.97 +by (Blast_tac 1);
    4.98  qed_spec_mp "Crypt_imp_OR1";
    4.99  
   4.100  
   4.101 @@ -303,14 +302,13 @@
   4.102  \                   : set_of_list evs)";
   4.103  by (parts_induct_tac 1);
   4.104  (*OR1: it cannot be a new Nonce, contradiction.*)
   4.105 -by (fast_tac (!claset addSIs [parts_insertI]
   4.106 -                      addSEs sees_Spy_partsEs
   4.107 -                      addss (!simpset)) 1);
   4.108 +by (blast_tac (!claset addSIs [parts_insertI]
   4.109 +                      addSEs sees_Spy_partsEs) 1);
   4.110  (*OR4*)
   4.111  by (REPEAT (Safe_step_tac 2));
   4.112 -by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   4.113 -by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   4.114 -                      addEs  sees_Spy_partsEs) 2);
   4.115 +by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   4.116 +by (blast_tac (!claset addSIs [Crypt_imp_OR1]
   4.117 +                       addEs  sees_Spy_partsEs) 2);
   4.118  (*OR3*)  (** LEVEL 5 **)
   4.119  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   4.120  by (step_tac (!claset delrules [disjCI, impCE]) 1);