Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
authorpaulson
Tue, 16 Sep 1997 13:54:41 +0200
changeset 3673 3b06747c3f37
parent 3672 56e4365a0c99
child 3674 65ec38fbb265
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification faster
src/HOL/Auth/Public.ML file | annotate | diff | comparison | revisions
src/HOL/Auth/Shared.ML file | annotate | diff | comparison | revisions 
--- 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, 
--- 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,
isabelle