|
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
|
|
|
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 |
|
|
|
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
|
|
|
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)"
|
|
|
47 |
|
|
|
48 |
(* Lemma 5.2 *)
|
|
|
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)))"
|
|
|
59 |
|
|
|
60 |
(* Lemma 5.3 *)
|
|
|
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)))"
|
|
|
67 |
|
|
|
68 |
(* Lemma 5.4 *)
|
|
|
69 |
inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
|
|
|
70 |
|
|
|
71 |
end
|