# HG changeset patch
# User paulson
# Date 867772776 -7200
# Node ID 6988394a600871ecec151e5bc6977e6d2a25cb3b
# Parent  ef918a90f9bf18ddd1d393a74bad61671fa9989d
Tidying; also simplified the lemma Says_Server_not

diff -r ef918a90f9bf -r 6988394a6008 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Jul 01 17:42:36 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Tue Jul 01 17:59:36 1997 +0200
@@ -21,8 +21,8 @@
 
 (*Simplest case: Alice goes directly to the server*)
 goal thy
- "!!A. A ~= Server                          \
-\ ==> EX K NA. EX evs: recur lost.          \
+ "!!A. A ~= Server                                                      \
+\ ==> EX K NA. EX evs: recur lost.                                      \
 \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
 \                     Agent Server|}  : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -34,8 +34,8 @@
 
 (*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.            \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
+\ ==> EX K. EX NA. EX evs: recur lost.                          \
 \       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,8 +54,8 @@
   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.                          \
-\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ ==> EX K. EX NA. EX evs: recur lost.                                 \
+\       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);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
@@ -324,14 +324,14 @@
 by (ALLGOALS (expand_case_tac "NA = ?y"));
 by (REPEAT_FIRST (ares_tac [exI]));
 by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
-                              addSEs sees_Spy_partsEs) 1));
+                               addSEs sees_Spy_partsEs) 1));
 val lemma = result();
 
 goalw thy [HPair_def]
- "!!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'";
+ "!!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 |]                                     \
+\      ==> B=B' & P=P'";
 by (REPEAT (eresolve_tac partsEs 1));
 by (prove_unique_tac lemma 1);
 qed "unique_NA";
@@ -358,7 +358,7 @@
 \           ALL K KK. KK <= Compl (range shrK) -->          \
 \                     (Key K : analz (Key``KK Un H)) =      \
 \                     (K : KK | Key K : analz H) |]         \
-\       ==> (Key K : analz (insert RB H)) --> \
+\       ==> (Key K : analz (insert RB H)) -->               \
 \           (Key K : parts{RB} | Key K : analz H)";
 by (etac responses.induct 1);
 by (ALLGOALS
@@ -377,9 +377,8 @@
 (*The Server does not send such messages.  This theorem lets us avoid
   assuming B~=Server in RA4.*)
 goal thy 
- "!!evs. evs : recur lost       \
-\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
-\                  ~: set evs";
+ "!!evs. evs : recur lost \
+\        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
 by (etac recur.induct 1);
 by (etac (respond.induct) 5);
 by (Auto_tac());