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