# HG changeset patch
# User paulson
# Date 846869258 -3600
# Node ID 913b4fc7670a0a95efbca2b424353457dba49c5c
# Parent  545ac77dab29cc9cb45137811be03cff7ced159a
New, purely illustrative result Crypt_synth_analz

diff -r 545ac77dab29 -r 913b4fc7670a src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Nov 01 15:46:56 1996 +0100
+++ b/src/HOL/Auth/Message.ML	Fri Nov 01 18:27:38 1996 +0100
@@ -414,9 +414,9 @@
   Effective, but can cause subgoals to blow up!
   Use with expand_if;  apparently split_tac does not cope with patterns
   such as "analz (insert (Crypt X K) H)" *)
-goal thy "analz (insert (Crypt X K) H) = \
-\         (if (Key (invKey K)  : analz H) then    \
-\               insert (Crypt X K) (analz (insert X H)) \
+goal thy "analz (insert (Crypt X K) H) =                \
+\         (if (Key (invKey K) : analz H)                \
+\          then insert (Crypt X K) (analz (insert X H)) \
 \          else insert (Crypt X K) (analz H))";
 by (case_tac "Key (invKey K)  : analz H " 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
@@ -698,6 +698,11 @@
 
 AddIffs [MPair_synth_analz];
 
+goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
+\              ==> (Crypt X K : synth (analz H)) = (X : synth (analz H))";
+by (Fast_tac 1);
+qed "Crypt_synth_analz";
+
 
 (*We do NOT want Crypt... messages broken up in protocols!!*)
 Delrules partsEs;