# HG changeset patch
# User paulson
# Date 868877241 -7200
# Node ID ab0a9fbed4c027f2a2b6c9c2d459f5788486e4d4
# Parent  6e11c7bfb9c7d668646dcc23d7742db18f39e049
Changing "lost" from a parameter of protocol definitions to a constant.

Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
            less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
            theorem was never used, and its original proof was also broken
            the introduction of the "Notes" constructor.

diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Event.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -10,53 +10,55 @@
 
 open Event;
 
+AddIffs [Spy_in_lost, Server_not_lost];
+
 (*** Function "sees" ***)
 
-(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
+(** Specialized rewrite rules for (sees A (Says...#evs)) **)
 
-goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
+goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
 by (Simp_tac 1);
 qed "sees_own";
 
-goal thy "sees lost B (Notes A X # evs) = \
-\         (if A=B then insert X (sees lost B evs) else sees lost B evs)";
+goal thy "sees B (Notes A X # evs) = \
+\         (if A=B then insert X (sees B evs) else sees B evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 qed "sees_Notes";
 
-(** Three special-case rules for rewriting of sees lost A **)
+(** Three special-case rules for rewriting of sees A **)
 
 goal thy "!!A. Server ~= B ==> \
-\          sees lost Server (Says A B X # evs) = sees lost Server evs";
+\          sees Server (Says A B X # evs) = sees Server evs";
 by (Asm_simp_tac 1);
 qed "sees_Server";
 
 goal thy "!!A. Friend i ~= B ==> \
-\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
+\          sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
 by (Asm_simp_tac 1);
 qed "sees_Friend";
 
-goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
+goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
 by (Simp_tac 1);
 qed "sees_Spy";
 
-goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
+goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (Fast_tac 1);
 qed "sees_Says_subset_insert";
 
-goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
+goal thy "sees A evs <= sees A (Says A' B X # evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (Fast_tac 1);
 qed "sees_subset_sees_Says";
 
-goal thy "sees lost A evs <= sees lost A (Notes A' X # evs)";
+goal thy "sees A evs <= sees A (Notes A' X # evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (Fast_tac 1);
 qed "sees_subset_sees_Notes";
 
 (*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.*)
-goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
-\         parts {Y} Un (UN A. parts (sees lost A evs))";
+goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
+\         parts {Y} Un (UN A. parts (sees A evs))";
 by (Step_tac 1);
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
@@ -64,8 +66,8 @@
 				       setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
-goal thy "(UN A. parts (sees lost A (Notes B Y # evs))) = \
-\         parts {Y} Un (UN A. parts (sees lost A evs))";
+goal thy "(UN A. parts (sees A (Notes B Y # evs))) = \
+\         parts {Y} Un (UN A. parts (sees A evs))";
 by (Step_tac 1);
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
@@ -73,7 +75,7 @@
 				       setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Notes";
 
-goal thy "Says A B X : set evs --> X : sees lost Spy evs";
+goal thy "Says A B X : set evs --> X : sees Spy evs";
 by (list.induct_tac "evs" 1);
 by (Auto_tac ());
 qed_spec_mp "Says_imp_sees_Spy";
@@ -90,7 +92,7 @@
 
 (*** Fresh nonces ***)
 
-goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
+goalw thy [used_def] "!!X. X: parts (sees B evs) ==> X: used evs";
 by (etac (impOfSubs parts_mono) 1);
 by (Fast_tac 1);
 qed "usedI";
@@ -124,12 +126,12 @@
 qed "used_subset_append";
 
 
-(** Simplifying   parts (insert X (sees lost A evs))
-      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
+(** Simplifying   parts (insert X (sees A evs))
+      = parts {X} Un parts (sees A evs) -- since general case loops*)
 
 val parts_insert_sees = 
     parts_insert |> read_instantiate_sg (sign_of thy)
-                                        [("H", "sees lost A evs")]
+                                        [("H", "sees A evs")]
                  |> standard;
 
 
@@ -140,7 +142,7 @@
   it will omit complicated reasoning about analz.*)
 val analz_mono_contra_tac = 
   let val impI' = read_instantiate_sg (sign_of thy)
-                [("P", "?Y ~: analz (sees lost ?A ?evs)")] impI;
+                [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
   in
     rtac impI THEN' 
     REPEAT1 o 
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Event.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -11,7 +11,7 @@
 Event = Message + List + 
 
 consts  (*Initial states of agents -- parameter of the construction*)
-  initState :: [agent set, agent] => msg set
+  initState :: agent => msg set
 
 datatype  (*Messages--could add another constructor for agent knowledge*)
   event = Says  agent agent msg
@@ -26,17 +26,22 @@
   sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
 
 consts  
-  sees :: [agent set, agent, event list] => msg set
+  lost :: agent set        (*agents whose private keys have been compromised*)
+  sees :: [agent, event list] => msg set
+
+rules
+  (*Spy has access to his own key for spoof messages, but Server is secure*)
+  Spy_in_lost     "Spy: lost"
+  Server_not_lost "Server ~: lost"
 
 primrec sees list
-  sees_Nil  "sees lost A []       = initState lost A"
-  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-
+  sees_Nil  "sees A []       = initState A"
+  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
 
 constdefs
   (*Set of items that might be visible to somebody: complement of the set
         of fresh items*)
   used :: event list => msg set
-    "used evs == parts (UN lost B. sees lost B evs)"
+    "used evs == parts (UN B. sees B evs)"
 
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -908,8 +908,6 @@
 val Un_absorb3 = result();
 Addsimps [Un_absorb3];
 
-Addsimps [Un_insert_left, Un_insert_right];
-
 (*By default only o_apply is built-in.  But in the presence of eta-expansion
   this means that some terms displayed as (f o g) will be rewritten, and others
   will not!*)
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -5,8 +5,6 @@
 
 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
 Version incorporating Lowe's fix (inclusion of B's identify in round 2).
-
-PROOFS BELOW MIGHT BE SIMPLIFIED using Yahalom's analz_mono_parts_induct_tac 
 *)
 
 open NS_Public;
@@ -16,10 +14,6 @@
 
 AddIffs [Spy_in_lost];
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = 
-    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
@@ -41,27 +35,35 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*Induction for regularity theorems.  If induction formula has the form
+   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
+   needless information about analz (insert X (sees Spy evs))  *)
+fun parts_induct_tac i = 
+    etac ns_public.induct i
+    THEN 
+    REPEAT (FIRSTGOAL analz_mono_contra_tac)
+    THEN 
+    prove_simple_subgoals_tac i;
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's private key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : ns_public \
-\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac ns_public.induct 1);
-by (prove_simple_subgoals_tac 1);
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
 goal thy 
- "!!evs. evs : ns_public \
-\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_priK";
 Addsimps [Spy_analz_priK];
 
-goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
+goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
 \                  evs : ns_public |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
@@ -70,87 +72,79 @@
 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
 
 
+(**** Authenticity properties obtained from NS2 ****)
+
+(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
+  is secret.  (Honest users generate fresh nonces.)*)
+goal thy 
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);       \
+\           evs : ns_public |]                      \
+\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees Spy evs)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*NS3*)
+by (blast_tac (!claset addSEs partsEs) 3);
+(*NS2*)
+by (blast_tac (!claset addSEs partsEs) 2);
+by (Fake_parts_insert_tac 1);
+qed "no_nonce_NS1_NS2";
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+goal thy 
+ "!!evs. [| Nonce NA ~: analz (sees Spy evs);  evs : ns_public |]      \
+\ ==> EX A' B'. ALL A B.                                               \
+\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
+\      A=A' & B=B'";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+(*NS1*)
+by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+(*Fake*)
+by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (ex_strip_tac 1);
+by (Fake_parts_insert_tac 1);
+val lemma = result();
+
+goal thy 
+ "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees Spy evs); \
+\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);                            \
+\           evs : ns_public |]                                                \
+\        ==> A=A' & B=B'";
+by (prove_unique_tac lemma 1);
+qed "unique_NA";
+
+
+(*Tactic for proving secrecy theorems*)
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
               (!simpset addsimps [not_parts_not_analz]
                         setloop split_tac [expand_if]));
 
-(**** Authenticity properties obtained from NS2 ****)
-
-(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
-  is secret.  (Honest users generate fresh nonces.)*)
-goal thy 
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  \
-\           Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\           evs : ns_public |]                      \
-\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (!claset addSEs partsEs) 4);
-(*NS2*)
-by (blast_tac (!claset addSEs partsEs) 3);
-(*Fake*)
-by (blast_tac (!claset addSIs [analz_insertI]
-                        addDs [impOfSubs analz_subset_parts,
-			       impOfSubs Fake_parts_insert]) 2);
-(*Base*)
-by (Blast_tac 1);
-qed "no_nonce_NS1_NS2";
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy 
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  evs : ns_public |]      \
-\ ==> EX A' B'. ALL A B.                                                    \
-\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
-\      A=A' & B=B'";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS1*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NA = ?y" 3 THEN
-    REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
-(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [analz_insertI]) 1);
-by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
-                       addSDs [impOfSubs Fake_parts_insert]
-                       addDs  [impOfSubs analz_subset_parts]) 1);
-val lemma = result();
-
-goal thy 
- "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
-\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
-\           Nonce NA ~: analz (sees lost Spy evs);                            \
-\           evs : ns_public |]                                                \
-\        ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
  "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
-\        ==>  Nonce NA ~: analz (sees lost Spy evs)";
+\        ==>  Nonce NA ~: analz (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addDs  [Says_imp_sees_Spy RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
 by (blast_tac (!claset addSEs [MPair_parts]
-		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
+		       addDs  [Says_imp_sees_Spy RS parts.Inj,
 			       parts.Body, unique_NA]) 3);
 (*NS1*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
-                      addIs  [impOfSubs analz_subset_parts]) 2);
+                       addIs  [impOfSubs analz_subset_parts]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 qed "Spy_not_see_NA";
@@ -159,15 +153,15 @@
 (*Authentication for A: if she receives message 2 and has used NA
   to start a run, then B has sent message 2.*)
 goal thy 
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
-\             : set evs;                                               \
-\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
-\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
+\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
+\             : set evs;                                                \
+\           A ~: lost;  B ~: lost;  evs : ns_public |]                  \
+\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
 \              : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
@@ -180,19 +174,14 @@
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
 goal thy 
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\           Nonce NA ~: analz (sees lost Spy evs);                 \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);                 \
 \           evs : ns_public |]                                     \
 \   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
-                       addIs  [analz_insertI]
-                       addDs  [impOfSubs analz_subset_parts]) 2);
-(*Base*)
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
 qed "B_trusts_NS1";
 
 
@@ -203,33 +192,28 @@
   [unicity of B makes Lowe's fix work]
   [proof closely follows that for unique_NA] *)
 goal thy 
- "!!evs. [| Nonce NB ~: analz (sees lost Spy evs);  evs : ns_public |]      \
+ "!!evs. [| Nonce NB ~: analz (sees Spy evs);  evs : ns_public |]      \
 \ ==> EX A' NA' B'. ALL A NA B.                                             \
 \      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}                       \
-\        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & B=B'";
+\        : parts (sees Spy evs)  -->  A=A' & NA=NA' & B=B'";
 by (etac rev_mp 1);
-by (analz_induct_tac 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
 (*NS2*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NB = ?y" 3 THEN
-    REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
+by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
 (*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]) 1);
+by (Fake_parts_insert_tac 1);
 val lemma = result();
 
 goal thy 
  "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
-\             : parts(sees lost Spy evs);                    \
+\             : parts(sees Spy evs);                         \
 \           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
-\             : parts(sees lost Spy evs);                    \
-\           Nonce NB ~: analz (sees lost Spy evs);           \
+\             : parts(sees Spy evs);                         \
+\           Nonce NB ~: analz (sees Spy evs);                \
 \           evs : ns_public |]                               \
 \        ==> A=A' & NA=NA' & B=B'";
 by (prove_unique_tac lemma 1);
@@ -241,12 +225,11 @@
  "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
 \             : set evs;                                              \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                \
-\ ==> Nonce NB ~: analz (sees lost Spy evs)";
+\ ==> Nonce NB ~: analz (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
-			      unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
 (*NS1*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
@@ -254,7 +237,7 @@
 (*NS2*)
 by (Step_tac 1);
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
 qed "Spy_not_see_NB";
@@ -270,8 +253,8 @@
 \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
-by (analz_induct_tac 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (parts_induct_tac 1);
 (*NS1*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
 (*Fake*)
@@ -280,7 +263,7 @@
 			       impOfSubs analz_subset_parts]) 1);
 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
 			      Spy_not_see_NB, unique_NB]) 1);
 qed "B_trusts_NS3";
 
@@ -288,8 +271,8 @@
 (**** Overall guarantee for B*)
 
 (*Matches only NS2, not NS1 (or NS3)*)
-val Says_imp_sees_Spy'' = 
-    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
+val Says_imp_sees_Spy' = 
+    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy;
 
 
 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
@@ -302,7 +285,7 @@
 \    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*Fake, NS2, NS3*)
@@ -318,7 +301,7 @@
 (*NS3*)
 by (Step_tac 1);
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
                        addDs  [unique_NB]) 1);
 qed "B_trusts_protocol";
 
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -9,8 +9,7 @@
 
 NS_Public = Public + 
 
-consts  lost       :: agent set        (*No need for it to be a variable*)
-	ns_public  :: event list set
+consts  ns_public  :: event list set
 
 inductive ns_public
   intrs 
@@ -21,7 +20,7 @@
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
     Fake "[| evs: ns_public;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
+             X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
@@ -44,8 +43,4 @@
 
   (**Oops message??**)
 
-rules
-  (*Spy has access to his own key for spoof messages*)
-  Spy_in_lost "Spy: lost"
-
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -18,10 +18,6 @@
 
 AddIffs [Spy_in_lost];
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = 
-    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
@@ -43,27 +39,35 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*Induction for regularity theorems.  If induction formula has the form
+   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
+   needless information about analz (insert X (sees Spy evs))  *)
+fun parts_induct_tac i = 
+    etac ns_public.induct i
+    THEN 
+    REPEAT (FIRSTGOAL analz_mono_contra_tac)
+    THEN 
+    prove_simple_subgoals_tac i;
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's private key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : ns_public \
-\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac ns_public.induct 1);
-by (prove_simple_subgoals_tac 1);
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
 goal thy 
- "!!evs. evs : ns_public \
-\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_priK";
 Addsimps [Spy_analz_priK];
 
-goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
+goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
 \                  evs : ns_public |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
@@ -72,6 +76,55 @@
 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
 
 
+(**** Authenticity properties obtained from NS2 ****)
+
+(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
+  is secret.  (Honest users generate fresh nonces.)*)
+goal thy 
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);       \
+\           evs : ns_public |]                      \
+\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees Spy evs)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*NS3*)
+by (blast_tac (!claset addSEs partsEs) 3);
+(*NS2*)
+by (blast_tac (!claset addSEs partsEs) 2);
+by (Fake_parts_insert_tac 1);
+qed "no_nonce_NS1_NS2";
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+goal thy 
+ "!!evs. [| Nonce NA ~: analz (sees Spy evs);  evs : ns_public |]      \
+\ ==> EX A' B'. ALL A B.                                               \
+\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
+\      A=A' & B=B'";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+(*NS1*)
+by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+(*Fake*)
+by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (ex_strip_tac 1);
+by (Fake_parts_insert_tac 1);
+val lemma = result();
+
+goal thy 
+ "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees Spy evs); \
+\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);                            \
+\           evs : ns_public |]                                                \
+\        ==> A=A' & B=B'";
+by (prove_unique_tac lemma 1);
+qed "unique_NA";
+
+
+(*Tactic for proving secrecy theorems*)
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
@@ -79,77 +132,19 @@
                         setloop split_tac [expand_if]));
 
 
-(**** Authenticity properties obtained from NS2 ****)
-
-(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
-  is secret.  (Honest users generate fresh nonces.)*)
-goal thy 
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  \
-\           Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\           evs : ns_public |]                      \
-\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (!claset addSEs partsEs) 4);
-(*NS2*)
-by (blast_tac (!claset addSEs partsEs) 3);
-(*Fake*)
-by (blast_tac (!claset addSIs [analz_insertI]
-                        addDs [impOfSubs analz_subset_parts,
-			       impOfSubs Fake_parts_insert]) 2);
-(*Base*)
-by (Blast_tac 1);
-qed "no_nonce_NS1_NS2";
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy 
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  evs : ns_public |]      \
-\ ==> EX A' B'. ALL A B.                                                    \
-\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
-\      A=A' & B=B'";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS1*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NA = ?y" 3 THEN
-    REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
-(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [analz_insertI]) 1);
-by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
-                       addSDs [impOfSubs Fake_parts_insert]
-                       addDs  [impOfSubs analz_subset_parts]) 1);
-val lemma = result();
-
-goal thy 
- "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
-\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
-\           Nonce NA ~: analz (sees lost Spy evs);                            \
-\           evs : ns_public |]                                                \
-\        ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
-
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
  "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
-\        ==>  Nonce NA ~: analz (sees lost Spy evs)";
+\        ==>  Nonce NA ~: analz (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addDs  [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addDs  [Says_imp_sees_Spy RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
 by (blast_tac (!claset addSEs [MPair_parts]
-		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
+		       addDs  [Says_imp_sees_Spy RS parts.Inj,
 			       parts.Body, unique_NA]) 3);
 (*NS1*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
@@ -168,7 +163,7 @@
 \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
@@ -179,25 +174,20 @@
 			       impOfSubs analz_subset_parts]) 1);
 (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
 			      Spy_not_see_NA, unique_NA]) 1);
 qed "A_trusts_NS2";
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
 goal thy 
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\           Nonce NA ~: analz (sees lost Spy evs);                 \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\           Nonce NA ~: analz (sees Spy evs);                 \
 \           evs : ns_public |]                                     \
 \   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
-                       addIs  [analz_insertI]
-                       addDs  [impOfSubs analz_subset_parts]) 2);
-(*Base*)
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
 qed "B_trusts_NS1";
 
 
@@ -207,31 +197,26 @@
 (*Unicity for NS2: nonce NB identifies agent A and nonce NA
   [proof closely follows that for unique_NA] *)
 goal thy 
- "!!evs. [| Nonce NB ~: analz (sees lost Spy evs);  evs : ns_public |]      \
+ "!!evs. [| Nonce NB ~: analz (sees Spy evs);  evs : ns_public |]      \
 \ ==> EX A' NA'. ALL A NA.                                                  \
 \      Crypt (pubK A) {|Nonce NA, Nonce NB|}                                \
-\        : parts (sees lost Spy evs)  -->  A=A' & NA=NA'";
+\        : parts (sees Spy evs)  -->  A=A' & NA=NA'";
 by (etac rev_mp 1);
-by (analz_induct_tac 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
 (*NS2*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NB = ?y" 3 THEN
-    REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
+by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
 (*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]) 1);
+by (Fake_parts_insert_tac 1);
 val lemma = result();
 
 goal thy 
- "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(sees lost Spy evs); \
-\           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \
-\           Nonce NB ~: analz (sees lost Spy evs);                            \
+ "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(sees Spy evs); \
+\           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees Spy evs); \
+\           Nonce NB ~: analz (sees Spy evs);                            \
 \           evs : ns_public |]                                                \
 \        ==> A=A' & NA=NA'";
 by (prove_unique_tac lemma 1);
@@ -243,7 +228,7 @@
  "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;  \
 \          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);    \
 \          A ~: lost;  B ~: lost;  evs : ns_public |]                   \
-\       ==> Nonce NB ~: analz (sees lost Spy evs)";
+\       ==> Nonce NB ~: analz (sees Spy evs)";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
@@ -256,10 +241,10 @@
 by (step_tac (!claset delrules [allI]) 1);
 by (Blast_tac 5);
 (*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
 (*NS2*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
 qed "Spy_not_see_NB";
@@ -276,8 +261,8 @@
 \        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
-by (analz_induct_tac 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*NS1*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
@@ -287,7 +272,7 @@
 			       impOfSubs analz_subset_parts]) 1);
 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
 by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
 			      Spy_not_see_NB, unique_NB]) 1);
 qed "B_trusts_NS3";
 
@@ -296,11 +281,11 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]           \
 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
-\     --> Nonce NB ~: analz (sees lost Spy evs)";
+\     --> Nonce NB ~: analz (sees Spy evs)";
 by (analz_induct_tac 1);
 (*NS1*)
 by (blast_tac (!claset addSEs partsEs
-                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*NS2 and NS3*)
@@ -308,12 +293,12 @@
 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
 (*NS2*)
 by (blast_tac (!claset addSEs partsEs
-                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
 (*NS3*)
-by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
-    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
+by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy RS parts.Inj RS unique_NB) 1
+    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy RS parts.Inj] 1));
 by (Step_tac 1);
 
 (*
@@ -322,14 +307,14 @@
 !!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
        ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
            : set evs -->
-           Nonce NB ~: analz (sees lost Spy evs)
+           Nonce NB ~: analz (sees Spy evs)
  1. !!evs Aa Ba B' NAa NBa evsa.
        [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
           Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
           Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa;
           Ba : lost;
           Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
-          Nonce NB ~: analz (sees lost Spy evsa) |]
+          Nonce NB ~: analz (sees Spy evsa) |]
        ==> False
 *)
 
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -13,8 +13,7 @@
 
 NS_Public_Bad = Public + 
 
-consts  lost       :: agent set        (*No need for it to be a variable*)
-	ns_public  :: event list set
+consts  ns_public  :: event list set
 
 inductive ns_public
   intrs 
@@ -25,7 +24,7 @@
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
     Fake "[| evs: ns_public;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
+             X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
@@ -47,8 +46,4 @@
 
   (**Oops message??**)
 
-rules
-  (*Spy has access to his own key for spoof messages*)
-  Spy_in_lost "Spy: lost"
-
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -15,14 +15,11 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
-\        ==> EX N K. EX evs: ns_shared lost.          \
+\        ==> EX N K. EX evs: ns_shared.          \
 \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
@@ -34,7 +31,7 @@
 (**** Inductive proofs about ns_shared ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
 by (etac ns_shared.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -43,48 +40,46 @@
 
 (*For reasoning about the encrypted portion of message NS3*)
 goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
-\                ==> X : parts (sees lost Spy evs)";
+\                ==> X : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "NS3_msg_in_parts_sees_Spy";
                               
 goal thy
     "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
-\           ==> K : parts (sees lost Spy evs)";
+\           ==> K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "Oops_parts_sees_Spy";
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_induct_tac = 
-    etac ns_shared.induct 1  THEN 
-    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
-    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
-    prove_simple_subgoals_tac 1;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i = 
+    etac ns_shared.induct i  THEN 
+    forward_tac [Oops_parts_sees_Spy] (i+7)  THEN
+    dtac NS3_msg_in_parts_sees_Spy (i+4)     THEN
+    prove_simple_subgoals_tac i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : ns_shared lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : ns_shared \
+\        ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : ns_shared lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : ns_shared \
+\        ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : ns_shared lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : ns_shared |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -93,9 +88,9 @@
 
 
 (*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : ns_shared lost ==>      \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : ns_shared ==>      \
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -119,7 +114,7 @@
 goal thy 
  "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
 \             : set evs;                                      \
-\           evs : ns_shared lost |]                           \
+\           evs : ns_shared |]                           \
 \        ==> K ~: range shrK &                                \
 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
 \            K' = shrK A";
@@ -132,15 +127,15 @@
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
  "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
-\            : parts (sees lost Spy evs);                              \
-\           A ~: lost;  evs : ns_shared lost |]                        \
+\            : parts (sees Spy evs);                              \
+\           A ~: lost;  evs : ns_shared |]                        \
 \         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
 \             Says Server A                                            \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Auto_tac());
 qed "A_trusts_NS2";
@@ -151,11 +146,11 @@
   Use Says_Server_message_form if applicable.*)
 goal thy 
  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
-\            : set evs;          evs : ns_shared lost |]                   \
+\            : set evs;          evs : ns_shared |]                   \
 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
-\            | X : analz (sees lost Spy evs)";
+\            | X : analz (sees Spy evs)";
 by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
                       addss (!simpset)) 1);
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
 by (blast_tac (!claset addEs  partsEs
@@ -163,18 +158,18 @@
 qed "Says_S_message_form";
 
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
-    forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
-    forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
+    forward_tac [Says_Server_message_form] 8 THEN
+    forward_tac [Says_S_message_form] 5 THEN 
     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
 
 
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-  Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+  Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 
@@ -185,10 +180,10 @@
   to encrypt messages containing other keys, in the actual protocol.
   We require that agents should behave like this subsequently also.*)
 goal thy 
- "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
-\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
-\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
-by parts_induct_tac;
+ "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
+\           (Crypt KAB X) : parts (sees Spy evs) &      \
+\           Key K : parts {X} --> Key K : parts (sees Spy evs)";
+by (parts_induct_tac 1);
 (*Deals with Faked messages*)
 by (blast_tac (!claset addSEs partsEs
                        addDs [impOfSubs parts_insert_subset_Un]) 1);
@@ -201,10 +196,10 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : ns_shared lost ==>                                \
+ "!!evs. evs : ns_shared ==>                                \
 \  ALL K KK. KK <= Compl (range shrK) -->                        \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -219,9 +214,9 @@
 
 
 goal thy
- "!!evs. [| evs : ns_shared lost;  KAB ~: range shrK |] ==>     \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>     \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -229,7 +224,7 @@
 (** The session key K uniquely identifies the message **)
 
 goal thy 
- "!!evs. evs : ns_shared lost ==>                                        \
+ "!!evs. evs : ns_shared ==>                                        \
 \      EX A' NA' B' X'. ALL A NA B X.                                    \
 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
 \       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
@@ -254,7 +249,7 @@
 \           Says Server A'                                   \
 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
 \                  : set evs;                                \
-\           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
+\           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
 
@@ -262,13 +257,13 @@
 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared |]            \
 \        ==> Says Server A                                             \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set evs -->                                            \
 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
-\        Key K ~: analz (sees lost Spy evs)";
+\        Key K ~: analz (sees Spy evs)";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
 by (ALLGOALS 
@@ -287,7 +282,7 @@
 by (spy_analz_tac 1);
 (*NS3*) (**LEVEL 6 **)
 by (step_tac (!claset delrules [impCE]) 1);
-by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
+by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
 			      Crypt_Spy_analz_lost]) 1);
@@ -300,8 +295,8 @@
  "!!evs. [| Says Server A                                               \
 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
-\           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
-\        |] ==> Key K ~: analz (sees lost Spy evs)";
+\           A ~: lost;  B ~: lost;  evs : ns_shared                \
+\        |] ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSDs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -314,14 +309,14 @@
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
- "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
-\           B ~: lost;  evs : ns_shared lost |]                        \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees Spy evs); \
+\           B ~: lost;  evs : ns_shared |]                        \
 \         ==> EX NA. Says Server A                                     \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*Fake case*)
 by (ALLGOALS Blast_tac);
@@ -329,16 +324,16 @@
 
 
 goal thy
- "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
-\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
+ "!!evs. [| B ~: lost;  evs : ns_shared |]                        \
+\        ==> Key K ~: analz (sees Spy evs) -->                    \
 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
 \            : set evs -->                                             \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
+\            Crypt K (Nonce NB) : parts (sees Spy evs) -->        \
 \            Says B A (Crypt K (Nonce NB)) : set evs";
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
-by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
-by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
+by (forward_tac [Oops_parts_sees_Spy] 8);
 by (TRYALL (rtac impI));
 by (REPEAT_FIRST
     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
@@ -349,25 +344,25 @@
 by (Blast_tac 2);
 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
 (*Subgoal 1: contradiction from the assumptions  
-  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
+  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees Spy evsa) *)
 by (dtac Crypt_imp_invKey_keysFor 1);
 (**LEVEL 11**)
 by (Asm_full_simp_tac 1);
 by (rtac disjI1 1);
 by (thin_tac "?PP-->?QQ" 1);
 by (case_tac "Ba : lost" 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3, 
 			      unique_session_keys]) 2);
 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
 			      Crypt_Spy_analz_lost]) 1);
 val lemma = result();
 
 goal thy
- "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
+ "!!evs. [| Crypt K (Nonce NB) : parts (sees Spy evs);           \
 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
 \           : set evs;                                                \
 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
-\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
+\           A ~: lost;  B ~: lost;  evs : ns_shared |]           \
 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
 by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
                        addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -12,69 +12,69 @@
 
 NS_Shared = Shared + 
 
-consts  ns_shared   :: agent set => event list set
-inductive "ns_shared lost"
+consts  ns_shared   :: event list set
+inductive "ns_shared"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: ns_shared lost"
+    Nil  "[]: ns_shared"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: ns_shared lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X # evs : ns_shared lost"
+    Fake "[| evs: ns_shared;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X # evs : ns_shared"
 
          (*Alice initiates a protocol run, requesting to talk to any B*)
-    NS1  "[| evs: ns_shared lost;  A ~= Server;  Nonce NA ~: used evs |]
+    NS1  "[| evs: ns_shared;  A ~= Server;  Nonce NA ~: used evs |]
           ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
-                :  ns_shared lost"
+                :  ns_shared"
 
          (*Server's response to Alice's message.
            !! It may respond more than once to A's request !!
 	   Server doesn't know who the true sender is, hence the A' in
                the sender field.*)
-    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
+    NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
              Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
           ==> Says Server A 
                 (Crypt (shrK A)
                    {|Nonce NA, Agent B, Key KAB,
                      (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
-                # evs : ns_shared lost"
+                # evs : ns_shared"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
             Can inductively show A ~= Server*)
-    NS3  "[| evs: ns_shared lost;  A ~= B;
+    NS3  "[| evs: ns_shared;  A ~= B;
              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
                : set evs;
              Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
-          ==> Says A B X # evs : ns_shared lost"
+          ==> Says A B X # evs : ns_shared"
 
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
-    NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
+    NS4  "[| evs: ns_shared;  A ~= B;  Nonce NB ~: used evs;
              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
           ==> Says B A (Crypt K (Nonce NB)) # evs
-                : ns_shared lost"
+                : ns_shared"
 
          (*Alice responds with Nonce NB if she has seen the key before.
            Maybe should somehow check Nonce NA again.
            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
            Letting the Spy add or subtract 1 lets him send ALL nonces.
            Instead we distinguish the messages by sending the nonce twice.*)
-    NS5  "[| evs: ns_shared lost;  A ~= B;  
+    NS5  "[| evs: ns_shared;  A ~= B;  
              Says B' A (Crypt K (Nonce NB)) : set evs;
              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set evs |]
-          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
+          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared"
   
          (*This message models possible leaks of session keys.
            The two Nonces identify the protocol run: the rule insists upon
            the true senders in order to make them accurate.*)
-    Oops "[| evs: ns_shared lost;  A ~= Spy;
+    Oops "[| evs: ns_shared;  A ~= Spy;
              Says B A (Crypt K (Nonce NB)) : set evs;
              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared"
 
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -17,14 +17,11 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\        ==> EX K. EX NA. EX evs: otway lost.          \
+\        ==> EX K. EX NA. EX evs: otway.          \
 \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \                 : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -36,7 +33,7 @@
 (**** Inductive proofs about otway ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
 by (etac otway.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -47,17 +44,17 @@
 (** For reasoning about the encrypted portion of messages **)
 
 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\                ==> X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\                ==> X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR2_analz_sees_Spy";
 
 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\                ==> X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\                ==> X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\                 ==> K : parts (sees lost Spy evs)";
+\                 ==> K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "Oops_parts_sees_Spy";
 
@@ -71,42 +68,36 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_induct_tac = 
-    let val tac = forw_inst_tac [("lost","lost")] 
-    in  etac otway.induct	   1 THEN 
-	tac OR2_parts_sees_Spy     4 THEN 
-        tac OR4_parts_sees_Spy     6 THEN
-        tac Oops_parts_sees_Spy    7 THEN
-	prove_simple_subgoals_tac  1
-    end;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i = 
+    etac otway.induct i			THEN 
+    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
+    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
+    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
+    prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : otway lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : otway lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : otway lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : otway |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -115,9 +106,9 @@
 
 
 (*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway lost ==>          \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : otway ==>          \
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -140,9 +131,8 @@
 (*Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.*)
 goal thy 
- "!!evs. [| Says Server B                                                 \
-\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
-\           evs : otway lost |]                                           \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\           evs : otway |]                                           \
 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -151,11 +141,11 @@
 qed "Says_Server_message_form";
 
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
-    dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
-    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+    dtac OR2_analz_sees_Spy 4 THEN 
+    dtac OR4_analz_sees_Spy 6 THEN
+    forward_tac [Says_Server_message_form] 7 THEN
     assume_tac 7 THEN
     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
 
@@ -163,8 +153,8 @@
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-  Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+  Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -174,10 +164,10 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway lost ==>                                    \
-\  ALL K KK. KK <= Compl (range shrK) -->                        \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : otway ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                   \
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -191,9 +181,9 @@
 
 
 goal thy
- "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -201,7 +191,7 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway lost ==>                                             \
+ "!!evs. evs : otway ==>                                                  \
 \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
@@ -223,7 +213,7 @@
 \            : set evs;                                            \ 
 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
 \            : set evs;                                            \
-\           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
+\           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
 
@@ -233,13 +223,13 @@
 
 (*Only OR1 can have caused such a part of a message to appear.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]                        \
+ "!!evs. [| A ~: lost;  evs : otway |]                             \
 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
-\             : parts (sees lost Spy evs) -->                      \
+\             : parts (sees Spy evs) -->                           \
 \            Says A B {|NA, Agent A, Agent B,                      \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
@@ -247,11 +237,11 @@
 (** The Nonce NA uniquely identifies A's message. **)
 
 goal thy 
- "!!evs. [| evs : otway lost; A ~: lost |]               \
-\ ==> EX B'. ALL B.                                      \
-\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
+ "!!evs. [| evs : otway; A ~: lost |]               \
+\ ==> EX B'. ALL B.                                 \
+\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
 \        --> B = B'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR1: creation of new Nonce.  Move assertion into global context*)
@@ -260,9 +250,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
-\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
-\          evs : otway lost;  A ~: lost |]                                    \
+ "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
+\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
+\          evs : otway;  A ~: lost |]                                     \
 \        ==> B = C";
 by (prove_unique_tac lemma 1);
 qed "unique_NA";
@@ -272,12 +262,12 @@
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   over-simplified version of this protocol: see OtwayRees_Bad.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]                      \
-\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
-\             : parts (sees lost Spy evs) -->                    \
-\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
-\             ~: parts (sees lost Spy evs)";
-by parts_induct_tac;
+ "!!evs. [| A ~: lost;  evs : otway |]                      \
+\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}        \
+\             : parts (sees Spy evs) -->                    \
+\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
+\             ~: parts (sees Spy evs)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
                                addSDs  [impOfSubs parts_insert_subset_Un]) 1));
@@ -287,8 +277,8 @@
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
-\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
+\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
 \             : set evs -->                                            \
@@ -297,7 +287,7 @@
 \                   Crypt (shrK A) {|NA, Key K|},                      \
 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
 \                   : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
@@ -311,10 +301,10 @@
 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
 by (blast_tac (!claset addSEs [MPair_parts]
-                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                      addSDs [Says_imp_sees_Spy RS parts.Inj]
                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                       addSEs [MPair_parts]
                       addIs  [unique_NA]) 1);
 qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -330,7 +320,7 @@
 \           Says A B {|NA, Agent A, Agent B,                       \
 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
 \            : set evs;                                            \
-\           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
+\           A ~: lost;  A ~= Spy;  evs : otway |]                  \
 \        ==> EX NB. Says Server B                                  \
 \                     {|NA,                                        \
 \                       Crypt (shrK A) {|NA, Key K|},              \
@@ -346,12 +336,12 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
-\        ==> Says Server B                                                 \
-\              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->              \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
-\            Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
+\        ==> Says Server B                                            \
+\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
+\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
+\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
+\            Key K ~: analz (sees Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -371,12 +361,12 @@
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 goal thy 
- "!!evs. [| Says Server B                                                \
-\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
-\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| Says Server B                                           \
+\            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
+\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
+\           A ~: lost;  B ~: lost;  evs : otway |]                  \
+\        ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -387,14 +377,14 @@
 (*Only OR2 can have caused such a part of a message to appear.  We do not
   know anything about X: it does NOT have to have the right form.*)
 goal thy 
- "!!evs. [| B ~: lost;  evs : otway lost |]                    \
+ "!!evs. [| B ~: lost;  evs : otway |]                         \
 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
-\             : parts (sees lost Spy evs) -->                  \
+\             : parts (sees Spy evs) -->                       \
 \            (EX X. Says B Server                              \
 \             {|NA, Agent A, Agent B, X,                       \
 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
 \             : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -403,11 +393,11 @@
 (** The Nonce NB uniquely identifies B's  message. **)
 
 goal thy 
- "!!evs. [| evs : otway lost; B ~: lost |]               \
+ "!!evs. [| evs : otway; B ~: lost |]                    \
 \ ==> EX NA' A'. ALL NA A.                               \
-\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
+\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
 \      --> NA = NA' & A = A'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR2: creation of new Nonce.  Move assertion into global context*)
@@ -417,10 +407,10 @@
 
 goal thy 
  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\                  : parts(sees lost Spy evs);         \
+\                  : parts(sees Spy evs);         \
 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
-\                  : parts(sees lost Spy evs);         \
-\          evs : otway lost;  B ~: lost |]             \
+\                  : parts(sees Spy evs);         \
+\          evs : otway;  B ~: lost |]             \
 \        ==> NC = NA & C = A";
 by (prove_unique_tac lemma 1);
 qed "unique_NB";
@@ -429,8 +419,8 @@
 (*If the encrypted message appears, and B has used Nonce NB,
   then it originated with the Server!*)
 goal thy 
- "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
-\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
+ "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway |]                        \
+\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs)             \
 \        --> (ALL X'. Says B Server                                      \
 \                       {|NA, Agent A, Agent B, X',                      \
 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
@@ -439,7 +429,7 @@
 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
 \                   : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
@@ -448,11 +438,11 @@
 (*OR3*)
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                        addSEs [MPair_parts]
                        addDs  [unique_NB]) 2);
 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
-                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
+                       addSDs [Says_imp_sees_Spy RS parts.Inj]
                        delrules [conjI, impCE] (*stop split-up*)) 1);
 qed_spec_mp "NB_Crypt_imp_Server_msg";
 
@@ -460,7 +450,7 @@
 (*Guarantee for B: if it gets a message with matching NB then the Server
   has sent the correct message.*)
 goal thy 
- "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
+ "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway;                    \
 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
 \            : set evs;                                            \
 \           Says B Server {|NA, Agent A, Agent B, X',              \
@@ -480,16 +470,16 @@
 
 
 goal thy 
- "!!evs. [| B ~: lost;  evs : otway lost |]                           \
-\        ==> Says Server B                                            \
-\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
-\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
-\            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
+ "!!evs. [| B ~: lost;  evs : otway |]                           \
+\        ==> Says Server B                                       \
+\              {|NA, Crypt (shrK A) {|NA, Key K|},               \
+\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
+\            (EX X. Says B Server {|NA, Agent A, Agent B, X,     \
 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \            : set evs)";
 by (etac otway.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
 		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
 by (ALLGOALS Blast_tac);
 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -502,7 +492,7 @@
  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
 \           Says A B {|NA, Agent A, Agent B,                                \
 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |]          \
+\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway |]               \
 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
 \            : set evs";
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -14,40 +14,40 @@
 
 OtwayRees = Shared + 
 
-consts  otway   :: agent set => event list set
-inductive "otway lost"
+consts  otway   :: event list set
+inductive "otway"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: otway lost"
+    Nil  "[]: otway"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : otway lost"
+    Fake "[| evs: otway;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
+    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
-                 # evs : otway lost"
+                 # evs : otway"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.
            Note that NB is encrypted.*)
-    OR2  "[| evs: otway lost;  B ~= Server;  Nonce NB ~: used evs;
+    OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, 
                     Crypt (shrK B)
                       {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
-                 # evs : otway lost"
+                 # evs : otway"
 
          (*The Server receives Bob's message and checks that the three NAs
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
-    OR3  "[| evs: otway lost;  B ~= Server;  Key KAB ~: used evs;
+    OR3  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
@@ -57,24 +57,24 @@
                   {|Nonce NA, 
                     Crypt (shrK A) {|Nonce NA, Key KAB|},
                     Crypt (shrK B) {|Nonce NB, Key KAB|}|}
-                 # evs : otway lost"
+                 # evs : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway lost;  A ~= B;  
+    OR4  "[| evs: otway;  A ~= B;  
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set evs;
              Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs |]
-          ==> Says B A {|Nonce NA, X|} # evs : otway lost"
+          ==> Says B A {|Nonce NA, X|} # evs : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
-    Oops "[| evs: otway lost;  B ~= Spy;
+    Oops "[| evs: otway;  B ~= Spy;
              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
 
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -21,7 +21,7 @@
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
-\        ==> EX K. EX NA. EX evs: otway lost.                                 \
+\        ==> EX K. EX NA. EX evs: otway.                                 \
 \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \             : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -33,7 +33,7 @@
 (**** Inductive proofs about otway ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
 by (etac otway.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -44,12 +44,12 @@
 (** For reasoning about the encrypted portion of messages **)
 
 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
-\                X : analz (sees lost Spy evs)";
+\                X : analz (sees Spy evs)";
 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\                  : set evs ==> K : parts (sees lost Spy evs)";
+\                  : set evs ==> K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "Oops_parts_sees_Spy";
 
@@ -60,40 +60,34 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_induct_tac = 
-    let val tac = forw_inst_tac [("lost","lost")] 
-    in  etac otway.induct	   1 THEN 
-        tac OR4_parts_sees_Spy     6 THEN
-        tac Oops_parts_sees_Spy    7 THEN
-	prove_simple_subgoals_tac  1
-    end;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i = 
+    etac otway.induct i			THEN 
+    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
+    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
+    prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : otway lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : otway lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : otway lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : otway |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -102,9 +96,9 @@
 
 
 (*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway lost ==>          \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : otway ==>          \
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -131,7 +125,7 @@
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
 \             : set evs;                                            \
-\           evs : otway lost |]                                     \
+\           evs : otway |]                                     \
 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -140,10 +134,10 @@
 qed "Says_Server_message_form";
 
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
-    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+    dtac OR4_analz_sees_Spy 6 THEN
+    forward_tac [Says_Server_message_form] 7 THEN
     assume_tac 7 THEN
     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
 
@@ -151,8 +145,8 @@
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-  Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+  Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -162,10 +156,10 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway lost ==>                                    \
-\  ALL K KK. KK <= Compl (range shrK) -->                        \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : otway ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                   \
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -179,9 +173,9 @@
 
 
 goal thy
- "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -189,7 +183,7 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway lost ==>                              \
+ "!!evs. evs : otway ==>                                   \
 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
 \       Says Server B                                      \
 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
@@ -218,7 +212,7 @@
 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
 \           : set evs;                                             \
-\          evs : otway lost |]                                     \
+\          evs : otway |]                                          \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -229,14 +223,14 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]                 \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
-\      : parts (sees lost Spy evs)                          \
+ "!!evs. [| A ~: lost;  evs : otway |]                 \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}   \
+\      : parts (sees Spy evs)                          \
 \     --> (EX NB. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*OR3*)
@@ -249,7 +243,7 @@
 goal thy 
  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \            : set evs;                                                 \
-\           A ~: lost;  evs : otway lost |]                             \
+\           A ~: lost;  evs : otway |]                                  \
 \        ==> EX NB. Says Server B                                       \
 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -264,13 +258,13 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
 \        ==> Says Server B                                                 \
 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
 \            : set evs -->                                                 \
 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
-\            Key K ~: analz (sees lost Spy evs)";
+\            Key K ~: analz (sees Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -295,8 +289,8 @@
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
 \             : set evs;                                            \
 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
-\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+\           A ~: lost;  B ~: lost;  evs : otway |]                  \
+\        ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -306,14 +300,14 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
- "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
-\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
-\         : parts (sees lost Spy evs)                                       \
+ "!!evs. [| B ~: lost;  evs : otway |]                                 \
+\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                \
+\         : parts (sees Spy evs)                                       \
 \        --> (EX NA. Says Server B                                          \
 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 (*OR3*)
@@ -324,7 +318,7 @@
 (*Guarantee for B: if it gets a well-formed certificate then the Server
   has sent the correct message in round 3.*)
 goal thy 
- "!!evs. [| B ~: lost;  evs : otway lost;                                   \
+ "!!evs. [| B ~: lost;  evs : otway;                                        \
 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \            : set evs |]                                                   \
 \        ==> EX NA. Says Server B                                           \
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -19,55 +19,55 @@
 
 OtwayRees_AN = Shared + 
 
-consts  otway   :: agent set => event list set
-inductive "otway lost"
+consts  otway   :: event list set
+inductive "otway"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: otway lost"
+    Nil  "[]: otway"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : otway lost"
+    Fake "[| evs: otway;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
-          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost"
+    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
+          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
-    OR2  "[| evs: otway lost;  B ~= Server;
+    OR2  "[| evs: otway;  B ~= Server;
              Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
-                 # evs : otway lost"
+                 # evs : otway"
 
          (*The Server receives Bob's message.  Then he sends a new
            session key to Bob with a packet for forwarding to Alice.*)
-    OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
+    OR3  "[| evs: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set evs |]
           ==> Says Server B 
                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
-              # evs : otway lost"
+              # evs : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway lost;  A ~= B;
+    OR4  "[| evs: otway;  A ~= B;
              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
              Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                : set evs |]
-          ==> Says B A X # evs : otway lost"
+          ==> Says B A X # evs : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  B is not assumed to know shrK A.*)
-    Oops "[| evs: otway lost;  B ~= Spy;
+    Oops "[| evs: otway;  B ~= Spy;
              Says Server B 
                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
                : set evs |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
 
 end
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -20,9 +20,6 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = 
-    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
@@ -50,17 +47,17 @@
 (** For reasoning about the encrypted portion of messages **)
 
 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
-\                X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\                X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR2_analz_sees_Spy";
 
 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
-\                X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\                X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\                 ==> K : parts (sees lost Spy evs)";
+\                 ==> K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
 qed "Oops_parts_sees_Spy";
 
@@ -74,36 +71,34 @@
 bind_thm ("OR4_parts_sees_Spy",
           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-val parts_induct_tac = 
-    etac otway.induct 1 THEN 
-    forward_tac [OR2_parts_sees_Spy] 4 THEN 
-    forward_tac [OR4_parts_sees_Spy] 6 THEN
-    forward_tac [Oops_parts_sees_Spy] 7 THEN
-    prove_simple_subgoals_tac 1;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i = 
+    etac otway.induct i			THEN 
+    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
+    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
+    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
+    prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : otway \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : otway \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
 \                  evs : otway |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
@@ -114,8 +109,8 @@
 
 (*Nobody can have used non-existent keys!*)
 goal thy "!!evs. evs : otway ==>          \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
@@ -161,8 +156,8 @@
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-  Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+  Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -172,10 +167,10 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway ==>                                         \
-\  ALL K KK. KK <= Compl (range shrK) -->                        \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : otway ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                   \
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -189,9 +184,9 @@
 
 
 goal thy
- "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>              \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -231,7 +226,7 @@
 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
-\            Key K ~: analz (sees lost Spy evs)";
+\            Key K ~: analz (sees Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -256,7 +251,7 @@
 \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
 \           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : otway |]                \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+\        ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -271,10 +266,10 @@
 goal thy 
  "!!evs. [| A ~: lost;  A ~= B;  evs : otway |]                \
 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
-\             : parts (sees lost Spy evs) -->                  \
+\             : parts (sees Spy evs) -->                       \
 \            Says A B {|NA, Agent A, Agent B,                  \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
@@ -285,16 +280,16 @@
 (*Only it is FALSE.  Somebody could make a fake message to Server
           substituting some other nonce NA' for NB.*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                         \
-\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
-\            Says A B {|NA, Agent A, Agent B,                      \
-\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
-\             : set evs -->                                    \
-\            (EX B NB. Says Server B                           \
-\                 {|NA,                                        \
-\                   Crypt (shrK A) {|NA, Key K|},              \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                    \
+\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) --> \
+\            Says A B {|NA, Agent A, Agent B,                        \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
+\             : set evs -->                                          \
+\            (EX B NB. Says Server B                                 \
+\                 {|NA,                                              \
+\                   Crypt (shrK A) {|NA, Key K|},                    \
 \                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (blast_tac (!claset addSIs [parts_insertI]
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -12,8 +12,7 @@
 
 OtwayRees_Bad = Shared + 
 
-consts  lost    :: agent set        (*No need for it to be a variable*)
-	otway   :: event list set
+consts  otway   :: event list set
 
 inductive otway
   intrs 
@@ -23,7 +22,7 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (sees lost Spy evs)) |]
+    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -37,7 +37,7 @@
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
-goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
+goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
 by (agent.induct_tac "C" 1);
 by (auto_tac (!claset addIs [range_eqI], !simpset));
 qed "keysFor_parts_initState";
@@ -47,22 +47,22 @@
 (*** Function "sees" ***)
 
 (*Agents see their own private keys!*)
-goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
+goal thy "A ~= Spy --> Key (priK A) : sees A evs";
 by (list.induct_tac "evs" 1);
 by (agent.induct_tac "A" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 qed_spec_mp "sees_own_priK";
 
 (*All public keys are visible to all*)
-goal thy "Key (pubK A) : sees lost B evs";
+goal thy "Key (pubK A) : sees B evs";
 by (list.induct_tac "evs" 1);
 by (agent.induct_tac "B" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Auto_tac ());
 qed_spec_mp "sees_pubK";
 
-(*Spy sees private keys of lost agents!*)
-goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs";
+(*Spy sees private keys of agents!*)
+goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
 by (list.induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
@@ -73,8 +73,8 @@
 
 
 (*For not_lost_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
-\              ==> X : analz (sees lost Spy evs)";
+goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs);  A: lost |] \
+\              ==> X : analz (sees Spy evs)";
 by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
 qed "Crypt_Spy_analz_lost";
 
@@ -93,7 +93,7 @@
 
 (*** Fresh nonces ***)
 
-goal thy "Nonce N ~: parts (initState lost B)";
+goal thy "Nonce N ~: parts (initState B)";
 by (agent.induct_tac "B" 1);
 by (Auto_tac ());
 qed "Nonce_notin_initState";
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Public.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -21,11 +21,11 @@
 
 primrec initState agent
         (*Agents know their private key and all public keys*)
-  initState_Server  "initState lost Server     =    
+  initState_Server  "initState Server     =    
  		         insert (Key (priK Server)) (Key `` range pubK)"
-  initState_Friend  "initState lost (Friend i) =    
+  initState_Friend  "initState (Friend i) =    
  		         insert (Key (priK (Friend i))) (Key `` range pubK)"
-  initState_Spy     "initState lost Spy        =    
+  initState_Spy     "initState Spy        =    
  		         (Key``invKey``pubK``lost) Un (Key `` range pubK)"
 
 
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -22,7 +22,7 @@
 (*Simplest case: Alice goes directly to the server*)
 goal thy
  "!!A. A ~= Server                                                      \
-\ ==> EX K NA. EX evs: recur lost.                                      \
+\ ==> EX K NA. EX evs: recur.                                      \
 \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
 \                     Agent Server|}  : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -35,7 +35,7 @@
 (*Case two: Alice, Bob and the server*)
 goal thy
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
-\ ==> EX K. EX NA. EX evs: recur lost.                          \
+\ ==> EX K. EX NA. EX evs: recur.                          \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
 \                  Agent Server|}  : set evs";
 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
@@ -54,7 +54,7 @@
   TOO SLOW to run every time!
 goal thy
  "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
-\ ==> EX K. EX NA. EX evs: recur lost.                                 \
+\ ==> EX K. EX NA. EX evs: recur.                                 \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
 \                  Agent Server|}  : set evs";
 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
@@ -75,7 +75,7 @@
 (**** Inductive proofs about recur ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
 by (etac recur.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -115,7 +115,7 @@
 val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
 
 goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
-\                ==> RA : analz (sees lost Spy evs)";
+\                ==> RA : analz (sees Spy evs)";
 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "RA4_analz_sees_Spy";
 
@@ -129,30 +129,25 @@
 bind_thm ("RA4_parts_sees_Spy",
           RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_induct_tac = 
-    let val tac = forw_inst_tac [("lost","lost")] 
-    in  etac recur.induct      1	      THEN
-	tac RA2_parts_sees_Spy 4              THEN
-        etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
-        forward_tac [respond_imp_responses] 5 THEN
-        tac RA4_parts_sees_Spy 6	      THEN
-	prove_simple_subgoals_tac 1
-    end;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i = 
+    etac recur.induct i				THEN
+    forward_tac [RA2_parts_sees_Spy] (i+3)	THEN
+    etac subst (i+3) (*RA2: DELETE needless definition of PA!*)  THEN
+    forward_tac [respond_imp_responses] (i+4)	THEN
+    forward_tac [RA4_parts_sees_Spy] (i+5)	THEN
+    prove_simple_subgoals_tac i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 
-(** Spy never sees another agent's long-term key (unless initially lost) **)
+(** Spy never sees another agent's shared key! (unless it's lost at start) **)
 
 goal thy 
- "!!evs. evs : recur lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : recur ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
@@ -164,14 +159,13 @@
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : recur lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : recur ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : recur lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : recur |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -191,9 +185,9 @@
 qed_spec_mp "Key_in_keysFor_parts";
 
 
-goal thy "!!evs. evs : recur lost ==>          \
-\       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : recur ==>          \
+\                Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*RA3*)
 by (best_tac (!claset addDs  [Key_in_keysFor_parts]
 	      addss  (!simpset addsimps [parts_insert_sees])) 2);
@@ -216,18 +210,18 @@
 
 (*** Proofs involving analz ***)
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
     etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
-    dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
+    dtac RA2_analz_sees_Spy 4 THEN 
     forward_tac [respond_imp_responses] 5                THEN
-    dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
+    dtac RA4_analz_sees_Spy 6;
 
 
 (** Session keys are not used to encrypt other session keys **)
 
 (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
-  Note that it holds for *any* set H (not just "sees lost Spy evs")
+  Note that it holds for *any* set H (not just "sees Spy evs")
   satisfying the inductive hypothesis.*)
 goal thy  
  "!!evs. [| RB : responses evs;                             \
@@ -243,10 +237,10 @@
 
 (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
 goal thy  
- "!!evs. evs : recur lost ==>                                   \
-\  ALL K KK. KK <= Compl (range shrK) -->                       \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : recur ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                   \
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac recur.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -262,30 +256,30 @@
 qed_spec_mp "analz_image_freshK";
 
 
-(*Instance of the lemma with H replaced by (sees lost Spy evs):
-   [| RB : responses evs;  evs : recur lost; |]
+(*Instance of the lemma with H replaced by (sees Spy evs):
+   [| RB : responses evs;  evs : recur; |]
    ==> KK <= Compl (range shrK) --> 
-       Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
-       (K : KK | Key K : analz (insert RB (sees lost Spy evs))) 
+       Key K : analz (insert RB (Key``KK Un sees Spy evs)) =
+       (K : KK | Key K : analz (insert RB (sees Spy evs))) 
 *)
 bind_thm ("resp_analz_image_freshK",
           raw_analz_image_freshK RSN
             (2, resp_analz_image_freshK_lemma) RS spec RS spec);
 
 goal thy
- "!!evs. [| evs : recur lost;  KAB ~: range shrK |] ==>              \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =      \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =      \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
 
 (*Everything that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees lost Spy evs);  \
-\                   evs : recur lost;  A ~: lost |]                       \
-\                ==> X : parts (sees lost Spy evs)";
+goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees Spy evs);  \
+\                   evs : recur;  A ~: lost |]                       \
+\                ==> X : parts (sees Spy evs)";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 (*RA3 requires a further induction*)
 by (etac responses.induct 2);
 by (ALLGOALS Asm_simp_tac);
@@ -302,11 +296,11 @@
 **)
 
 goal thy 
- "!!evs. [| evs : recur lost; A ~: lost |]                   \
+ "!!evs. [| evs : recur; A ~: lost |]                   \
 \ ==> EX B' P'. ALL B P.                                     \
-\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
+\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees Spy evs) \
 \          -->  B=B' & P=P'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (etac responses.induct 3);
 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
@@ -319,9 +313,9 @@
 val lemma = result();
 
 goalw thy [HPair_def]
- "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(sees lost Spy evs); \
-\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees lost Spy evs); \
-\        evs : recur lost;  A ~: lost |]                                     \
+ "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(sees Spy evs); \
+\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees Spy evs); \
+\        evs : recur;  A ~: lost |]                                     \
 \      ==> B=B' & P=P'";
 by (REPEAT (eresolve_tac partsEs 1));
 by (prove_unique_tac lemma 1);
@@ -333,8 +327,8 @@
 ***)
 
 goal thy
- "!!evs. [| RB : responses evs;  evs : recur lost |] \
-\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
+ "!!evs. [| RB : responses evs;  evs : recur |] \
+\ ==> (Key (shrK B) : analz (insert RB (sees Spy evs))) = (B:lost)";
 by (etac responses.induct 1);
 by (ALLGOALS
     (asm_simp_tac 
@@ -368,7 +362,7 @@
 (*The Server does not send such messages.  This theorem lets us avoid
   assuming B~=Server in RA4.*)
 goal thy 
- "!!evs. evs : recur lost \
+ "!!evs. evs : recur \
 \        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
 by (etac recur.induct 1);
 by (etac (respond.induct) 5);
@@ -399,8 +393,8 @@
 by (expand_case_tac "K = KBC" 1);
 by (dtac respond_Key_in_parts 1);
 by (blast_tac (!claset addSIs [exI]
-                      addSEs partsEs
-                      addDs [Key_in_parts_respond]) 1);
+                       addSEs partsEs
+                       addDs [Key_in_parts_respond]) 1);
 by (expand_case_tac "K = KAB" 1);
 by (REPEAT (ares_tac [exI] 2));
 by (ex_strip_tac 1);
@@ -422,10 +416,10 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur lost |]         \
+ "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
 \        ==> ALL A A' N. A ~: lost & A' ~: lost -->                 \
 \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
-\            Key K ~: analz (insert RB (sees lost Spy evs))";
+\            Key K ~: analz (insert RB (sees Spy evs))";
 by (etac respond.induct 1);
 by (forward_tac [respond_imp_responses] 2);
 by (forward_tac [respond_imp_not_used] 2);
@@ -450,10 +444,10 @@
 
 
 goal thy
- "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}          \
-\              : parts (sees lost Spy evs);                \
-\           A ~: lost;  A' ~: lost;  evs : recur lost |]   \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}     \
+\              : parts (sees Spy evs);                \
+\           A ~: lost;  A' ~: lost;  evs : recur |]   \
+\        ==> Key K ~: analz (sees Spy evs)";
 by (etac rev_mp 1);
 by (etac recur.induct 1);
 by analz_sees_tac;
@@ -499,11 +493,11 @@
   used to prove B's presence to A at the run's conclusion.*)
 goalw thy [HPair_def]
  "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
-\             : parts (sees lost Spy evs);                        \
-\            A ~: lost;  evs : recur lost |]                      \
+\             : parts (sees Spy evs);                        \
+\            A ~: lost;  evs : recur |]                      \
 \     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*RA3*)
 by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
@@ -516,12 +510,12 @@
 
 (*Certificates can only originate with the Server.*)
 goal thy 
- "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
-\           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
-\        ==> EX C RC. Says Server C RC : set evs  &          \
+ "!!evs. [| Crypt (shrK A) Y : parts (sees Spy evs);    \
+\           A ~: lost;  A ~= Spy;  evs : recur |]       \
+\        ==> EX C RC. Says Server C RC : set evs  &     \
 \                     Crypt (shrK A) Y : parts {RC}";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*RA4*)
 by (Blast_tac 4);
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Recur.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -48,25 +48,25 @@
                 RA|}  : responses evs"
 
 
-consts     recur   :: agent set => event list set
-inductive "recur lost"
+consts     recur   :: event list set
+inductive "recur"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: recur lost"
+    Nil  "[]: recur"
 
          (*The spy MAY say anything he CAN say.  Common to
            all similar protocols.*)
-    Fake "[| evs: recur lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : recur lost"
+    Fake "[| evs: recur;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X  # evs : recur"
 
          (*Alice initiates a protocol run.
            "Agent Server" is just a placeholder, to terminate the nesting.*)
-    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
+    RA1  "[| evs: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
           ==> Says A B 
                 (Hash[Key(shrK A)] 
                  {|Agent A, Agent B, Nonce NA, Agent Server|})
-              # evs : recur lost"
+              # evs : recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
            XA should be the Hash of the remaining components with KA, but
@@ -74,27 +74,27 @@
            P is the previous recur message from Alice's caller.
            NOTE: existing proofs don't need PA and are complicated by its
                 presence!  See parts_Fake_tac.*)
-    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
+    RA2  "[| evs: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
              Says A' B PA : set evs;  
              PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
-              # evs : recur lost"
+              # evs : recur"
 
          (*The Server receives Bob's message and prepares a response.*)
-    RA3  "[| evs: recur lost;  B ~= Server;
+    RA3  "[| evs: recur;  B ~= Server;
              Says B' Server PB : set evs;
              (PB,RB,K) : respond evs |]
-          ==> Says Server B RB # evs : recur lost"
+          ==> Says Server B RB # evs : recur"
 
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
-    RA4  "[| evs: recur lost;  A ~= B;  
+    RA4  "[| evs: recur;  A ~= B;  
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
                          XA, Agent A, Agent B, Nonce NA, P|} : set evs;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
                          RA|} : set evs |]
-          ==> Says B A RA # evs : recur lost"
+          ==> Says B A RA # evs : recur"
 
 (**No "oops" message can easily be expressed.  Each session key is
    associated--in two separate messages--with two nonces.
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -22,7 +22,7 @@
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
-goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
+goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
 by (agent.induct_tac "C" 1);
 by (Auto_tac ());
 qed "keysFor_parts_initState";
@@ -32,15 +32,15 @@
 (*** Function "sees" ***)
 
 (*Agents see their own shared keys!*)
-goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
+goal thy "A ~= Spy --> Key (shrK A) : sees A evs";
 by (list.induct_tac "evs" 1);
 by (agent.induct_tac "A" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
 qed_spec_mp "sees_own_shrK";
 
-(*Spy sees shared keys of lost agents!*)
-goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
+(*Spy sees shared keys of agents!*)
+goal thy "!!A. A: lost ==> Key (shrK A) : sees Spy evs";
 by (list.induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
@@ -49,8 +49,8 @@
 AddSIs [sees_own_shrK, Spy_sees_lost];
 
 (*For not_lost_tac*)
-goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
-\              ==> X : analz (sees lost Spy evs)";
+goal thy "!!A. [| Crypt (shrK A) X : analz (sees Spy evs);  A: lost |] \
+\              ==> X : analz (sees Spy evs)";
 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
 qed "Crypt_Spy_analz_lost";
 
@@ -90,7 +90,7 @@
 
 (*** Fresh nonces ***)
 
-goal thy "Nonce N ~: parts (initState lost B)";
+goal thy "Nonce N ~: parts (initState B)";
 by (agent.induct_tac "B" 1);
 by (Auto_tac ());
 qed "Nonce_notin_initState";
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -19,9 +19,9 @@
 
 primrec initState agent
         (*Server knows all long-term keys; other agents know only their own*)
-  initState_Server  "initState lost Server     = Key `` range shrK"
-  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
-  initState_Spy     "initState lost Spy        = Key``shrK``lost"
+  initState_Server  "initState Server     = Key `` range shrK"
+  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
+  initState_Spy     "initState Spy        = Key``shrK``lost"
 
 
 rules
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -22,13 +22,30 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-AddIffs [Spy_in_lost, Server_not_lost];
-Addsimps [certificate_def];
+(** We mostly DO NOT unfold the definition of "certificate".  The attached
+    lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
+    contexts.
+**)
+
+goalw thy [certificate_def] 
+    "parts (insert (certificate B KB) H) =  \
+\    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
+by (rtac refl 1);
+qed "parts_insert_certificate";
 
-goal thy "!!A. A ~: lost ==> A ~= Spy";
+goalw thy [certificate_def] 
+    "analz (insert (certificate B KB) H) =  \
+\    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
+by (rtac refl 1);
+qed "analz_insert_certificate";
+Addsimps [parts_insert_certificate, analz_insert_certificate];
+
+goalw thy [certificate_def] 
+    "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
 by (Blast_tac 1);
-qed "not_lost_not_eq_Spy";
-Addsimps [not_lost_not_eq_Spy];
+qed "eq_certificate_iff";
+AddIffs [eq_certificate_iff];
+
 
 (*Injectiveness of key-generating functions*)
 AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
@@ -38,11 +55,6 @@
 	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
 
 
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = 
-    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
-
 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
 
 goal thy "pubK A ~= clientK arg";
@@ -102,11 +114,10 @@
 
 (*And one for ClientFinished.  Either FINISHED message may come first.*)
 goal thy 
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
-\  Says A B (Crypt (clientK(NA,NB,M))                 \
-\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
-\                   Nonce NA, Agent XA,               \
-\                   certificate A (pubK A),      \
+ "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.              \
+\  Says A B (Crypt (clientK(NA,NB,M))                           \
+\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},        \
+\                   Nonce NA, Agent XA, certificate A (pubK A), \
 \                   Nonce NB, Agent XB, Agent B|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -116,7 +127,7 @@
 
 (*Another one, for CertVerify (which is optional)*)
 goal thy 
- "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
+ "!!A B. A ~= B ==> EX NB M. EX evs: tls.   \
 \  Says A B (Crypt (priK A)                 \
 \            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -137,28 +148,36 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*Induction for regularity theorems.  If induction formula has the form
+   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
+   needless information about analz (insert X (sees Spy evs))  *)
+fun parts_induct_tac i = 
+    etac tls.induct i
+    THEN 
+    REPEAT (FIRSTGOAL analz_mono_contra_tac)
+    THEN 
+    fast_tac (!claset addss (!simpset)) i THEN
+    ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's private key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : tls \
-\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac tls.induct 1);
-by (prove_simple_subgoals_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2);
+ "!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
 goal thy 
- "!!evs. evs : tls \
-\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_priK";
 Addsimps [Spy_analz_priK];
 
-goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
+goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
 \                  evs : tls |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
@@ -168,22 +187,20 @@
 
 
 (*This lemma says that no false certificates exist.  One might extend the
-  model to include bogus certificates for the lost agents, but there seems
+  model to include bogus certificates for the agents, but there seems
   little point in doing so: the loss of their private keys is a worse
   breach of security.*)
 goalw thy [certificate_def]
  "!!evs. evs : tls     \
-\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
-by (etac tls.induct 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (Blast_tac 1);
+\        ==> certificate B KB : parts (sees Spy evs) --> KB = pubK B";
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
 bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
 
 
 (*Replace key KB in ClientCertKeyEx by (pubK B) *)
 val ClientCertKeyEx_tac = 
-    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
+    forward_tac [Says_imp_sees_Spy RS parts.Inj RS 
 		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
     THEN' assume_tac
     THEN' hyp_subst_tac;
@@ -193,7 +210,6 @@
     ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
     ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
     ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
-    rewrite_goals_tac  [certificate_def]  THEN
     ALLGOALS (asm_simp_tac 
               (!simpset addsimps [not_parts_not_analz]
                         setloop split_tac [expand_if]))  THEN
@@ -207,36 +223,32 @@
 (*** Hashing of nonces ***)
 
 (*Every Nonce that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
+goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees Spy evs);  \
 \                   evs : tls |]  \
-\                ==> Nonce N : parts (sees lost Spy evs)";
+\                ==> Nonce N : parts (sees Spy evs)";
 by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
-			             setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-		               addSEs partsEs) 1));
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+	               addSEs partsEs) 1);
 qed "Hash_imp_Nonce1";
 
 (*Lemma needed to prove Hash_Hash_imp_Nonce*)
 goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
-\                       : parts (sees lost Spy evs);     \
+\                       : parts (sees Spy evs);     \
 \                   evs : tls |]  \
-\                ==> Nonce M : parts (sees lost Spy evs)";
+\                ==> Nonce M : parts (sees Spy evs)";
 by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
-			             setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
-		       addSEs partsEs) 1);
+by (parts_induct_tac 1);
+by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
+by (Fake_parts_insert_tac 1);
 qed "Hash_imp_Nonce2";
 AddSDs [Hash_imp_Nonce2];
 
 
 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
-\                ==> Crypt (pubK B) X : parts (sees lost Spy evs)";
+\                ==> Crypt (pubK B) X : parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 by (blast_tac (!claset addIs [parts_insertI]) 1);
@@ -245,17 +257,16 @@
 
 (*NEEDED??*)
 goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
-\                      : parts (sees lost Spy evs);      \
+\                      : parts (sees Spy evs);      \
 \                   evs : tls |]                         \
-\                ==> Nonce M : parts (sees lost Spy evs)";
+\                ==> Nonce M : parts (sees Spy evs)";
 by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
-			             setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
-			      Says_imp_sees_Spy' RS parts.Inj]
-		      addSEs partsEs) 1);
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees,
+				       Says_imp_sees_Spy RS parts.Inj]
+		               addSEs partsEs) 1));
 qed "Hash_Hash_imp_Nonce";
 
 
@@ -263,14 +274,13 @@
   Every Nonce that's hashed is already in past traffic. 
   This general formulation is tricky to prove and hard to use, since the
   2nd premise is typically proved by simplification.*)
-goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
+goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
 \                   Nonce N : parts {X};  evs : tls |]  \
-\                ==> Nonce N : parts (sees lost Spy evs)";
+\                ==> Nonce N : parts (sees Spy evs)";
 by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+by (parts_induct_tac 1);
 by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
-			      Says_imp_sees_Spy' RS parts.Inj]
+			      Says_imp_sees_Spy RS parts.Inj]
 		      addSEs partsEs) 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
 by (Fake_parts_insert_tac 1);
@@ -285,16 +295,15 @@
   Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   assume A~:lost; otherwise, the Spy can forge A's signature.*)
-goalw thy [certificate_def]
+goal thy
  "!!evs. [| X = Crypt (priK A)                                        \
 \                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
 \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
 \    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
 \          : set evs --> \
-\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
+\        X : parts (sees Spy evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
 by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
@@ -305,25 +314,23 @@
 (*If CERTIFICATE VERIFY is present then A has chosen M.*)
 goal thy
  "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
-\             : parts (sees lost Spy evs);                                \
+\             : parts (sees Spy evs);                                \
 \           evs : tls;  A ~: lost |]                                      \
 \        ==> Notes A {|Agent B, Nonce M|} : set evs";
 be rev_mp 1;
-by (etac tls.induct 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
 qed "UseCertVerify";
 
 
 (*No collection of keys can help the spy get new private keys*)
 goal thy  
  "!!evs. evs : tls ==>                                    \
-\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
+\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees Spy evs))) =  \
 \            (priK B : KK | B : lost)";
 by (etac tls.induct 1);
 by (ALLGOALS
-    (asm_simp_tac (analz_image_keys_ss 
+    (asm_simp_tac (analz_image_keys_ss
 		   addsimps (certificate_def::keys_distinct))));
 (*Fake*) 
 by (spy_analz_tac 2);
@@ -343,8 +350,8 @@
 goal thy  
  "!!evs. evs : tls ==>                                 \
 \    ALL KK. KK <= (range clientK Un range serverK) -->           \
-\            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
-\            (Nonce N : analz (sees lost Spy evs))";
+\            (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
+\            (Nonce N : analz (sees Spy evs))";
 by (etac tls.induct 1);
 by (ClientCertKeyEx_tac 6);
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -352,8 +359,8 @@
 writeln"SLOW simplification: 50 secs!??";
 by (ALLGOALS
     (asm_simp_tac (analz_image_keys_ss 
-		   addsimps (analz_image_priK::certificate_def::
-			     keys_distinct))));
+                   addsimps (analz_image_priK::certificate_def::
+                             keys_distinct))));
 by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
 (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
@@ -369,7 +376,7 @@
 goal thy
  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
 \        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
-\            Nonce M ~: analz (sees lost Spy evs)";
+\            Nonce M ~: analz (sees Spy evs)";
 by (analz_induct_tac 1);
 (*ClientHello*)
 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
@@ -382,7 +389,7 @@
 by (REPEAT (blast_tac (!claset addSEs partsEs
 			       addDs  [Notes_Crypt_parts_sees,
 				       impOfSubs analz_subset_parts,
-				       Says_imp_sees_Spy' RS analz.Inj]) 1));
+				       Says_imp_sees_Spy RS analz.Inj]) 1));
 bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
 
 
@@ -395,13 +402,13 @@
   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
 
 goal thy 
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
-\        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+ "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
+\        ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*SpyKeys*)
 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
 (*Fake*) 
 by (spy_analz_tac 2);
 (*Base*)
@@ -412,13 +419,13 @@
 AddSEs [clientK_notin_parts RSN (2, rev_notE)];
 
 goal thy 
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
-\        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+ "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
+\        ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*SpyKeys*)
 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
 (*Fake*) 
 by (spy_analz_tac 2);
 (*Base*)
@@ -434,7 +441,7 @@
 
 goal thy 
  "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
-\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
+\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*ClientFinished: since M is fresh, a different instance of clientK was used.*)
@@ -450,7 +457,7 @@
 
 goal thy 
  "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
-\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
+\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*ServerFinished: since M is fresh, a different instance of serverK was used.*)
@@ -465,10 +472,10 @@
 AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
 
 
-(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*)
+(*NEEDED??*)
 goal thy
  "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
-\           A ~: lost;  evs : tls |] ==> KB = pubK B";
+\           A ~= Spy;  evs : tls |] ==> KB = pubK B";
 be rev_mp 1;
 by (analz_induct_tac 1);
 qed "A_Crypt_pubB";
@@ -476,36 +483,25 @@
 
 (*** Unicity results for M, the pre-master-secret ***)
 
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
-  It simplifies the proof by discarding needless information about
-	analz (insert X (sees lost Spy evs)) 
-*)
-fun analz_mono_parts_induct_tac i = 
-    etac tls.induct i           THEN 
-    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
-    REPEAT_FIRST analz_mono_contra_tac;
-
-
 (*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
 goal thy 
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
+ "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
 \        ==> EX B'. ALL B.   \
-\              Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'";
+\              Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'";
 by (etac rev_mp 1);
-by (analz_mono_parts_induct_tac 1);
-by (prove_simple_subgoals_tac 1);
-by (asm_simp_tac (!simpset addsimps [all_conj_distrib]
-                           setloop split_tac [expand_if]) 2);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
 (*ClientCertKeyEx*)
-by (expand_case_tac "M = ?y" 2 THEN
-    REPEAT (blast_tac (!claset addSEs partsEs) 2));
-by (Fake_parts_insert_tac 1);
+by (ClientCertKeyEx_tac 1);
+by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+by (expand_case_tac "M = ?y" 1 THEN
+    blast_tac (!claset addSEs partsEs) 1);
 val lemma = result();
 
 goal thy 
- "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees lost Spy evs); \
-\           Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \
-\           Nonce M ~: analz (sees lost Spy evs);                 \
+ "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees Spy evs); \
+\           Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \
+\           Nonce M ~: analz (sees Spy evs);                 \
 \           evs : tls |]                                          \
 \        ==> B=B'";
 by (prove_unique_tac lemma 1);
@@ -514,12 +510,11 @@
 
 (*In A's note to herself, M determines A and B.*)
 goal thy 
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]            \
+ "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]            \
 \ ==> EX A' B'. ALL A B.                                                   \
 \        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
 by (etac rev_mp 1);
-by (analz_mono_parts_induct_tac 1);
-by (prove_simple_subgoals_tac 1);
+by (parts_induct_tac 1);
 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
 (*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
 by (expand_case_tac "M = ?y" 1 THEN
@@ -529,7 +524,7 @@
 goal thy 
  "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
 \           Notes A' {|Agent B', Nonce M|} : set evs;  \
-\           Nonce M ~: analz (sees lost Spy evs);      \
+\           Nonce M ~: analz (sees Spy evs);      \
 \           evs : tls |]                               \
 \        ==> A=A' & B=B'";
 by (prove_unique_tac lemma 1);
@@ -550,13 +545,13 @@
 \                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
 \           evs : tls;  A ~: lost;  B ~: lost |]                        \
 \        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
-\        X : parts (sees lost Spy evs) --> Says B A X : set evs";
+\        X : parts (sees Spy evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
 by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
 by (REPEAT (rtac impI 1));
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
@@ -566,16 +561,17 @@
 (*This version refers not to SERVER FINISHED but to any message from B.
   We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   have changed A's identity in all other messages, so we can't be sure
-  that B sends his message to A.*)
+  that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
+  to bind A's identify with M, then we could replace A' by A below.*)
 goal thy
- "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
-\            Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs)  --> \
+ "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                     \
+\        ==> Notes A {|Agent B, Nonce M|} : set evs -->              \
+\            Crypt (serverK(NA,NB,M)) Y : parts (sees Spy evs)  -->  \
 \            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
 by (analz_induct_tac 1);
 by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
@@ -584,11 +580,11 @@
 (*...otherwise delete induction hyp and use unicity of M.*)
 by (thin_tac "?PP-->?QQ" 1);
 by (Step_tac 1);
-by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
 by (blast_tac (!claset addSEs [MPair_parts]
 		       addDs  [Notes_Crypt_parts_sees,
-			       Says_imp_sees_Spy' RS parts.Inj,
+			       Says_imp_sees_Spy RS parts.Inj,
 			       unique_M]) 1);
 qed_spec_mp "TrustServerMsg";
 
@@ -601,18 +597,18 @@
 goal thy
  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
 \        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
-\            Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) -->  \
+\            Crypt (clientK(NA,NB,M)) Y : parts (sees Spy evs) -->  \
 \            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
 by (analz_induct_tac 1);
 by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 (*ClientFinished.  If the message is old then apply induction hypothesis...*)
 by (step_tac (!claset delrules [conjI]) 1);
-by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
 by (blast_tac (!claset addSEs [MPair_parts]
 		       addDs  [Notes_unique_M]) 1);
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/TLS.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -13,7 +13,7 @@
 Server, who is in charge of all public keys.
 
 The model assumes that no fraudulent certificates are present, but it does
-assume that some private keys are lost to the spy.
+assume that some private keys are to the spy.
 
 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
 Allen, Transport Layer Security Working Group, 21 May 1997,
@@ -56,14 +56,8 @@
   (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
   clientK_range "range clientK <= Compl (range serverK)"
 
-  (*Spy has access to his own key for spoof messages, but Server is secure*)
-  Spy_in_lost     "Spy: lost"
-  Server_not_lost "Server ~: lost"
 
-
-consts  lost :: agent set        (*No need for it to be a variable*)
-	tls  :: event list set
-
+consts    tls :: event list set
 inductive tls
   intrs 
     Nil  (*Initial trace is empty*)
@@ -71,7 +65,7 @@
 
     Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
          "[| evs: tls;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
+             X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X # evs : tls"
 
     SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -41,41 +41,38 @@
 
 (** For reasoning about the encrypted portion of messages **)
 
-goal thy "!!evs. Says A' B X : set evs \
-\                ==> X : analz (sees lost Spy evs)";
+goal thy "!!evs. Says A' B X : set evs ==> X : analz (sees Spy evs)";
 by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
 qed "WL4_analz_sees_Spy";
 
 bind_thm ("WL4_parts_sees_Spy",
           WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-val parts_induct_tac = 
-    etac woolam.induct 1  THEN 
-    forward_tac [WL4_parts_sees_Spy] 6  THEN
+(*For proving the easier theorems about X ~: parts (sees Spy evs) *)
+fun parts_induct_tac i = 
+    etac woolam.induct i  THEN 
+    forward_tac [WL4_parts_sees_Spy] (i+5)  THEN
     prove_simple_subgoals_tac 1;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : woolam \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : woolam ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : woolam \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : woolam ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
 \                  evs : woolam |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
@@ -91,10 +88,10 @@
 
 (*If the encrypted message appears then it originated with Alice*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : woolam |]                   \
-\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
-\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
-by parts_induct_tac;
+ "!!evs. [| A ~: lost;  evs : woolam |]                        \
+\        ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs)  \
+\            --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "NB_Crypt_imp_Alice_msg";
@@ -121,7 +118,7 @@
 \        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs           \
 \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
 \               : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
@@ -129,10 +126,10 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
- "!!evs. [| B ~: lost;  evs : woolam |]                                  \
-\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)  \
+ "!!evs. [| B ~: lost;  evs : woolam |]                             \
+\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees Spy evs)  \
 \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed_spec_mp "NB_Crypt_imp_Server_msg";
 
@@ -161,10 +158,10 @@
 
 (*B only issues challenges in response to WL1.  Useful??*)
 goal thy 
- "!!evs. [| B ~= Spy;  evs : woolam |]                   \
+ "!!evs. [| B ~= Spy;  evs : woolam |]        \
 \    ==> Says B A (Nonce NB) : set evs        \
 \        --> (EX A'. Says A' B (Agent A) : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
@@ -172,11 +169,11 @@
 
 (**CANNOT be proved because A doesn't know where challenges come from...
 goal thy 
- "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                \
-\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
-\        Says B A (Nonce NB) : set evs                            \
+ "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]           \
+\    ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) &  \
+\        Says B A (Nonce NB) : set evs                       \
 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Step_tac 1);
 by (blast_tac (!claset addSEs partsEs) 1);
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -16,8 +16,7 @@
 
 WooLam = Shared + 
 
-consts  lost    :: agent set        (*No need for it to be a variable*)
-	woolam  :: event list set
+consts  woolam  :: event list set
 inductive woolam
   intrs 
          (*Initial trace is empty*)
@@ -27,7 +26,7 @@
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
     Fake "[| evs: woolam;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
+             X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X  # evs : woolam"
 
          (*Alice initiates a protocol run*)
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -16,14 +16,11 @@
 HOL_quantifiers := false;
 Pretty.setdepth 25;
 
-(*Replacing the variable by a constant improves speed*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\        ==> EX X NB K. EX evs: yahalom lost.     \
+\        ==> EX X NB K. EX evs: yahalom.     \
 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
@@ -35,7 +32,7 @@
 (**** Inductive proofs about yahalom ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
 by (etac yahalom.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -47,8 +44,8 @@
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
-\                X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\                X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
 
 bind_thm ("YM4_parts_sees_Spy",
@@ -56,45 +53,47 @@
 
 (*Relates to both YM4 and Oops*)
 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
-\                K : parts (sees lost Spy evs)";
+\                K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs partsEs
-                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
+                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "YM4_Key_parts_sees_Spy";
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_sees_tac = 
-    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
-    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
-    prove_simple_subgoals_tac  1;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_sees_tac i = 
+    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
+    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
+    prove_simple_subgoals_tac  i;
 
-val parts_induct_tac = 
-    etac yahalom.induct 1 THEN parts_sees_tac;
+(*Induction for regularity theorems.  If induction formula has the form
+   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
+   needless information about analz (insert X (sees Spy evs))  *)
+fun parts_induct_tac i = 
+    etac yahalom.induct i
+    THEN 
+    REPEAT (FIRSTGOAL analz_mono_contra_tac)
+    THEN  parts_sees_tac i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : yahalom lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : yahalom lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : yahalom lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : yahalom |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -103,9 +102,9 @@
 
 
 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom lost ==>          \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : yahalom ==>          \
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*YM4: Key K is not fresh!*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
 (*YM3*)
@@ -130,7 +129,7 @@
 goal thy 
  "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
 \             : set evs;                                                   \
-\           evs : yahalom lost |]                                          \
+\           evs : yahalom |]                                          \
 \        ==> K ~: range shrK";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
@@ -139,18 +138,18 @@
 qed "Says_Server_message_form";
 
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
-    forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+    forward_tac [YM4_analz_sees_Spy] 6 THEN
+    forward_tac [Says_Server_message_form] 7 THEN
     assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
 
 
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-  Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+  Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -158,10 +157,10 @@
 (** Session keys are not used to encrypt other session keys **)
 
 goal thy  
- "!!evs. evs : yahalom lost ==>                                 \
+ "!!evs. evs : yahalom ==>                                 \
 \  ALL K KK. KK <= Compl (range shrK) -->                       \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+\            (Key K : analz (Key``KK Un (sees Spy evs))) = \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -174,9 +173,9 @@
 qed_spec_mp "analz_image_freshK";
 
 goal thy
- "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>             \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =       \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -184,7 +183,7 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : yahalom lost ==>                                     \
+ "!!evs. evs : yahalom ==>                                     \
 \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
 \          Says Server A                                            \
 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
@@ -209,7 +208,7 @@
 \          Says Server A'                                           \
 \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
 \           : set evs;                                              \
-\          evs : yahalom lost |]                                    \
+\          evs : yahalom |]                                    \
 \       ==> A=A' & B=B' & na=na' & nb=nb'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -218,13 +217,13 @@
 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]         \
 \        ==> Says Server A                                        \
 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
 \             : set evs -->                                       \
 \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
-\            Key K ~: analz (sees lost Spy evs)";
+\            Key K ~: analz (sees Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -250,37 +249,26 @@
 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
 \             : set evs;                                          \
 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
+\        ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
-  It simplifies the proof by discarding needless information about
-	analz (insert X (sees lost Spy evs)) 
-*)
-fun analz_mono_parts_induct_tac i = 
-    etac yahalom.induct i
-    THEN 
-    REPEAT_FIRST analz_mono_contra_tac
-    THEN  parts_sees_tac;
-
-
 (** Security Guarantee for A upon receiving YM3 **)
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
-\            : parts (sees lost Spy evs);                              \
-\           A ~: lost;  evs : yahalom lost |]                          \
+\            : parts (sees Spy evs);                              \
+\           A ~: lost;  evs : yahalom |]                          \
 \         ==> Says Server A                                            \
 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
 \             : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "A_trusts_YM3";
 
@@ -290,15 +278,15 @@
 (*B knows, by the first part of A's message, that the Server distributed 
   the key for A and B.  But this part says nothing about nonces.*)
 goal thy 
- "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
-\           B ~: lost;  evs : yahalom lost |]                           \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
+\           B ~: lost;  evs : yahalom |]                           \
 \        ==> EX NA NB. Says Server A                                    \
 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
 \                                           Nonce NA, Nonce NB|},       \
 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*YM3*)
 by (Blast_tac 1);
@@ -308,15 +296,15 @@
   the key quoting nonce NB.  This part says nothing about agent names. 
   Secrecy of NB is crucial.*)
 goal thy 
- "!!evs. evs : yahalom lost                                             \
-\        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
+ "!!evs. evs : yahalom                                             \
+\        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
+\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
 \            (EX A B NA. Says Server A                                  \
 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
 \                                  Nonce NA, Nonce NB|},                \
 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set evs)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
 (*YM3 & Fake*)
 by (Blast_tac 2);
 by (Fake_parts_insert_tac 1);
@@ -325,7 +313,7 @@
 (*A is uncompromised because NB is secure*)
 by (not_lost_tac "A" 1);
 (*A's certificate guarantees the existence of the Server message*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
 			      A_trusts_YM3]) 1);
 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
 
@@ -364,7 +352,7 @@
  "!!evs. [| Says Server A                                                \
 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
 \             : set evs;                                                 \
-\           NB ~= NB';  evs : yahalom lost |]                            \
+\           NB ~= NB';  evs : yahalom |]                            \
 \        ==> ~ KeyWithNonce K NB evs";
 by (blast_tac (!claset addDs [unique_session_keys]) 1);
 qed "Says_Server_KeyWithNonce";
@@ -384,11 +372,11 @@
 val lemma = result();
 
 goal thy 
- "!!evs. evs : yahalom lost ==>                                         \
+ "!!evs. evs : yahalom ==>                                         \
 \        (ALL KK. KK <= Compl (range shrK) -->                          \
 \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
-\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =     \
-\             (Nonce NB : analz (sees lost Spy evs)))";
+\             (Nonce NB : analz (Key``KK Un (sees Spy evs))) =     \
+\             (Nonce NB : analz (sees Spy evs)))";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
@@ -410,7 +398,7 @@
 by (spy_analz_tac 1);
 (*YM4*)  (** LEVEL 7 **)
 by (not_lost_tac "A" 1);
-by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
+by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
     THEN REPEAT (assume_tac 1));
 by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
 qed_spec_mp "Nonce_secrecy";
@@ -423,9 +411,9 @@
  "!!evs. [| Says Server A                                                 \
 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
 \           : set evs;                                                    \
-\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
-\        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
-\            (Nonce NB : analz (sees lost Spy evs))";
+\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
+\        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
+\            (Nonce NB : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps 
 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
 qed "single_Nonce_secrecy";
@@ -434,11 +422,11 @@
 (*** The Nonce NB uniquely identifies B's message. ***)
 
 goal thy 
- "!!evs. evs : yahalom lost ==>                                            \
+ "!!evs. evs : yahalom ==>                                            \
 \   EX NA' A' B'. ALL NA A B.                                              \
-\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees lost Spy evs) \
+\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 (*Fake*)
 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
     THEN Fake_parts_insert_tac 1);
@@ -451,10 +439,10 @@
 
 goal thy 
  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
-\                  : parts (sees lost Spy evs);            \
+\                  : parts (sees Spy evs);            \
 \          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
-\                  : parts (sees lost Spy evs);            \
-\          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
+\                  : parts (sees Spy evs);            \
+\          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
 \        ==> NA' = NA & A' = A & B' = B";
 by (prove_unique_tac lemma 1);
 qed "unique_NB";
@@ -467,29 +455,27 @@
 \            : set evs;          B ~: lost;                               \
 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
 \            : set evs;                                                   \
-\          nb ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
+\          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
 \        ==> NA' = NA & A' = A & B' = B";
 by (not_lost_tac "B'" 1);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
                        addSEs [MPair_parts]
                        addDs  [unique_NB]) 1);
 qed "Says_unique_NB";
 
-val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
-
 
 (** A nonce value is never used both as NA and as NB **)
 
 goal thy 
- "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
-\ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
+ "!!evs. [| B ~: lost;  evs : yahalom  |]            \
+\ ==> Nonce NB ~: analz (sees Spy evs) -->           \
 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
-\       : parts(sees lost Spy evs)                   \
+\       : parts(sees Spy evs)                        \
 \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
-\       ~: parts(sees lost Spy evs)";
-by (analz_mono_parts_induct_tac 1);
+\       ~: parts(sees Spy evs)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
                        addSIs [parts_insertI]
                        addSEs partsEs) 1);
 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
@@ -498,7 +484,7 @@
 goal thy 
  "!!evs. [| Says Server A                                                \
 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
-\           evs : yahalom lost |]                                        \
+\           evs : yahalom |]                                             \
 \        ==> EX B'. Says B' Server                                       \
 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
 \                   : set evs";
@@ -509,15 +495,14 @@
 qed "Says_Server_imp_YM2";
 
 
-(*A vital theorem for B, that nonce NB remains secure from the Spy.
-  Unusually, the Fake case requires Spy:lost.*)
+(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
 \ ==> Says B Server                                                    \
 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
 \     : set evs -->                                                    \
 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
-\     Nonce NB ~: analz (sees lost Spy evs)";
+\     Nonce NB ~: analz (sees Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -526,13 +511,13 @@
                           analz_insert_freshK] @ pushes)
                setloop split_tac [expand_if])));
 (*Prove YM3 by showing that no NB can also be an NA*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
 	               addSEs [MPair_parts]
-		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 4
+		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
     THEN flexflex_tac);
 (*YM2: similar freshness reasoning*) 
 by (blast_tac (!claset addSEs partsEs
-		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
+		       addDs  [Says_imp_sees_Spy RS analz.Inj,
 			       impOfSubs analz_subset_parts]) 3);
 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
 by (blast_tac (!claset addSIs [parts_insertI]
@@ -543,12 +528,12 @@
 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
 by (REPEAT (Safe_step_tac 1));
 by (not_lost_tac "Aa" 1);
-by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
+by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
 by (forward_tac [Says_Server_message_form] 3);
 by (forward_tac [Says_Server_imp_YM2] 4);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
-(*  use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *)
-by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key,
+(*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
+by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
 			      impOfSubs Fake_analz_insert]) 1);
 (** LEVEL 14 **)
 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
@@ -558,11 +543,11 @@
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
 by (expand_case_tac "NB = NBa" 1);
 (*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac);
+by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
 (*case NB ~= NBa*)
 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
 by (blast_tac (!claset addSEs [MPair_parts]
-		       addDs  [Says_imp_sees_Spy' RS parts.Inj, 
+		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
 
@@ -579,20 +564,20 @@
 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
 \                       Crypt K (Nonce NB)|} : set evs;                     \
 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
-\           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
 \         ==> Says Server A                                                 \
 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
 \                               Nonce NA, Nonce NB|},                       \
 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
 \               : set evs";
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
+by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
     dtac B_trusts_YM4_shrK 1);
 by (dtac B_trusts_YM4_newK 3);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addDs [Says_unique_NB']) 1);
+by (blast_tac (!claset addDs [Says_unique_NB]) 1);
 qed "B_trusts_YM4";
 
 
@@ -601,19 +586,19 @@
 
 (*The encryption in message YM2 tells us it cannot be faked.*)
 goal thy 
- "!!evs. evs : yahalom lost                                            \
-\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
-\        : parts (sees lost Spy evs) -->                               \
-\      B ~: lost -->                                                   \
+ "!!evs. evs : yahalom                                            \
+\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
+\        : parts (sees Spy evs) -->                               \
+\      B ~: lost -->                                              \
 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
 \         : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
 
 (*If the server sends YM3 then B sent YM2*)
 goal thy 
- "!!evs. evs : yahalom lost                                                 \
+ "!!evs. evs : yahalom                                                      \
 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
 \         : set evs -->                                                     \
 \      B ~: lost -->                                                        \
@@ -624,7 +609,7 @@
 (*YM4*)
 by (Blast_tac 2);
 (*YM3*)
-by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy' RS parts.Inj]
+by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
 		      addSEs [MPair_parts]) 1);
 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
 
@@ -632,7 +617,7 @@
 goal thy
  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
 \             : set evs;                                                    \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
 \         : set evs";
 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
@@ -646,14 +631,14 @@
   A has said NB.  We can't be sure about the rest of A's message, but only
   NB matters for freshness.*)  
 goal thy 
- "!!evs. evs : yahalom lost                                             \
-\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
-\            Crypt (shrK B) {|Agent A, Key K|}                          \
-\              : parts (sees lost Spy evs) -->                          \
-\            B ~: lost -->                                              \
+ "!!evs. evs : yahalom                                             \
+\        ==> Key K ~: analz (sees Spy evs) -->                     \
+\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
+\            Crypt (shrK B) {|Agent A, Key K|}                     \
+\              : parts (sees Spy evs) -->                          \
+\            B ~: lost -->                                         \
 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
 (*Fake*)
 by (Fake_parts_insert_tac 1);
 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
@@ -664,7 +649,7 @@
 by (not_lost_tac "Aa" 1);
 by (blast_tac (!claset addSEs [MPair_parts]
                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
-		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
+		       addDs  [Says_imp_sees_Spy RS parts.Inj,
 			       unique_session_keys]) 1);
 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
 
@@ -678,14 +663,14 @@
 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
 \                       Crypt K (Nonce NB)|} : set evs;                     \
 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
-\           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (dtac B_trusts_YM4 1);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
-by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
 by (rtac lemma 1);
 by (rtac Spy_not_see_encrypted_key 2);
 by (REPEAT_FIRST assume_tac);
 by (blast_tac (!claset addSEs [MPair_parts]
-	       	       addDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
+	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed_spec_mp "YM4_imp_A_Said_YM3";
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -12,58 +12,58 @@
 
 Yahalom = Shared + 
 
-consts  yahalom   :: agent set => event list set
-inductive "yahalom lost"
+consts  yahalom   :: event list set
+inductive "yahalom"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: yahalom lost"
+    Nil  "[]: yahalom"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: yahalom lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : yahalom lost"
+    Fake "[| evs: yahalom;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
+    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
+          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
-    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
+    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
              Says A' B {|Agent A, Nonce NA|} : set evs |]
           ==> Says B Server 
                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
-                # evs : yahalom lost"
+                # evs : yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
-    YM3  "[| evs: yahalom lost;  A ~= Server;  Key KAB ~: used evs;
+    YM3  "[| evs: yahalom;  A ~= Server;  Key KAB ~: used evs;
              Says B' Server 
                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
                : set evs |]
           ==> Says Server A
                    {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
                      Crypt (shrK B) {|Agent A, Key KAB|}|}
-                # evs : yahalom lost"
+                # evs : yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom lost;  A ~= Server;  
+    YM4  "[| evs: yahalom;  A ~= Server;  
              Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
                         X|}  : set evs;
              Says A B {|Agent A, Nonce NA|} : set evs |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
 
          (*This message models possible leaks of session keys.  The Nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct.*)
-    Oops "[| evs: yahalom lost;  A ~= Spy;
+    Oops "[| evs: yahalom;  A ~= Spy;
              Says Server A {|Crypt (shrK A)
                                    {|Agent B, Key K, Nonce NA, Nonce NB|},
                              X|}  : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
 
 
 constdefs 
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Mon Jul 14 12:47:21 1997 +0200
@@ -18,13 +18,13 @@
 HOL_quantifiers := false;
 
 (*Replacing the variable by a constant improves speed*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
+val Says_imp_sees_Spy' =  Says_imp_sees_Spy;
 
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |]        \
-\        ==> EX X NB K. EX evs: yahalom lost.          \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+\        ==> EX X NB K. EX evs: yahalom.          \
 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
@@ -36,7 +36,7 @@
 (**** Inductive proofs about yahalom ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
 by (etac yahalom.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -48,7 +48,7 @@
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
-\                X : analz (sees lost Spy evs)";
+\                X : analz (sees Spy evs)";
 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
 
@@ -57,45 +57,47 @@
 
 (*Relates to both YM4 and Oops*)
 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
-\                K : parts (sees lost Spy evs)";
+\                K : parts (sees Spy evs)";
 by (blast_tac (!claset addSEs partsEs
                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
 qed "YM4_Key_parts_sees_Spy";
 
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
-  We instantiate the variable to "lost" since leaving it as a Var would
-  interfere with simplification.*)
-val parts_sees_tac = 
-    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
-    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
-    prove_simple_subgoals_tac  1;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_sees_tac i = 
+    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
+    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
+    prove_simple_subgoals_tac  i;
 
-val parts_induct_tac = 
-    etac yahalom.induct 1 THEN parts_sees_tac;
+(*Induction for regularity theorems.  If induction formula has the form
+   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
+   needless information about analz (insert X (sees Spy evs))  *)
+fun parts_induct_tac i = 
+    etac yahalom.induct i
+    THEN 
+    REPEAT (FIRSTGOAL analz_mono_contra_tac)
+    THEN  parts_sees_tac i;
 
 
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
- "!!evs. evs : yahalom lost \
-\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
- "!!evs. evs : yahalom lost \
-\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
-\                  evs : yahalom lost |] ==> A:lost";
+goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
+\                  evs : yahalom |] ==> A:lost";
 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
@@ -104,9 +106,9 @@
 
 
 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom lost ==>          \
-\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : yahalom ==>          \
+\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
 (*YM4: Key K is not fresh!*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
 (*YM3*)
@@ -129,8 +131,8 @@
   Oops as well as main secrecy property.*)
 goal thy 
  "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\            : set evs;                                                 \
-\           evs : yahalom lost |]                                       \
+\            : set evs;                                            \
+\           evs : yahalom |]                                       \
 \        ==> K ~: range shrK & A ~= B";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
@@ -138,10 +140,10 @@
 qed "Says_Server_message_form";
 
 
-(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
 val analz_sees_tac = 
-    dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
-    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+    dtac YM4_analz_sees_Spy 6 THEN
+    forward_tac [Says_Server_message_form] 7 THEN
     assume_tac 7 THEN
     REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
 
@@ -149,8 +151,8 @@
 (****
  The following is to prove theorems of the form
 
-          Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
-          Key K : analz (sees lost Spy evs)
+          Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+          Key K : analz (sees Spy evs)
 
  A more general formula must be proved inductively.
 
@@ -159,10 +161,10 @@
 (** Session keys are not used to encrypt other session keys **)
 
 goal thy  
- "!!evs. evs : yahalom lost ==>                                  \
-\  ALL K KK. KK <= Compl (range shrK) -->                        \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
-\            (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : yahalom ==>                                  \
+\  ALL K KK. KK <= Compl (range shrK) -->                   \
+\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
+\            (K : KK | Key K : analz (sees Spy evs))";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -175,9 +177,9 @@
 qed_spec_mp "analz_image_freshK";
 
 goal thy
- "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
-\        (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>        \
+\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
+\        (K = KAB | Key K : analz (sees Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -185,10 +187,10 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : yahalom lost ==>                                     \
-\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
-\          Says Server A                                            \
-\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
+ "!!evs. evs : yahalom ==>                                     \
+\      EX A' B' na' nb' X'. ALL A B na nb X.                   \
+\          Says Server A                                       \
+\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}   \
 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
 by (etac yahalom.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -198,8 +200,8 @@
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
-                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
-                      addss (!simpset addsimps [parts_insertI])) 1);
+                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
+                       addss (!simpset addsimps [parts_insertI])) 1);
 val lemma = result();
 
 goal thy 
@@ -209,7 +211,7 @@
 \          Says Server A'                                           \
 \           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
 \           : set evs;                                              \
-\          evs : yahalom lost |]                                    \
+\          evs : yahalom |]                                         \
 \       ==> A=A' & B=B' & na=na' & nb=nb'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -218,14 +220,14 @@
 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
-\           evs : yahalom lost |]                                    \
-\        ==> Says Server A                                           \
-\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
-\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
-\             : set evs -->                                          \
-\            Says A Spy {|na, nb, Key K|} ~: set evs -->             \
-\            Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                     \
+\           evs : yahalom |]                                    \
+\        ==> Says Server A                                      \
+\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
+\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
+\             : set evs -->                                     \
+\            Says A Spy {|na, nb, Key K|} ~: set evs -->        \
+\            Key K ~: analz (sees Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
@@ -246,13 +248,13 @@
 
 (*Final version*)
 goal thy 
- "!!evs. [| Says Server A                                         \
-\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
-\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
-\           : set evs;                                            \
-\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
-\        ==> Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| Says Server A                                    \
+\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
+\                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
+\           : set evs;                                       \
+\           Says A Spy {|na, nb, Key K|} ~: set evs;         \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
+\        ==> Key K ~: analz (sees Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -264,14 +266,14 @@
   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
 goal thy
  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
-\            : parts (sees lost Spy evs);                              \
-\           A ~: lost;  evs : yahalom lost |]                          \
+\            : parts (sees Spy evs);                                   \
+\           A ~: lost;  evs : yahalom |]                               \
 \         ==> EX nb. Says Server A                                     \
 \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
 \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
 \                    : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
 qed "A_trusts_YM3";
@@ -283,15 +285,15 @@
   the key for A and B, and has associated it with NB. *)
 goal thy 
  "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
-\            : parts (sees lost Spy evs);                            \
-\           B ~: lost;  evs : yahalom lost |]                        \
+\            : parts (sees Spy evs);                                 \
+\           B ~: lost;  evs : yahalom |]                             \
 \        ==> EX NA. Says Server A                                    \
 \                    {|Nonce NB,                                     \
 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
 \                       : set evs";
 by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*YM3*)
 by (Blast_tac 1);
@@ -306,7 +308,7 @@
 goal thy 
  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
 \             : set evs;                                                 \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]                     \
 \        ==> EX NA. Says Server A                                        \
 \                    {|Nonce NB,                                         \
 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
@@ -322,13 +324,13 @@
 
 (*The encryption in message YM2 tells us it cannot be faked.*)
 goal thy 
- "!!evs. evs : yahalom lost                                            \
-\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) -->  \
-\      B ~: lost -->                                                   \
-\      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
-\                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
+ "!!evs. evs : yahalom                                                  \
+\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees Spy evs) -->  \
+\      B ~: lost -->                                                    \
+\      (EX NB. Says B Server {|Agent B, Nonce NB,                       \
+\                              Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
 \         : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*YM2*)
 by (Blast_tac 1);
@@ -336,7 +338,7 @@
 
 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
 goal thy 
- "!!evs. evs : yahalom lost                                              \
+ "!!evs. evs : yahalom                                                   \
 \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
 \         : set evs -->                                                  \
 \      B ~: lost -->                                                     \
@@ -357,7 +359,7 @@
 goal thy
  "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
 \             : set evs;                                                    \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]                   \
 \   ==> EX nb'. Says B Server                                               \
 \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
 \                 : set evs";
@@ -368,29 +370,18 @@
 
 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
 
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
-  It simplifies the proof by discarding needless information about
-	analz (insert X (sees lost Spy evs)) 
-*)
-fun analz_mono_parts_induct_tac i = 
-    etac yahalom.induct i
-    THEN 
-    REPEAT_FIRST analz_mono_contra_tac
-    THEN  parts_sees_tac;
-
-
 (*Assuming the session key is secure, if both certificates are present then
   A has said NB.  We can't be sure about the rest of A's message, but only
   NB matters for freshness.*)  
 goal thy 
- "!!evs. evs : yahalom lost                                             \
-\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
-\            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
-\              : parts (sees lost Spy evs) -->                          \
-\            B ~: lost -->                                              \
+ "!!evs. evs : yahalom                                        \
+\        ==> Key K ~: analz (sees Spy evs) -->                \
+\            Crypt K (Nonce NB) : parts (sees Spy evs) -->    \
+\            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}      \
+\              : parts (sees Spy evs) -->                     \
+\            B ~: lost -->                                    \
 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
 (*Fake*)
 by (Fake_parts_insert_tac 1);
 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
@@ -412,7 +403,7 @@
  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
 \                       Crypt K (Nonce NB)|} : set evs;                 \
 \           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
+\           A ~: lost;  B ~: lost;  evs : yahalom |]                    \
 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
 by (dtac B_trusts_YM4_shrK 1);
diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -15,35 +15,35 @@
 
 Yahalom2 = Shared + 
 
-consts  yahalom   :: agent set => event list set
-inductive "yahalom lost"
+consts  yahalom   :: event list set
+inductive "yahalom"
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: yahalom lost"
+    Nil  "[]: yahalom"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: yahalom lost;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : yahalom lost"
+    Fake "[| evs: yahalom;  B ~= Spy;  
+             X: synth (analz (sees Spy evs)) |]
+          ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
+    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
+          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
-    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
+    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
              Says A' B {|Agent A, Nonce NA|} : set evs |]
           ==> Says B Server 
                   {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
-                # evs : yahalom lost"
+                # evs : yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
            new session key to Alice, with a packet for forwarding to Bob.
            !! Fields are reversed in the 2nd packet to prevent attacks!! *)
-    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
+    YM3  "[| evs: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
              Says B' Server {|Agent B, Nonce NB,
 			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
                : set evs |]
@@ -51,23 +51,23 @@
                {|Nonce NB, 
                  Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
                  Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
-                 # evs : yahalom lost"
+                 # evs : yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom lost;  A ~= Server;  
+    YM4  "[| evs: yahalom;  A ~= Server;  
              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                         X|}  : set evs;
              Says A B {|Agent A, Nonce NA|} : set evs |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct. *)
-    Oops "[| evs: yahalom lost;  A ~= Spy;
+    Oops "[| evs: yahalom;  A ~= Spy;
              Says Server A {|Nonce NB, 
                              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                              X|}  : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
 
 end