# HG changeset patch
# User paulson
# Date 874410881 -7200
# Node ID 3b06747c3f37891e3299793ee815861fa55cfd48
# Parent  56e4365a0c99a66fca6aeee7935820358b0e6cf1
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
faster

diff -r 56e4365a0c99 -r 3b06747c3f37 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Tue Sep 16 13:32:22 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Tue Sep 16 13:54:41 1997 +0200
@@ -130,7 +130,7 @@
 
 (*Tactic for possibility theorems*)
 fun possibility_tac st = st |>
-    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
+    REPEAT (*omit used_Says so that Nonces start from different traces!*)
     (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
@@ -150,7 +150,8 @@
 (*Reverse the normal simplification of "image" to build up (not break down)
   the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
 val analz_image_keys_ss = 
-     !simpset delsimps [image_insert, image_Un]
+     !simpset addcongs [if_weak_cong]
+	      delsimps [image_insert, image_Un]
               addsimps [image_insert RS sym, image_Un RS sym,
 			rangeI, 
 			insert_Key_singleton, 
diff -r 56e4365a0c99 -r 3b06747c3f37 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Sep 16 13:32:22 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Sep 16 13:54:41 1997 +0200
@@ -197,8 +197,10 @@
 
 (*** Tactics for possibility theorems ***)
 
+(*Omitting used_Says makes the tactic much faster: it leaves expressions
+    such as  Nonce ?N ~: used evs that match Nonce_supply*)
 fun possibility_tac st = st |>
-   (REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
+   (REPEAT 
     (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
@@ -231,7 +233,8 @@
   the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
   erase occurrences of forwarded message components (X).*)
 val analz_image_freshK_ss = 
-     !simpset delsimps [image_insert, image_Un]
+     !simpset addcongs [if_weak_cong]
+	      delsimps [image_insert, image_Un]
               addsimps ([image_insert RS sym, image_Un RS sym,
                          analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
                          insert_Key_singleton, subset_Compl_range,