src/HOL/Auth/OtwayRees.ML
changeset 4091 771b1f6422a8
parent 3961 6a8996fb7d99
child 4422 21238c9d363e
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 03 12:22:43 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Nov 03 12:24:13 1997 +0100
     1.3 @@ -45,17 +45,17 @@
     1.4  
     1.5  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
     1.6  \                ==> X : analz (spies evs)";
     1.7 -by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
     1.8 +by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
     1.9  qed "OR2_analz_spies";
    1.10  
    1.11  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    1.12  \                ==> X : analz (spies evs)";
    1.13 -by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.14 +by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.15  qed "OR4_analz_spies";
    1.16  
    1.17  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    1.18  \                 ==> K : parts (spies evs)";
    1.19 -by (blast_tac (!claset addSEs spies_partsEs) 1);
    1.20 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.21  qed "Oops_parts_spies";
    1.22  
    1.23  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.24 @@ -92,12 +92,12 @@
    1.25  
    1.26  goal thy 
    1.27   "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.28 -by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.29 +by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    1.30  qed "Spy_analz_shrK";
    1.31  Addsimps [Spy_analz_shrK];
    1.32  
    1.33  goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    1.34 -by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.35 +by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    1.36  qed "Spy_see_shrK_D";
    1.37  
    1.38  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.39 @@ -110,10 +110,10 @@
    1.40  by (parts_induct_tac 1);
    1.41  (*Fake*)
    1.42  by (best_tac
    1.43 -      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.44 +      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.45                 addIs  [impOfSubs analz_subset_parts]
    1.46                 addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.47 -               addss  (!simpset)) 1);
    1.48 +               addss  (simpset())) 1);
    1.49  by (ALLGOALS Blast_tac);
    1.50  qed_spec_mp "new_keys_not_used";
    1.51  
    1.52 @@ -195,7 +195,7 @@
    1.53  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
    1.54  \     B=B' & NA=NA' & NB=NB' & X=X'";
    1.55  by (etac otway.induct 1);
    1.56 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.57 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    1.58  by (ALLGOALS Clarify_tac);
    1.59  (*Remaining cases: OR3 and OR4*)
    1.60  by (ex_strip_tac 2);
    1.61 @@ -203,7 +203,7 @@
    1.62  by (expand_case_tac "K = ?y" 1);
    1.63  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.64  (*...we assume X is a recent message, and handle this case by contradiction*)
    1.65 -by (blast_tac (!claset addSEs spies_partsEs
    1.66 +by (blast_tac (claset() addSEs spies_partsEs
    1.67                         delrules [conjI] (*no split-up into 4 subgoals*)) 1);
    1.68  val lemma = result();
    1.69  
    1.70 @@ -239,10 +239,10 @@
    1.71  \        --> B = B'";
    1.72  by (parts_induct_tac 1);
    1.73  by (Fake_parts_insert_tac 1);
    1.74 -by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
    1.75 +by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
    1.76  (*OR1: creation of new Nonce.  Move assertion into global context*)
    1.77  by (expand_case_tac "NA = ?y" 1);
    1.78 -by (blast_tac (!claset addSEs spies_partsEs) 1);
    1.79 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.80  val lemma = result();
    1.81  
    1.82  goal thy 
    1.83 @@ -264,7 +264,7 @@
    1.84  \             ~: parts (spies evs)";
    1.85  by (parts_induct_tac 1);
    1.86  by (Fake_parts_insert_tac 1);
    1.87 -by (REPEAT (blast_tac (!claset addSEs spies_partsEs
    1.88 +by (REPEAT (blast_tac (claset() addSEs spies_partsEs
    1.89                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
    1.90  qed_spec_mp"no_nonce_OR1_OR2";
    1.91  
    1.92 @@ -285,20 +285,20 @@
    1.93  by (parts_induct_tac 1);
    1.94  by (Fake_parts_insert_tac 1);
    1.95  (*OR1: it cannot be a new Nonce, contradiction.*)
    1.96 -by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
    1.97 +by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
    1.98  (*OR3 and OR4*)
    1.99 -by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.100 +by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.101  by (rtac conjI 1);
   1.102  by (ALLGOALS Clarify_tac);
   1.103  (*OR4*)
   1.104 -by (blast_tac (!claset addSIs [Crypt_imp_OR1]
   1.105 +by (blast_tac (claset() addSIs [Crypt_imp_OR1]
   1.106                         addEs  spies_partsEs) 3);
   1.107  (*OR3, two cases*)  (** LEVEL 5 **)
   1.108 -by (blast_tac (!claset addSEs [MPair_parts]
   1.109 +by (blast_tac (claset() addSEs [MPair_parts]
   1.110                         addSDs [Says_imp_spies RS parts.Inj]
   1.111                         addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.112                         delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   1.113 -by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.114 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.115                         addSEs [MPair_parts]
   1.116                         addIs  [unique_NA]) 1);
   1.117  qed_spec_mp "NA_Crypt_imp_Server_msg";
   1.118 @@ -318,7 +318,7 @@
   1.119  \                       Crypt (shrK A) {|NA, Key K|},              \
   1.120  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   1.121  \                       : set evs";
   1.122 -by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.123 +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
   1.124                         addEs  spies_partsEs) 1);
   1.125  qed "A_trusts_OR4";
   1.126  
   1.127 @@ -337,15 +337,15 @@
   1.128  by (etac otway.induct 1);
   1.129  by analz_spies_tac;
   1.130  by (ALLGOALS
   1.131 -    (asm_simp_tac (!simpset addcongs [conj_cong] 
   1.132 +    (asm_simp_tac (simpset() addcongs [conj_cong] 
   1.133                              addsimps [analz_insert_eq, analz_insert_freshK]
   1.134                              addsimps (pushes@expand_ifs))));
   1.135  (*Oops*)
   1.136 -by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   1.137 +by (blast_tac (claset() addSDs [unique_session_keys]) 4);
   1.138  (*OR4*) 
   1.139  by (Blast_tac 3);
   1.140  (*OR3*)
   1.141 -by (blast_tac (!claset addSEs spies_partsEs
   1.142 +by (blast_tac (claset() addSEs spies_partsEs
   1.143                         addIs [impOfSubs analz_subset_parts]) 2);
   1.144  (*Fake*) 
   1.145  by (spy_analz_tac 1);
   1.146 @@ -359,7 +359,7 @@
   1.147  \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.148  \        ==> Key K ~: analz (spies evs)";
   1.149  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.150 -by (blast_tac (!claset addSEs [lemma]) 1);
   1.151 +by (blast_tac (claset() addSEs [lemma]) 1);
   1.152  qed "Spy_not_see_encrypted_key";
   1.153  
   1.154  
   1.155 @@ -390,10 +390,10 @@
   1.156  \      --> NA = NA' & A = A'";
   1.157  by (parts_induct_tac 1);
   1.158  by (Fake_parts_insert_tac 1);
   1.159 -by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.160 +by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   1.161  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.162  by (expand_case_tac "NB = ?y" 1);
   1.163 -by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.164 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.165  val lemma = result();
   1.166  
   1.167  goal thy 
   1.168 @@ -421,16 +421,16 @@
   1.169  by (parts_induct_tac 1);
   1.170  by (Fake_parts_insert_tac 1);
   1.171  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.172 -by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
   1.173 +by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
   1.174  (*OR4*)
   1.175 -by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   1.176 +by (blast_tac (claset() addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   1.177  (*OR3*)
   1.178 -by (safe_tac (!claset delrules [disjCI, impCE]));
   1.179 -by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.180 -by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.181 +by (safe_tac (claset() delrules [disjCI, impCE]));
   1.182 +by (blast_tac (claset() delrules [conjI] (*stop split-up*)) 3); 
   1.183 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.184                         addSEs [MPair_parts]
   1.185                         addDs  [unique_NB]) 2);
   1.186 -by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.187 +by (blast_tac (claset() addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.188                         addSDs [Says_imp_spies RS parts.Inj]
   1.189                         delrules [conjI, impCE] (*stop split-up*)) 1);
   1.190  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.191 @@ -449,7 +449,7 @@
   1.192  \                   Crypt (shrK A) {|NA, Key K|},                  \
   1.193  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   1.194  \                   : set evs";
   1.195 -by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.196 +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
   1.197                         addSEs spies_partsEs) 1);
   1.198  qed "B_trusts_OR3";
   1.199  
   1.200 @@ -467,7 +467,7 @@
   1.201  \            : set evs)";
   1.202  by (etac otway.induct 1);
   1.203  by (ALLGOALS Asm_simp_tac);
   1.204 -by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   1.205 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
   1.206  		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   1.207  by (ALLGOALS Blast_tac);
   1.208  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.209 @@ -484,6 +484,6 @@
   1.210  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   1.211  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.212  \            : set evs";
   1.213 -by (blast_tac (!claset addSDs  [A_trusts_OR4]
   1.214 +by (blast_tac (claset() addSDs  [A_trusts_OR4]
   1.215                         addSEs [OR3_imp_OR2]) 1);
   1.216  qed "A_auths_B";