# HG changeset patch
# User paulson
# Date 844763282 -7200
# Node ID 6ac12b9478d5d9e8e0e6ffb9ad1b46fdb45500ec
# Parent  0debdc018d262fc5840ba73fafc9fee4298d02fc
Put in the theorem Says_Crypt_not_lost

diff -r 0debdc018d26 -r 6ac12b9478d5 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Oct 08 10:27:31 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Oct 08 10:28:02 1996 +0200
@@ -9,6 +9,10 @@
 *)
 
 
+Addsimps [de_Morgan_conj, de_Morgan_disj, not_all, not_ex];
+(**Addsimps [all_conj_distrib, ex_disj_distrib];**)
+
+
 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
 by (excluded_middle_tac "P" 1);
 by (asm_simp_tac (!simpset addsimps prems) 1);
@@ -164,9 +168,6 @@
 by (Auto_tac ());
 qed_spec_mp "Says_imp_sees_Spy";
 
-Addsimps [Says_imp_sees_Spy];
-AddIs    [Says_imp_sees_Spy];
-
 goal thy  
  "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
 \           C   : lost |]                                         \
@@ -175,6 +176,14 @@
                       addss (!simpset)) 1);
 qed "Says_Crypt_lost";
 
+goal thy  
+ "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
+\           X ~: analz (sees lost Spy evs) |]                     \
+\        ==> C ~: lost";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+                      addss (!simpset)) 1);
+qed "Says_Crypt_not_lost";
+
 goal thy "initState lost C <= Key `` range shrK";
 by (agent.induct_tac "C" 1);
 by (Auto_tac ());