Step_tac -> Safe_tac
authorpaulson
Mon Sep 29 11:47:01 1997 +0200 (1997-09-29)
changeset 37306933d20f335f
parent 3729 6be7cf5086ab
child 3731 71366483323b
Step_tac -> Safe_tac
src/HOL/Auth/Message.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/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Mon Sep 29 11:46:33 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Mon Sep 29 11:47:01 1997 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  (** Inverse of keys **)
     1.5  
     1.6  goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
     1.7 -by (Step_tac 1);
     1.8 +by Safe_tac;
     1.9  by (rtac box_equals 1);
    1.10  by (REPEAT (rtac invKey 2));
    1.11  by (Asm_simp_tac 1);
    1.12 @@ -135,7 +135,7 @@
    1.13  val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
    1.14  
    1.15  goal thy "parts{} = {}";
    1.16 -by (Step_tac 1);
    1.17 +by Safe_tac;
    1.18  by (etac parts.induct 1);
    1.19  by (ALLGOALS Blast_tac);
    1.20  qed "parts_empty";
    1.21 @@ -373,7 +373,7 @@
    1.22  (** General equational properties **)
    1.23  
    1.24  goal thy "analz{} = {}";
    1.25 -by (Step_tac 1);
    1.26 +by Safe_tac;
    1.27  by (etac analz.induct 1);
    1.28  by (ALLGOALS Blast_tac);
    1.29  qed "analz_empty";
    1.30 @@ -554,7 +554,7 @@
    1.31  (*If there are no pairs or encryptions then analz does nothing*)
    1.32  goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
    1.33  \         analz H = H";
    1.34 -by (Step_tac 1);
    1.35 +by Safe_tac;
    1.36  by (etac analz.induct 1);
    1.37  by (ALLGOALS Blast_tac);
    1.38  qed "analz_trivial";
     2.1 --- a/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:46:33 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:47:01 1997 +0200
     2.3 @@ -230,7 +230,7 @@
     2.4  \       -->         A=A' & NA=NA' & B=B' & X=X'";
     2.5  by (etac ns_shared.induct 1);
     2.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     2.7 -by (Step_tac 1);
     2.8 +by Safe_tac;
     2.9  (*NS3*)
    2.10  by (ex_strip_tac 2);
    2.11  by (Blast_tac 2);
    2.12 @@ -278,7 +278,7 @@
    2.13  (*Fake*) 
    2.14  by (spy_analz_tac 1);
    2.15  (*NS3, Server sub-case*) (**LEVEL 6 **)
    2.16 -by (step_tac (!claset delrules [impCE]) 1);
    2.17 +by (clarify_tac (!claset delrules [impCE]) 1);
    2.18  by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
    2.19  by (assume_tac 2);
    2.20  by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 29 11:46:33 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 29 11:47:01 1997 +0200
     3.3 @@ -196,7 +196,7 @@
     3.4  \     B=B' & NA=NA' & NB=NB' & X=X'";
     3.5  by (etac otway.induct 1);
     3.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     3.7 -by (Step_tac 1);
     3.8 +by (ALLGOALS Clarify_tac);
     3.9  (*Remaining cases: OR3 and OR4*)
    3.10  by (ex_strip_tac 2);
    3.11  by (Best_tac 2);
    3.12 @@ -286,22 +286,21 @@
    3.13  by (Fake_parts_insert_tac 1);
    3.14  (*OR1: it cannot be a new Nonce, contradiction.*)
    3.15  by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
    3.16 -(*OR3 and OR4*) 
    3.17 -(*OR4*)
    3.18 -by (REPEAT (Safe_step_tac 2));
    3.19 -by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
    3.20 -by (blast_tac (!claset addSIs [Crypt_imp_OR1]
    3.21 -                       addEs  spies_partsEs) 2);
    3.22 -(*OR3*)  (** LEVEL 5 **)
    3.23 +(*OR3 and OR4*)
    3.24  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
    3.25 -by (step_tac (!claset delrules [disjCI, impCE]) 1);
    3.26 +by (rtac conjI 1);
    3.27 +by (ALLGOALS Clarify_tac);
    3.28 +(*OR4*)
    3.29 +by (blast_tac (!claset addSIs [Crypt_imp_OR1]
    3.30 +                       addEs  spies_partsEs) 3);
    3.31 +(*OR3, two cases*)  (** LEVEL 5 **)
    3.32  by (blast_tac (!claset addSEs [MPair_parts]
    3.33 -                      addSDs [Says_imp_spies RS parts.Inj]
    3.34 -                      addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
    3.35 -                      delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
    3.36 +                       addSDs [Says_imp_spies RS parts.Inj]
    3.37 +                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
    3.38 +                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
    3.39  by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
    3.40 -                      addSEs [MPair_parts]
    3.41 -                      addIs  [unique_NA]) 1);
    3.42 +                       addSEs [MPair_parts]
    3.43 +                       addIs  [unique_NA]) 1);
    3.44  qed_spec_mp "NA_Crypt_imp_Server_msg";
    3.45  
    3.46  
    3.47 @@ -426,7 +425,7 @@
    3.48  (*OR4*)
    3.49  by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
    3.50  (*OR3*)
    3.51 -by (step_tac (!claset delrules [disjCI, impCE]) 1);
    3.52 +by (safe_tac (!claset delrules [disjCI, impCE]));
    3.53  by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
    3.54  by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
    3.55                         addSEs [MPair_parts]
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:46:33 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:47:01 1997 +0200
     4.3 @@ -190,7 +190,7 @@
     4.4  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
     4.5  by (etac otway.induct 1);
     4.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     4.7 -by (Step_tac 1);
     4.8 +by (ALLGOALS Clarify_tac);
     4.9  (*Remaining cases: OR3 and OR4*)
    4.10  by (ex_strip_tac 2);
    4.11  by (Blast_tac 2);
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 29 11:46:33 1997 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 29 11:47:01 1997 +0200
     5.3 @@ -199,7 +199,7 @@
     5.4  \     B=B' & NA=NA' & NB=NB' & X=X'";
     5.5  by (etac otway.induct 1);
     5.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     5.7 -by (Step_tac 1);
     5.8 +by (ALLGOALS Clarify_tac);
     5.9  (*Remaining cases: OR3 and OR4*)
    5.10  by (ex_strip_tac 2);
    5.11  by (Blast_tac 2);
    5.12 @@ -290,26 +290,25 @@
    5.13  by (Fake_parts_insert_tac 1);
    5.14  (*OR1: it cannot be a new Nonce, contradiction.*)
    5.15  by (blast_tac (!claset addSIs [parts_insertI]
    5.16 -                      addSEs spies_partsEs) 1);
    5.17 +                       addSEs spies_partsEs) 1);
    5.18 +(*OR3 and OR4*)
    5.19 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    5.20 +by (ALLGOALS Clarify_tac);
    5.21  (*OR4*)
    5.22 -by (REPEAT (Safe_step_tac 2));
    5.23 -by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
    5.24  by (blast_tac (!claset addSIs [Crypt_imp_OR1]
    5.25                         addEs  spies_partsEs) 2);
    5.26  (*OR3*)  (** LEVEL 5 **)
    5.27 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    5.28 -by (step_tac (!claset delrules [disjCI, impCE]) 1);
    5.29 -(*The hypotheses at this point suggest an attack in which nonce NA is used
    5.30 +(*The hypotheses at this point suggest an attack in which nonce NB is used
    5.31    in two different roles:
    5.32            Says B' Server
    5.33 -           {|Nonce NAa, Agent Aa, Agent A,
    5.34 -             Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
    5.35 -             Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
    5.36 -          : set evsa;
    5.37 +           {|Nonce NA, Agent Aa, Agent A,
    5.38 +             Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
    5.39 +             Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
    5.40 +          : set evs3;
    5.41            Says A B
    5.42 -           {|Nonce NA, Agent A, Agent B,
    5.43 -             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
    5.44 -          : set evsa 
    5.45 +           {|Nonce NB, Agent A, Agent B,
    5.46 +             Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
    5.47 +          : set evs3;
    5.48  *)
    5.49  writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
    5.50  
     6.1 --- a/src/HOL/Auth/Public.ML	Mon Sep 29 11:46:33 1997 +0200
     6.2 +++ b/src/HOL/Auth/Public.ML	Mon Sep 29 11:47:01 1997 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4  AddIffs [inj_pubK RS inj_eq];
     6.5  
     6.6  goal thy "!!A B. (priK A = priK B) = (A=B)";
     6.7 -by (Step_tac 1);
     6.8 +by Safe_tac;
     6.9  by (dres_inst_tac [("f","invKey")] arg_cong 1);
    6.10  by (Full_simp_tac 1);
    6.11  qed "priK_inj_eq";
    6.12 @@ -89,7 +89,7 @@
    6.13         THEN_BEST_FIRST 
    6.14           (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    6.15           (has_fewer_prems 1, size_of_thm)
    6.16 -         (Step_tac 1));
    6.17 +         Safe_tac);
    6.18  
    6.19  
    6.20  (*** Fresh nonces ***)
    6.21 @@ -115,7 +115,7 @@
    6.22  by (ALLGOALS (asm_simp_tac
    6.23  	      (!simpset addsimps [used_Cons]
    6.24  			setloop split_tac [expand_event_case, expand_if])));
    6.25 -by (Step_tac 1);
    6.26 +by Safe_tac;
    6.27  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
    6.28  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
    6.29  val lemma = result();
     7.1 --- a/src/HOL/Auth/Recur.ML	Mon Sep 29 11:46:33 1997 +0200
     7.2 +++ b/src/HOL/Auth/Recur.ML	Mon Sep 29 11:47:01 1997 +0200
     7.3 @@ -303,7 +303,7 @@
     7.4  by (Fake_parts_insert_tac 1);
     7.5  by (etac responses.induct 3);
     7.6  by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
     7.7 -by (step_tac (!claset addSEs partsEs) 1);
     7.8 +by (clarify_tac (!claset addSEs partsEs) 1);
     7.9  (*RA1,2: creation of new Nonce.  Move assertion into global context*)
    7.10  by (ALLGOALS (expand_case_tac "NA = ?y"));
    7.11  by (REPEAT_FIRST (ares_tac [exI]));
    7.12 @@ -388,7 +388,7 @@
    7.13  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
    7.14  (*Base case*)
    7.15  by (Blast_tac 1);
    7.16 -by (Step_tac 1);
    7.17 +by Safe_tac;
    7.18  by (expand_case_tac "K = KBC" 1);
    7.19  by (dtac respond_Key_in_parts 1);
    7.20  by (blast_tac (!claset addSIs [exI]
    7.21 @@ -429,7 +429,7 @@
    7.22  by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib])));
    7.23  (** LEVEL 5 **)
    7.24  by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
    7.25 -by (step_tac (!claset addSEs [MPair_parts]) 1);
    7.26 +by (safe_tac (!claset addSEs [MPair_parts]));
    7.27  by (REPEAT (blast_tac (!claset addSDs [respond_certificate]
    7.28  		               addDs [resp_analz_insert]
    7.29  			       addIs  [impOfSubs analz_subset_parts]) 4));
    7.30 @@ -446,14 +446,15 @@
    7.31  
    7.32  goal thy
    7.33   "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
    7.34 -\           A ~: bad;  A' ~: bad;  evs : recur |]   \
    7.35 +\           A ~: bad;  A' ~: bad;  evs : recur |]                      \
    7.36  \        ==> Key K ~: analz (spies evs)";
    7.37  by (etac rev_mp 1);
    7.38  by (etac recur.induct 1);
    7.39  by analz_spies_tac;
    7.40  by (ALLGOALS
    7.41      (asm_simp_tac
    7.42 -     (!simpset addsimps [parts_insert_spies, analz_insert_freshK] 
    7.43 +     (!simpset addsimps [analz_insert_eq, parts_insert_spies, 
    7.44 +			 analz_insert_freshK] 
    7.45                 setloop split_tac [expand_if])));
    7.46  (*RA4*)
    7.47  by (spy_analz_tac 5);
    7.48 @@ -464,11 +465,11 @@
    7.49  (*Base*)
    7.50  by (Blast_tac 1);
    7.51  (*RA3 remains*)
    7.52 -by (step_tac (!claset delrules [impCE]) 1);
    7.53 +by (safe_tac (!claset delrules [impCE]));
    7.54  (*RA3, case 2: K is an old key*)
    7.55  by (blast_tac (!claset addSDs [resp_analz_insert]
    7.56                         addSEs partsEs
    7.57 -                       addDs [Key_in_parts_respond]) 2);
    7.58 +                       addDs  [Key_in_parts_respond]) 2);
    7.59  (*RA3, case 1: use lemma previously proved by induction*)
    7.60  by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
    7.61  			       (2,rev_notE)]) 1);
     8.1 --- a/src/HOL/Auth/Shared.ML	Mon Sep 29 11:46:33 1997 +0200
     8.2 +++ b/src/HOL/Auth/Shared.ML	Mon Sep 29 11:47:01 1997 +0200
     8.3 @@ -112,7 +112,7 @@
     8.4  by (ALLGOALS (asm_simp_tac
     8.5  	      (!simpset addsimps [used_Cons]
     8.6  			setloop split_tac [expand_event_case, expand_if])));
     8.7 -by (Step_tac 1);
     8.8 +by Safe_tac;
     8.9  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
    8.10  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
    8.11  val lemma = result();
     9.1 --- a/src/HOL/Auth/WooLam.ML	Mon Sep 29 11:46:33 1997 +0200
     9.2 +++ b/src/HOL/Auth/WooLam.ML	Mon Sep 29 11:47:01 1997 +0200
     9.3 @@ -175,6 +175,6 @@
     9.4  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
     9.5  by (parts_induct_tac 1);
     9.6  by (Fake_parts_insert_tac 1);
     9.7 -by (Step_tac 1);
     9.8 +by Safe_tac;
     9.9  by (blast_tac (!claset addSEs partsEs) 1);
    9.10  **)
    10.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Sep 29 11:46:33 1997 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.ML	Mon Sep 29 11:47:01 1997 +0200
    10.3 @@ -190,7 +190,7 @@
    10.4  \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    10.5  by (etac yahalom.induct 1);
    10.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    10.7 -by (Step_tac 1);
    10.8 +by (Clarify_tac 1);
    10.9  (*Remaining case: YM3*)
   10.10  by (expand_case_tac "K = ?y" 1);
   10.11  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));