1 (* Title: HOLCF/IOA/ABP/Abschannels.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* The transmission channel -- finite version *} |
|
6 |
|
7 theory Abschannel_finite |
|
8 imports Abschannel IOA Action Lemmas |
|
9 begin |
|
10 |
|
11 primrec reverse :: "'a list => 'a list" |
|
12 where |
|
13 reverse_Nil: "reverse([]) = []" |
|
14 | reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" |
|
15 |
|
16 definition |
|
17 ch_fin_asig :: "'a abs_action signature" where |
|
18 "ch_fin_asig = ch_asig" |
|
19 |
|
20 definition |
|
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 |
|
33 definition |
|
34 ch_fin_ioa :: "('a abs_action, 'a list)ioa" where |
|
35 "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})" |
|
36 |
|
37 definition |
|
38 srch_fin_ioa :: "('m action, 'm packet list)ioa" where |
|
39 "srch_fin_ioa = rename ch_fin_ioa srch_actions" |
|
40 |
|
41 definition |
|
42 rsch_fin_ioa :: "('m action, bool list)ioa" where |
|
43 "rsch_fin_ioa = rename ch_fin_ioa rsch_actions" |
|
44 |
|
45 definition |
|
46 srch_fin_asig :: "'m action signature" where |
|
47 "srch_fin_asig = asig_of(srch_fin_ioa)" |
|
48 |
|
49 definition |
|
50 rsch_fin_asig :: "'m action signature" where |
|
51 "rsch_fin_asig = asig_of(rsch_fin_ioa)" |
|
52 |
|
53 definition |
|
54 srch_fin_trans :: "('m action, 'm packet list)transition set" where |
|
55 "srch_fin_trans = trans_of(srch_fin_ioa)" |
|
56 |
|
57 definition |
|
58 rsch_fin_trans :: "('m action, bool list)transition set" where |
|
59 "rsch_fin_trans = trans_of(rsch_fin_ioa)" |
|
60 |
|
61 end |
|