# HG changeset patch
# User paulson
# Date 844178309 -7200
# Node ID d3b93e1765bce2f0f644687401260874d1b40c8a
# Parent  bb54fbba0071604208a1e7b4acde0a36049c982c
Moved sees_lost_agent_subset_sees_Spy to common file

diff -r bb54fbba0071 -r d3b93e1765bc src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Oct 01 15:49:29 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Oct 01 15:58:29 1996 +0200
@@ -178,12 +178,24 @@
 Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
 
 
-goal thy "!!K. newK evs = invKey K ==> newK evs = K";
-by (rtac (invKey_eq RS iffD1) 1);
-by (Simp_tac 1);
-val newK_invKey = result();
+(** Power of the Spy **)
 
-AddSDs [newK_invKey];
+(*The Spy can see more than anybody else, except for their initial state*)
+goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
+by (list.induct_tac "evs" 1);
+by (event.induct_tac "a" 2);
+by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
+                                addss (!simpset))));
+qed "sees_agent_subset_sees_Spy";
+
+(*The Spy can see more than anybody else who's lost their key!*)
+goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
+by (list.induct_tac "evs" 1);
+by (event.induct_tac "a" 2);
+by (agent.induct_tac "A" 1);
+by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+qed_spec_mp "sees_lost_agent_subset_sees_Spy";
+
 
 (** Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the analz_insert rules **)
@@ -235,7 +247,14 @@
                  |> standard;
 
 
-(** Specialized rewriting for  **)
+(*** Specialized rewriting for analz_insert_Key_newK ***)
+
+goal thy "!!K. newK evs = invKey K ==> newK evs = K";
+by (rtac (invKey_eq RS iffD1) 1);
+by (Simp_tac 1);
+val newK_invKey = result();
+
+AddSDs [newK_invKey];
 
 Delsimps [image_insert];
 Addsimps [image_insert RS sym];