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