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