|
1 (* Title: HOLCF/IOA/ABP/Abschannels.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 The transmission channel -- finite version |
|
7 *) |
|
8 |
|
9 Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List + |
|
10 |
|
11 consts |
|
12 |
|
13 ch_fin_asig :: 'a abs_action signature |
|
14 |
|
15 ch_fin_trans :: ('a abs_action, 'a list)transition set |
|
16 |
|
17 ch_fin_ioa :: ('a abs_action, 'a list)ioa |
|
18 |
|
19 srch_fin_asig, |
|
20 rsch_fin_asig :: 'm action signature |
|
21 |
|
22 srch_fin_trans :: ('m action, 'm packet list)transition set |
|
23 rsch_fin_trans :: ('m action, bool list)transition set |
|
24 |
|
25 srch_fin_ioa :: ('m action, 'm packet list)ioa |
|
26 rsch_fin_ioa :: ('m action, bool list)ioa |
|
27 |
|
28 reverse :: 'a list => 'a list |
|
29 |
|
30 primrec |
|
31 reverse List.list |
|
32 reverse_Nil "reverse([]) = []" |
|
33 reverse_Cons "reverse(x#xs) = reverse(xs)@[x]" |
|
34 |
|
35 defs |
|
36 |
|
37 srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)" |
|
38 rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)" |
|
39 |
|
40 srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)" |
|
41 rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)" |
|
42 |
|
43 srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa srch_actions" |
|
44 rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa rsch_actions" |
|
45 |
|
46 |
|
47 ch_fin_asig_def "ch_fin_asig == ch_asig" |
|
48 |
|
49 ch_fin_trans_def "ch_fin_trans == |
|
50 {tr. let s = fst(tr); |
|
51 t = snd(snd(tr)) |
|
52 in |
|
53 case fst(snd(tr)) |
|
54 of S(b) => ((t = s) | |
|
55 (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | |
|
56 R(b) => s ~= [] & |
|
57 b = hd(s) & |
|
58 ((t = s) | (t = tl(s))) }" |
|
59 |
|
60 ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)" |
|
61 |
|
62 end |
|
63 |
|
64 |
|
65 |
|
66 |
|
67 |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 |
|
75 |
|
76 |
|
77 |
|
78 |
|
79 |
|
80 |