1 (* Title: HOLCF/IOA/ABP/Impl.thy |
1 (* Title: HOLCF/IOA/ABP/Impl.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 |
|
5 The implementation. |
|
6 *) |
4 *) |
7 |
5 |
8 Impl_finite = Sender + Receiver + Abschannel_finite + |
6 header {* The implementation *} |
9 |
|
10 types |
|
11 |
7 |
12 'm impl_fin_state |
8 theory Impl_finite |
13 = "'m sender_state * 'm receiver_state * 'm packet list * bool list" |
9 imports Sender Receiver Abschannel_finite |
|
10 begin |
|
11 |
|
12 types |
|
13 'm impl_fin_state |
|
14 = "'m sender_state * 'm receiver_state * 'm packet list * bool list" |
14 (* sender_state * receiver_state * srch_state * rsch_state *) |
15 (* sender_state * receiver_state * srch_state * rsch_state *) |
15 |
16 |
16 constdefs |
17 constdefs |
17 |
18 |
18 impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa |
19 impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" |
19 "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || |
20 "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || |
20 rsch_fin_ioa)" |
21 rsch_fin_ioa)" |
21 |
22 |
22 sen_fin :: 'm impl_fin_state => 'm sender_state |
23 sen_fin :: "'m impl_fin_state => 'm sender_state" |
23 "sen_fin == fst" |
24 "sen_fin == fst" |
24 |
25 |
25 rec_fin :: 'm impl_fin_state => 'm receiver_state |
26 rec_fin :: "'m impl_fin_state => 'm receiver_state" |
26 "rec_fin == fst o snd" |
27 "rec_fin == fst o snd" |
27 |
28 |
28 srch_fin :: 'm impl_fin_state => 'm packet list |
29 srch_fin :: "'m impl_fin_state => 'm packet list" |
29 "srch_fin == fst o snd o snd" |
30 "srch_fin == fst o snd o snd" |
30 |
31 |
31 rsch_fin :: 'm impl_fin_state => bool list |
32 rsch_fin :: "'m impl_fin_state => bool list" |
32 "rsch_fin == snd o snd o snd" |
33 "rsch_fin == snd o snd o snd" |
33 |
34 |
|
35 ML {* use_legacy_bindings (the_context ()) *} |
|
36 |
34 end |
37 end |
35 |
|