src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61999 89291b5d0ede
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/ABP/Impl_finite.thy
     2     Author:     Olaf M├╝ller
     3 *)
     4 
     5 section {* The implementation *}
     6 
     7 theory Impl_finite
     8 imports Sender Receiver Abschannel_finite
     9 begin
    10 
    11 type_synonym
    12   'm impl_fin_state
    13     = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    14 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    15 
    16 definition
    17   impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
    18   "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
    19                   rsch_fin_ioa)"
    20 
    21 definition
    22   sen_fin :: "'m impl_fin_state => 'm sender_state" where
    23   "sen_fin = fst"
    24 
    25 definition
    26   rec_fin :: "'m impl_fin_state => 'm receiver_state" where
    27   "rec_fin = fst o snd"
    28 
    29 definition
    30   srch_fin :: "'m impl_fin_state => 'm packet list" where
    31   "srch_fin = fst o snd o snd"
    32 
    33 definition
    34   rsch_fin :: "'m impl_fin_state => bool list" where
    35   "rsch_fin = snd o snd o snd"
    36 
    37 end