--- a/src/HOL/Auth/OtwayRees.ML Fri Dec 13 10:18:48 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Fri Dec 13 10:20:55 1996 +0100
@@ -165,8 +165,8 @@
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
@@ -257,7 +257,7 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 14 secs*)
+by (ALLGOALS (*Takes 12 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
@@ -451,15 +451,14 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_full_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
- analz_insert_Key_newK] @ pushes)
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
+ analz_insert_Key_newK] @ pushes)
+ setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 3);
(*OR4, OR2, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*Oops*) (** LEVEL 5 **)
by (fast_tac (!claset delrules [disjE]
addDs [unique_session_keys] addss (!simpset)) 1);
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Dec 13 10:18:48 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Dec 13 10:20:55 1996 +0100
@@ -151,16 +151,17 @@
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-(*OR1 and OR3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
-(*Fake, OR2, OR4: these messages send unknown (X) components*)
-by (REPEAT
- (best_tac
+(*Fake, OR4: these messages send unknown (X) components*)
+by (EVERY
+ (map
+ (best_tac
(!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono),
Suc_leD]
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)) 1));
+ addss (!simpset))) [5,1]));
+(*Remaining subgoals*)
+by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -336,15 +337,14 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_full_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
- analz_insert_Key_newK] @ pushes)
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
+ analz_insert_Key_newK] @ pushes)
+ setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 2);
(*OR4, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*Oops*)
by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
--- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Dec 13 10:18:48 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Dec 13 10:20:55 1996 +0100
@@ -336,15 +336,14 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_full_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
- analz_insert_Key_newK] @ pushes)
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
+ analz_insert_Key_newK] @ pushes)
+ setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 3);
(*OR4, OR2, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*Oops*) (** LEVEL 5 **)
by (fast_tac (!claset delrules [disjE]
addDs [unique_session_keys] addss (!simpset)) 1);