1(*  Title:      HOL/HOLCF/IOA/Storage/Spec.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The specification of a memory\<close>
6
7theory Spec
8imports IOA.IOA Action
9begin
10
11definition
12  spec_sig :: "action signature" where
13  "spec_sig = (\<Union>l.{Free l} \<union> {New},
14               \<Union>l.{Loc l},
15               {})"
16
17definition
18  spec_trans :: "(action, nat set \<times> bool)transition set" where
19  "spec_trans =
20   {tr. let s = fst(tr); used = fst s; c = snd s;
21            t = snd(snd(tr)); used' = fst t; c' = snd t
22        in
23        case fst(snd(tr))
24        of
25        New       \<Rightarrow> used' = used \<and> c'  |
26        Loc l     \<Rightarrow> c \<and> l \<notin> used \<and> used'= used \<union> {l} \<and> \<not>c'   |
27        Free l    \<Rightarrow> used'=used - {l} \<and> c'=c}"
28
29definition
30  spec_ioa :: "(action, nat set \<times> bool)ioa" where
31  "spec_ioa = (spec_sig, {({},False)}, spec_trans,{},{})"
32
33end
34