1(* Title: HOL/HOLCF/IOA/ABP/Abschannel.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>The transmission channel\<close> 6 7theory Abschannel 8imports IOA.IOA Action Lemmas 9begin 10 11datatype 'a abs_action = S 'a | R 'a 12 13 14(********************************************************** 15 G e n e r i c C h a n n e l 16 *********************************************************) 17 18definition 19 ch_asig :: "'a abs_action signature" where 20 "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" 21 22definition 23 ch_trans :: "('a abs_action, 'a list)transition set" where 24 "ch_trans = 25 {tr. let s = fst(tr); 26 t = snd(snd(tr)) 27 in 28 case fst(snd(tr)) 29 of S(b) => ((t = s) | (t = s @ [b])) | 30 R(b) => s ~= [] & 31 b = hd(s) & 32 ((t = s) | (t = tl(s)))}" 33 34definition 35 ch_ioa :: "('a abs_action, 'a list)ioa" where 36 "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})" 37 38 39(********************************************************** 40 C o n c r e t e C h a n n e l s b y R e n a m i n g 41 *********************************************************) 42 43definition 44 rsch_actions :: "'m action => bool abs_action option" where 45 "rsch_actions (akt) = 46 (case akt of 47 Next => None | 48 S_msg(m) => None | 49 R_msg(m) => None | 50 S_pkt(packet) => None | 51 R_pkt(packet) => None | 52 S_ack(b) => Some(S(b)) | 53 R_ack(b) => Some(R(b)))" 54 55definition 56 srch_actions :: "'m action =>(bool * 'm) abs_action option" where 57 "srch_actions akt = 58 (case akt of 59 Next => None | 60 S_msg(m) => None | 61 R_msg(m) => None | 62 S_pkt(p) => Some(S(p)) | 63 R_pkt(p) => Some(R(p)) | 64 S_ack(b) => None | 65 R_ack(b) => None)" 66 67definition 68 srch_ioa :: "('m action, 'm packet list)ioa" where 69 "srch_ioa = rename ch_ioa srch_actions" 70definition 71 rsch_ioa :: "('m action, bool list)ioa" where 72 "rsch_ioa = rename ch_ioa rsch_actions" 73 74definition 75 srch_asig :: "'m action signature" where 76 "srch_asig = asig_of(srch_ioa)" 77 78definition 79 rsch_asig :: "'m action signature" where 80 "rsch_asig = asig_of(rsch_ioa)" 81 82definition 83 srch_trans :: "('m action, 'm packet list)transition set" where 84 "srch_trans = trans_of(srch_ioa)" 85definition 86 rsch_trans :: "('m action, bool list)transition set" where 87 "rsch_trans = trans_of(rsch_ioa)" 88 89end 90