src/HOLCF/IOA/NTP/Impl.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@3073
     1
(*  Title:      HOL/IOA/NTP/Impl.thy
mueller@3073
     2
    ID:         $Id$
mueller@3073
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3073
     4
wenzelm@12218
     5
The implementation.
mueller@3073
     6
*)
mueller@3073
     7
mueller@3073
     8
Impl = Sender + Receiver + Abschannel +
mueller@3073
     9
mueller@3073
    10
types 
mueller@3073
    11
mueller@3073
    12
'm impl_state 
mueller@3073
    13
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
mueller@3073
    14
(*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
mueller@3073
    15
mueller@3073
    16
mueller@3073
    17
consts
mueller@3073
    18
 impl_ioa    :: ('m action, 'm impl_state)ioa
mueller@3073
    19
 sen         :: 'm impl_state => 'm sender_state
mueller@3073
    20
 rec         :: 'm impl_state => 'm receiver_state
mueller@3073
    21
 srch        :: 'm impl_state => 'm packet multiset
mueller@3073
    22
 rsch        :: 'm impl_state => bool multiset
mueller@3073
    23
 inv1, inv2, 
mueller@3073
    24
 inv3, inv4  :: 'm impl_state => bool
mueller@3073
    25
 hdr_sum     :: 'm packet multiset => bool => nat
mueller@3073
    26
mueller@3073
    27
defs
mueller@3073
    28
mueller@3073
    29
 impl_def
mueller@3073
    30
  "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
mueller@3073
    31
mueller@3073
    32
 sen_def   "sen == fst"
mueller@3073
    33
 rec_def   "rec == fst o snd"
mueller@3073
    34
 srch_def "srch == fst o snd o snd"
mueller@3073
    35
 rsch_def "rsch == snd o snd o snd"
mueller@3073
    36
mueller@3073
    37
hdr_sum_def
wenzelm@3852
    38
   "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
mueller@3073
    39
mueller@3073
    40
(* Lemma 5.1 *)
mueller@3073
    41
inv1_def 
mueller@3073
    42
  "inv1(s) ==                                                                 
mueller@3073
    43
     (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 
mueller@3073
    44
   & (!b. count (ssent(sen s)) b                                              
mueller@3073
    45
          = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
mueller@3073
    46
mueller@3073
    47
(* Lemma 5.2 *)
mueller@3073
    48
 inv2_def "inv2(s) ==                                                   
mueller@3073
    49
  (rbit(rec(s)) = sbit(sen(s)) &                                       
mueller@3073
    50
   ssending(sen(s)) &                                                  
mueller@3073
    51
   count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
mueller@3073
    52
   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))  
mueller@3073
    53
   |                                                                   
mueller@3073
    54
  (rbit(rec(s)) = (~sbit(sen(s))) &                                    
mueller@3073
    55
   rsending(rec(s)) &                                                  
mueller@3073
    56
   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
mueller@3073
    57
   count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
mueller@3073
    58
mueller@3073
    59
(* Lemma 5.3 *)
mueller@3073
    60
 inv3_def "inv3(s) ==                                                   
mueller@3073
    61
   rbit(rec(s)) = sbit(sen(s))                                         
mueller@3073
    62
   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))                        
mueller@3073
    63
        -->  count (rrcvd(rec s)) (sbit(sen(s)),m)                     
mueller@3073
    64
             + count (srch s) (sbit(sen(s)),m)                         
mueller@3073
    65
            <= count (rsent(rec s)) (~sbit(sen s)))"
mueller@3073
    66
mueller@3073
    67
(* Lemma 5.4 *)
mueller@3073
    68
 inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
mueller@3073
    69
mueller@3073
    70
end