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