src/HOL/IOA/ABP/Impl_finite.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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_finite = Sender + Receiver +  Abschannel_finite +
    10   
    11 types 
    12 
    13 'm impl_fin_state 
    14 = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    15 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    16 
    17 constdefs
    18 
    19  impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
    20  "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
    21                    rsch_fin_ioa)"
    22 
    23  sen_fin         :: 'm impl_fin_state => 'm sender_state
    24  "sen_fin == fst"
    25 
    26  rec_fin         :: 'm impl_fin_state => 'm receiver_state
    27  "rec_fin == fst o snd"
    28 
    29  srch_fin        :: 'm impl_fin_state => 'm packet list
    30  "srch_fin == fst o snd o snd"
    31 
    32  rsch_fin        :: 'm impl_fin_state => bool list
    33  "rsch_fin == snd o snd o snd"
    34 
    35 end
    36