equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/example/Impl.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The implementation |
|
7 *) |
|
8 |
1 Impl = Sender + Receiver + Channels + |
9 Impl = Sender + Receiver + Channels + |
2 |
10 |
3 types |
11 types |
4 |
12 |
5 'm impl_state |
13 'm impl_state |
15 rsch :: "'m impl_state => bool multiset" |
23 rsch :: "'m impl_state => bool multiset" |
16 inv1, inv2, |
24 inv1, inv2, |
17 inv3, inv4 :: "'m impl_state => bool" |
25 inv3, inv4 :: "'m impl_state => bool" |
18 hdr_sum :: "'m packet multiset => bool => nat" |
26 hdr_sum :: "'m packet multiset => bool => nat" |
19 |
27 |
20 rules |
28 defs |
21 |
29 |
22 impl_def |
30 impl_def |
23 "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" |
31 "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" |
24 |
32 |
25 sen_def "sen == fst" |
33 sen_def "sen == fst" |