isabelle: src/HOL/TLA/Memory/MemClerkParameters.thy@aefdb9e664c9 (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
60592 c9bd1d902f04 isabelle update_cartouches; wenzelm parents: 60588 diff changeset	5	section \<open>RPC-Memory example: Parameters of the memory clerk\<close>
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
58310 91ea607a34d8 updated news blanchet parents: 58249 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 *)
60588 750c533459b1 more symbols; wenzelm parents: 58889 diff changeset	20	MClkRelayArg :: "memOp \<Rightarrow> 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 *)
60588 750c533459b1 more symbols; wenzelm parents: 58889 diff changeset	25	MClkReplyVal :: "Vals \<Rightarrow> 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
	Tue, 23 May 2017 10:59:01 +0200
changeset 65908	aefdb9e664c9
parent 60592	c9bd1d902f04
permissions	-rw-r--r--