# HG changeset patch
# User paulson
# Date 866640209 -7200
# Node ID 0b804b390b0ed730f4b531b3c4a2ece5d7775c7b
# Parent  6d2887123fa03007432138b8e5f1c005671a8c65
Removed Says_Crypt_lost and Says_Crypt_not_lost.
Installed not_lost_tac

diff -r 6d2887123fa0 -r 0b804b390b0e src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Wed Jun 18 15:21:30 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Wed Jun 18 15:23:29 1997 +0200
@@ -77,11 +77,6 @@
 AddIffs [sees_pubK];
 AddSIs  [sees_own_priK, Spy_sees_lost];
 
-(*Added for Yahalom/lost_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
-\              ==> X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
-qed "Crypt_Spy_analz_lost";
 
 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
 
@@ -133,18 +128,23 @@
   items known to be fresh*)
 val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
 
-goal thy  
- "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
-\        ==> X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "Says_Crypt_lost";
+(*For not_lost_tac*)
+goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
+\              ==> X : analz (sees lost Spy evs)";
+by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
+qed "Crypt_Spy_analz_lost";
 
-goal thy  
- "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;        \
-\           X ~: analz (sees lost Spy evs) |]                     \
-\        ==> C ~: lost";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "Says_Crypt_not_lost";
+(*Prove that the agent is uncompromised by the confidentiality of 
+  a component of a message she's said.*)
+fun not_lost_tac s =
+    case_tac ("(" ^ s ^ ") : lost") THEN'
+    SELECT_GOAL 
+      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+       REPEAT_DETERM (etac MPair_analz 1) THEN
+       THEN_BEST_FIRST 
+         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
+         (has_fewer_prems 1, size_of_thm)
+         (Step_tac 1));
 
 Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
 Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)