# HG changeset patch
# User paulson
# Date 844677686 -7200
# Node ID b14a08bf61bf164ae679eb330108a48f08c94ad9
# Parent  275ef0f28e1f58f6852678d3466875ca66c17034
New theorem Crypt_Fake_parts_insert

diff -r 275ef0f28e1f -r b14a08bf61bf src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Mon Oct 07 10:40:51 1996 +0200
+++ b/src/HOL/Auth/Message.ML	Mon Oct 07 10:41:26 1996 +0200
@@ -654,6 +654,16 @@
 by (Deepen_tac 0 1);
 qed "Fake_parts_insert";
 
+goal thy
+     "!!H. [| Crypt Y K : parts (insert X H);  X: synth (analz G);  \
+\             Key K ~: analz G |]                                   \
+\          ==> Crypt Y K : parts G Un parts H";
+by (dtac (impOfSubs Fake_parts_insert) 1);
+ba 1;
+by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
+                      addss (!simpset)) 1);
+qed "Crypt_Fake_parts_insert";
+
 goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
 \              analz (insert X H) <= synth (analz H) Un analz H";
 by (rtac subsetI 1);