src/HOL/Auth/Shared.ML

 
 Theory of Shared Keys (common to all symmetric-key protocols)
 
 Server keys; initial states of agents; new nonces and keys; function "sees" 
 *)
+
+
+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);

 goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
 by (list.induct_tac "evs" 1);
 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 |]                                         \
 \        ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
                       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 ());
 qed "initState_subset";