Simple tidying

--- a/src/HOL/Auth/OtwayRees.ML	Mon Oct 07 10:47:01 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Oct 07 10:55:51 1996 +0200
@@ -12,7 +12,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-
 open OtwayRees;
 
 proof_timing:=true;
@@ -89,20 +88,26 @@
         tac Reveal_parts_sees_Spy 7
     end;
 
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
+fun parts_induct_tac i = SELECT_GOAL
+    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
+	     (*Fake message*)
+	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+					   impOfSubs Fake_parts_insert]
+                                    addss (!simpset)) 2)) THEN
+     (*Base case*)
+     fast_tac (!claset addss (!simpset)) 1 THEN
+     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
 
-(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees another agent's shared key! (unless it's lost at start)*)
 goal thy 
  "!!evs. [| evs : otway lost;  A ~: lost |]    \
 \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
+by (parts_induct_tac 1);
 by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]) 1);
 qed "Spy_not_see_shrK";
 
 bind_thm ("Spy_not_analz_shrK",
@@ -139,10 +144,7 @@
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evs' --> \
 \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
@@ -214,9 +216,7 @@
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evs' --> \
 \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
 (*OR1 and OR3*)
 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
 (*Fake, OR2, OR4: these messages send unknown (X) components*)
@@ -248,7 +248,43 @@
 Addsimps [new_keys_not_used, new_keys_not_analzd];
 
 
-(** Lemmas concerning the form of items passed in messages **)
+
+(*** Proofs involving analz ***)
+
+(*Describes the form of Key K when the following message is sent.  The use of
+  "parts" strengthens the induction hyp for proving the Fake case.  The
+  assumption A ~: lost prevents its being a Faked message.  (Based
+  on NS_Shared/Says_S_message_form) *)
+goal thy
+ "!!evs. evs: otway lost ==>                                           \
+\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) &   \
+\          A ~: lost -->                                               \
+\        (EX evt: otway lost. K = newK evt)";
+by (parts_induct_tac 1);
+by (Auto_tac());
+qed_spec_mp "Reveal_message_lemma";
+
+(*EITHER describes the form of Key K when the following message is sent, 
+  OR     reduces it to the Fake case.*)
+
+goal thy 
+ "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
+\           evs : otway lost |]                      \
+\        ==> (EX evt: otway lost. K = newK evt)          \
+\          | Key K : analz (sees lost Spy evs)";
+br (Reveal_message_lemma RS disjCI) 1;
+ba 1;
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+                      addDs [impOfSubs analz_subset_parts]
+                      addss (!simpset)) 1);
+qed "Reveal_message_form";
+
+
+(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+val analz_Fake_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")] Reveal_message_form 7;
 
 
 (****
@@ -283,51 +319,13 @@
 
 (** Session keys are not used to encrypt other session keys **)
 
-(*Describes the form of Key K when the following message is sent.  The use of
-  "parts" strengthens the induction hyp for proving the Fake case.  The
-  assumptions on A are needed to prevent its being a Faked message.  (Based
-  on NS_Shared/Says_S_message_form) *)
-goal thy
- "!!evs. evs: otway lost ==>                                           \
-\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
-\          A ~: lost -->                                           \
-\        (EX evt: otway lost. K = newK evt)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
-val lemma = result() RS mp;
-
-
-(*EITHER describes the form of Key K when the following message is sent, 
-  OR     reduces it to the Fake case.*)
-goal thy 
- "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
-\           evs : otway lost |]                      \
-\        ==> (EX evt: otway lost. K = newK evt)          \
-\          | Key K : analz (sees lost Spy evs)";
-by (excluded_middle_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 2);
-by (forward_tac [lemma] 1);
-by (fast_tac (!claset addEs  partsEs
-                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-by (Fast_tac 1);
-qed "Reveal_message_form";
-
-
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
  "!!evs. evs : otway lost ==> \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (dtac Reveal_message_form 7);
+by analz_Fake_tac;
 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
 by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
 by (ALLGOALS (*Takes 28 secs*)
@@ -339,7 +337,7 @@
 (*Reveal case 2, OR4, OR2, Fake*) 
 by (EVERY (map spy_analz_tac [7,5,3,2]));
 (*Reveal case 1, OR3, Base*)
-by (Auto_tac());
+by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
 qed_spec_mp "analz_image_newK";
 
 
@@ -370,9 +368,8 @@
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
 by (Fast_tac 2);
-by (excluded_middle_tac "K = Key(newK evsa)" 1);
-by (Asm_simp_tac 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
+by (expand_case_tac "K = ?y" 1);
+by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a very new message, and handle this case by contradiction*)
 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
@@ -403,42 +400,27 @@
 
 (*Only OR1 can have caused such a part of a message to appear.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]               \
-\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
-\             : parts (sees lost Spy evs) -->                  \
-\            Says A B {|NA, Agent A, Agent B,               \
+ "!!evs. [| A ~: lost;  evs : otway lost |]                        \
+\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)               \
+\             : parts (sees lost Spy evs) -->                      \
+\            Says A B {|NA, Agent A, Agent B,                      \
 \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
 \             : set_of_list evs";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
+by (parts_induct_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
 
-(** The Nonce NA uniquely identifies A's  message. **)
+(** The Nonce NA uniquely identifies A's message. **)
 
 goal thy 
  "!!evs. [| evs : otway lost; A ~: lost |]               \
 \ ==> EX B'. ALL B.    \
 \        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
 \        --> B = B'";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (Step_tac 1);
+by (parts_induct_tac 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR1: creation of new Nonce.  Move assertion into global context*)
-by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (expand_case_tac "NA = ?y" 1);
 by (best_tac (!claset addSEs partsEs
                       addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
 val lemma = result();
@@ -497,26 +479,21 @@
 \                   Crypt {|NA, Key K|} (shrK A),                      \
 \                   Crypt {|NB, Key K|} (shrK B)|}                     \
 \                   : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 1);
+by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (fast_tac (!claset addSIs [parts_insertI]
                       addSEs partsEs
                       addEs [Says_imp_old_nonces RS less_irrefl]
                       addss (!simpset)) 1);
-(*OR3 and OR4*)  (** LEVEL 5 **)
+(*OR3 and OR4*) 
 (*OR4*)
 by (REPEAT (Safe_step_tac 2));
 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
                       addEs  partsEs
                       addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
-(*OR3*)  (** LEVEL 8 **)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
+(*OR3*)  (** LEVEL 5 **)
+by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
 by (fast_tac (!claset addSEs [MPair_parts]
                       addSDs [Says_imp_sees_Spy RS parts.Inj]
@@ -547,7 +524,7 @@
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "A_can_trust";
+qed "A_trust_OR4";
 
 
 (*Describes the form of K and NA when the Server sends this message.*)
@@ -577,9 +554,7 @@
 \            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (forward_tac [Reveal_message_form] 7);
+by analz_Fake_tac;
 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
 by (ALLGOALS
     (asm_full_simp_tac 
@@ -599,7 +574,7 @@
 by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
 (*So now we have  Aa ~: lost *)
-by (dtac A_can_trust 1);
+by (dtac A_trust_OR4 1);
 by (REPEAT (assume_tac 1));
 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -643,13 +618,8 @@
 \             {|NA, Agent A, Agent B, X',                      \
 \               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
 \             : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
+by (parts_induct_tac 1);
+by (auto_tac (!claset, !simpset addcongs [conj_cong]));
 qed_spec_mp "Crypt_imp_OR2";
 
 
@@ -657,23 +627,13 @@
 
 goal thy 
  "!!evs. [| evs : otway lost; B ~: lost |]               \
-\ ==> EX NA' A'. ALL NA A.                              \
+\ ==> EX NA' A'. ALL NA A.                               \
 \      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
 \      --> NA = NA' & A = A'";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset delrules [conjI,conjE]
-		      addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (Step_tac 1);
+by (parts_induct_tac 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR2: creation of new Nonce.  Move assertion into global context*)
-by (excluded_middle_tac "NB = Nonce (newN evsa)" 1);
-by (Asm_simp_tac 1);
-by (fast_tac (!claset addSIs [exI]) 1);
+by (expand_case_tac "NB = ?y" 1);
 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
 val lemma = result();
 
@@ -706,12 +666,7 @@
 \                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
 \                        Crypt {|NB, Key K|} (shrK B)|}                  \
 \                   : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 1);
+by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (fast_tac (!claset addSIs [parts_insertI]
                       addSEs partsEs
@@ -753,10 +708,10 @@
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "B_can_trust";
+qed "B_trust_OR3";
 
 
-B_can_trust RS Spy_not_see_encrypted_key;
+B_trust_OR3 RS Spy_not_see_encrypted_key;
 
 
 (** A session key uniquely identifies a pair of senders in the message
@@ -769,8 +724,7 @@
 \         C=A | C=B";
 by (Simp_tac 1);        (*Miniscoping*)
 by (etac otway.induct 1);
-by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
-by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
+by analz_Fake_tac;
 (*spy_analz_tac just does not work here: it is an entirely different proof!*)
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
@@ -778,9 +732,8 @@
                                       parts_insert2])));
 by (REPEAT_FIRST (etac exE));
 (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
-by (excluded_middle_tac "K = newK evsa" 4);
-by (Asm_simp_tac 4);
-by (REPEAT (ares_tac [exI] 4));
+by (expand_case_tac "K = ?y" 4);
+by (REPEAT (ares_tac [exI] 5));
 (*...we prove this case by contradiction: the key is too new!*)
 by (fast_tac (!claset addSEs partsEs
                       addEs [Says_imp_old_keys RS less_irrefl]

--- a/src/HOL/Auth/OtwayRees.thy	Mon Oct 07 10:47:01 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Mon Oct 07 10:55:51 1996 +0200
@@ -73,12 +73,12 @@
 
          (*This message models possible leaks of session keys.  Alice's Nonce
            identifies the protocol run.*)
-    Reveal "[| evs: otway lost;  A ~= Spy;
-               Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
-                 : set_of_list evs;
-               Says A  B {|Nonce NA, Agent A, Agent B, 
-                           Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
-                 : set_of_list evs |]
-            ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
+    Revl "[| evs: otway lost;  A ~= Spy;
+             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
+               : set_of_list evs;
+             Says A  B {|Nonce NA, Agent A, Agent B, 
+                         Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+               : set_of_list evs |]
+          ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
 
 end

--- a/src/HOL/Auth/Shared.ML	Mon Oct 07 10:47:01 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Oct 07 10:55:51 1996 +0200
@@ -9,6 +9,18 @@
 *)
 
 
+val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
+by (excluded_middle_tac "P" 1);
+by (asm_simp_tac (!simpset addsimps prems) 1);
+by (asm_simp_tac (!simpset addsimps prems) 1);
+val expand_case = result();
+
+fun expand_case_tac P i =
+    res_inst_tac [("P",P)] expand_case i THEN
+    Simp_tac (i+1) THEN 
+    Simp_tac i;
+
+
 
 (*GOALS.ML??*)
 fun prlim n = (goals_limit:=n; pr());
@@ -107,7 +119,6 @@
 
 AddSIs [sees_own_shrK, Spy_sees_lost];
 
-
 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
 
 goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)";
@@ -156,6 +167,14 @@
 Addsimps [Says_imp_sees_Spy];
 AddIs    [Says_imp_sees_Spy];
 
+goal thy  
+ "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
+\           C   : lost |]                                         \
+\        ==> X : analz (sees lost Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+                      addss (!simpset)) 1);
+qed "Says_Crypt_lost";
+
 goal thy "initState lost C <= Key `` range shrK";
 by (agent.induct_tac "C" 1);
 by (Auto_tac ());

--- a/src/HOL/Auth/Shared.thy	Mon Oct 07 10:47:01 1996 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon Oct 07 10:55:51 1996 +0200
@@ -23,7 +23,7 @@
         (*Server knows all 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_Spy     "initState lost Spy        = Key``shrK``lost"
 
 
 datatype  (*Messages, and components of agent stores*)