products/sources/formale Sprachen/Delphi/Bille 0.71/__history/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: MemoryParameters.thy   Sprache: Unknown

(*  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.0 Sekunden  (vorverarbeitet)  ]