1 (* Title: HOL/IOA/example/Spec.thy |
1 (* Title: HOL/IOA/example/Spec.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 |
|
5 The specification of a memory. |
|
6 *) |
4 *) |
7 |
5 |
8 Spec = IOA + Action + |
6 header {* The specification of a memory *} |
9 |
7 |
|
8 theory Spec |
|
9 imports IOA Action |
|
10 begin |
10 |
11 |
11 consts |
12 consts |
12 |
13 |
13 spec_sig :: "action signature" |
14 spec_sig :: "action signature" |
14 spec_trans :: "(action, nat set * bool)transition set" |
15 spec_trans :: "(action, nat set * bool)transition set" |
15 spec_ioa :: "(action, nat set * bool)ioa" |
16 spec_ioa :: "(action, nat set * bool)ioa" |
16 |
17 |
17 defs |
18 defs |
18 |
19 |
19 sig_def "spec_sig == (UN l.{Free l} Un {New}, |
20 sig_def: "spec_sig == (UN l.{Free l} Un {New}, |
20 UN l.{Loc l}, |
21 UN l.{Loc l}, |
21 {})" |
22 {})" |
22 |
23 |
23 trans_def "spec_trans == |
24 trans_def: "spec_trans == |
24 {tr. let s = fst(tr); used = fst s; c = snd s; |
25 {tr. let s = fst(tr); used = fst s; c = snd s; |
25 t = snd(snd(tr)); used' = fst t; c' = snd t |
26 t = snd(snd(tr)); used' = fst t; c' = snd t |
26 in |
27 in |
27 case fst(snd(tr)) |
28 case fst(snd(tr)) |
28 of |
29 of |
29 New => used' = used & c' | |
30 New => used' = used & c' | |
30 Loc l => c & l~:used & used'= used Un {l} & ~c' | |
31 Loc l => c & l~:used & used'= used Un {l} & ~c' | |
31 Free l => used'=used - {l} & c'=c}" |
32 Free l => used'=used - {l} & c'=c}" |
32 |
33 |
33 ioa_def "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})" |
34 ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})" |
|
35 |
|
36 ML {* use_legacy_bindings (the_context ()) *} |
34 |
37 |
35 end |
38 end |