# HG changeset patch
# User paulson
# Date 850468855 -3600
# Node ID 14539397fc04d64d86df735d4535bfaf58902b22
# Parent  4148aa5b00a2919cff9b18f4bae5d750f2171155
Streamlined some proofs

diff -r 4148aa5b00a2 -r 14539397fc04 src/HOL/Auth/OtwayRees.ML
--- 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);
diff -r 4148aa5b00a2 -r 14539397fc04 src/HOL/Auth/OtwayRees_AN.ML
--- 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);
diff -r 4148aa5b00a2 -r 14539397fc04 src/HOL/Auth/OtwayRees_Bad.ML
--- 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);