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