1(* Title: HOL/TLA/Memory/RPCParameters.thy 2 Author: Stephan Merz, University of Munich 3*) 4 5section \<open>RPC-Memory example: RPC parameters\<close> 6 7theory RPCParameters 8imports MemoryParameters 9begin 10 11(* 12 For simplicity, specify the instance of RPC that is used in the 13 memory implementation. 14*) 15 16datatype rpcOp = memcall memOp | othercall Vals 17datatype rpcState = rpcA | rpcB 18 19axiomatization RPCFailure :: Vals and BadCall :: Vals 20where 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 32definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool" 33 where "IsLegalRcvArg ra == 34 case ra of (memcall m) \<Rightarrow> True 35 | (othercall v) \<Rightarrow> False" 36 37definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp" 38 where "RPCRelayArg ra == 39 case ra of (memcall m) \<Rightarrow> m 40 | (othercall v) \<Rightarrow> undefined" 41 42lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF 43 NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric] 44 45end 46