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

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: RPCParameters.thy
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	3	ID: $Id$
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5	Copyright: 1997 University of Munich
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	6	*)
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	8	header {* RPC-Memory example: RPC parameters *}
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	10	theory RPCParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	11	imports MemoryParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	12	begin
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	13
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	14	(*
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	15	For simplicity, specify the instance of RPC that is used in the
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	16	memory implementation.
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	17	*)
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	18
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	19	datatype rpcOp = memcall memOp \| othercall Vals
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	20	datatype rpcState = rpcA \| rpcB
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	22	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	23	(* some particular return values *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	24	RPCFailure :: Vals
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	25	BadCall :: Vals
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27	(* 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	28	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	29	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	30	memory call for illegal arguments. *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	31	IsLegalRcvArg :: "rpcOp => bool"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	32	RPCRelayArg :: "rpcOp => memOp"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	33
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	34	axioms
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	35	(* RPCFailure is different from MemVals and exceptions *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	36	RFNoMemVal: "RPCFailure ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	37	NotAResultNotRF: "NotAResult ~= RPCFailure"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	38	OKNotRF: "OK ~= RPCFailure"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	39	BANotRF: "BadArg ~= RPCFailure"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	40
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	41	defs
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	42	IsLegalRcvArg_def: "IsLegalRcvArg 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) => True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	44	\| (othercall v) => False"
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	45	RPCRelayArg_def: "RPCRelayArg ra ==
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	46	case ra of (memcall m) => m
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 28524 diff changeset	47	\| (othercall v) => undefined"
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	48
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	49	lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	50	NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	51
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	52	end

author	wenzelm
	Mon, 06 Sep 2010 19:23:54 +0200
changeset 39162	e6ec5283cd22
parent 32960	69916a850301
child 41589	bbd861837ebc
permissions	-rw-r--r--