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