isabelle: src/HOL/TLA/Memory/MemoryParameters.thy@c43ed29bd197 (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: MemoryParameters.thy
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 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
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Theory Name: MemoryParameters
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10	RPC-Memory example: Memory parameters
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	12
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	13	theory MemoryParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	14	imports RPCMemoryParams
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	15	begin
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5184 diff changeset	17	(* the memory operations *)
db63752140c7 updated (Stephan Merz); wenzelm parents: 5184 diff changeset	18	datatype memOp = read Locs \| write Locs Vals
db63752140c7 updated (Stephan Merz); wenzelm parents: 5184 diff changeset	19
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	(* memory locations and contents *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	22	MemLoc :: "Locs set"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	23	MemVal :: "Vals set"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	(* some particular values *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	OK :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27	BadArg :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	28	MemFailure :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	29	NotAResult :: "Vals" (* defined here for simplicity *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	30
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	31	(* the initial value stored in each memory cell *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32	InitVal :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	33
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	34	axioms
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	35	(* basic assumptions about the above constants and predicates *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	36	BadArgNoMemVal: "BadArg ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	37	MemFailNoMemVal: "MemFailure ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	38	InitValMemVal: "InitVal : MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	39	NotAResultNotVal: "NotAResult ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	40	NotAResultNotOK: "NotAResult ~= OK"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	41	NotAResultNotBA: "NotAResult ~= BadArg"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	42	NotAResultNotMF: "NotAResult ~= MemFailure"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	43
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	44	ML {* use_legacy_bindings (the_context ()) *}
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	45
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	46	end

author	wenzelm
	Wed, 07 Sep 2005 20:22:39 +0200
changeset 17309	c43ed29bd197
parent 9517	f58863b1406a
child 21624	6f79647cf536
permissions	-rw-r--r--