# HG changeset patch
# User paulson
# Date 944657556 -3600
# Node ID 2ce57ef2a4aab2c5b593850dda2ce5a6ff91d241
# Parent  37ebdaf3bb91bc3d7e5f2c98e1150ac97e894863
used image_eq_UN to speed up slow proofs of base cases

diff -r 37ebdaf3bb91 -r 2ce57ef2a4aa src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/Message.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -856,7 +856,8 @@
   concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    Force_tac i THEN ALLGOALS Asm_simp_tac;
+    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    ALLGOALS Asm_simp_tac;
 
 fun Fake_parts_insert_tac i = 
     blast_tac (claset() addIs [parts_insertI]
diff -r 37ebdaf3bb91 -r 2ce57ef2a4aa src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -13,6 +13,8 @@
 
 AddIffs [Spy_in_bad];
 
+Addsimps [image_eq_UN];  (*accelerates proofs involving nested images*)
+
 (*A "possibility property": there are traces that reach the end*)
 Goal
    "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
diff -r 37ebdaf3bb91 -r 2ce57ef2a4aa src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -17,6 +17,8 @@
 
 AddIffs [Spy_in_bad];
 
+Addsimps [image_eq_UN];  (*accelerates proofs involving nested images*)
+
 (*A "possibility property": there are traces that reach the end*)
 Goal
   "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
diff -r 37ebdaf3bb91 -r 2ce57ef2a4aa src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/Public.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -149,7 +149,7 @@
 (*Tactic for possibility theorems*)
 fun possibility_tac st = st |>
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
+    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, Nonce_supply]));
diff -r 37ebdaf3bb91 -r 2ce57ef2a4aa src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/TLS.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -179,7 +179,7 @@
     ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
-    ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
+    ALLGOALS (asm_simp_tac (simpset() addsimps [image_eq_UN, insert_absorb]));
 
 
 (*** Properties of items found in Notes ***)
@@ -405,9 +405,9 @@
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
 (*SpyKeys*)
-by (Blast_tac 3);
+by (Blast_tac 2);
 (*Fake*)
-by (blast_tac (claset() addIs [parts_insertI]) 2);
+by (blast_tac (claset() addIs [parts_insertI]) 1);
 (** LEVEL 6 **)
 (*Oops*)
 by (REPEAT 
@@ -440,11 +440,9 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);        (*5 seconds*)
 (*SpyKeys*)
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 2);
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed "sessionK_not_spied";