stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
even for conditional rewrites
(*
File: RPCParameters.thy
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: RPCParameters
Logic Image: TLA
RPC-Memory example: RPC parameters
For simplicity, specify the instance of RPC that is used in the
memory implementation.
*)
RPCParameters = MemoryParameters +
datatype rpcOps = remoteCall
datatype rpcState = rpcA | rpcB
types
(* type of RPC arguments other than memory calls *)
noMemArgType
(* legal arguments for (our instance of) the RPC component *)
rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)"
arities
noMemArgType :: term
consts
(* some particular return values *)
RPCFailure :: "Vals"
BadCall :: "Vals"
(* Translate an rpc call to a memory call and test if the current argument
is legal for the receiver (i.e., the memory). This can now be a little
simpler than for the generic RPC component. RelayArg returns an arbitrary
memory call for illegal arguments. *)
IsLegalRcvArg :: "rpcArgType => bool"
RPCRelayArg :: "rpcArgType => memArgType"
rules
(* RPCFailure is different from MemVals and exceptions *)
RFNoMemVal "~(MemVal RPCFailure)"
NotAResultNotRF "NotAResult ~= RPCFailure"
OKNotRF "OK ~= RPCFailure"
BANotRF "BadArg ~= RPCFailure"
IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)"
RPCRelayArg_def "RPCRelayArg ra ==
case ra of Inl (rm) => (snd rm)
| Inr (rn) => Inl (read, @ l. True)"
end