# HG changeset patch
# User paulson
# Date 846146189 -7200
# Node ID 9677fdf5fc2332bf747d7c8c876057fae63f6c60
# Parent  959f791b6f0f9a647250e53709165b5876a50dab
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac

diff -r 959f791b6f0f -r 9677fdf5fc23 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Oct 24 10:33:27 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Oct 24 10:36:29 1996 +0200
@@ -118,6 +118,12 @@
 
 AddSIs [sees_own_shrK, Spy_sees_lost];
 
+(*Added for Yahalom/lost_tac*)
+goal thy "!!A. [| Crypt X (shrK A) : analz (sees lost Spy evs);  A: lost |] \
+\              ==> X : analz (sees lost Spy evs)";
+by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
+qed "Crypt_Spy_analz_lost";
+
 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
 
 goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
@@ -242,7 +248,8 @@
     ORELSE' etac FalseE;
 
 (*Analysis of Fake cases and of messages that forward unknown parts
-  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
+  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
+  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 fun spy_analz_tac i =
   SELECT_GOAL 
    (EVERY [  (*push in occurrences of X...*)
@@ -250,12 +257,12 @@
              (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
              (*...allowing further simplifications*)
            simp_tac (!simpset setloop split_tac [expand_if]) 1,
-           REPEAT (resolve_tac [impI,notI] 1),
+           REPEAT (resolve_tac [allI,impI,notI] 1),
            dtac (impOfSubs Fake_analz_insert) 1,
            eresolve_tac [asm_rl, synth.Inj] 1,
            Fast_tac 1,
            Asm_full_simp_tac 1,
-           IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
+           IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono]) 2 1)
            ]) i;
 
 
@@ -276,6 +283,7 @@
 val newK_invKey = result();
 
 AddSDs [newK_invKey];
+AddSDs [sym RS newK_invKey];
 
 Delsimps [image_insert];
 Addsimps [image_insert RS sym];
@@ -301,3 +309,6 @@
 qed "analz_image_newK_lemma";
 
 
+(*Useful in many uniqueness proofs*)
+fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
+