| author | wenzelm |
| Tue, 03 Oct 2000 22:34:49 +0200 | |
| changeset 10143 | 86c39bba873f |
| parent 3072 | a31419014be5 |
| 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/Impl.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 implementation |
|
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 |
Impl_finite = Sender + Receiver + Abschannel_finite + |
|
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 |
types |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
'm impl_fin_state |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
= "'m sender_state * 'm receiver_state * 'm packet list * bool list" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
(* sender_state * receiver_state * srch_state * rsch_state *) |
|
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 |
constdefs |
|
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 |
impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
"impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
rsch_fin_ioa)" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
sen_fin :: 'm impl_fin_state => 'm sender_state |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
"sen_fin == fst" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
rec_fin :: 'm impl_fin_state => 'm receiver_state |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
"rec_fin == fst o snd" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
srch_fin :: 'm impl_fin_state => 'm packet list |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
30 |
"srch_fin == fst o snd o snd" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
rsch_fin :: 'm impl_fin_state => bool list |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
"rsch_fin == snd o snd o snd" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
end |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |