src/HOL/IOA/ABP/Receiver.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1476 608483c2122a
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
mueller@1139
     1
(*  Title:      HOL/IOA/example/Receiver.thy
nipkow@1050
     2
    ID:         $Id$
mueller@1139
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1139
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
The implementation: receiver
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Receiver = List + IOA + Action + Lemmas +
nipkow@1050
    10
nipkow@1050
    11
types 
nipkow@1050
    12
nipkow@1050
    13
'm receiver_state
nipkow@1050
    14
= "'m list * bool"
nipkow@1050
    15
(* messages  mode *)
nipkow@1050
    16
nipkow@1050
    17
consts
nipkow@1050
    18
clasohm@1376
    19
  receiver_asig :: 'm action signature
clasohm@1376
    20
  receiver_trans:: ('m action, 'm receiver_state)transition set
clasohm@1376
    21
  receiver_ioa  :: ('m action, 'm receiver_state)ioa
clasohm@1376
    22
  rq            :: 'm receiver_state => 'm list
clasohm@1376
    23
  rbit          :: 'm receiver_state => bool
nipkow@1050
    24
nipkow@1050
    25
defs
nipkow@1050
    26
nipkow@1050
    27
rq_def       "rq == fst"
nipkow@1050
    28
rbit_def     "rbit == snd"
nipkow@1050
    29
clasohm@1151
    30
receiver_asig_def "receiver_asig ==            
clasohm@1151
    31
 (UN pkt. {R_pkt(pkt)},                       
clasohm@1151
    32
  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
clasohm@1151
    33
  {})"
nipkow@1050
    34
clasohm@1151
    35
receiver_trans_def "receiver_trans ==                                    
clasohm@1151
    36
 {tr. let s = fst(tr);                                                  
clasohm@1151
    37
          t = snd(snd(tr))                                              
clasohm@1151
    38
      in                                                                
clasohm@1151
    39
      case fst(snd(tr))                                                 
clasohm@1151
    40
      of   
clasohm@1151
    41
      Next    =>  False |     
clasohm@1151
    42
      S_msg(m) => False |                                               
clasohm@1151
    43
      R_msg(m) => (rq(s) ~= [])  &                                     
clasohm@1476
    44
                   m = hd(rq(s))  &                             
clasohm@1476
    45
                   rq(t) = tl(rq(s))   &                              
clasohm@1151
    46
                  rbit(t)=rbit(s)  |                                 
clasohm@1151
    47
      S_pkt(pkt) => False |                                          
clasohm@1151
    48
      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
clasohm@1476
    49
                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
clasohm@1476
    50
                         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
clasohm@1151
    51
      S_ack(b) => b = rbit(s)                        &               
clasohm@1151
    52
                      rq(t) = rq(s)                    &             
clasohm@1151
    53
                      rbit(t)=rbit(s) |                              
clasohm@1151
    54
      R_ack(b) => False}"
nipkow@1050
    55
clasohm@1151
    56
receiver_ioa_def "receiver_ioa == 
clasohm@1151
    57
 (receiver_asig, {([],False)}, receiver_trans)"
nipkow@1050
    58
nipkow@1050
    59
end