1(* Title: HOL/HOLCF/IOA/ABP/Abschannel_finite.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>The transmission channel -- finite version\<close> 6 7theory Abschannel_finite 8imports Abschannel IOA.IOA Action Lemmas 9begin 10 11primrec reverse :: "'a list => 'a list" 12where 13 reverse_Nil: "reverse([]) = []" 14| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" 15 16definition 17 ch_fin_asig :: "'a abs_action signature" where 18 "ch_fin_asig = ch_asig" 19 20definition 21 ch_fin_trans :: "('a abs_action, 'a list)transition set" where 22 "ch_fin_trans = 23 {tr. let s = fst(tr); 24 t = snd(snd(tr)) 25 in 26 case fst(snd(tr)) 27 of S(b) => ((t = s) | 28 (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | 29 R(b) => s ~= [] & 30 b = hd(s) & 31 ((t = s) | (t = tl(s)))}" 32 33definition 34 ch_fin_ioa :: "('a abs_action, 'a list)ioa" where 35 "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})" 36 37definition 38 srch_fin_ioa :: "('m action, 'm packet list)ioa" where 39 "srch_fin_ioa = rename ch_fin_ioa srch_actions" 40 41definition 42 rsch_fin_ioa :: "('m action, bool list)ioa" where 43 "rsch_fin_ioa = rename ch_fin_ioa rsch_actions" 44 45definition 46 srch_fin_asig :: "'m action signature" where 47 "srch_fin_asig = asig_of(srch_fin_ioa)" 48 49definition 50 rsch_fin_asig :: "'m action signature" where 51 "rsch_fin_asig = asig_of(rsch_fin_ioa)" 52 53definition 54 srch_fin_trans :: "('m action, 'm packet list)transition set" where 55 "srch_fin_trans = trans_of(srch_fin_ioa)" 56 57definition 58 rsch_fin_trans :: "('m action, bool list)transition set" where 59 "rsch_fin_trans = trans_of(rsch_fin_ioa)" 60 61end 62