isabelle: src/HOL/TLA/Memory/MemClerkParameters.thy@878f33040280 (annotated)

41589 bbd861837ebc tuned headers; wenzelm parents: 36866 diff changeset	1	(* Title: HOL/TLA/Memory/MemClerkParameters.thy
bbd861837ebc tuned headers; wenzelm parents: 36866 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
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	5	header {* RPC-Memory example: Parameters of the memory clerk *}
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 MemClerkParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	8	imports RPCParameters
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
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	11	datatype mClkState = clkA \| clkB
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	12
42018 878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	13	(* types sent on the clerk's send and receive channels are argument types
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	14	of the memory and the RPC, respectively *)
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	15	type_synonym mClkSndArgType = "memOp"
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	16	type_synonym mClkRcvArgType = "rpcOp"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	18	definition
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	(* translate a memory call to an RPC call *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	20	MClkRelayArg :: "memOp => rpcOp"
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	21	where "MClkRelayArg marg = memcall marg"
426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	22
426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	23	definition
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24	(* translate RPC failures to memory failures *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	MClkReplyVal :: "Vals => Vals"
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	26	where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	28	end

author	wenzelm
	Sun, 20 Mar 2011 23:07:06 +0100
changeset 42018	878f33040280
parent 41589	bbd861837ebc
child 58249	180f1b3508ed
permissions	-rw-r--r--