1138
|
1 |
(* Title: HOL/IOA/example/Abschannels.thy
|
1050
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller
|
1138
|
4 |
Copyright 1994 TU Muenchen
|
1050
|
5 |
|
|
6 |
The transmission channel
|
|
7 |
*)
|
|
8 |
|
|
9 |
Abschannel = IOA + Action + Lemmas + List +
|
1138
|
10 |
|
|
11 |
|
1050
|
12 |
datatype ('a)act = S('a) | R('a)
|
|
13 |
|
1138
|
14 |
|
1050
|
15 |
consts
|
|
16 |
|
1376
|
17 |
ch_asig :: 'a act signature
|
|
18 |
ch_trans :: ('a act, 'a list)transition set
|
|
19 |
ch_ioa :: ('a act, 'a list)ioa
|
1050
|
20 |
|
1376
|
21 |
rsch_actions :: 'm action => bool act option
|
1050
|
22 |
srch_actions :: "'m action =>(bool * 'm) act option"
|
|
23 |
|
|
24 |
srch_asig,
|
1376
|
25 |
rsch_asig :: 'm action signature
|
1050
|
26 |
|
1376
|
27 |
srch_trans :: ('m action, 'm packet list)transition set
|
|
28 |
rsch_trans :: ('m action, bool list)transition set
|
1050
|
29 |
|
1376
|
30 |
srch_ioa :: ('m action, 'm packet list)ioa
|
|
31 |
rsch_ioa :: ('m action, bool list)ioa
|
1050
|
32 |
|
|
33 |
|
|
34 |
defs
|
|
35 |
|
|
36 |
srch_asig_def "srch_asig == asig_of(srch_ioa)"
|
|
37 |
rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
|
|
38 |
|
|
39 |
srch_trans_def "srch_trans == trans_of(srch_ioa)"
|
|
40 |
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
|
|
41 |
|
|
42 |
srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
|
|
43 |
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
|
|
44 |
|
1138
|
45 |
|
|
46 |
(**********************************************************
|
|
47 |
G e n e r i c C h a n n e l
|
|
48 |
*********************************************************)
|
|
49 |
|
1050
|
50 |
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
|
|
51 |
|
1151
|
52 |
ch_trans_def "ch_trans ==
|
|
53 |
{tr. let s = fst(tr);
|
|
54 |
t = snd(snd(tr))
|
|
55 |
in
|
|
56 |
case fst(snd(tr))
|
|
57 |
of S(b) => ((t = s) | (t = s @ [b])) |
|
|
58 |
R(b) => s ~= [] &
|
|
59 |
b = hd(s) &
|
|
60 |
((t = s) | (t = tl(s))) }"
|
1050
|
61 |
|
|
62 |
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
|
|
63 |
|
1138
|
64 |
(**********************************************************
|
|
65 |
C o n c r e t e C h a n n e l s b y R e n a m i n g
|
|
66 |
*********************************************************)
|
|
67 |
|
1151
|
68 |
rsch_actions_def "rsch_actions (akt) ==
|
|
69 |
case akt of
|
|
70 |
Next => None |
|
|
71 |
S_msg(m) => None |
|
|
72 |
R_msg(m) => None |
|
|
73 |
S_pkt(packet) => None |
|
|
74 |
R_pkt(packet) => None |
|
|
75 |
S_ack(b) => Some(S(b)) |
|
|
76 |
R_ack(b) => Some(R(b))"
|
1050
|
77 |
|
1151
|
78 |
srch_actions_def "srch_actions (akt) ==
|
|
79 |
case akt of
|
|
80 |
Next => None |
|
|
81 |
S_msg(m) => None |
|
|
82 |
R_msg(m) => None |
|
|
83 |
S_pkt(p) => Some(S(p)) |
|
|
84 |
R_pkt(p) => Some(R(p)) |
|
|
85 |
S_ack(b) => None |
|
|
86 |
R_ack(b) => None"
|
1050
|
87 |
|
|
88 |
|
|
89 |
end
|
|
90 |
|
|
91 |
|
|
92 |
|
|
93 |
|
|
94 |
|
|
95 |
|
|
96 |
|
|
97 |
|
|
98 |
|
|
99 |
|
|
100 |
|
|
101 |
|
|
102 |
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 |
|
|
107 |
|