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