src/HOL/IOA/ABP/Sender.thy
changeset 1151 c820b3cc3df0
parent 1139 993e475e70e2
child 1376 92f83b9d17e1
     1.1 --- a/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:14:58 1995 +0200
     1.2 +++ b/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:47:10 1995 +0200
     1.3 @@ -27,31 +27,31 @@
     1.4  sbit_def     "sbit == snd"
     1.5  
     1.6  sender_asig_def
     1.7 -  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
     1.8 -\                  UN pkt. {S_pkt(pkt)},                   \
     1.9 -\                  {})"
    1.10 +  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
    1.11 +                  UN pkt. {S_pkt(pkt)},                   
    1.12 +                  {})"
    1.13  
    1.14 -sender_trans_def "sender_trans ==                                     \
    1.15 -\ {tr. let s = fst(tr);                                               \
    1.16 -\          t = snd(snd(tr))                                           \
    1.17 -\      in case fst(snd(tr))                                           \
    1.18 -\      of   \
    1.19 -\      Next     => if sq(s)=[] then t=s else False |                \
    1.20 -\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
    1.21 -\                  sbit(t)=sbit(s)  |                                 \
    1.22 -\      R_msg(m) => False |                                            \
    1.23 -\      S_pkt(pkt) => sq(s) ~= []  &                                   \
    1.24 -\		     hdr(pkt) = sbit(s)      &                        \
    1.25 -\                    msg(pkt) = hd(sq(s))    &                   \
    1.26 -\                    sq(t) = sq(s)           &                        \
    1.27 -\                    sbit(t) = sbit(s) |                              \
    1.28 -\      R_pkt(pkt) => False |                                          \
    1.29 -\      S_ack(b)   => False |                                          \
    1.30 -\      R_ack(b)   => if b = sbit(s) then                              \
    1.31 -\		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   \
    1.32 -\		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    1.33 +sender_trans_def "sender_trans ==                                     
    1.34 + {tr. let s = fst(tr);                                               
    1.35 +          t = snd(snd(tr))                                           
    1.36 +      in case fst(snd(tr))                                           
    1.37 +      of   
    1.38 +      Next     => if sq(s)=[] then t=s else False |                
    1.39 +      S_msg(m) => sq(t)=sq(s)@[m]   &                                
    1.40 +                  sbit(t)=sbit(s)  |                                 
    1.41 +      R_msg(m) => False |                                            
    1.42 +      S_pkt(pkt) => sq(s) ~= []  &                                   
    1.43 +		     hdr(pkt) = sbit(s)      &                        
    1.44 +                    msg(pkt) = hd(sq(s))    &                   
    1.45 +                    sq(t) = sq(s)           &                        
    1.46 +                    sbit(t) = sbit(s) |                              
    1.47 +      R_pkt(pkt) => False |                                          
    1.48 +      S_ack(b)   => False |                                          
    1.49 +      R_ack(b)   => if b = sbit(s) then                              
    1.50 +		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
    1.51 +		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    1.52  
    1.53 -sender_ioa_def "sender_ioa == \
    1.54 -\ (sender_asig, {([],True)}, sender_trans)"
    1.55 +sender_ioa_def "sender_ioa == 
    1.56 + (sender_asig, {([],True)}, sender_trans)"
    1.57  
    1.58  end