--- a/src/HOL/Auth/Message.ML Fri Nov 08 14:07:56 1996 +0100
+++ b/src/HOL/Auth/Message.ML Fri Nov 08 14:13:56 1996 +0100
@@ -664,7 +664,7 @@
\ Key K ~: analz G |] \
\ ==> Crypt Y K : parts G Un parts H";
by (dtac (impOfSubs Fake_parts_insert) 1);
-ba 1;
+by (assume_tac 1);
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 1);
qed "Crypt_Fake_parts_insert";
--- a/src/HOL/Auth/NS_Shared.ML Fri Nov 08 14:07:56 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Fri Nov 08 14:13:56 1996 +0100
@@ -70,9 +70,9 @@
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
(DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 2)) THEN
(*Base case*)
fast_tac (!claset addss (!simpset)) 1 THEN
@@ -143,10 +143,10 @@
by (parts_induct_tac 1);
by (REPEAT_FIRST
(fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un, Suc_leD]
- addss (!simpset))));
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un, Suc_leD]
+ addss (!simpset))));
qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
@@ -230,7 +230,7 @@
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
by (fast_tac (!claset addEs partsEs
addSDs [A_trust_NS2, Says_Server_message_form]
- addIs [Says_imp_old_keys]
+ addIs [Says_imp_old_keys]
addss (!simpset)) 1);
qed "Says_S_message_form";
@@ -342,7 +342,7 @@
(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1);
by (fast_tac (!claset addSDs [ spec]
- delrules [conjI] addss (!simpset)) 1);
+ delrules [conjI] addss (!simpset)) 1);
qed "unique_session_keys";
@@ -373,16 +373,16 @@
(*NS3 and Oops subcases*) (**LEVEL 7 **)
by (step_tac (!claset delrules [impCE]) 1);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
-be conjE 2;
+by (etac conjE 2);
by (mp_tac 2);
(**LEVEL 11 **)
by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 2);
-ba 3;
+by (assume_tac 3);
by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
(*NS3*)
by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 1);
-ba 2;
+by (assume_tac 2);
by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -460,10 +460,10 @@
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
(*Contradiction from the assumption
Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
-bd Crypt_imp_invKey_keysFor 1;
+by (dtac Crypt_imp_invKey_keysFor 1);
(**LEVEL 10**)
by (Asm_full_simp_tac 1);
-br disjI1 1;
+by (rtac disjI1 1);
by (thin_tac "?PP-->?QQ" 1);
by (case_tac "Ba : lost" 1);
by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
@@ -480,5 +480,5 @@
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
- addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
+ addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
qed "A_trust_NS4";
--- a/src/HOL/Auth/Yahalom.ML Fri Nov 08 14:07:56 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Fri Nov 08 14:13:56 1996 +0100
@@ -79,9 +79,9 @@
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
(DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 2)) THEN
(*Base case*)
fast_tac (!claset addss (!simpset)) 1 THEN
@@ -164,10 +164,10 @@
(*Fake and Oops: these messages send unknown (X) components*)
by (EVERY
(map (fast_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
+ (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
addss (!simpset))) [3,1]));
(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
by (fast_tac
@@ -340,8 +340,8 @@
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
(*Oops*) (** LEVEL 6 **)
by (fast_tac (!claset delrules [disjE]
- addDs [unique_session_keys]
- addss (!simpset)) 1);
+ addDs [unique_session_keys]
+ addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -465,8 +465,8 @@
REPEAT_DETERM (etac MPair_analz 1) THEN
THEN_BEST_FIRST
(dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
- (has_fewer_prems 1, size_of_thm)
- (Step_tac 1));
+ (has_fewer_prems 1, size_of_thm)
+ (Step_tac 1));
(*Variant useful for proving secrecy of NB*)
@@ -496,12 +496,12 @@
dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
mp_tac));
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
by (ALLGOALS Asm_simp_tac);
by (fast_tac (!claset addss (!simpset)) 1);
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
- addSIs [parts_insertI]
+ addSIs [parts_insertI]
addSEs partsEs
addEs [Says_imp_old_nonces RS less_irrefl]
addss (!simpset)) 1);
@@ -539,7 +539,7 @@
by (Step_tac 1);
by (lost_tac "A" 1);
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
- A_trust_YM3]) 1);
+ A_trust_YM3]) 1);
val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
@@ -571,7 +571,7 @@
by (Step_tac 1);
by (lost_tac "A" 1);
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
- A_trust_YM3]) 1);
+ A_trust_YM3]) 1);
result() RS mp RSN (2, rev_mp);
@@ -609,8 +609,8 @@
(Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
assume_tac ORELSE'
depth_tac (!claset delrules [conjI]
- addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
- impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
+ addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
+ impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
(*The only nonces that can be found with the help of session keys are
those distributed as nonce NB by the Server. The form of the theorem
@@ -628,8 +628,8 @@
(asm_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
analz_image_newK,
- insert_Key_singleton, insert_Key_image]
- @ pushes)
+ insert_Key_singleton, insert_Key_image]
+ @ pushes)
setloop split_tac [expand_if])));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
@@ -639,20 +639,20 @@
by (EVERY (map grind_tac [3,2,1]));
(*Oops*)
by (Full_simp_tac 2);
-by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2));
+by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2));
by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
by (grind_tac 2);
by (fast_tac (!claset delrules [bexI]
- addDs [unique_session_keys]
- addss (!simpset)) 2);
+ addDs [unique_session_keys]
+ addss (!simpset)) 2);
(*YM4*)
(** LEVEL 11 **)
-br (impI RS allI) 1;
+by (rtac (impI RS allI) 1);
by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN
Fast_tac 1);
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
by (asm_simp_tac (!simpset addsimps [analz_image_newK]
- setloop split_tac [expand_if]) 1);
+ setloop split_tac [expand_if]) 1);
(** LEVEL 15 **)
by (grind_tac 1);
by (REPEAT (dtac not_analz_insert 1));
@@ -661,8 +661,8 @@
THEN REPEAT (assume_tac 1));
by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
by (fast_tac (!claset delrules [conjI]
- addIs [impOfSubs (subset_insertI RS analz_mono)]
- addss (!simpset)) 1);
+ addIs [impOfSubs (subset_insertI RS analz_mono)]
+ addss (!simpset)) 1);
val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
@@ -679,7 +679,7 @@
by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
by (dtac Nonce_secrecy 1 THEN assume_tac 1);
by (fast_tac (!claset addDs [unique_session_keys]
- addss (!simpset)) 1);
+ addss (!simpset)) 1);
val single_Nonce_secrecy = result();
@@ -719,7 +719,7 @@
by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
(** LEVEL 14 **)
by (lost_tac "Aa" 1);
-bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1;
+by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1);
by (forward_tac [Says_Server_message_form] 3);
by (forward_tac [Says_Server_imp_YM2] 4);
by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
@@ -727,11 +727,11 @@
(** LEVEL 20 **)
by (REPEAT_FIRST hyp_subst_tac);
by (lost_tac "Ba" 1);
-bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1;
+by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
addSEs [MPair_parts]) 1);
by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1));
-bd Spy_not_see_encrypted_key 1;
+by (dtac Spy_not_see_encrypted_key 1);
by (REPEAT (assume_tac 1 ORELSE Fast_tac 1));
by (spy_analz_tac 1);
(*Oops case*) (** LEVEL 28 **)
@@ -740,7 +740,7 @@
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
by (expand_case_tac "NB = NBa" 1);
by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
-br conjI 1;
+by (rtac conjI 1);
by (no_nonce_tac 1);
(** LEVEL 35 **)
by (thin_tac "?PP|?QQ" 1); (*subsumption!*)
@@ -769,10 +769,10 @@
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
dtac B_trusts_YM4_shrK 1);
-bd B_trusts_YM4_newK 3;
+by (dtac B_trusts_YM4_newK 3);
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
-by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
+by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
qed "B_trust_YM4";
--- a/src/HOL/Auth/Yahalom2.ML Fri Nov 08 14:07:56 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Fri Nov 08 14:13:56 1996 +0100
@@ -80,9 +80,9 @@
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
(DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 2)) THEN
(*Base case*)
fast_tac (!claset addss (!simpset)) 1 THEN
@@ -157,16 +157,16 @@
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
+by (dtac YM4_Key_parts_sees_Spy 5);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
(*Fake and Oops: these messages send unknown (X) components*)
by (EVERY
(map (fast_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
+ (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
addss (!simpset))) [3,1]));
(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
by (fast_tac
@@ -307,8 +307,8 @@
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
(*Oops*)
by (fast_tac (!claset delrules [disjE]
- addDs [unique_session_keys]
- addss (!simpset)) 1);
+ addDs [unique_session_keys]
+ addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -392,6 +392,6 @@
\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
\ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
\ : set_of_list evs";
-be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
+by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
qed "B_trust_YM4";