author  wenzelm 
Sat, 03 Sep 2005 16:50:22 +0200  
changeset 17244  0b2ff9541727 
parent 14981  e73f8140af78 
child 19739  c58ef2aa5430 
permissions  rwrr 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

1 
(* Title: HOL/IOA/NTP/Impl.thy 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

2 
ID: $Id$ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

3 
Author: Tobias Nipkow & Konrad Slind 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

4 
*) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

5 

17244  6 
header {* The implementation *} 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

7 

17244  8 
theory Impl 
9 
imports Sender Receiver Abschannel 

10 
begin 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

11 

17244  12 
types 
13 

14 
'm impl_state 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

15 
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

16 
(* sender_state * receiver_state * srch_state * rsch_state *) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

17 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

18 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

19 
consts 
17244  20 
impl_ioa :: "('m action, 'm impl_state)ioa" 
21 
sen :: "'m impl_state => 'm sender_state" 

22 
rec :: "'m impl_state => 'm receiver_state" 

23 
srch :: "'m impl_state => 'm packet multiset" 

24 
rsch :: "'m impl_state => bool multiset" 

25 
inv1 :: "'m impl_state => bool" 

26 
inv2 :: "'m impl_state => bool" 

27 
inv3 :: "'m impl_state => bool" 

28 
inv4 :: "'m impl_state => bool" 

29 
hdr_sum :: "'m packet multiset => bool => nat" 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

30 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

31 
defs 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

32 

17244  33 
impl_def: 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

34 
"impl_ioa == (sender_ioa  receiver_ioa  srch_ioa  rsch_ioa)" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

35 

17244  36 
sen_def: "sen == fst" 
37 
rec_def: "rec == fst o snd" 

38 
srch_def: "srch == fst o snd o snd" 

39 
rsch_def: "rsch == snd o snd o snd" 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

40 

17244  41 
hdr_sum_def: 
3852  42 
"hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

43 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

44 
(* Lemma 5.1 *) 
17244  45 
inv1_def: 
46 
"inv1(s) == 

47 
(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 

48 
& (!b. count (ssent(sen s)) b 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

49 
= hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

50 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

51 
(* Lemma 5.2 *) 
17244  52 
inv2_def: "inv2(s) == 
53 
(rbit(rec(s)) = sbit(sen(s)) & 

54 
ssending(sen(s)) & 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

55 
count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & 
17244  56 
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) 
57 
 

58 
(rbit(rec(s)) = (~sbit(sen(s))) & 

59 
rsending(rec(s)) & 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

60 
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) & 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

61 
count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

62 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

63 
(* Lemma 5.3 *) 
17244  64 
inv3_def: "inv3(s) == 
65 
rbit(rec(s)) = sbit(sen(s)) 

66 
> (!m. sq(sen(s))=[]  m ~= hd(sq(sen(s))) 

67 
> count (rrcvd(rec s)) (sbit(sen(s)),m) 

68 
+ count (srch s) (sbit(sen(s)),m) 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

69 
<= count (rsent(rec s)) (~sbit(sen s)))" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

70 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

71 
(* Lemma 5.4 *) 
17244  72 
inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) > sq(sen(s)) ~= []" 
73 

74 
ML {* use_legacy_bindings (the_context ()) *} 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

75 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

76 
end 