isabelle: src/HOL/TLA/Memory/MemClerkParameters.thy@5fe899199f85 (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: MemClerkParameters.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: Parameters of the memory clerk *}
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 MemClerkParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	11	imports RPCParameters
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
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	14	datatype mClkState = clkA \| clkB
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	15
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16	types
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17	(* types sent on the clerk's send and receive channels are argument types
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18	of the memory and the RPC, respectively *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	19	mClkSndArgType = "memOp"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	20	mClkRcvArgType = "rpcOp"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	22	constdefs
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	23	(* translate a memory call to an RPC call *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	24	MClkRelayArg :: "memOp => rpcOp"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	25	"MClkRelayArg marg == memcall marg"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	(* translate RPC failures to memory failures *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27	MClkReplyVal :: "Vals => Vals"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	28	"MClkReplyVal v == if v = RPCFailure then MemFailure else v"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	29
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	30	end

author	wenzelm
	Sat, 14 Jun 2008 23:19:51 +0200
changeset 27208	5fe899199f85
parent 21624	6f79647cf536
child 36866	426d5781bb25
permissions	-rw-r--r--