# HG changeset patch
# User paulson
# Date 867771282 -7200
# Node ID 3aced7fa7d8b4b5a4fb0fd869d979ecc052d71a0
# Parent  1be4fee7606bc441bba939168d2a62f9528ed43a
New theorem priK_inj_eq, injectivity of priK

diff -r 1be4fee7606b -r 3aced7fa7d8b src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Tue Jul 01 17:34:13 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Tue Jul 01 17:34:42 1997 +0200
@@ -11,9 +11,6 @@
 
 open Public;
 
-(*Injectiveness of new nonces*)
-AddIffs [inj_newN RS inj_eq];
-
 (*Holds because Friend is injective: thus cannot prove for all f*)
 goal thy "(Friend x : Friend``A) = (x:A)";
 by (Auto_tac());
@@ -52,6 +49,14 @@
 (*** Basic properties of pubK & priK ***)
 
 AddIffs [inj_pubK RS inj_eq];
+
+goal thy "!!A B. (priK A = priK B) = (A=B)";
+by (Step_tac 1);
+by (dres_inst_tac [("f","invKey")] arg_cong 1);
+by (Full_simp_tac 1);
+qed "priK_inj_eq";
+
+AddIffs [priK_inj_eq];
 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
 
 goalw thy [isSymKey_def] "~ isSymKey (pubK A)";