src/HOL/Auth/Message.thy
changeset 14126 28824746d046
parent 13956 8fe7e12290e1
child 14145 2e31b8cc8788
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Jul 24 16:35:51 2003 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Jul 24 16:36:29 2003 +0200
     1.3 @@ -19,13 +19,20 @@
     1.4    key = nat
     1.5  
     1.6  consts
     1.7 -  invKey :: "key=>key"
     1.8 +  all_symmetric :: bool        --{*true if all keys are symmetric*}
     1.9 +  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    1.10 +
    1.11 +specification (invKey)
    1.12 +  invKey_cases: "(\<forall>K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)"
    1.13 +    by (rule exI [of _ id], auto)
    1.14  
    1.15 -axioms
    1.16 -  invKey [simp] : "invKey (invKey K) = K"
    1.17 +
    1.18 +lemma invKey [simp]: "invKey (invKey K) = K"
    1.19 +by (simp add: invKey_cases)
    1.20  
    1.21 -  (*The inverse of a symmetric key is itself;
    1.22 -    that of a public key is the private key and vice versa*)
    1.23 +
    1.24 +text{*The inverse of a symmetric key is itself; that of a public key
    1.25 +      is the private key and vice versa*}
    1.26  
    1.27  constdefs
    1.28    symKeys :: "key set"
    1.29 @@ -764,7 +771,7 @@
    1.30  
    1.31  ML
    1.32  {*
    1.33 -(*ML bindings for definitions and axioms*)
    1.34 +(*ML bindings for definitions*)
    1.35  
    1.36  val invKey = thm "invKey"
    1.37  val keysFor_def = thm "keysFor_def"