1(* Title: HOL/HOLCF/IOA/Storage/Impl.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>The implementation of a memory\<close> 6 7theory Impl 8imports IOA.IOA Action 9begin 10 11definition 12 impl_sig :: "action signature" where 13 "impl_sig = (\<Union>l.{Free l} \<union> {New}, 14 \<Union>l.{Loc l}, 15 {})" 16 17definition 18 impl_trans :: "(action, nat * bool)transition set" where 19 "impl_trans = 20 {tr. let s = fst(tr); k = fst s; b = snd s; 21 t = snd(snd(tr)); k' = fst t; b' = snd t 22 in 23 case fst(snd(tr)) 24 of 25 New \<Rightarrow> k' = k \<and> b' | 26 Loc l \<Rightarrow> b \<and> l= k \<and> k'= (Suc k) \<and> \<not>b' | 27 Free l \<Rightarrow> k'=k \<and> b'=b}" 28 29definition 30 impl_ioa :: "(action, nat * bool)ioa" where 31 "impl_ioa = (impl_sig, {(0,False)}, impl_trans,{},{})" 32 33lemma in_impl_asig: 34 "New \<in> actions(impl_sig) \<and> 35 Loc l \<in> actions(impl_sig) \<and> 36 Free l \<in> actions(impl_sig) " 37 by (simp add: impl_sig_def actions_def asig_projections) 38 39end 40