|
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
|
|
|
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
|