# HG changeset patch
# User paulson
# Date 854375379 -3600
# Node ID c57b585eecd90444a80ada237073eaf505f08c27
# Parent  06b6a499f8aede411b0ee88b267a4a00a762dbd0
Tidied unicity theorems

diff -r 06b6a499f8ae -r c57b585eecd9 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Mon Jan 27 15:06:21 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Mon Jan 27 15:29:39 1997 +0100
@@ -325,10 +325,10 @@
 **)
 
 goal thy 
- "!!evs. [| evs : recur lost; A ~: lost |]               \
-\ ==> EX B' P'. ALL B P.    \
-\        Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
-\          : parts (sees lost Spy evs)  -->  B=B' & P=P'";
+ "!!evs. [| evs : recur lost; A ~: lost |]                   \
+\ ==> EX B' P'. ALL B P.                                     \
+\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
+\          -->  B=B' & P=P'";
 by (parts_induct_tac 1);
 by (etac responses.induct 3);
 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
@@ -341,11 +341,9 @@
 val lemma = result();
 
 goalw thy [HPair_def]
- "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}   \
-\            : parts (sees lost Spy evs);                          \
-\          Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
-\            : parts (sees lost Spy evs);                          \
-\          evs : recur lost;  A ~: lost |]                         \
+ "!!evs.[| 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 |]                                    \
 \        ==> B=B' & P=P'";
 by (REPEAT (eresolve_tac partsEs 1));
 by (prove_unique_tac lemma 1);
@@ -412,8 +410,8 @@
 
 
 goal thy 
- "!!K'. (PB,RB,KXY) : respond evs               \
-\  ==> EX A' B'. ALL A B N.              \
+ "!!K'. (PB,RB,KXY) : respond evs                          \
+\  ==> EX A' B'. ALL A B N.                                \
 \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
 \          -->   (A'=A & B'=B) | (A'=B & B'=A)";
 by (etac respond.induct 1);
@@ -434,11 +432,11 @@
 val lemma = result();
 
 goal thy 
- "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};    \
+ "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
 \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
-\          (PB,RB,KXY) : respond evs |]               \
+\          (PB,RB,KXY) : respond evs |]                            \
 \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1);  (*50 seconds??, due to the disjunctions*)
+by (prove_unique_tac lemma 1);
 qed "unique_session_keys";