isabelle: src/HOL/TLA/Memory/RPCParameters.thy@aefdb9e664c9 (annotated)

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

author	wenzelm
	Tue, 23 May 2017 10:59:01 +0200
changeset 65908	aefdb9e664c9
parent 62145	5b946c81dfbf
permissions	-rw-r--r--