src/HOL/IOA/ABP/Sender.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1476 608483c2122a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/IOA/example/Sender.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 The implementation: sender
     7 *)
     8 
     9 Sender = IOA + Action + List + Lemmas +
    10 
    11 types
    12 
    13 'm sender_state = "'m list  *  bool"
    14 (*                messages     Alternating Bit   *)
    15 
    16 consts
    17 
    18 sender_asig   :: 'm action signature
    19 sender_trans  :: ('m action, 'm sender_state)transition set
    20 sender_ioa    :: ('m action, 'm sender_state)ioa
    21 sq            :: 'm sender_state => 'm list
    22 sbit          :: 'm sender_state => bool
    23 
    24 defs
    25 
    26 sq_def       "sq == fst"
    27 sbit_def     "sbit == snd"
    28 
    29 sender_asig_def
    30   "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
    31                   UN pkt. {S_pkt(pkt)},                   
    32                   {})"
    33 
    34 sender_trans_def "sender_trans ==                                     
    35  {tr. let s = fst(tr);                                               
    36           t = snd(snd(tr))                                           
    37       in case fst(snd(tr))                                           
    38       of   
    39       Next     => if sq(s)=[] then t=s else False |                
    40       S_msg(m) => sq(t)=sq(s)@[m]   &                                
    41                   sbit(t)=sbit(s)  |                                 
    42       R_msg(m) => False |                                            
    43       S_pkt(pkt) => sq(s) ~= []  &                                   
    44                      hdr(pkt) = sbit(s)      &                        
    45                     msg(pkt) = hd(sq(s))    &                   
    46                     sq(t) = sq(s)           &                        
    47                     sbit(t) = sbit(s) |                              
    48       R_pkt(pkt) => False |                                          
    49       S_ack(b)   => False |                                          
    50       R_ack(b)   => if b = sbit(s) then                              
    51                      sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
    52                      sq(t)=sq(s) & sbit(t)=sbit(s)}"
    53 
    54 sender_ioa_def "sender_ioa == 
    55  (sender_asig, {([],True)}, sender_trans)"
    56 
    57 end