New, purely illustrative result Crypt_synth_analz
authorpaulson
Fri Nov 01 18:27:38 1996 +0100 (1996-11-01)
changeset 2154913b4fc7670a
parent 2153 545ac77dab29
child 2155 dc85854810eb
New, purely illustrative result Crypt_synth_analz
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Nov 01 15:46:56 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Nov 01 18:27:38 1996 +0100
     1.3 @@ -414,9 +414,9 @@
     1.4    Effective, but can cause subgoals to blow up!
     1.5    Use with expand_if;  apparently split_tac does not cope with patterns
     1.6    such as "analz (insert (Crypt X K) H)" *)
     1.7 -goal thy "analz (insert (Crypt X K) H) = \
     1.8 -\         (if (Key (invKey K)  : analz H) then    \
     1.9 -\               insert (Crypt X K) (analz (insert X H)) \
    1.10 +goal thy "analz (insert (Crypt X K) H) =                \
    1.11 +\         (if (Key (invKey K) : analz H)                \
    1.12 +\          then insert (Crypt X K) (analz (insert X H)) \
    1.13  \          else insert (Crypt X K) (analz H))";
    1.14  by (case_tac "Key (invKey K)  : analz H " 1);
    1.15  by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
    1.16 @@ -698,6 +698,11 @@
    1.17  
    1.18  AddIffs [MPair_synth_analz];
    1.19  
    1.20 +goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
    1.21 +\              ==> (Crypt X K : synth (analz H)) = (X : synth (analz H))";
    1.22 +by (Fast_tac 1);
    1.23 +qed "Crypt_synth_analz";
    1.24 +
    1.25  
    1.26  (*We do NOT want Crypt... messages broken up in protocols!!*)
    1.27  Delrules partsEs;