src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: Parameters of the memory clerk *}
     6 
     7 theory MemClerkParameters
     8 imports RPCParameters
     9 begin
    10 
    11 datatype mClkState = clkA | clkB
    12 
    13 (* types sent on the clerk's send and receive channels are argument types
    14    of the memory and the RPC, respectively *)
    15 type_synonym mClkSndArgType = "memOp"
    16 type_synonym mClkRcvArgType = "rpcOp"
    17 
    18 definition
    19   (* translate a memory call to an RPC call *)
    20   MClkRelayArg     :: "memOp => rpcOp"
    21   where "MClkRelayArg marg = memcall marg"
    22 
    23 definition
    24   (* translate RPC failures to memory failures *)
    25   MClkReplyVal     :: "Vals => Vals"
    26   where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
    27 
    28 end