41589
|
1 |
(* Title: HOL/TLA/Memory/MemoryParameters.thy
|
|
2 |
Author: Stephan Merz, University of Munich
|
21624
|
3 |
*)
|
3807
|
4 |
|
60592
|
5 |
section \<open>RPC-Memory example: Memory parameters\<close>
|
3807
|
6 |
|
17309
|
7 |
theory MemoryParameters
|
|
8 |
imports RPCMemoryParams
|
|
9 |
begin
|
3807
|
10 |
|
6255
|
11 |
(* the memory operations *)
|
58310
|
12 |
datatype memOp = read Locs | "write" Locs Vals
|
6255
|
13 |
|
3807
|
14 |
consts
|
|
15 |
(* memory locations and contents *)
|
17309
|
16 |
MemLoc :: "Locs set"
|
|
17 |
MemVal :: "Vals set"
|
3807
|
18 |
|
|
19 |
(* some particular values *)
|
|
20 |
OK :: "Vals"
|
|
21 |
BadArg :: "Vals"
|
|
22 |
MemFailure :: "Vals"
|
|
23 |
NotAResult :: "Vals" (* defined here for simplicity *)
|
17309
|
24 |
|
3807
|
25 |
(* the initial value stored in each memory cell *)
|
|
26 |
InitVal :: "Vals"
|
|
27 |
|
47968
|
28 |
axiomatization where
|
3807
|
29 |
(* basic assumptions about the above constants and predicates *)
|
60587
|
30 |
BadArgNoMemVal: "BadArg \<notin> MemVal" and
|
|
31 |
MemFailNoMemVal: "MemFailure \<notin> MemVal" and
|
47968
|
32 |
InitValMemVal: "InitVal : MemVal" and
|
60587
|
33 |
NotAResultNotVal: "NotAResult \<notin> MemVal" and
|
|
34 |
NotAResultNotOK: "NotAResult \<noteq> OK" and
|
|
35 |
NotAResultNotBA: "NotAResult \<noteq> BadArg" and
|
|
36 |
NotAResultNotMF: "NotAResult \<noteq> MemFailure"
|
17309
|
37 |
|
21624
|
38 |
lemmas [simp] =
|
|
39 |
BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
|
|
40 |
NotAResultNotOK NotAResultNotBA NotAResultNotMF
|
|
41 |
NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
|
|
42 |
|
60588
|
43 |
lemma MemValNotAResultE: "\<lbrakk> x \<in> MemVal; (x \<noteq> NotAResult \<Longrightarrow> P) \<rbrakk> \<Longrightarrow> P"
|
21624
|
44 |
using NotAResultNotVal by blast
|
17309
|
45 |
|
3807
|
46 |
end
|