|
1050
|
1 |
(* Title: HOL/IOA/ABP/Abschannel_finite.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 act signature"
|
|
|
14 |
|
|
|
15 |
ch_fin_trans :: "('a act, 'a list)transition set"
|
|
|
16 |
|
|
|
17 |
ch_fin_ioa :: "('a act, '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 |
|