equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/example/Spec.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* The implementation of a memory *} |
|
6 |
|
7 theory Impl |
|
8 imports IOA Action |
|
9 begin |
|
10 |
|
11 definition |
|
12 impl_sig :: "action signature" where |
|
13 "impl_sig = (UN l.{Free l} Un {New}, |
|
14 UN l.{Loc l}, |
|
15 {})" |
|
16 |
|
17 definition |
|
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 => k' = k & b' | |
|
26 Loc l => b & l= k & k'= (Suc k) & ~b' | |
|
27 Free l => k'=k & b'=b}" |
|
28 |
|
29 definition |
|
30 impl_ioa :: "(action, nat * bool)ioa" where |
|
31 "impl_ioa = (impl_sig, {(0,False)}, impl_trans,{},{})" |
|
32 |
|
33 lemma in_impl_asig: |
|
34 "New : actions(impl_sig) & |
|
35 Loc l : actions(impl_sig) & |
|
36 Free l : actions(impl_sig) " |
|
37 by (simp add: impl_sig_def actions_def asig_projections) |
|
38 |
|
39 end |