1(*  Title:      HOL/HOLCF/IOA/ABP/Impl.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The implementation\<close>
6
7theory Impl
8imports Sender Receiver Abschannel
9begin
10
11type_synonym
12  'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
13  (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
14
15definition
16 impl_ioa :: "('m action, 'm impl_state)ioa" where
17 "impl_ioa = (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
18
19definition
20 sen :: "'m impl_state => 'm sender_state" where
21 "sen = fst"
22
23definition
24 rec :: "'m impl_state => 'm receiver_state" where
25 "rec = fst \<circ> snd"
26
27definition
28 srch :: "'m impl_state => 'm packet list" where
29 "srch = fst \<circ> snd \<circ> snd"
30
31definition
32 rsch :: "'m impl_state => bool list" where
33 "rsch = snd \<circ> snd \<circ> snd"
34
35end
36