src/HOL/Auth/Public.ML
changeset 4422 21238c9d363e
parent 4091 771b1f6422a8
child 4477 b3e5857d8d99
--- 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! **)