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;
wenzelm@41589
     1
(*  Title:      HOL/TLA/Memory/RPCParameters.thy
wenzelm@41589
     2
    Author:     Stephan Merz, University of Munich
wenzelm@21624
     3
*)
wenzelm@3807
     4
wenzelm@60592
     5
section \<open>RPC-Memory example: RPC parameters\<close>
wenzelm@3807
     6
wenzelm@17309
     7
theory RPCParameters
wenzelm@17309
     8
imports MemoryParameters
wenzelm@17309
     9
begin
wenzelm@3807
    10
wenzelm@21624
    11
(*
wenzelm@21624
    12
  For simplicity, specify the instance of RPC that is used in the
wenzelm@21624
    13
  memory implementation.
wenzelm@21624
    14
*)
wenzelm@21624
    15
blanchet@58310
    16
datatype rpcOp = memcall memOp | othercall Vals
blanchet@58310
    17
datatype rpcState = rpcA | rpcB
wenzelm@3807
    18
wenzelm@62145
    19
axiomatization RPCFailure :: Vals and BadCall :: Vals
wenzelm@62145
    20
where
wenzelm@3807
    21
  (* RPCFailure is different from MemVals and exceptions *)
wenzelm@60587
    22
  RFNoMemVal:        "RPCFailure \<notin> MemVal" and
wenzelm@60587
    23
  NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
wenzelm@60587
    24
  OKNotRF:           "OK \<noteq> RPCFailure" and
wenzelm@60587
    25
  BANotRF:           "BadArg \<noteq> RPCFailure"
wenzelm@3807
    26
wenzelm@62145
    27
(* Translate an rpc call to a memory call and test if the current argument
wenzelm@62145
    28
   is legal for the receiver (i.e., the memory). This can now be a little
wenzelm@62145
    29
   simpler than for the generic RPC component. RelayArg returns an arbitrary
wenzelm@62145
    30
   memory call for illegal arguments. *)
wenzelm@62145
    31
wenzelm@62145
    32
definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
wenzelm@62145
    33
  where "IsLegalRcvArg ra ==
wenzelm@62145
    34
    case ra of (memcall m) \<Rightarrow> True
wenzelm@62145
    35
             | (othercall v) \<Rightarrow> False"
wenzelm@62145
    36
wenzelm@62145
    37
definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
wenzelm@62145
    38
  where "RPCRelayArg ra ==
wenzelm@62145
    39
    case ra of (memcall m) \<Rightarrow> m
wenzelm@62145
    40
             | (othercall v) \<Rightarrow> undefined"
wenzelm@17309
    41
wenzelm@21624
    42
lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
wenzelm@21624
    43
  NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
wenzelm@17309
    44
wenzelm@3807
    45
end