equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/ABP/Impl.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Olaf Mueller |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 The implementation |
|
7 *) |
|
8 |
|
9 Impl = Sender + Receiver + Abschannel + |
|
10 |
|
11 types |
|
12 |
|
13 'm impl_state |
|
14 = "'m sender_state * 'm receiver_state * 'm packet list * bool list" |
|
15 (* sender_state * receiver_state * srch_state * rsch_state *) |
|
16 |
|
17 |
|
18 consts |
|
19 impl_ioa :: "('m action, 'm impl_state)ioa" |
|
20 sen :: "'m impl_state => 'm sender_state" |
|
21 rec :: "'m impl_state => 'm receiver_state" |
|
22 srch :: "'m impl_state => 'm packet list" |
|
23 rsch :: "'m impl_state => bool list" |
|
24 |
|
25 defs |
|
26 |
|
27 impl_def |
|
28 "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" |
|
29 |
|
30 sen_def "sen == fst" |
|
31 rec_def "rec == fst o snd" |
|
32 srch_def "srch == fst o snd o snd" |
|
33 rsch_def "rsch == snd o snd o snd" |
|
34 |
|
35 end |