Better comments
authorpaulson
Mon Aug 03 10:37:34 1998 +0200 (1998-08-03)
changeset 5234701fa0ed77b7
parent 5233 3571ff68ceda
child 5235 c404f25c58e8
Better comments
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Aug 03 10:36:39 1998 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Aug 03 10:37:34 1998 +0200
     1.3 @@ -31,6 +31,9 @@
     1.4  datatype  (*We allow any number of friendly agents*)
     1.5    agent = Server | Friend nat | Spy
     1.6  
     1.7 +
     1.8 +(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
     1.9 +  expressed using natural numbers.*)
    1.10  datatype  
    1.11    atomic = AGENT  agent	(*Agent names*)
    1.12           | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    1.13 @@ -38,26 +41,31 @@
    1.14           | KEY    key   (*Crypto keys*)
    1.15  
    1.16  datatype
    1.17 -  msg = Atomic atomic
    1.18 -      | Hash   msg       (*Hashing*)
    1.19 -      | MPair  msg msg   (*Compound messages*)
    1.20 -      | Crypt  key msg   (*Encryption, public- or shared-key*)
    1.21 +     msg = Atomic atomic
    1.22 +	 | Hash   msg       (*Hashing*)
    1.23 +	 | MPair  msg msg   (*Compound messages*)
    1.24 +	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    1.25  
    1.26 -(*Allows messages of the form {|A,B,NA|}, etc...*)
    1.27 +(*These translations complete the illustion that "msg" has seven constructors*)
    1.28  syntax
    1.29 -  Agent          :: agent => msg
    1.30 -  Number         :: nat   => msg
    1.31 -  Nonce          :: nat   => msg
    1.32 -  Key            :: key   => msg
    1.33 +  Agent       :: agent => msg
    1.34 +  Number      :: nat   => msg
    1.35 +  Nonce       :: nat   => msg
    1.36 +  Key         :: key   => msg
    1.37 +
    1.38 +translations
    1.39 +  "Agent x"   == "Atomic (AGENT x)"
    1.40 +  "Number x"  == "Atomic (NUMBER x)"
    1.41 +  "Nonce x"   == "Atomic (NONCE x)"
    1.42 +  "Key x"     == "Atomic (KEY x)"
    1.43 +  "Key``x"    == "Atomic `` (KEY `` x)"
    1.44 +
    1.45 +
    1.46 +(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    1.47 +syntax
    1.48    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    1.49  
    1.50  translations
    1.51 -  "Agent x"       == "Atomic (AGENT x)"
    1.52 -  "Number x"	  == "Atomic (NUMBER x)"
    1.53 -  "Nonce x"	  == "Atomic (NONCE x)"
    1.54 -  "Key x"	  == "Atomic (KEY x)"
    1.55 -  "Key``x"	  == "Atomic `` (KEY `` x)"
    1.56 -
    1.57    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.58    "{|x, y|}"      == "MPair x y"
    1.59