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