|
1051
|
1 |
(* Title: HOL/IOA/NTP/Impl.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
|
4 |
Copyright 1994 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 multiset * bool multiset"
|
|
|
15 |
(* sender_state * receiver_state * srch_state * rsch_state *)
|
|
|
16 |
|
|
|
17 |
|
|
|
18 |
consts
|
|
1376
|
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
|
|
1051
|
24 |
inv1, inv2,
|
|
1376
|
25 |
inv3, inv4 :: 'm impl_state => bool
|
|
|
26 |
hdr_sum :: 'm packet multiset => bool => nat
|
|
1051
|
27 |
|
|
|
28 |
defs
|
|
|
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
|
|
1151
|
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)"
|
|
1051
|
47 |
|
|
|
48 |
(* Lemma 5.2 *)
|
|
1151
|
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)))"
|
|
1051
|
59 |
|
|
|
60 |
(* Lemma 5.3 *)
|
|
1151
|
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)))"
|
|
1051
|
67 |
|
|
|
68 |
(* Lemma 5.4 *)
|
|
|
69 |
inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
|
|
|
70 |
|
|
|
71 |
end
|