diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Thu Jul 24 16:35:51 2003 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Jul 24 16:36:29 2003 +0200
@@ -11,14 +11,24 @@
 theory Shared = Event:
 
 consts
-  shrK    :: "agent => key"  (*symmetric keys*)
+  shrK    :: "agent => key"  (*symmetric keys*);
+
+specification (shrK)
+  inj_shrK: "inj shrK"
+  --{*No two agents have the same long-term key*}
+   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
+   apply (simp add: inj_on_def split: agent.split) 
+   done
 
-axioms
-  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
-  inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
+text{*All keys are symmetric*}
+
+defs  all_symmetric_def: "all_symmetric == True"
 
+lemma isSym_keys: "K \<in> symKeys"	
+by (simp add: symKeys_def all_symmetric_def invKey_cases) 
+
+text{*Server knows all long-term keys; other agents know only their own*}
 primrec
-        (*Server knows all long-term keys; other agents know only their own*)
   initState_Server:  "initState Server     = Key ` range shrK"
   initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
   initState_Spy:     "initState Spy        = Key`shrK`bad"