# Theory Impl_finite

Up to index of Isabelle/HOLCF/IOA/ABP

theory Impl_finite
imports Sender Receiver Abschannel_finite
begin

    (*  Title:      HOLCF/IOA/ABP/Impl.thy
        ID:         $Id: Impl_finite.thy,v 1.4 2005/09/03 14:50:22 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* The implementation *}

    theory Impl_finite
    imports Sender Receiver Abschannel_finite
    begin

    types
      'm impl_fin_state
        = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)

    constdefs

     impl_fin_ioa    :: "('m action, 'm impl_fin_state)ioa"
     "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
                       rsch_fin_ioa)"

     sen_fin         :: "'m impl_fin_state => 'm sender_state"
     "sen_fin == fst"

     rec_fin         :: "'m impl_fin_state => 'm receiver_state"
     "rec_fin == fst o snd"

     srch_fin        :: "'m impl_fin_state => 'm packet list"
     "srch_fin == fst o snd o snd"

     rsch_fin        :: "'m impl_fin_state => bool list"
     "rsch_fin == snd o snd o snd"

    ML {* use_legacy_bindings (the_context ()) *}

    end