|
168
|
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 |
|
|
156
|
9 |
Impl = Sender + Receiver + Channels +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
|
|
|
13 |
'm impl_state
|
|
|
14 |
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
|
|
|
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 multiset"
|
|
|
23 |
rsch :: "'m impl_state => bool multiset"
|
|
|
24 |
inv1, inv2,
|
|
|
25 |
inv3, inv4 :: "'m impl_state => bool"
|
|
|
26 |
hdr_sum :: "'m packet multiset => bool => nat"
|
|
|
27 |
|
|
168
|
28 |
defs
|
|
156
|
29 |
|
|
|
30 |
impl_def
|
|
|
31 |
"impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
|
|
|
32 |
|
|
|
33 |
sen_def "sen == fst"
|
|
|
34 |
rec_def "rec == fst o snd"
|
|
|
35 |
srch_def "srch == fst o snd o snd"
|
|
|
36 |
rsch_def "rsch == snd o snd o snd"
|
|
|
37 |
|
|
|
38 |
hdr_sum_def
|
|
|
39 |
"hdr_sum(M,b) == countm(M,%pkt.hdr(pkt) = b)"
|
|
|
40 |
|
|
|
41 |
(* Lemma 5.1 *)
|
|
|
42 |
inv1_def
|
|
249
|
43 |
"inv1(s) ==
|
|
|
44 |
(!b. count(rsent(rec(s)),b) = count(srcvd(sen(s)),b) + count(rsch(s),b))
|
|
|
45 |
& (!b. count(ssent(sen(s)),b)
|
|
|
46 |
= hdr_sum(rrcvd(rec(s)),b) + hdr_sum(srch(s),b))"
|
|
156
|
47 |
|
|
|
48 |
(* Lemma 5.2 *)
|
|
249
|
49 |
inv2_def "inv2(s) ==
|
|
|
50 |
(rbit(rec(s)) = sbit(sen(s)) &
|
|
|
51 |
ssending(sen(s)) &
|
|
|
52 |
count(rsent(rec(s)),~sbit(sen(s))) <= count(ssent(sen(s)),~sbit(sen(s))) &
|
|
|
53 |
count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))))
|
|
|
54 |
|
|
|
|
55 |
(rbit(rec(s)) = (~sbit(sen(s))) &
|
|
|
56 |
rsending(rec(s)) &
|
|
|
57 |
count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))) &
|
|
|
58 |
count(rsent(rec(s)),sbit(sen(s))) <= count(ssent(sen(s)),sbit(sen(s))))"
|
|
156
|
59 |
|
|
|
60 |
(* Lemma 5.3 *)
|
|
249
|
61 |
inv3_def "inv3(s) ==
|
|
|
62 |
rbit(rec(s)) = sbit(sen(s))
|
|
|
63 |
--> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
|
|
|
64 |
--> count(rrcvd(rec(s)),<sbit(sen(s)),m>)
|
|
|
65 |
+ count(srch(s),<sbit(sen(s)),m>)
|
|
|
66 |
<= count(rsent(rec(s)),~sbit(sen(s))))"
|
|
156
|
67 |
|
|
|
68 |
(* Lemma 5.4 *)
|
|
|
69 |
inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
|
|
|
70 |
|
|
|
71 |
end
|