src/HOL/TLA/Memory/RPCParameters.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 47968 3119ad2b5ad3
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/RPCParameters.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: RPC parameters *}
     6 
     7 theory RPCParameters
     8 imports MemoryParameters
     9 begin
    10 
    11 (*
    12   For simplicity, specify the instance of RPC that is used in the
    13   memory implementation.
    14 *)
    15 
    16 datatype rpcOp = memcall memOp | othercall Vals
    17 datatype rpcState = rpcA | rpcB
    18 
    19 consts
    20   (* some particular return values *)
    21   RPCFailure     :: Vals
    22   BadCall        :: Vals
    23   
    24   (* Translate an rpc call to a memory call and test if the current argument
    25      is legal for the receiver (i.e., the memory). This can now be a little
    26      simpler than for the generic RPC component. RelayArg returns an arbitrary
    27      memory call for illegal arguments. *)
    28   IsLegalRcvArg  :: "rpcOp => bool"
    29   RPCRelayArg    :: "rpcOp => memOp"
    30 
    31 axioms
    32   (* RPCFailure is different from MemVals and exceptions *)
    33   RFNoMemVal:        "RPCFailure ~: MemVal"
    34   NotAResultNotRF:   "NotAResult ~= RPCFailure"
    35   OKNotRF:           "OK ~= RPCFailure"
    36   BANotRF:           "BadArg ~= RPCFailure"
    37 
    38 defs
    39   IsLegalRcvArg_def: "IsLegalRcvArg ra ==
    40                          case ra of (memcall m) => True
    41                                   | (othercall v) => False"
    42   RPCRelayArg_def:   "RPCRelayArg ra ==
    43                          case ra of (memcall m) => m
    44                                   | (othercall v) => undefined"
    45 
    46 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
    47   NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
    48 
    49 end