src/HOL/IOA/ABP/Impl.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/IOA/example/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 list * bool list"
    15 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    16 
    17 
    18 constdefs
    19 
    20  impl_ioa    :: ('m action, 'm impl_state)ioa
    21  "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
    22 
    23  sen         :: 'm impl_state => 'm sender_state
    24  "sen == fst"
    25 
    26  rec         :: 'm impl_state => 'm receiver_state
    27  "rec == fst o snd"
    28 
    29  srch        :: 'm impl_state => 'm packet list
    30  "srch == fst o snd o snd"
    31 
    32  rsch        :: 'm impl_state => bool list
    33  "rsch == snd o snd o snd"
    34 
    35 end