doc-src/TutorialI/Protocol/Message.thy
changeset 25341 ca3761e38a87
parent 23929 6a98d0826daf
child 26807 4cd176ea28dc
equal deleted inserted replaced
25340:6a3b20f0ae61 25341:ca3761e38a87
    32 Keys are just natural numbers.  Function @{text invKey} maps a public key to
    32 Keys are just natural numbers.  Function @{text invKey} maps a public key to
    33 the matching private key, and vice versa:
    33 the matching private key, and vice versa:
    34 *}
    34 *}
    35 
    35 
    36 types key = nat
    36 types key = nat
    37 consts invKey :: "key=>key"
    37 consts invKey :: "key \<Rightarrow> key"
    38 (*<*)
    38 (*<*)
    39 consts all_symmetric :: bool        --{*true if all keys are symmetric*}
    39 consts all_symmetric :: bool        --{*true if all keys are symmetric*}
    40 
    40 
    41 specification (invKey)
    41 specification (invKey)
    42   invKey [simp]: "invKey (invKey K) = K"
    42   invKey [simp]: "invKey (invKey K) = K"