|
(* Title: HOL/TLA/Memory/MemoryParameters.thy
Author: Stephan Merz, University of Munich
*)
section \<open>RPC-Memory example: Memory parameters\<close>
theory MemoryParameters
imports RPCMemoryParams
begin
(* the memory operations *)
datatype memOp = read Locs | "write" Locs Vals
consts
(* memory locations and contents *)
MemLoc :: "Locs set"
MemVal :: "Vals set"
(* some particular values *)
OK :: "Vals"
BadArg :: "Vals"
MemFailure :: "Vals"
NotAResult :: "Vals" (* defined here for simplicity *)
(* the initial value stored in each memory cell *)
InitVal :: "Vals"
axiomatization where
(* basic assumptions about the above constants and predicates *)
BadArgNoMemVal: "BadArg \ MemVal" and
MemFailNoMemVal: "MemFailure \ MemVal" and
InitValMemVal: "InitVal \ MemVal" and
NotAResultNotVal: "NotAResult \ MemVal" and
NotAResultNotOK: "NotAResult \ OK" and
NotAResultNotBA: "NotAResult \ BadArg" and
NotAResultNotMF: "NotAResult \ MemFailure"
lemmas [simp] =
BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
NotAResultNotOK NotAResultNotBA NotAResultNotMF
NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
lemma MemValNotAResultE: "\ x \ MemVal; (x \ NotAResult \ P) \ \ P"
using NotAResultNotVal by blast
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
