src/HOL/TLA/Memory/MemoryParameters.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 47968 3119ad2b5ad3
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/MemoryParameters.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: Memory parameters *}
     6 
     7 theory MemoryParameters
     8 imports RPCMemoryParams
     9 begin
    10 
    11 (* the memory operations *)
    12 datatype memOp = read Locs | "write" Locs Vals
    13 
    14 consts
    15   (* memory locations and contents *)
    16   MemLoc         :: "Locs set"
    17   MemVal         :: "Vals set"
    18 
    19   (* some particular values *)
    20   OK             :: "Vals"
    21   BadArg         :: "Vals"
    22   MemFailure     :: "Vals"
    23   NotAResult     :: "Vals"  (* defined here for simplicity *)
    24 
    25   (* the initial value stored in each memory cell *)
    26   InitVal        :: "Vals"
    27 
    28 axioms
    29   (* basic assumptions about the above constants and predicates *)
    30   BadArgNoMemVal:    "BadArg ~: MemVal"
    31   MemFailNoMemVal:   "MemFailure ~: MemVal"
    32   InitValMemVal:     "InitVal : MemVal"
    33   NotAResultNotVal:  "NotAResult ~: MemVal"
    34   NotAResultNotOK:   "NotAResult ~= OK"
    35   NotAResultNotBA:   "NotAResult ~= BadArg"
    36   NotAResultNotMF:   "NotAResult ~= MemFailure"
    37 
    38 lemmas [simp] =
    39   BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
    40   NotAResultNotOK NotAResultNotBA NotAResultNotMF
    41   NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
    42 
    43 lemma MemValNotAResultE: "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P"
    44   using NotAResultNotVal by blast
    45 
    46 end