# HG changeset patch
# User paulson
# Date 875526421 -7200
# Node ID 6933d20f335f8b5484d125edff58e46b22833887
# Parent  6be7cf5086abe3391a936ceb47b5d0d6937c07fa
Step_tac -> Safe_tac

diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -28,7 +28,7 @@
 (** Inverse of keys **)
 
 goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
-by (Step_tac 1);
+by Safe_tac;
 by (rtac box_equals 1);
 by (REPEAT (rtac invKey 2));
 by (Asm_simp_tac 1);
@@ -135,7 +135,7 @@
 val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
 
 goal thy "parts{} = {}";
-by (Step_tac 1);
+by Safe_tac;
 by (etac parts.induct 1);
 by (ALLGOALS Blast_tac);
 qed "parts_empty";
@@ -373,7 +373,7 @@
 (** General equational properties **)
 
 goal thy "analz{} = {}";
-by (Step_tac 1);
+by Safe_tac;
 by (etac analz.induct 1);
 by (ALLGOALS Blast_tac);
 qed "analz_empty";
@@ -554,7 +554,7 @@
 (*If there are no pairs or encryptions then analz does nothing*)
 goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
 \         analz H = H";
-by (Step_tac 1);
+by Safe_tac;
 by (etac analz.induct 1);
 by (ALLGOALS Blast_tac);
 qed "analz_trivial";
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -230,7 +230,7 @@
 \       -->         A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by Safe_tac;
 (*NS3*)
 by (ex_strip_tac 2);
 by (Blast_tac 2);
@@ -278,7 +278,7 @@
 (*Fake*) 
 by (spy_analz_tac 1);
 (*NS3, Server sub-case*) (**LEVEL 6 **)
-by (step_tac (!claset delrules [impCE]) 1);
+by (clarify_tac (!claset delrules [impCE]) 1);
 by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
 by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -196,7 +196,7 @@
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
 by (Best_tac 2);
@@ -286,22 +286,21 @@
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
-(*OR3 and OR4*) 
-(*OR4*)
-by (REPEAT (Safe_step_tac 2));
-by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
-by (blast_tac (!claset addSIs [Crypt_imp_OR1]
-                       addEs  spies_partsEs) 2);
-(*OR3*)  (** LEVEL 5 **)
+(*OR3 and OR4*)
 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
+by (rtac conjI 1);
+by (ALLGOALS Clarify_tac);
+(*OR4*)
+by (blast_tac (!claset addSIs [Crypt_imp_OR1]
+                       addEs  spies_partsEs) 3);
+(*OR3, two cases*)  (** LEVEL 5 **)
 by (blast_tac (!claset addSEs [MPair_parts]
-                      addSDs [Says_imp_spies RS parts.Inj]
-                      addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
-                      delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
+                       addSDs [Says_imp_spies RS parts.Inj]
+                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
+                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
-                      addSEs [MPair_parts]
-                      addIs  [unique_NA]) 1);
+                       addSEs [MPair_parts]
+                       addIs  [unique_NA]) 1);
 qed_spec_mp "NA_Crypt_imp_Server_msg";
 
 
@@ -426,7 +425,7 @@
 (*OR4*)
 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
 (*OR3*)
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
+by (safe_tac (!claset delrules [disjCI, impCE]));
 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
                        addSEs [MPair_parts]
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -190,7 +190,7 @@
 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
 by (Blast_tac 2);
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -199,7 +199,7 @@
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
 by (Blast_tac 2);
@@ -290,26 +290,25 @@
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI]
-                      addSEs spies_partsEs) 1);
+                       addSEs spies_partsEs) 1);
+(*OR3 and OR4*)
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
+by (ALLGOALS Clarify_tac);
 (*OR4*)
-by (REPEAT (Safe_step_tac 2));
-by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
 by (blast_tac (!claset addSIs [Crypt_imp_OR1]
                        addEs  spies_partsEs) 2);
 (*OR3*)  (** LEVEL 5 **)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
-(*The hypotheses at this point suggest an attack in which nonce NA is used
+(*The hypotheses at this point suggest an attack in which nonce NB is used
   in two different roles:
           Says B' Server
-           {|Nonce NAa, Agent Aa, Agent A,
-             Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
-             Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
-          : set evsa;
+           {|Nonce NA, Agent Aa, Agent A,
+             Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
+             Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
+          : set evs3;
           Says A B
-           {|Nonce NA, Agent A, Agent B,
-             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
-          : set evsa 
+           {|Nonce NB, Agent A, Agent B,
+             Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
+          : set evs3;
 *)
 writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
 
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -16,7 +16,7 @@
 AddIffs [inj_pubK RS inj_eq];
 
 goal thy "!!A B. (priK A = priK B) = (A=B)";
-by (Step_tac 1);
+by Safe_tac;
 by (dres_inst_tac [("f","invKey")] arg_cong 1);
 by (Full_simp_tac 1);
 qed "priK_inj_eq";
@@ -89,7 +89,7 @@
        THEN_BEST_FIRST 
          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
          (has_fewer_prems 1, size_of_thm)
-         (Step_tac 1));
+         Safe_tac);
 
 
 (*** Fresh nonces ***)
@@ -115,7 +115,7 @@
 by (ALLGOALS (asm_simp_tac
 	      (!simpset addsimps [used_Cons]
 			setloop split_tac [expand_event_case, expand_if])));
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
 val lemma = result();
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -303,7 +303,7 @@
 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);
+by (clarify_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]));
@@ -388,7 +388,7 @@
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
 (*Base case*)
 by (Blast_tac 1);
-by (Step_tac 1);
+by Safe_tac;
 by (expand_case_tac "K = KBC" 1);
 by (dtac respond_Key_in_parts 1);
 by (blast_tac (!claset addSIs [exI]
@@ -429,7 +429,7 @@
 by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib])));
 (** LEVEL 5 **)
 by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
-by (step_tac (!claset addSEs [MPair_parts]) 1);
+by (safe_tac (!claset addSEs [MPair_parts]));
 by (REPEAT (blast_tac (!claset addSDs [respond_certificate]
 		               addDs [resp_analz_insert]
 			       addIs  [impOfSubs analz_subset_parts]) 4));
@@ -446,14 +446,15 @@
 
 goal thy
  "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
-\           A ~: bad;  A' ~: bad;  evs : recur |]   \
+\           A ~: bad;  A' ~: bad;  evs : recur |]                      \
 \        ==> Key K ~: analz (spies evs)";
 by (etac rev_mp 1);
 by (etac recur.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac
-     (!simpset addsimps [parts_insert_spies, analz_insert_freshK] 
+     (!simpset addsimps [analz_insert_eq, parts_insert_spies, 
+			 analz_insert_freshK] 
                setloop split_tac [expand_if])));
 (*RA4*)
 by (spy_analz_tac 5);
@@ -464,11 +465,11 @@
 (*Base*)
 by (Blast_tac 1);
 (*RA3 remains*)
-by (step_tac (!claset delrules [impCE]) 1);
+by (safe_tac (!claset delrules [impCE]));
 (*RA3, case 2: K is an old key*)
 by (blast_tac (!claset addSDs [resp_analz_insert]
                        addSEs partsEs
-                       addDs [Key_in_parts_respond]) 2);
+                       addDs  [Key_in_parts_respond]) 2);
 (*RA3, case 1: use lemma previously proved by induction*)
 by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
 			       (2,rev_notE)]) 1);
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -112,7 +112,7 @@
 by (ALLGOALS (asm_simp_tac
 	      (!simpset addsimps [used_Cons]
 			setloop split_tac [expand_event_case, expand_if])));
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
 val lemma = result();
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -175,6 +175,6 @@
 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
-by (Step_tac 1);
+by Safe_tac;
 by (blast_tac (!claset addSEs partsEs) 1);
 **)
diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -190,7 +190,7 @@
 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
 by (etac yahalom.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (Clarify_tac 1);
 (*Remaining case: YM3*)
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));