--- a/src/HOL/Auth/OtwayRees.ML Mon Nov 03 12:22:43 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Mon Nov 03 12:24:13 1997 +0100
@@ -45,17 +45,17 @@
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
\ ==> X : analz (spies evs)";
-by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
qed "OR2_analz_spies";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
\ ==> X : analz (spies evs)";
-by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (spies evs)";
-by (blast_tac (!claset addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
qed "Oops_parts_spies";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
@@ -92,12 +92,12 @@
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
-by (blast_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);
@@ -110,10 +110,10 @@
by (parts_induct_tac 1);
(*Fake*)
by (best_tac
- (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (!simpset)) 1);
+ addss (simpset())) 1);
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
@@ -195,7 +195,7 @@
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
@@ -203,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 (blast_tac (!claset addSEs spies_partsEs
+by (blast_tac (claset() addSEs spies_partsEs
delrules [conjI] (*no split-up into 4 subgoals*)) 1);
val lemma = result();
@@ -239,10 +239,10 @@
\ --> B = B'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 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);
-by (blast_tac (!claset addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
goal thy
@@ -264,7 +264,7 @@
\ ~: parts (spies evs)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (REPEAT (blast_tac (!claset addSEs spies_partsEs
+by (REPEAT (blast_tac (claset() addSEs spies_partsEs
addSDs [impOfSubs parts_insert_subset_Un]) 1));
qed_spec_mp"no_nonce_OR1_OR2";
@@ -285,20 +285,20 @@
by (parts_induct_tac 1);
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);
+by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
(*OR3 and OR4*)
-by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
by (rtac conjI 1);
by (ALLGOALS Clarify_tac);
(*OR4*)
-by (blast_tac (!claset addSIs [Crypt_imp_OR1]
+by (blast_tac (claset() addSIs [Crypt_imp_OR1]
addEs spies_partsEs) 3);
(*OR3, two cases*) (** LEVEL 5 **)
-by (blast_tac (!claset addSEs [MPair_parts]
+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);
-by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
addIs [unique_NA]) 1);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -318,7 +318,7 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
-by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
+by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
addEs spies_partsEs) 1);
qed "A_trusts_OR4";
@@ -337,15 +337,15 @@
by (etac otway.induct 1);
by analz_spies_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addcongs [conj_cong]
+ (asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
addsimps (pushes@expand_ifs))));
(*Oops*)
-by (blast_tac (!claset addSDs [unique_session_keys]) 4);
+by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset addSEs spies_partsEs
+by (blast_tac (claset() addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -359,7 +359,7 @@
\ A ~: bad; B ~: bad; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (blast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (claset() addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -390,10 +390,10 @@
\ --> NA = NA' & A = A'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 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);
-by (blast_tac (!claset addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
goal thy
@@ -421,16 +421,16 @@
by (parts_induct_tac 1);
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);
+by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
(*OR4*)
-by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
+by (blast_tac (claset() addSEs [MPair_parts, Crypt_imp_OR2]) 2);
(*OR3*)
-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]
+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]
addDs [unique_NB]) 2);
-by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
+by (blast_tac (claset() addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
addSDs [Says_imp_spies RS parts.Inj]
delrules [conjI, impCE] (*stop split-up*)) 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -449,7 +449,7 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
-by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
+by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
addSEs spies_partsEs) 1);
qed "B_trusts_OR3";
@@ -467,7 +467,7 @@
\ : set evs)";
by (etac otway.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts, Crypt_imp_OR2]) 3);
by (ALLGOALS Blast_tac);
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -484,6 +484,6 @@
\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
\ : set evs";
-by (blast_tac (!claset addSDs [A_trusts_OR4]
+by (blast_tac (claset() addSDs [A_trusts_OR4]
addSEs [OR3_imp_OR2]) 1);
qed "A_auths_B";