1230150Sadrian(* Title: HOL/HOLCF/IOA/ABP/Abschannel_finite.thy 2230150Sadrian Author: Olaf M��ller 3230150Sadrian*) 4230150Sadrian 5230150Sadriansection \<open>The transmission channel -- finite version\<close> 6230150Sadrian 7230150Sadriantheory Abschannel_finite 8230150Sadrianimports Abschannel IOA.IOA Action Lemmas 9230150Sadrianbegin 10230150Sadrian 11230150Sadrianprimrec reverse :: "'a list => 'a list" 12230150Sadrianwhere 13230150Sadrian reverse_Nil: "reverse([]) = []" 14230150Sadrian| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" 15230150Sadrian 16230150Sadriandefinition 17230150Sadrian ch_fin_asig :: "'a abs_action signature" where 18230150Sadrian "ch_fin_asig = ch_asig" 19230150Sadrian 20230150Sadriandefinition 21230150Sadrian ch_fin_trans :: "('a abs_action, 'a list)transition set" where 22230150Sadrian "ch_fin_trans = 23230150Sadrian {tr. let s = fst(tr); 24230150Sadrian t = snd(snd(tr)) 25230150Sadrian in 26230150Sadrian case fst(snd(tr)) 27230150Sadrian of S(b) => ((t = s) | 28230150Sadrian (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | 29230150Sadrian R(b) => s ~= [] & 30230150Sadrian b = hd(s) & 31230150Sadrian ((t = s) | (t = tl(s)))}" 32230150Sadrian 33230150Sadriandefinition 34230150Sadrian ch_fin_ioa :: "('a abs_action, 'a list)ioa" where 35230150Sadrian "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})" 36230150Sadrian 37300823Siandefinition 38230150Sadrian srch_fin_ioa :: "('m action, 'm packet list)ioa" where 39230150Sadrian "srch_fin_ioa = rename ch_fin_ioa srch_actions" 40230150Sadrian 41230150Sadriandefinition 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