isabelle: src/HOL/TLA/Memory/MemoryParameters.thy@e8552cba702d (annotated)

41589 bbd861837ebc tuned headers; wenzelm parents: 36504 diff changeset	1	(* Title: HOL/TLA/Memory/MemoryParameters.thy
bbd861837ebc tuned headers; wenzelm parents: 36504 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: Memory parameters *}
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: 9517 diff changeset	7	theory MemoryParameters
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	8	imports RPCMemoryParams
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	9	begin
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5184 diff changeset	11	(* the memory operations *)
36504 7cc639e20cb2 avoid clash with keyword 'write'; wenzelm parents: 21624 diff changeset	12	datatype memOp = read Locs \| "write" Locs Vals
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5184 diff changeset	13
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	15	(* memory locations and contents *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	16	MemLoc :: "Locs set"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	17	MemVal :: "Vals set"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	(* some particular values *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20	OK :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	BadArg :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	22	MemFailure :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	23	NotAResult :: "Vals" (* defined here for simplicity *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	24
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	(* the initial value stored in each memory cell *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	InitVal :: "Vals"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	28	axioms
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	29	(* basic assumptions about the above constants and predicates *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	30	BadArgNoMemVal: "BadArg ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	31	MemFailNoMemVal: "MemFailure ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	32	InitValMemVal: "InitVal : MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	33	NotAResultNotVal: "NotAResult ~: MemVal"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	34	NotAResultNotOK: "NotAResult ~= OK"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	35	NotAResultNotBA: "NotAResult ~= BadArg"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	36	NotAResultNotMF: "NotAResult ~= MemFailure"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 9517 diff changeset	37
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	38	lemmas [simp] =
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	39	BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	40	NotAResultNotOK NotAResultNotBA NotAResultNotMF
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	41	NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	42
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	43	lemma MemValNotAResultE: "[\| x : MemVal; (x ~= NotAResult ==> P) \|] ==> P"
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	44	using NotAResultNotVal by blast
17309 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
	Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389	e8552cba702d
parent 41589	bbd861837ebc
child 47968	3119ad2b5ad3
permissions	-rw-r--r--