isabelle: src/HOL/TLA/Memory/RPCParameters.thy@0318b43ee95c (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
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 58310 diff changeset	5	section {* RPC-Memory example: RPC parameters *}
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
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20	(* some particular return values *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	21	RPCFailure :: Vals
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	22	BadCall :: Vals
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	23
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24	(* Translate an rpc call to a memory call and test if the current argument
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	is legal for the receiver (i.e., the memory). This can now be a little
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	simpler than for the generic RPC component. RelayArg returns an arbitrary
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27	memory call for illegal arguments. *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	28	IsLegalRcvArg :: "rpcOp => bool"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	29	RPCRelayArg :: "rpcOp => memOp"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	30
47968 3119ad2b5ad3 eliminated old 'axioms'; wenzelm parents: 41589 diff changeset	31	axiomatization where
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32	(* RPCFailure is different from MemVals and exceptions *)
60587 0318b43ee95c more symbols; wenzelm parents: 58889 diff changeset	33	RFNoMemVal: "RPCFailure \<notin> MemVal" and
0318b43ee95c more symbols; wenzelm parents: 58889 diff changeset	34	NotAResultNotRF: "NotAResult \<noteq> RPCFailure" and
0318b43ee95c more symbols; wenzelm parents: 58889 diff changeset	35	OKNotRF: "OK \<noteq> RPCFailure" and
0318b43ee95c more symbols; wenzelm parents: 58889 diff changeset	36	BANotRF: "BadArg \<noteq> RPCFailure"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	37
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	38	defs
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	39	IsLegalRcvArg_def: "IsLegalRcvArg ra ==
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	40	case ra of (memcall m) => True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	41	\| (othercall v) => False"
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	42	RPCRelayArg_def: "RPCRelayArg ra ==
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	43	case ra of (memcall m) => m
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	44	\| (othercall v) => undefined"
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	45
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	46	lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	47	NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	48
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	49	end

author	wenzelm
	Fri, 26 Jun 2015 11:44:22 +0200
changeset 60587	0318b43ee95c
parent 58889	5b7a9633cfa8
child 60588	750c533459b1
permissions	-rw-r--r--