src/HOL/TLA/Memory/RPCParameters.thy
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
     1.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -16,32 +16,28 @@
     1.4  datatype rpcOp = memcall memOp | othercall Vals
     1.5  datatype rpcState = rpcA | rpcB
     1.6  
     1.7 -consts
     1.8 -  (* some particular return values *)
     1.9 -  RPCFailure     :: Vals
    1.10 -  BadCall        :: Vals
    1.11 -  
    1.12 -  (* Translate an rpc call to a memory call and test if the current argument
    1.13 -     is legal for the receiver (i.e., the memory). This can now be a little
    1.14 -     simpler than for the generic RPC component. RelayArg returns an arbitrary
    1.15 -     memory call for illegal arguments. *)
    1.16 -  IsLegalRcvArg  :: "rpcOp \<Rightarrow> bool"
    1.17 -  RPCRelayArg    :: "rpcOp \<Rightarrow> memOp"
    1.18 -
    1.19 -axiomatization where
    1.20 +axiomatization RPCFailure :: Vals and BadCall :: Vals
    1.21 +where
    1.22    (* RPCFailure is different from MemVals and exceptions *)
    1.23    RFNoMemVal:        "RPCFailure \<notin> MemVal" and
    1.24    NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
    1.25    OKNotRF:           "OK \<noteq> RPCFailure" and
    1.26    BANotRF:           "BadArg \<noteq> RPCFailure"
    1.27  
    1.28 -defs
    1.29 -  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
    1.30 -                         case ra of (memcall m) \<Rightarrow> True
    1.31 -                                  | (othercall v) \<Rightarrow> False"
    1.32 -  RPCRelayArg_def:   "RPCRelayArg ra ==
    1.33 -                         case ra of (memcall m) \<Rightarrow> m
    1.34 -                                  | (othercall v) \<Rightarrow> undefined"
    1.35 +(* Translate an rpc call to a memory call and test if the current argument
    1.36 +   is legal for the receiver (i.e., the memory). This can now be a little
    1.37 +   simpler than for the generic RPC component. RelayArg returns an arbitrary
    1.38 +   memory call for illegal arguments. *)
    1.39 +
    1.40 +definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
    1.41 +  where "IsLegalRcvArg ra ==
    1.42 +    case ra of (memcall m) \<Rightarrow> True
    1.43 +             | (othercall v) \<Rightarrow> False"
    1.44 +
    1.45 +definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
    1.46 +  where "RPCRelayArg ra ==
    1.47 +    case ra of (memcall m) \<Rightarrow> m
    1.48 +             | (othercall v) \<Rightarrow> undefined"
    1.49  
    1.50  lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
    1.51    NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]