src/HOL/TLA/Memory/MemoryParameters.thy

Added specific code generator for number_of.

(*
    File:        MemoryParameters.thy
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

    Theory Name: MemoryParameters
    Logic Image: TLA

    RPC-Memory example: Memory parameters
*)

MemoryParameters = Datatype + RPCMemoryParams +

(* 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"

rules
  (* basic assumptions about the above constants and predicates *)
  BadArgNoMemVal    "BadArg ~: MemVal"
  MemFailNoMemVal   "MemFailure ~: MemVal"
  InitValMemVal     "InitVal : MemVal"
  NotAResultNotVal  "NotAResult ~: MemVal"
  NotAResultNotOK   "NotAResult ~= OK"
  NotAResultNotBA   "NotAResult ~= BadArg"
  NotAResultNotMF   "NotAResult ~= MemFailure"
end