isabelle: src/HOL/TLA/Memory/MemClerkParameters.thy@61dd8c145da7 (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
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	22	definition
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"
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	25	where "MClkRelayArg marg = memcall marg"
426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	26
426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	27	definition
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	28	(* translate RPC failures to memory failures *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	29	MClkReplyVal :: "Vals => Vals"
36866 426d5781bb25 modernized specifications; wenzelm parents: 21624 diff changeset	30	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	31
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32	end

author	haftmann
	Fri, 11 Jun 2010 17:14:02 +0200
changeset 37407	61dd8c145da7
parent 36866	426d5781bb25
child 41589	bbd861837ebc
permissions	-rw-r--r--