# HG changeset patch
# User paulson
# Date 882281846 -3600
# Node ID 21238c9d363e7a938e10216ca79c42e14eda7f0b
# Parent  88639289be39298b5a13b2759e4f829b6813cda5
Simplified proofs using rewrites for f``A where f is injective

diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Message.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -18,11 +18,19 @@
 AddIffs atomic.inject;
 AddIffs msg.inject;
 
-(*Holds because Friend is injective: thus cannot prove for all f*)
+(*Equations hold because constructors are injective; cannot prove for all f*)
 goal thy "(Friend x : Friend``A) = (x:A)";
 by (Auto_tac());
 qed "Friend_image_eq";
-Addsimps [Friend_image_eq];
+
+goal thy "(Key x : Key``A) = (x:A)";
+by (Auto_tac());
+qed "Key_image_eq";
+
+goal thy "(Nonce x ~: Key``A)";
+by (Auto_tac());
+qed "Nonce_Key_image_eq";
+Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
 
 
 (** Inverse of keys **)
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -57,9 +57,13 @@
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
 
+AddDs [impOfSubs analz_subset_parts];
+AddDs [Says_imp_spies RS parts.Inj];
+AddDs [impOfSubs Fake_parts_insert];
+
 goal thy 
  "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
+by (Auto_tac());
 qed "Spy_analz_priK";
 Addsimps [Spy_analz_priK];
 
@@ -135,15 +139,12 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (claset() addDs  [Says_imp_spies RS parts.Inj]
-                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (claset() addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
 by (blast_tac (claset() addSEs [MPair_parts]
-		       addDs  [Says_imp_spies RS parts.Inj,
-			       parts.Body, unique_NA]) 3);
+		        addDs  [parts.Body, unique_NA]) 3);
 (*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs
-                       addIs  [impOfSubs analz_subset_parts]) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 qed "Spy_not_see_NA";
@@ -166,9 +167,7 @@
 (*NS1*)
 by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
-                       addDs  [Spy_not_see_NA, 
-			       impOfSubs analz_subset_parts]) 1);
+by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
 qed "A_trusts_NS2";
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
@@ -198,7 +197,8 @@
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
+    (asm_simp_tac (simpset() addsimps [all_conj_distrib, 
+				       parts_insert_spies])));
 (*NS2*)
 by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
 (*Fake*)
@@ -228,18 +228,18 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
+by (blast_tac (claset() addDs [unique_NB]) 4);
 (*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
-                       addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
-                       addEs partsEs
-		       addIs [impOfSubs analz_subset_parts]) 3);
+by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
+                        addEs partsEs) 3);
 (*NS1*)
 by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 qed "Spy_not_see_NB";
 
+AddDs [Spy_not_see_NB];
+
 
 (*Authentication for B: if he receives message 3 and has used NB
   in message 2, then A has sent message 3.*)
@@ -254,15 +254,12 @@
 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
 by (parts_induct_tac 1);
 by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A (this use of unique_NB is more robust) *)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Spy_not_see_NB]
-			addIs [unique_NB RS conjunct1]) 3);
+(*NS3: because NB determines A*)
+by (blast_tac (claset() addDs [unique_NB]) 3);
 (*NS1: by freshness*)
 by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
-                        addDs  [Spy_not_see_NB, 
-			        impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 1);
 qed "B_trusts_NS3";
 
 
@@ -288,13 +285,10 @@
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Clarify_tac);
 (*NS3: because NB determines A and NA*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
-                               Spy_not_see_NB, unique_NB]) 3);
+by (blast_tac (claset() addDs [unique_NB]) 3);
 (*NS1*)
 by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
-                        addDs  [Spy_not_see_NB, 
-			        impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 1);
 qed "B_trusts_protocol";
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -214,9 +214,7 @@
 (*Takes 9 secs*)
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -173,9 +173,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -165,9 +165,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -176,9 +176,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Public.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -34,6 +34,24 @@
 
 AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
 
+
+(** "Image" equations that hold for injective functions **)
+
+goal thy "(invKey x : invKey``A) = (x:A)";
+by (Auto_tac());
+qed "invKey_image_eq";
+
+(*holds because invKey is injective*)
+goal thy "(pubK x : pubK``A) = (x:A)";
+by (Auto_tac());
+qed "pubK_image_eq";
+
+goal thy "(priK x ~: pubK``A)";
+by (Auto_tac());
+qed "priK_pubK_image_eq";
+Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
+
+
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -247,8 +247,6 @@
 by (ALLGOALS 
     (asm_simp_tac
      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
-(*Base*)
-by (Blast_tac 1);
 (*Fake*) 
 by (spy_analz_tac 1);
 val raw_analz_image_freshK = result();
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/TLS.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -197,14 +197,14 @@
     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
-                        addsimps (expand_ifs@pushes)
-                        addsplits [expand_if]))  THEN
+                         addsimps (expand_ifs@pushes)
+                         addsplits [expand_if]))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
-			addsimps [insert_absorb]
-                        addsplits [expand_if]));
+			 addsimps [insert_absorb]
+                         addsplits [expand_if]));
 
 
 (*** Properties of items found in Notes ***)
@@ -228,7 +228,7 @@
 by (blast_tac (claset() addIs [parts_insertI]) 1);
 (*Client, Server Accept*)
 by (REPEAT (blast_tac (claset() addSEs spies_partsEs
-                               addSDs [Notes_Crypt_parts_spies]) 1));
+                                addSDs [Notes_Crypt_parts_spies]) 1));
 qed "Notes_master_imp_Crypt_PMS";
 
 (*Compared with the theorem above, both premise and conclusion are stronger*)
@@ -380,9 +380,7 @@
     (asm_simp_tac (analz_image_keys_ss
 		   addsimps (certificate_def::keys_distinct))));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_priK";
 
 
@@ -412,16 +410,14 @@
 by (ClientKeyExch_tac 7);
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_keys_lemma));
-by (ALLGOALS    (*15 seconds*)
+by (ALLGOALS    (*18 seconds*)
     (asm_simp_tac (analz_image_keys_ss 
 		   addsimps (expand_ifs@pushes)
 		   addsimps [range_sessionkeys_not_priK, 
                              analz_image_priK, certificate_def])));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_keys";
 
 (*Knowing some session keys is no help in getting new nonces*)
@@ -542,7 +538,7 @@
 by (Blast_tac 3);
 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
 by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
-			       Says_imp_spies RS analz.Inj]) 2);
+				Says_imp_spies RS analz.Inj]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
@@ -659,7 +655,7 @@
 \            Notes A {|Agent B, Nonce PMS|} : set evs --> \
 \            X : parts (spies evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
-by (analz_induct_tac 1);        (*22 seconds*)
+by (analz_induct_tac 1);        (*26 seconds*)
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
 (*proves ServerResume*)
 by (ALLGOALS Clarify_tac);
@@ -668,7 +664,7 @@
 (*Fake: the Spy doesn't have the critical session key!*)
 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
-				     not_parts_not_analz]) 2);
+				      not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 val lemma = normalize_thm [RSmp] (result());
 
@@ -731,7 +727,7 @@
 \           evs : tls;  A ~: bad;  B ~: bad |]          \
 \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
 by (blast_tac (claset() addIs [lemma]
-                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
+                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
 qed_spec_mp "TrustServerMsg";
 
 
@@ -760,7 +756,7 @@
 (*Fake: the Spy doesn't have the critical session key!*)
 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
-				     not_parts_not_analz]) 2);
+				      not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 val lemma = normalize_thm [RSmp] (result());
 
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -165,9 +165,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 goal thy
@@ -386,11 +384,9 @@
 		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
 		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
 		 Says_Server_KeyWithNonce])));
-(*Base*)
-by (Blast_tac 1);
 (*Fake*) 
 by (spy_analz_tac 1);
-(*YM4*)  (** LEVEL 7 **)
+(*YM4*)  (** LEVEL 6 **)
 by (not_bad_tac "A" 1);
 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
     THEN REPEAT (assume_tac 1));
diff -r 88639289be39 -r 21238c9d363e src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -167,9 +167,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 goal thy