src/HOL/Auth/OtwayRees_AN.ML

--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 23 11:43:48 1997 +0100
@@ -17,6 +17,10 @@
 set proof_timing;
 HOL_quantifiers := false;
 
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
@@ -45,12 +49,13 @@
 
 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
 \                X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+bd (Says_imp_spies RS analz.Inj) 1;
+by (Blast_tac 1);
 qed "OR4_analz_spies";
 
 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
 \                  : set evs ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
 qed "Oops_parts_spies";
 
 (*OR4_analz_spies lets us treat those cases using the same 
@@ -75,7 +80,6 @@
 goal thy 
  "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
 by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
@@ -86,12 +90,8 @@
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
+	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (*Nobody can have used non-existent keys!*)
@@ -101,9 +101,9 @@
 (*Fake*)
 by (best_tac
       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addIs  [impOfSubs analz_subset_parts]
-               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
-               addss  (simpset())) 1);
+		addIs  [impOfSubs analz_subset_parts]
+		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
+		addss  (simpset())) 1);
 (*OR3*)
 by (Blast_tac 1);
 qed_spec_mp "new_keys_not_used";
@@ -195,8 +195,7 @@
 by (expand_case_tac "K = ?y" 1);
 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 spies_partsEs
-                       delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
+by (Blast_tac 1);
 val lemma = result();
 
 
@@ -227,7 +226,7 @@
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  : set evs)";
 by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
 (*OR3*)
 by (Blast_tac 1);
@@ -244,8 +243,7 @@
 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \                   : set evs";
-by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
-                      addEs  spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
 qed "A_trusts_OR4";
 
 
@@ -272,8 +270,7 @@
 (*OR4*) 
 by (Blast_tac 3);
 (*OR3*)
-by (blast_tac (claset() addSEs spies_partsEs
-                       addIs [impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
 (*Fake*) 
 by (spy_analz_tac 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -302,7 +299,7 @@
 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set evs)";
 by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
 (*OR3*)
 by (Blast_tac 1);
@@ -319,6 +316,5 @@
 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
-                       addEs  spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
 qed "B_trusts_OR3";