# HG changeset patch
# User paulson
# Date 844182461 -7200
# Node ID 1b3343fa1278663236c23f5533e5a195dfd93542
# Parent  d3b93e1765bce2f0f644687401260874d1b40c8a
Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm

diff -r d3b93e1765bc -r 1b3343fa1278 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Tue Oct 01 15:58:29 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Tue Oct 01 17:07:41 1996 +0200
@@ -40,26 +40,6 @@
 qed "ns_shared_mono";
 
 
-(*The Spy can see more than anybody else, except for their initial state*)
-goal thy 
- "!!evs. evs : ns_shared lost ==> \
-\     sees lost A evs <= initState lost A Un sees lost Spy evs";
-by (etac ns_shared.induct 1);
-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 
- "!!evs. evs : ns_shared lost ==> \
-\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
-by (etac ns_shared.induct 1);
-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";
-
-
 (*Nobody sends themselves messages*)
 goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set_of_list evs";
 by (etac ns_shared.induct 1);
@@ -393,10 +373,10 @@
  "!!evs. [| A ~: lost;  B ~: lost;  \
 \           evs : ns_shared lost;  evt: ns_shared lost |]  \
 \        ==> Says Server A                                             \
-\              (Crypt {|N, Agent B, Key(newK evt),                     \
-\                       Crypt {|Key(newK evt), Agent A|} (shrK B)|} (shrK A)) \
+\              (Crypt {|N, Agent B, Key K,                     \
+\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
 \             : set_of_list evs --> \
-\        Key(newK evt) ~: analz (sees lost Spy evs)";
+\        Key K ~: analz (sees lost Spy evs)";
 by (etac ns_shared.induct 1);
 by (ALLGOALS 
     (asm_simp_tac