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

author	wenzelm
	Thu, 29 Apr 2010 16:53:08 +0200
changeset 36504	7cc639e20cb2
parent 21624	6f79647cf536
child 41589	bbd861837ebc
permissions	-rw-r--r--