src/HOLCF/IOA/NTP/Impl.thy
changeset 3073 88366253a09a
child 3852 e694c660055b
equal deleted inserted replaced
3072:a31419014be5 3073:88366253a09a
       
     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