Conversion to use blast_tac (with other improvements)
authorpaulson
Wed, 07 May 1997 13:01:43 +0200
changeset 3121 cbb6c0c1c58a
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
--- a/src/HOL/Auth/Message.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Wed May 07 13:01:43 1997 +0200
@@ -35,7 +35,7 @@
 
 goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
 by (Blast_tac 1);
-qed "keysFor_UN";
+qed "keysFor_UN1";
 
 (*Monotonicity*)
 goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
@@ -67,9 +67,11 @@
 by (Auto_tac());
 qed "keysFor_insert_Crypt";
 
-Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
+Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
           keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
           keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
+AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
+	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
 
 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
 by (Blast_tac 1);
@@ -173,8 +175,12 @@
 by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
 qed "parts_UN1";
 
-(*Added to simplify arguments to parts, analz and synth*)
+(*Added to simplify arguments to parts, analz and synth.
+  NOTE: the UN versions are no longer used!*)
 Addsimps [parts_Un, parts_UN, parts_UN1];
+AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
+	parts_UN RS equalityD1 RS subsetD RS UN_E,
+	parts_UN1 RS equalityD1 RS subsetD RS UN1_E];
 
 goal thy "insert X (parts H) <= parts(insert X H)";
 by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
@@ -809,6 +815,21 @@
 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
 val pushes = pushKeys@pushCrypts;
 
+
+(*** Tactics useful for many protocol proofs ***)
+
+(*Prove base case (subgoal i) and simplify others*)
+fun prove_simple_subgoals_tac i = 
+    fast_tac (!claset addss (!simpset)) i THEN
+    ALLGOALS Asm_simp_tac;
+
+fun Fake_parts_insert_tac i = 
+    blast_tac (!claset addDs [impOfSubs analz_subset_parts,
+			      impOfSubs Fake_parts_insert]) i;
+
+(*Apply rules to break down assumptions of the form
+  Y : parts(insert X H)  and  Y : analz(insert X H)
+*)
 val Fake_insert_tac = 
     dresolve_tac [impOfSubs Fake_analz_insert,
                   impOfSubs Fake_parts_insert] THEN'
--- a/src/HOL/Auth/NS_Public.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Wed May 07 13:01:43 1997 +0200
@@ -12,15 +12,12 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-val op addss = op unsafe_addss;
-
 AddIffs [Spy_in_lost];
 
 (*Replacing the variable by a constant improves search speed by 50%!*)
 val Says_imp_sees_Spy' = 
     read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
 
-
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
@@ -42,17 +39,6 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac ns_public.induct 1 THEN 
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
-
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
 
@@ -60,8 +46,9 @@
 goal thy 
  "!!evs. evs : ns_public \
 \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by (etac ns_public.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
@@ -74,7 +61,7 @@
 
 goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
 \                  evs : ns_public |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_priK]) 1);
+by (blast_tac (!claset addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
 
 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
@@ -82,7 +69,7 @@
 
 
 fun analz_induct_tac i = 
-    etac ns_public.induct i     THEN
+    etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
               (!simpset addsimps [not_parts_not_analz]
                         setloop split_tac [expand_if]));
@@ -100,16 +87,15 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (fast_tac (!claset addSEs partsEs) 4);
+by (blast_tac (!claset addSEs partsEs) 4);
 (*NS2*)
-by (fast_tac (!claset addSEs partsEs) 3);
+by (blast_tac (!claset addSEs partsEs) 3);
 (*Fake*)
-by (deepen_tac (!claset addSIs [analz_insertI]
+by (blast_tac (!claset addSIs [analz_insertI]
                         addDs [impOfSubs analz_subset_parts,
-			       impOfSubs Fake_parts_insert]
-			addss (!simpset)) 0 2);
+			       impOfSubs Fake_parts_insert]) 2);
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 qed "no_nonce_NS1_NS2";
 
 
@@ -124,17 +110,16 @@
 (*NS1*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
 by (expand_case_tac "NA = ?y" 3 THEN
-    REPEAT (fast_tac (!claset addSEs partsEs) 3));
+    REPEAT (blast_tac (!claset addSEs partsEs) 3));
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
                       addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
+                      addDs  [impOfSubs analz_subset_parts]) 1);
 val lemma = result();
 
 goal thy 
@@ -155,14 +140,14 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
+                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                        addSEs [MPair_parts]
-			addDs  [parts.Body, unique_NA]) 0 3);
+by (blast_tac (!claset addSEs [MPair_parts]
+		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
+			       parts.Body, unique_NA]) 3);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs sees_Spy_partsEs
                       addIs  [impOfSubs analz_subset_parts]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
@@ -184,15 +169,11 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addDs  [Spy_not_see_NA, 
+			       impOfSubs analz_subset_parts]) 1);
 qed "A_trusts_NS2";
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
@@ -205,13 +186,11 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*Fake*)
-by (best_tac (!claset addSIs [disjI2]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addIs  [analz_insertI]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addIs  [analz_insertI]
+                       addDs  [impOfSubs analz_subset_parts]) 2);
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 qed "B_trusts_NS1";
 
 
@@ -231,17 +210,16 @@
 (*NS2*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
 by (expand_case_tac "NB = ?y" 3 THEN
-    REPEAT (fast_tac (!claset addSEs partsEs) 3));
+    REPEAT (blast_tac (!claset addSEs partsEs) 3));
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
                       addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts] 
-                      addss (!simpset)) 1);
+                      addDs  [impOfSubs analz_subset_parts]) 1);
 val lemma = result();
 
 goal thy 
@@ -265,26 +243,21 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addDs  [unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+			      unique_NB]) 4);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*NS2*)
 by (Step_tac 1);
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
-by (fast_tac (!claset addIs  [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
+by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
 qed "Spy_not_see_NB";
 
 
-(*Matches only NS2, not NS1 (or NS3)*)
-val Says_imp_sees_Spy'' = 
-    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
-
-
 (*Authentication for B: if he receives message 3 and has used NB
   in message 2, then A has sent message 3.*)
 goal thy 
@@ -296,28 +269,27 @@
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK B) NB : parts H*)
 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
-by (etac ns_public.induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (analz_induct_tac 1);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts] 
-                      addss (!simpset)) 1);
-(*NS3*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addDs  [Spy_not_see_NB, 
+			       impOfSubs analz_subset_parts]) 1);
+(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
-                      addDs  [unique_NB]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+			      Spy_not_see_NB, unique_NB]) 1);
 qed "B_trusts_NS3";
 
 
 (**** Overall guarantee for B*)
 
+(*Matches only NS2, not NS1 (or NS3)*)
+val Says_imp_sees_Spy'' = 
+    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
+
+
 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
 goal thy 
@@ -333,19 +305,18 @@
 by (ALLGOALS Asm_simp_tac);
 (*Fake, NS2, NS3*)
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
 by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
+by (blast_tac (!claset addSIs [disjI2]
                       addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]
-                      addss (!simpset)) 1);
+                             impOfSubs Fake_parts_insert]) 1);
 (*NS3*)
 by (Step_tac 1);
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
-                      addDs  [unique_NB]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
+                       addDs  [unique_NB]) 1);
 qed "B_trusts_protocol";
 
--- a/src/HOL/Auth/NS_Public_Bad.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed May 07 13:01:43 1997 +0200
@@ -16,15 +16,12 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-val op addss = op unsafe_addss;
-
 AddIffs [Spy_in_lost];
 
 (*Replacing the variable by a constant improves search speed by 50%!*)
 val Says_imp_sees_Spy' = 
     read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
 
-
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
@@ -46,17 +43,6 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac ns_public.induct 1 THEN 
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
-
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
 
@@ -64,8 +50,9 @@
 goal thy 
  "!!evs. evs : ns_public \
 \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by (etac ns_public.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
@@ -78,7 +65,7 @@
 
 goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
 \                  evs : ns_public |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_priK]) 1);
+by (blast_tac (!claset addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
 
 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
@@ -86,7 +73,7 @@
 
 
 fun analz_induct_tac i = 
-    etac ns_public.induct i     THEN
+    etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
               (!simpset addsimps [not_parts_not_analz]
                         setloop split_tac [expand_if]));
@@ -105,16 +92,15 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (fast_tac (!claset addSEs partsEs) 4);
+by (blast_tac (!claset addSEs partsEs) 4);
 (*NS2*)
-by (fast_tac (!claset addSEs partsEs) 3);
+by (blast_tac (!claset addSEs partsEs) 3);
 (*Fake*)
-by (deepen_tac (!claset addSIs [analz_insertI]
+by (blast_tac (!claset addSIs [analz_insertI]
                         addDs [impOfSubs analz_subset_parts,
-			       impOfSubs Fake_parts_insert]
-			addss (!simpset)) 0 2);
+			       impOfSubs Fake_parts_insert]) 2);
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 qed "no_nonce_NS1_NS2";
 
 
@@ -129,17 +115,16 @@
 (*NS1*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
 by (expand_case_tac "NA = ?y" 3 THEN
-    REPEAT (fast_tac (!claset addSEs partsEs) 3));
+    REPEAT (blast_tac (!claset addSEs partsEs) 3));
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
                       addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
+                      addDs  [impOfSubs analz_subset_parts]) 1);
 val lemma = result();
 
 goal thy 
@@ -160,15 +145,15 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
+                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                        addSEs [MPair_parts]
-			addDs  [parts.Body, unique_NA]) 0 3);
+by (blast_tac (!claset addSEs [MPair_parts]
+		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
+			       parts.Body, unique_NA]) 3);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
-                      addIs  [impOfSubs analz_subset_parts]) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+                       addIs  [impOfSubs analz_subset_parts]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 qed "Spy_not_see_NA";
@@ -187,20 +172,15 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
-(*NS2*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addDs  [Spy_not_see_NA, 
+			       impOfSubs analz_subset_parts]) 1);
+(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                        addDs  [unique_NA]) 1 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+			      Spy_not_see_NA, unique_NA]) 1);
 qed "A_trusts_NS2";
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
@@ -213,14 +193,12 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*Fake*)
-by (best_tac (!claset addSIs [disjI2]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addIs  [analz_insertI]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addIs  [analz_insertI]
+                       addDs  [impOfSubs analz_subset_parts]) 2);
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
-qed_spec_mp "B_trusts_NS1";
+by (Blast_tac 1);
+qed "B_trusts_NS1";
 
 
 
@@ -238,17 +216,16 @@
 (*NS2*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
 by (expand_case_tac "NB = ?y" 3 THEN
-    REPEAT (fast_tac (!claset addSEs partsEs) 3));
+    REPEAT (blast_tac (!claset addSEs partsEs) 3));
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
                       addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts] 
-                      addss (!simpset)) 1);
+                      addDs  [impOfSubs analz_subset_parts]) 1);
 val lemma = result();
 
 goal thy 
@@ -271,22 +248,21 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*NS2 and NS3*)
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (step_tac (!claset delrules [allI]) 1);
-by (Fast_tac 5);
-by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 5);
+(*NS3*)
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+			      Spy_not_see_NB, unique_NB]) 4);
 (*NS2*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
-(*NS3*)
-by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
-    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
-by (Fast_tac 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
+by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
 qed "Spy_not_see_NB";
 
 
@@ -305,22 +281,15 @@
 by (analz_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (rtac (ccontr RS disjI2) 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
-    THEN Fast_tac 1);
-by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts] 
-                      addss (!simpset)) 1);
-(*NS3*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+                       addDs  [Spy_not_see_NB, 
+			       impOfSubs analz_subset_parts]) 1);
+(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
-    THEN Fast_tac 1);
-by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addDs  [unique_NB]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+			      Spy_not_see_NB, unique_NB]) 1);
 qed "B_trusts_NS3";
 
 
@@ -331,18 +300,18 @@
 \     --> Nonce NB ~: analz (sees lost Spy evs)";
 by (analz_induct_tac 1);
 (*NS1*)
-by (fast_tac (!claset addSEs partsEs
-                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+by (blast_tac (!claset addSEs partsEs
+                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*NS2 and NS3*)
 by (Step_tac 1);
-by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
+by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
 (*NS2*)
-by (fast_tac (!claset addSEs partsEs
-                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
+by (blast_tac (!claset addSEs partsEs
+                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
 (*NS3*)
 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
     THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
--- a/src/HOL/Auth/NS_Shared.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Wed May 07 13:01:43 1997 +0200
@@ -15,6 +15,9 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
+(*Replacing the variable by a constant improves search speed by 50%!*)
+val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
+
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
@@ -35,7 +38,7 @@
 by (rtac subsetI 1);
 by (etac ns_shared.induct 1);
 by (REPEAT_FIRST
-    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
                               :: ns_shared.intrs))));
 qed "ns_shared_mono";
 
@@ -51,29 +54,23 @@
 (*For reasoning about the encrypted portion of message NS3*)
 goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
 \                ==> X : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "NS3_msg_in_parts_sees_Spy";
                               
 goal thy
     "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
 \           ==> K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "Oops_parts_sees_Spy";
 
-val parts_Fake_tac = 
-    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
-    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_induct_tac = 
+    etac ns_shared.induct 1  THEN 
+    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
+    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
+    prove_simple_subgoals_tac 1;
 
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -83,8 +80,9 @@
 goal thy 
  "!!evs. evs : ns_shared lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -97,7 +95,7 @@
 
 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
 \                  evs : ns_shared lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -107,15 +105,15 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : ns_shared lost ==>      \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               unsafe_addss (!simpset)) 1);
+               addss (!simpset)) 1);
 (*NS2, NS4, NS5*)
-by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
+by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
 qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
@@ -152,7 +150,8 @@
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (Auto_tac());
 qed "A_trusts_NS2";
 
@@ -163,20 +162,19 @@
 goal thy 
  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
 \            : set_of_list evs;  evs : ns_shared lost |]                   \
-\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))  \
+\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \            | X : analz (sees lost Spy evs)";
 by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      unsafe_addss (!simpset)) 1);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
+                      addss (!simpset)) 1);
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
-by (fast_tac (!claset addEs  partsEs
-                      addSDs [A_trusts_NS2, Says_Server_message_form]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addEs  partsEs
+                      addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
 qed "Says_S_message_form";
 
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
     forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
@@ -200,15 +198,12 @@
  "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
 \        (Crypt KAB X) : parts (sees lost Spy evs) & \
 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
-by (etac ns_shared.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
+by parts_induct_tac;
 (*Deals with Faked messages*)
-by (best_tac (!claset addSEs partsEs
-                      addDs [impOfSubs parts_insert_subset_Un]
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSEs partsEs
+                       addDs [impOfSubs parts_insert_subset_Un]) 1);
 (*Base, NS4 and NS5*)
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (Auto_tac());
 result();
 
 
@@ -221,7 +216,7 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac ns_shared.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 (*Takes 24 secs*)
@@ -229,7 +224,7 @@
 (*NS4, Fake*) 
 by (EVERY (map spy_analz_tac [3,2]));
 (*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
@@ -253,13 +248,12 @@
 by (Step_tac 1);
 (*NS3*)
 by (ex_strip_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 (*NS2: it can't be a new key*)
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (fast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
-                      addSEs sees_Spy_partsEs
-                      addss (!simpset addsimps [parts_insertI])) 1);
+by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
+                      addSEs sees_Spy_partsEs) 1);
 val lemma = result();
 
 (*In messages of this form, the session key uniquely identifies the rest*)
@@ -286,7 +280,7 @@
 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
 \        Key K ~: analz (sees lost Spy evs)";
 by (etac ns_shared.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS 
     (asm_simp_tac 
      (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
@@ -294,17 +288,16 @@
 (*NS4, Fake*) 
 by (EVERY (map spy_analz_tac [4,1]));
 (*NS2*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
-                      addIs [parts_insertI, impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
 (*Oops*)
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
+by (blast_tac (!claset addDs [unique_session_keys]) 2);
 (*NS3*) (**LEVEL 6 **)
 by (step_tac (!claset delrules [impCE]) 1);
-by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
+by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
-by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 
@@ -316,7 +309,7 @@
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
 \        |] ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSDs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
@@ -330,7 +323,7 @@
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
 qed "Agent_not_see_encrypted_key";
 
 
@@ -349,13 +342,10 @@
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set_of_list evs";
 by (etac rev_mp 1);
-by (etac ns_shared.induct 1);
-by parts_Fake_tac;
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*Fake case*)
-by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]
-                      addss  (!simpset)) 2);
-by (Auto_tac());
+by (ALLGOALS Blast_tac);
 qed "B_trusts_NS3";
 
 
@@ -368,28 +358,28 @@
 \            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
-by parts_Fake_tac;
+by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
+by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
 by (TRYALL (rtac impI));
 by (REPEAT_FIRST
     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-(**LEVEL 6**)
-by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
-                      addDs [impOfSubs analz_subset_parts]) 1);
-by (Fast_tac 2);
+(**LEVEL 7**)
+by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
+                       addDs [impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 2);
 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
 (*Subgoal 1: contradiction from the assumptions  
   Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
 by (dtac Crypt_imp_invKey_keysFor 1);
-(**LEVEL 10**)
+(**LEVEL 11**)
 by (Asm_full_simp_tac 1);
 by (rtac disjI1 1);
 by (thin_tac "?PP-->?QQ" 1);
 by (case_tac "Ba : lost" 1);
-by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN 
-    REPEAT (assume_tac 1));
-by (best_tac (!claset addDs [unique_session_keys]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
+			      unique_session_keys]) 2);
+by (blast_tac (!claset addDs [Says_Crypt_lost]) 1);
 val lemma = result();
 
 goal thy
@@ -399,6 +389,6 @@
 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
 \        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
-                      addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
+by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
+                       addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
 qed "A_trusts_NS4";
--- a/src/HOL/Auth/OtwayRees.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Wed May 07 13:01:43 1997 +0200
@@ -18,8 +18,7 @@
 HOL_quantifiers := false;
 
 (*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = 
-    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
+val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
 
 
 (*A "possibility property": there are traces that reach the end*)
@@ -81,35 +80,30 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
-  harder to complete, since simplification does less for us.*)
-val parts_Fake_tac = 
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_induct_tac = 
     let val tac = forw_inst_tac [("lost","lost")] 
-    in  tac OR2_parts_sees_Spy     4 THEN 
+    in  etac otway.induct	   1 THEN 
+	tac OR2_parts_sees_Spy     4 THEN 
         tac OR4_parts_sees_Spy     6 THEN
-        tac Oops_parts_sees_Spy    7
+        tac Oops_parts_sees_Spy    7 THEN
+	prove_simple_subgoals_tac  1
     end;
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                            unsafe_addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
 
+
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
  "!!evs. evs : otway lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -132,7 +126,7 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : otway lost ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -167,7 +161,7 @@
 
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
@@ -194,7 +188,7 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -254,7 +248,8 @@
 \            Says A B {|NA, Agent A, Agent B,                      \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
 
@@ -265,7 +260,8 @@
 \ ==> EX B'. ALL B.    \
 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
 \        --> B = B'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR1: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "NA = ?y" 1);
@@ -290,7 +286,8 @@
 \             : parts (sees lost Spy evs) -->                    \
 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
 \             ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
                                addSDs  [impOfSubs parts_insert_subset_Un]) 1));
 qed_spec_mp"no_nonce_OR1_OR2";
@@ -309,7 +306,8 @@
 \                   Crypt (shrK A) {|NA, Key K|},                      \
 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
 \                   : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
 (*OR3 and OR4*) 
@@ -364,7 +362,7 @@
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
                             addsimps [not_parts_not_analz, analz_insert_freshK]
@@ -418,7 +416,8 @@
 \             {|NA, Agent A, Agent B, X,                       \
 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
 \             : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
 
@@ -430,7 +429,8 @@
 \ ==> EX NA' A'. ALL NA A.                               \
 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
 \      --> NA = NA' & A = A'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR2: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "NB = ?y" 1);
@@ -461,7 +461,8 @@
 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
 \                   : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
 (*OR4*)
--- a/src/HOL/Auth/OtwayRees_AN.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed May 07 13:01:43 1997 +0200
@@ -69,22 +69,17 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
-  harder to complete, since simplification does less for us.*)
-val parts_Fake_tac = 
-    forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_induct_tac = 
+    let val tac = forw_inst_tac [("lost","lost")] 
+    in  etac otway.induct	   1 THEN 
+        tac OR4_parts_sees_Spy     6 THEN
+        tac Oops_parts_sees_Spy    7 THEN
+	prove_simple_subgoals_tac  1
+    end;
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
@@ -93,8 +88,9 @@
 goal thy 
  "!!evs. evs : otway lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -117,7 +113,7 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : otway lost ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -154,7 +150,7 @@
 
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
     assume_tac 7 THEN
@@ -180,7 +176,7 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 (*14 seconds*)
@@ -250,7 +246,8 @@
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*OR3*)
 by (Blast_tac 1);
@@ -285,7 +282,7 @@
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
                             addsimps [not_parts_not_analz,
@@ -340,7 +337,8 @@
 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*OR3*)
 by (Blast_tac 1);
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed May 07 13:01:43 1997 +0200
@@ -20,9 +20,11 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-(*No need to declare Says_imp_sees_Spy' because "lost" is a CONSTANT*)
+(*Replacing the variable by a constant improves search speed by 50%!*)
+val Says_imp_sees_Spy' = 
+    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
 
-(*Weak liveness: there are traces that reach the end*)
+(*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX K. EX NA. EX evs: otway.          \
@@ -49,12 +51,12 @@
 
 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
 qed "OR2_analz_sees_Spy";
 
 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
@@ -72,21 +74,13 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-val parts_Fake_tac = 
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
+val parts_induct_tac = 
+    etac otway.induct 1 THEN 
     forward_tac [OR2_parts_sees_Spy] 4 THEN 
     forward_tac [OR4_parts_sees_Spy] 6 THEN
-    forward_tac [Oops_parts_sees_Spy] 7;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
+    forward_tac [Oops_parts_sees_Spy] 7 THEN
+    prove_simple_subgoals_tac 1;
 
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +90,9 @@
 goal thy 
  "!!evs. evs : otway \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -120,7 +115,7 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : otway ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -128,7 +123,7 @@
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
                unsafe_addss (!simpset)) 1);
 (*OR1-3*)
-by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
+by (ALLGOALS Blast_tac);
 qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
@@ -150,12 +145,13 @@
 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (prove_simple_subgoals_tac 1);
+by (Blast_tac 1); 
 qed "Says_Server_message_form";
 
 
 (*For proofs involving analz.*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     dtac OR2_analz_sees_Spy 4 THEN 
     dtac OR4_analz_sees_Spy 6 THEN
     forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
@@ -181,12 +177,12 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Base*)
-by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake, OR2, OR4*) 
 by (REPEAT (spy_analz_tac 1));
 qed_spec_mp "analz_image_freshK";
@@ -217,8 +213,7 @@
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message, and handle this case by contradiction*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
-                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
-                      addss (!simpset addsimps [parts_insertI])) 1);
+                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
 val lemma = result();
 
 goal thy 
@@ -240,7 +235,7 @@
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
                             addsimps [not_parts_not_analz, analz_insert_freshK]
@@ -280,7 +275,8 @@
 \            Says A B {|NA, Agent A, Agent B,                  \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
@@ -300,7 +296,8 @@
 \                   Crypt (shrK A) {|NA, Key K|},              \
 \                   Crypt (shrK B) {|NB, Key K|}|}             \
 \                   : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI]
                       addSEs sees_Spy_partsEs) 1);
--- a/src/HOL/Auth/Public.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Wed May 07 13:01:43 1997 +0200
@@ -80,7 +80,7 @@
 (*Added for Yahalom/lost_tac*)
 goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
 \              ==> X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
 qed "Crypt_Spy_analz_lost";
 
 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
@@ -120,8 +120,8 @@
 by (Step_tac 1);
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
-    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
-                       setloop split_tac [expand_if]))));
+    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
+				            setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
 goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
@@ -136,16 +136,14 @@
 goal thy  
  "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
 \        ==> X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "Says_Crypt_lost";
 
 goal thy  
  "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;        \
 \           X ~: analz (sees lost Spy evs) |]                     \
 \        ==> C ~: lost";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "Says_Crypt_not_lost";
 
 Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
--- a/src/HOL/Auth/ROOT.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/ROOT.ML	Wed May 07 13:01:43 1997 +0200
@@ -12,6 +12,9 @@
 proof_timing := true;
 goals_limit := 1;
 
+(*New version of addss isn't ready--too slow*)
+val op addss = op unsafe_addss;
+
 (*Shared-key protocols*)
 time_use_thy "NS_Shared";
 time_use_thy "OtwayRees";
--- a/src/HOL/Auth/Recur.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Wed May 07 13:01:43 1997 +0200
@@ -82,7 +82,7 @@
 by (rtac subsetI 1);
 by (etac recur.induct 1);
 by (REPEAT_FIRST
-    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
                               :: recur.intrs))));
 qed "recur_mono";
 
@@ -128,7 +128,7 @@
 
 goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
 \                ==> RA : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "RA4_analz_sees_Spy";
 
 (*RA2_analz... and RA4_analz... let us treat those cases using the same 
@@ -141,26 +141,19 @@
 bind_thm ("RA4_parts_sees_Spy",
           RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
-  harder to complete, since simplification does less for us.*)
-val parts_Fake_tac = 
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_induct_tac = 
     let val tac = forw_inst_tac [("lost","lost")] 
-    in  tac RA2_parts_sees_Spy 4              THEN
+    in  etac recur.induct      1	      THEN
+	tac RA2_parts_sees_Spy 4              THEN
         etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
         forward_tac [respond_imp_responses] 5 THEN
-        tac RA4_parts_sees_Spy 6
+        tac RA4_parts_sees_Spy 6	      THEN
+	prove_simple_subgoals_tac 1
     end;
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                            unsafe_addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
@@ -171,14 +164,14 @@
 goal thy 
  "!!evs. evs : recur lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
 (*RA3*)
-by (fast_tac (!claset addDs [Key_in_parts_respond]
-                      addss (!simpset addsimps [parts_insert_sees])) 2);
+by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
 (*RA2*)
-by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
-                      unsafe_addss (!simpset)) 1);
+by (blast_tac (!claset addSEs partsEs  addDs [parts_cut]) 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -191,7 +184,7 @@
 
 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
 \                  evs : recur lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -212,10 +205,10 @@
 
 goal thy "!!evs. evs : recur lost ==>          \
 \       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*RA3*)
 by (best_tac (!claset addDs  [Key_in_keysFor_parts]
-                      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
+	      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -236,7 +229,7 @@
 (*** Proofs involving analz ***)
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
     dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
     forward_tac [respond_imp_responses] 5                THEN
@@ -267,14 +260,14 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac recur.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS 
     (asm_simp_tac
      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
 (*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
 (*RA4, RA2, Fake*) 
 by (REPEAT (spy_analz_tac 1));
 val raw_analz_image_freshK = result();
@@ -304,17 +297,13 @@
 \                   evs : recur lost;  A ~: lost |]                       \
 \                ==> X : parts (sees lost Spy evs)";
 by (etac rev_mp 1);
-by (etac recur.induct 1);
-by parts_Fake_tac;
+by parts_induct_tac;
 (*RA3 requires a further induction*)
-by (etac responses.induct 5);
+by (etac responses.induct 2);
 by (ALLGOALS Asm_simp_tac);
 (*Fake*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]
-                      addss (!simpset addsimps [parts_insert_sees])) 2);
-(*Two others*)
-by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
+by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
+by (Fake_parts_insert_tac 1);
 qed "Hash_imp_body";
 
 
@@ -329,14 +318,15 @@
 \ ==> EX B' P'. ALL B P.                                     \
 \        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
 \          -->  B=B' & P=P'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (etac responses.induct 3);
 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
 by (step_tac (!claset addSEs partsEs) 1);
 (*RA1,2: creation of new Nonce.  Move assertion into global context*)
 by (ALLGOALS (expand_case_tac "NA = ?y"));
 by (REPEAT_FIRST (ares_tac [exI]));
-by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
+by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
                               addSEs sees_Spy_partsEs) 1));
 val lemma = result();
 
@@ -379,7 +369,7 @@
      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
 (*Simplification using two distinct treatments of "image"*)
 by (simp_tac (!simpset addsimps [parts_insert2]) 1);
-by (fast_tac (!claset delrules [allE]) 1);
+by (blast_tac (!claset delrules [allE]) 1);
 qed "resp_analz_insert_lemma";
 
 bind_thm ("resp_analz_insert",
@@ -417,11 +407,11 @@
 by (etac respond.induct 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
 (*Base case*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (Step_tac 1);
 by (expand_case_tac "K = KBC" 1);
 by (dtac respond_Key_in_parts 1);
-by (best_tac (!claset addSIs [exI]
+by (blast_tac (!claset addSIs [exI]
                       addSEs partsEs
                       addDs [Key_in_parts_respond]) 1);
 by (expand_case_tac "K = KAB" 1);
@@ -457,19 +447,18 @@
      (analz_image_freshK_ss addsimps 
        [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
 by (ALLGOALS Simp_tac);
-by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
 by (step_tac (!claset addSEs [MPair_parts]) 1);
 (** LEVEL 7 **)
-by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
+by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
                       addDs  [impOfSubs analz_subset_parts]) 4);
-by (fast_tac (!claset addSDs [respond_certificate]) 3);
-by (best_tac (!claset addSEs partsEs
-                      addDs [Key_in_parts_respond]
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [respond_certificate]) 3);
+by (blast_tac (!claset addSEs partsEs
+                       addDs [Key_in_parts_respond]) 2);
 by (dtac unique_session_keys 1);
 by (etac respond_certificate 1);
 by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "respond_Spy_not_see_session_key";
 
 
@@ -480,7 +469,7 @@
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (etac rev_mp 1);
 by (etac recur.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac
      (!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
@@ -492,17 +481,16 @@
 (*Fake*)
 by (spy_analz_tac 2);
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*RA3 remains*)
 by (step_tac (!claset delrules [impCE]) 1);
 (*RA3, case 2: K is an old key*)
-by (best_tac (!claset addSDs [resp_analz_insert]
-                      addSEs partsEs
-                      addDs [Key_in_parts_respond]
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [resp_analz_insert]
+                       addSEs partsEs
+                       addDs [Key_in_parts_respond]) 2);
 (*RA3, case 1: use lemma previously proved by induction*)
-by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
-                              (2,rev_notE)]) 1);
+by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
+			       (2,rev_notE)]) 1);
 qed "Spy_not_see_session_key";
 
 
@@ -516,8 +504,8 @@
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_session_key));
 by (REPEAT_FIRST
-    (deepen_tac
-     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])) 0));
+    (blast_tac
+     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
 qed "Agent_not_see_session_key";
 
 
@@ -544,9 +532,10 @@
 \        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
 \             : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*RA3*)
-by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
+by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
 qed_spec_mp "Hash_auth_sender";
 
 (** These two results subsume (for all agents) the guarantees proved
@@ -561,18 +550,15 @@
 \        ==> EX C RC. Says Server C RC : set_of_list evs &   \
 \                     Crypt (shrK A) Y : parts {RC}";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*RA4*)
-by (Fast_tac 4);
+by (Blast_tac 4);
 (*RA3*)
 by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
-    THEN Fast_tac 3);
+    THEN Blast_tac 3);
 (*RA1*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 (*RA2: it cannot be a new Nonce, contradiction.*)
-by (deepen_tac (!claset delrules [impCE]
-                      addSIs [disjI2]
-                      addSEs [MPair_parts]
-                      addDs  [parts.Body]
-                      unsafe_addss  (!simpset)) 0 1);
+by (Blast_tac 1);
 qed "Cert_imp_Server_msg";
--- a/src/HOL/Auth/Shared.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Wed May 07 13:01:43 1997 +0200
@@ -56,7 +56,7 @@
 
 goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
 by (agent.induct_tac "C" 1);
-by (auto_tac (!claset addIs [range_eqI], !simpset));
+by (Auto_tac ());
 qed "keysFor_parts_initState";
 Addsimps [keysFor_parts_initState];
 
@@ -210,14 +210,14 @@
 (** Fresh keys never clash with long-term shared keys **)
 
 goal thy "Key (shrK A) : used evs";
-by (Best_tac 1);
+by (Blast_tac 1);
 qed "shrK_in_used";
 AddIffs [shrK_in_used];
 
-(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
+(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   from long-term shared keys*)
 goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
-by (Best_tac 1);
+by (Blast_tac 1);
 qed "Key_not_used";
 
 (*A session key cannot clash with a long-term shared key*)
@@ -237,7 +237,7 @@
 by (list.induct_tac "l" 1);
 by (event.induct_tac "a" 2);
 by (ALLGOALS Asm_simp_tac);
-by (Best_tac 1);
+by (Blast_tac 1);
 qed "used_nil_subset";
 
 goal thy "used l <= used (l@l')";
@@ -245,7 +245,7 @@
 by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
 by (event.induct_tac "a" 1);
 by (Asm_simp_tac 1);
-by (Best_tac 1);
+by (Blast_tac 1);
 qed "used_subset_append";
 
 
@@ -372,8 +372,8 @@
 goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
 by (list.induct_tac "evs" 1);
 by (event.induct_tac "a" 2);
-by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
-                                addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
 qed "sees_agent_subset_sees_Spy";
 
 (*The Spy can see more than anybody else who's lost their key!*)
@@ -381,7 +381,8 @@
 by (list.induct_tac "evs" 1);
 by (event.induct_tac "a" 2);
 by (agent.induct_tac "A" 1);
-by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
 qed_spec_mp "sees_lost_agent_subset_sees_Spy";
 
 
--- a/src/HOL/Auth/WooLam.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML	Wed May 07 13:01:43 1997 +0200
@@ -28,8 +28,7 @@
           woolam.WL4 RS woolam.WL5) 2);
 by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
-                                    addss (!simpset setSolver safe_solver))));
+by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE])));
 result();
 
 
@@ -54,18 +53,12 @@
 bind_thm ("WL4_parts_sees_Spy",
           WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
+val parts_induct_tac = 
+    etac woolam.induct 1  THEN 
+    forward_tac [WL4_parts_sees_Spy] 6  THEN
+    prove_simple_subgoals_tac  1;
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
@@ -74,8 +67,8 @@
 goal thy 
  "!!evs. evs : woolam \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -88,7 +81,7 @@
 
 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
 \                  evs : woolam |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -105,8 +98,9 @@
  "!!evs. [| A ~: lost;  evs : woolam |]                   \
 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
 \        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
-by (parts_induct_tac 1);
-by (Fast_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "NB_Crypt_imp_Alice_msg";
 
 (*Guarantee for Server: if it gets a message containing a certificate from 
@@ -117,7 +111,7 @@
 \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
 \            : set_of_list evs |]                                  \
 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
+by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
                       addSEs [MPair_parts]
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "Server_trusts_WL4";
@@ -131,8 +125,9 @@
 \        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
 \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
 \               : set_of_list evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Fast_tac);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS Blast_tac);
 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
 
 
@@ -141,7 +136,8 @@
  "!!evs. [| B ~: lost;  evs : woolam |]                   \
 \    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
 \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 qed_spec_mp "NB_Crypt_imp_Server_msg";
 
 (*Partial guarantee for B: if it gets a message of correct form then the Server
@@ -150,7 +146,7 @@
  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
 \           B ~: lost;  evs : woolam |]                                  \
 \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
-by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
+by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "B_got_WL5";
 
@@ -162,7 +158,7 @@
  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
 \           A ~: lost;  B ~: lost;  evs : woolam  |] \
 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addIs  [Server_trusts_WL4]
+by (blast_tac (!claset addIs  [Server_trusts_WL4]
                       addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
 qed "B_trusts_WL5";
 
@@ -172,8 +168,9 @@
  "!!evs. [| B ~= Spy;  evs : woolam |]                   \
 \    ==> Says B A (Nonce NB) : set_of_list evs        \
 \        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Fast_tac);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS Blast_tac);
 bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
 
 
@@ -183,7 +180,8 @@
 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
 \        Says B A (Nonce NB) : set_of_list evs        \
 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 by (Step_tac 1);
-by (best_tac (!claset addSEs partsEs) 1);
+by (blast_tac (!claset addSEs partsEs) 1);
 **)
--- a/src/HOL/Auth/Yahalom.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed May 07 13:01:43 1997 +0200
@@ -16,7 +16,8 @@
 HOL_quantifiers := false;
 Pretty.setdepth 25;
 
-val op addss = op unsafe_addss;
+(*Replacing the variable by a constant improves speed*)
+val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
 
 
 (*A "possibility property": there are traces that reach the end*)
@@ -38,7 +39,7 @@
 by (rtac subsetI 1);
 by (etac yahalom.induct 1);
 by (REPEAT_FIRST
-    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
                               :: yahalom.intrs))));
 qed "yahalom_mono";
 
@@ -57,7 +58,7 @@
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
 
 bind_thm ("YM4_parts_sees_Spy",
@@ -67,26 +68,20 @@
 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
 \                  : set_of_list evs ==> \
 \                K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
-                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (blast_tac (!claset addSEs partsEs
+                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
 qed "YM4_Key_parts_sees_Spy";
 
-(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
-  harder: the simplifier does less.*)
-val parts_Fake_tac = 
-    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_sees_tac = 
+    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
+    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
+    prove_simple_subgoals_tac  1;
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
+val parts_induct_tac = 
+    etac yahalom.induct 1 THEN parts_sees_tac;
 
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +91,9 @@
 goal thy 
  "!!evs. evs : yahalom lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -110,7 +106,7 @@
 
 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
 \                  evs : yahalom lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -120,11 +116,11 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : yahalom lost ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*YM4: Key K is not fresh!*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
 (*YM3*)
-by (fast_tac (!claset addss (!simpset)) 2);
+by (Blast_tac 2);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -149,12 +145,13 @@
 \        ==> K ~: range shrK";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
 qed "Says_Server_message_form";
 
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
     assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
@@ -177,12 +174,12 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
 (*YM4, Fake*) 
 by (REPEAT (spy_analz_tac 1));
 qed_spec_mp "analz_image_freshK";
@@ -207,14 +204,13 @@
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (Step_tac 1);
 by (ex_strip_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 (*Remaining case: YM3*)
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
-                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
-                      addss (!simpset addsimps [parts_insertI])) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
 val lemma = result();
 
 goal thy 
@@ -240,7 +236,8 @@
 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
 \             : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 qed "A_trusts_YM3";
 
 
@@ -255,22 +252,19 @@
 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
      (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*YM3*)
-by (fast_tac (!claset delrules [impCE]
-                      addSEs sees_Spy_partsEs
-                      addIs [impOfSubs analz_subset_parts]
-                      addss (!simpset addsimps [parts_insert2])) 2);
+by (blast_tac (!claset delrules [impCE]
+                       addSEs sees_Spy_partsEs
+                       addIs [impOfSubs analz_subset_parts]) 2);
 (*OR4, Fake*) 
 by (REPEAT_FIRST spy_analz_tac);
 (*Oops*)
-by (fast_tac (!claset delrules [disjE] 
-                      addDs [unique_session_keys]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 
@@ -284,7 +278,7 @@
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
@@ -300,7 +294,7 @@
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
 qed "Agent_not_see_encrypted_key";
 
 
@@ -317,9 +311,10 @@
 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*YM3*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "B_trusts_YM4_shrK";
 
 
@@ -330,19 +325,15 @@
 \   EX NA' A' B'. ALL NA A B. \
 \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by (etac yahalom.induct 1 THEN parts_Fake_tac);
-(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
-by (REPEAT (etac exE 2) THEN 
-    best_tac (!claset addSIs [exI]
-                      addDs [impOfSubs Fake_parts_insert]
-                      addss (!simpset)) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
+by parts_induct_tac;
+(*Fake*)
+by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
+    THEN Fake_parts_insert_tac 1);
+by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*YM2: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "NB = ?y" 1);
 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 val lemma = result();
 
 goal thy 
@@ -358,7 +349,7 @@
 fun lost_tac s =
     case_tac ("(" ^ s ^ ") : lost") THEN'
     SELECT_GOAL 
-      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+      (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN
        REPEAT_DETERM (etac MPair_analz 1) THEN
        THEN_BEST_FIRST 
          (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
@@ -376,31 +367,34 @@
 \          evs : yahalom lost |]  \
 \        ==> NA' = NA & A' = A & B' = B";
 by (lost_tac "B'" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
-                      addSEs [MPair_parts]
-                      addDs  [unique_NB]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addSEs [MPair_parts]
+                       addDs  [unique_NB]) 1);
 qed "Says_unique_NB";
 
+(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
+  It simplifies the proof by discarding needless information about
+	analz (insert X (sees lost Spy evs)) 
+*)
+val analz_mono_parts_induct_tac = 
+    etac yahalom.induct 1 
+    THEN 
+    REPEAT_FIRST  
+      (rtac impI THEN' 
+       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
+       mp_tac)  
+    THEN  parts_sees_tac;
+
 goal thy 
  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
-\ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
-\      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
-\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (REPEAT_FIRST 
-    (rtac impI THEN' 
-     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
-     mp_tac));
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]
-                      addss (!simpset)) 2);
-by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addss (!simpset)) 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
-                      addSIs [parts_insertI]
-                      addSEs partsEs
-                      addss (!simpset)) 1);
+\ ==> Nonce NB ~: analz (sees lost Spy evs) -->  \
+\     Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
+\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
+by analz_mono_parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
+                       addSIs [parts_insertI]
+                       addSEs partsEs) 1);
 val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
 
 
@@ -419,23 +413,15 @@
 \                                  Nonce NA, Nonce NB|},                \
 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (REPEAT_FIRST
-    (rtac impI THEN'
-     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
-by (ALLGOALS Asm_simp_tac);
-(*Fake, YM3, YM4*)
-by (Fast_tac 2);
-by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
-                      addDs [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
-(*YM4*)
+by analz_mono_parts_induct_tac;
+(*YM4 & Fake*)
+by (Blast_tac 2);
+by (Fake_parts_insert_tac 1);
+(*YM3*)
 by (Step_tac 1);
 by (lost_tac "A" 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
-                             A_trusts_YM3]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
+			      A_trusts_YM3]) 1);
 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
 
 
@@ -448,26 +434,19 @@
 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
 \            (EX A B NA. Says Server A                                  \
-\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
-\                                  Nonce NA, Nonce NB|},       \
+\                        {|Crypt (shrK A) {|Agent B, Key K,             \
+\                                  Nonce NA, Nonce NB|},                \
 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (TRYALL (rtac impI));
-by (REPEAT_FIRST
-    (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
-by (ALLGOALS Asm_simp_tac);
-(*Fake, YM3, YM4*)
-by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]) 1);
-by (Fast_tac 1);
-(*YM4*)
+by analz_mono_parts_induct_tac;
+(*YM4 & Fake*)
+by (Blast_tac 2);
+by (Fake_parts_insert_tac 1);
+(*YM3*)
 by (Step_tac 1);
 by (lost_tac "A" 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
-                             A_trusts_YM3]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
+			      A_trusts_YM3]) 1);
 result() RS mp RSN (2, rev_mp);
 
 
@@ -482,7 +461,7 @@
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "Says_Server_imp_YM2";
 
 
@@ -491,9 +470,9 @@
 val no_nonce_tac = SELECT_GOAL
    (REPEAT (resolve_tac [impI, notI] 1) THEN
     REPEAT (hyp_subst_tac 1) THEN
-    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
+    etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
     THEN
-    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
+    etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd) 4
     THEN 
     REPEAT_FIRST assume_tac);
 
@@ -509,30 +488,30 @@
 goal thy  
  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
 \        P --> (X : analz (G Un H)) = (X : analz H)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
 qed "Nonce_secrecy_lemma";
 
 goal thy 
- "!!evs. evs : yahalom lost ==>                                          \
+ "!!evs. evs : yahalom lost ==>                                              \
 \        (ALL KK. KK <= Compl (range shrK) -->                               \
-\             (ALL K: KK. ALL A B na X.                                       \
+\             (ALL K: KK. ALL A B na X.                                      \
 \                 Says Server A                                              \
 \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
-\                 ~: set_of_list evs)   -->  \
-\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =      \
+\                 ~: set_of_list evs)   -->                                  \
+\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =          \
 \             (Nonce NB : analz (sees lost Spy evs)))";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
 by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
 by (rtac ccontr 7);
-by (subgoal_tac "ALL A B na X.                                       \
+by (subgoal_tac "ALL A B na X.                                               \
 \                 Says Server A                                              \
 \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
 \                 ~: set_of_list evsa" 7);
 by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
-by (subgoal_tac "ALL A B na X.                                       \
-\                 Says Server A                                              \
+by (subgoal_tac "ALL A B na X.                                                \
+\                 Says Server A                                               \
 \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
 \                 ~: set_of_list evsa" 5);
 by (ALLGOALS  (*22 seconds*)
@@ -542,15 +521,14 @@
                not_parts_not_analz, analz_image_freshK]
               @ pushes @ ball_simps))));
 (*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
 (*Fake*) (** LEVEL 10 **)
 by (spy_analz_tac 1);
 (*YM3*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 (*Oops*)
-(*20 secs*)
-by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
-                      addss (!simpset)) 2);
+by (Asm_full_simp_tac 2); 
+by (blast_tac (!claset addDs [unique_session_keys]) 2);
 (*YM4*)
 (** LEVEL 13 **)
 by (REPEAT (resolve_tac [impI, allI] 1));
@@ -562,10 +540,10 @@
 by (step_tac (!claset addSDs [not_analz_insert]) 1);
 by (lost_tac "A" 1);
 (** LEVEL 20 **)
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
+by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
     THEN REPEAT (assume_tac 1));
 by (thin_tac "All ?PP" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "Nonce_secrecy";
 
 
@@ -581,8 +559,8 @@
 \           KAB ~: range shrK;  evs : yahalom lost |]                  \
 \        ==>  NB = NB'";
 by (rtac ccontr 1);
-by (subgoal_tac "ALL A B na X.                                       \
-\                 Says Server A                                              \
+by (subgoal_tac "ALL A B na X.                                                \
+\                 Says Server A                                               \
 \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
 \                 ~: set_of_list evs" 1);
 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
@@ -592,6 +570,8 @@
 qed "single_Nonce_secrecy";
 
 
+val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
+
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
 \ ==> Says B Server                                                    \
@@ -600,55 +580,53 @@
 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
 \     Nonce NB ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
      (!simpset addsimps ([not_parts_not_analz,
                           analz_insert_freshK] @ pushes)
                setloop split_tac [expand_if])));
-by (fast_tac (!claset addSIs [parts_insertI]
-                      addSEs sees_Spy_partsEs
-                      addss (!simpset)) 2);
+by (blast_tac (!claset addSIs [parts_insertI]
+                       addSEs sees_Spy_partsEs) 2);
 (*Proof of YM2*) (** LEVEL 4 **)
-by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
-                               impOfSubs analz_subset_parts]
-                        addSEs partsEs) 3 2);
+by (blast_tac (!claset addSEs partsEs
+		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
+			       impOfSubs analz_subset_parts]) 2);
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
-by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
+by (blast_tac (!claset addDs [Says_unique_NB']) 2 THEN flexflex_tac);
 (*Fake*)
 by (spy_analz_tac 1);
 (*YM4*) (** LEVEL 8 **)
 by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-(*43 secs??*)
+(*  SLOW: 13s*)
 by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
 by (lost_tac "Aa" 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
+by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
 by (forward_tac [Says_Server_message_form] 3);
 by (forward_tac [Says_Server_imp_YM2] 4);
-(** LEVEL 15 **)
-by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
+by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
+(** LEVEL 16 **)
+(*  use unique_NB to identify message components  *)
 by (lost_tac "Ba" 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
-                      addSEs [MPair_parts]) 1);
-by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
+by (subgoal_tac "Aa=A & Ba=B & NAa=NA" 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addSEs [MPair_parts] addDs [unique_NB]) 2);
+by (blast_tac (!claset addDs [Spy_not_see_encrypted_key,
+			      impOfSubs Fake_analz_insert]
+		       addIs [impOfSubs analz_mono]) 1);
 (** LEVEL 20 **)
-by (dtac Spy_not_see_encrypted_key 1);
-by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
-by (spy_analz_tac 1);
-(*Oops case*) (** LEVEL 23 **)
+(*Oops case*)
 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
 by (step_tac (!claset delrules [disjE, conjI]) 1);
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
 by (expand_case_tac "NB = NBa" 1);
-by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
+by (blast_tac (!claset addDs [Says_unique_NB']) 1);
 by (rtac conjI 1);
 by (no_nonce_tac 1);
 (** LEVEL 30 **)
-by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
-by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
+by (blast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
 val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
 
 
@@ -671,11 +649,11 @@
 \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
 \                   : set_of_list evs";
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
+by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
     dtac B_trusts_YM4_shrK 1);
 by (dtac B_trusts_YM4_newK 3);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
-by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
+by (blast_tac (!claset addDs [Says_unique_NB']) 1);
 qed "B_trusts_YM4";
--- a/src/HOL/Auth/Yahalom2.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Wed May 07 13:01:43 1997 +0200
@@ -17,8 +17,6 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-val op addss = op unsafe_addss;
-
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
@@ -38,7 +36,7 @@
 by (rtac subsetI 1);
 by (etac yahalom.induct 1);
 by (REPEAT_FIRST
-    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
                               :: yahalom.intrs))));
 qed "yahalom_mono";
 
@@ -57,7 +55,7 @@
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
 
 bind_thm ("YM4_parts_sees_Spy",
@@ -67,26 +65,18 @@
 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
 \                  : set_of_list evs ==> \
 \                K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
+by (blast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "YM4_Key_parts_sees_Spy";
 
-(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
-  harder: the simplifier does less.*)
-val parts_Fake_tac = 
-    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
-    (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
-             (*Fake message*)
-             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                                           impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
-     (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
-     ALLGOALS Asm_simp_tac) i;
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
+  We instantiate the variable to "lost" since leaving it as a Var would
+  interfere with simplification.*)
+val parts_induct_tac = 
+    etac yahalom.induct 1 THEN 
+    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
+    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
+    prove_simple_subgoals_tac  1;
 
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +86,9 @@
 goal thy 
  "!!evs. evs : yahalom lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -110,7 +101,7 @@
 
 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
 \                  evs : yahalom lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -120,11 +111,11 @@
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : yahalom lost ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
 (*YM4: Key K is not fresh!*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
 (*YM3*)
-by (fast_tac (!claset addss (!simpset)) 2);
+by (blast_tac (!claset addss (!simpset)) 2);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -149,12 +140,12 @@
 \        ==> K ~: range shrK & A ~= B";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
 qed "Says_Server_message_form";
 
 
 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
-val analz_Fake_tac = 
+val analz_sees_tac = 
     dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
     assume_tac 7 THEN
@@ -179,12 +170,12 @@
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
 (*YM4, Fake*) 
 by (REPEAT (spy_analz_tac 1));
 qed_spec_mp "analz_image_freshK";
@@ -212,7 +203,7 @@
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs sees_Spy_partsEs
                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
                       addss (!simpset addsimps [parts_insertI])) 1);
 val lemma = result();
@@ -234,30 +225,28 @@
 
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
-\           evs : yahalom lost |]            \
+\           evs : yahalom lost |]                                    \
 \        ==> Says Server A                                           \
-\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},           \
-\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}          \
-\             : set_of_list evs -->                               \
-\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
+\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},          \
+\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}         \
+\             : set_of_list evs -->                                  \
+\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->     \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
      (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*YM3*)
-by (fast_tac (!claset delrules [impCE]
+by (blast_tac (!claset delrules [impCE]
                       addSEs sees_Spy_partsEs
                       addIs [impOfSubs analz_subset_parts]
                       addss (!simpset addsimps [parts_insert2])) 2);
 (*OR4, Fake*) 
 by (REPEAT_FIRST spy_analz_tac);
 (*Oops*)
-by (fast_tac (!claset delrules [disjE] 
-                      addDs [unique_session_keys]
-                      addss (!simpset)) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 
@@ -271,7 +260,7 @@
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
@@ -287,7 +276,7 @@
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
 qed "Agent_not_see_encrypted_key";
 
 
@@ -303,9 +292,9 @@
 \                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
 \                    : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*The nested conjunctions are entirely useless*)
-by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 qed "A_trusts_YM3";
 
 
@@ -321,9 +310,10 @@
 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
 \                       : set_of_list evs";
 by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
 (*YM3*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "B_trusts_YM4_shrK";
 
 (*With this variant we don't bother to use the 2nd part of YM4 at all, since
@@ -342,5 +332,5 @@
 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
 \                   : set_of_list evs";
 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
-by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
+by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
 qed "B_trusts_YM4";