src/HOL/TLA/Memory/RPCParameters.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/TLA/Memory/RPCParameters.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 section \<open>RPC-Memory example: RPC parameters\<close>
     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 axiomatization RPCFailure :: Vals and BadCall :: Vals
    20 where
    21   (* RPCFailure is different from MemVals and exceptions *)
    22   RFNoMemVal:        "RPCFailure \<notin> MemVal" and
    23   NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
    24   OKNotRF:           "OK \<noteq> RPCFailure" and
    25   BANotRF:           "BadArg \<noteq> RPCFailure"
    26 
    27 (* Translate an rpc call to a memory call and test if the current argument
    28    is legal for the receiver (i.e., the memory). This can now be a little
    29    simpler than for the generic RPC component. RelayArg returns an arbitrary
    30    memory call for illegal arguments. *)
    31 
    32 definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
    33   where "IsLegalRcvArg ra ==
    34     case ra of (memcall m) \<Rightarrow> True
    35              | (othercall v) \<Rightarrow> False"
    36 
    37 definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
    38   where "RPCRelayArg ra ==
    39     case ra of (memcall m) \<Rightarrow> m
    40              | (othercall v) \<Rightarrow> undefined"
    41 
    42 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
    43   NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
    44 
    45 end