--- a/src/HOL/Auth/Message.thy Wed Sep 03 18:20:57 2003 +0200
+++ b/src/HOL/Auth/Message.thy Thu Sep 04 11:08:24 2003 +0200
@@ -23,14 +23,11 @@
invKey :: "key=>key" --{*inverse of a symmetric key*}
specification (invKey)
- invKey_cases: "(\<forall>K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)"
+ invKey [simp]: "invKey (invKey K) = K"
+ invKey_symmetric: "all_symmetric --> invKey = id"
by (rule exI [of _ id], auto)
-lemma invKey [simp]: "invKey (invKey K) = K"
-by (simp add: invKey_cases)
-
-
text{*The inverse of a symmetric key is itself; that of a public key
is the private key and vice versa*}
--- a/src/HOL/Auth/Shared.thy Wed Sep 03 18:20:57 2003 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Sep 04 11:08:24 2003 +0200
@@ -25,7 +25,7 @@
defs all_symmetric_def: "all_symmetric == True"
lemma isSym_keys: "K \<in> symKeys"
-by (simp add: symKeys_def all_symmetric_def invKey_cases)
+by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
text{*Server knows all long-term keys; other agents know only their own*}
primrec