Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/RPCParameters.thy
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04 
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -16,32 +16,28 @@
 datatype rpcOp = memcall memOp | othercall Vals
 datatype rpcState = rpcA | rpcB
 
-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  :: "rpcOp \<Rightarrow> bool"
-  RPCRelayArg    :: "rpcOp \<Rightarrow> memOp"
-
-axiomatization where
+axiomatization RPCFailure :: Vals and BadCall :: Vals
+where
   (* RPCFailure is different from MemVals and exceptions *)
   RFNoMemVal:        "RPCFailure \<notin> MemVal" and
   NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
   OKNotRF:           "OK \<noteq> RPCFailure" and
   BANotRF:           "BadArg \<noteq> RPCFailure"
 
-defs
-  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
-                         case ra of (memcall m) \<Rightarrow> True
-                                  | (othercall v) \<Rightarrow> False"
-  RPCRelayArg_def:   "RPCRelayArg ra ==
-                         case ra of (memcall m) \<Rightarrow> m
-                                  | (othercall v) \<Rightarrow> undefined"
+(* 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. *)
+
+definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
+  where "IsLegalRcvArg ra ==
+    case ra of (memcall m) \<Rightarrow> True
+             | (othercall v) \<Rightarrow> False"
+
+definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
+  where "RPCRelayArg ra ==
+    case ra of (memcall m) \<Rightarrow> m
+             | (othercall v) \<Rightarrow> undefined"
 
 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
   NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
isabelle