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