src/HOL/Auth/OtwayRees_AN.ML
changeset 4091 771b1f6422a8
parent 3961 6a8996fb7d99
child 4155 53f60f51333c
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Nov 03 12:22:43 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Nov 03 12:24:13 1997 +0100
     1.3 @@ -45,12 +45,12 @@
     1.4  
     1.5  goal thy "!!evs. Says S' B {|X, Crypt(shrK 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 "OR4_analz_spies";
    1.10  
    1.11  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.12  \                  : set evs ==> K : parts (spies evs)";
    1.13 -by (blast_tac (!claset addSEs spies_partsEs) 1);
    1.14 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.15  qed "Oops_parts_spies";
    1.16  
    1.17  (*OR4_analz_spies lets us treat those cases using the same 
    1.18 @@ -82,12 +82,12 @@
    1.19  
    1.20  goal thy 
    1.21   "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.22 -by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.23 +by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    1.24  qed "Spy_analz_shrK";
    1.25  Addsimps [Spy_analz_shrK];
    1.26  
    1.27  goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    1.28 -by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.29 +by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    1.30  qed "Spy_see_shrK_D";
    1.31  
    1.32  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.33 @@ -100,10 +100,10 @@
    1.34  by (parts_induct_tac 1);
    1.35  (*Fake*)
    1.36  by (best_tac
    1.37 -      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.38 +      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.39                 addIs  [impOfSubs analz_subset_parts]
    1.40                 addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.41 -               addss  (!simpset)) 1);
    1.42 +               addss  (simpset())) 1);
    1.43  (*OR3*)
    1.44  by (Blast_tac 1);
    1.45  qed_spec_mp "new_keys_not_used";
    1.46 @@ -189,7 +189,7 @@
    1.47  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    1.48  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.49  by (etac otway.induct 1);
    1.50 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.51 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    1.52  by (ALLGOALS Clarify_tac);
    1.53  (*Remaining cases: OR3 and OR4*)
    1.54  by (ex_strip_tac 2);
    1.55 @@ -197,7 +197,7 @@
    1.56  by (expand_case_tac "K = ?y" 1);
    1.57  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.58  (*...we assume X is a recent message and handle this case by contradiction*)
    1.59 -by (blast_tac (!claset addSEs spies_partsEs
    1.60 +by (blast_tac (claset() addSEs spies_partsEs
    1.61                         delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
    1.62  val lemma = result();
    1.63  
    1.64 @@ -230,7 +230,7 @@
    1.65  \                  : set evs)";
    1.66  by (parts_induct_tac 1);
    1.67  by (Fake_parts_insert_tac 1);
    1.68 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    1.69 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
    1.70  (*OR3*)
    1.71  by (Blast_tac 1);
    1.72  qed_spec_mp "NA_Crypt_imp_Server_msg";
    1.73 @@ -246,7 +246,7 @@
    1.74  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    1.75  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    1.76  \                   : set evs";
    1.77 -by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.78 +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
    1.79                        addEs  spies_partsEs) 1);
    1.80  qed "A_trusts_OR4";
    1.81  
    1.82 @@ -266,15 +266,15 @@
    1.83  by (etac otway.induct 1);
    1.84  by analz_spies_tac;
    1.85  by (ALLGOALS
    1.86 -    (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
    1.87 +    (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
    1.88                              addsimps [analz_insert_eq, analz_insert_freshK]
    1.89                              addsimps (pushes@expand_ifs))));
    1.90  (*Oops*)
    1.91 -by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    1.92 +by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    1.93  (*OR4*) 
    1.94  by (Blast_tac 3);
    1.95  (*OR3*)
    1.96 -by (blast_tac (!claset addSEs spies_partsEs
    1.97 +by (blast_tac (claset() addSEs spies_partsEs
    1.98                         addIs [impOfSubs analz_subset_parts]) 2);
    1.99  (*Fake*) 
   1.100  by (spy_analz_tac 1);
   1.101 @@ -289,7 +289,7 @@
   1.102  \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.103  \        ==> Key K ~: analz (spies evs)";
   1.104  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.105 -by (blast_tac (!claset addSEs [lemma]) 1);
   1.106 +by (blast_tac (claset() addSEs [lemma]) 1);
   1.107  qed "Spy_not_see_encrypted_key";
   1.108  
   1.109  
   1.110 @@ -305,7 +305,7 @@
   1.111  \                     : set evs)";
   1.112  by (parts_induct_tac 1);
   1.113  by (Fake_parts_insert_tac 1);
   1.114 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.115 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   1.116  (*OR3*)
   1.117  by (Blast_tac 1);
   1.118  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.119 @@ -321,6 +321,6 @@
   1.120  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.121  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.122  \                     : set evs";
   1.123 -by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.124 +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
   1.125                         addEs  spies_partsEs) 1);
   1.126  qed "B_trusts_OR3";