src/HOL/IOA/ABP/Abschannel.thy

updated version

(*  Title:      HOL/IOA/ABP/Abschannels.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1995  TU Muenchen

The transmission channel 
*)

Abschannel = IOA + Action + Lemmas + List +
 
datatype ('a)act =   S('a) | R('a)

consts
 
ch_asig  :: "'a act signature"

ch_trans :: "('a act, 'a list)transition set"

ch_ioa   :: "('a act, 'a list)ioa"

rsch_actions  :: "'m action => bool act option"
srch_actions  :: "'m action =>(bool * 'm) act option"

srch_asig, 
rsch_asig  :: "'m action signature"

srch_trans :: "('m action, 'm packet list)transition set"
rsch_trans :: "('m action, bool list)transition set"

srch_ioa   :: "('m action, 'm packet list)ioa"
rsch_ioa   :: "('m action, bool list)ioa"   


defs

srch_asig_def "srch_asig == asig_of(srch_ioa)"
rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"

srch_trans_def "srch_trans == trans_of(srch_ioa)"  
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"

srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"


ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"

ch_trans_def "ch_trans ==                                       \
\ {tr. let s = fst(tr);                                         \
\          t = snd(snd(tr))                                     \
\      in                                                       \
\      case fst(snd(tr))                                        \
\        of S(b) => ((t = s) | (t = s @ [b]))  |                \
\           R(b) => s ~= [] &                                   \
\	            b = hd(s) &                                 \
\	            ((t = s) | (t = tl(s)))    }"
  
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"

rsch_actions_def "rsch_actions (akt) ==                      \
\	    case akt of   \
\           Next    =>  None |          \
\           S_msg(m) => None |         \
\	    R_msg(m) => None |         \
\           S_pkt(packet) => None |    \
\	    R_pkt(packet) => None |    \
\	    S_ack(b) => Some(S(b)) |   \
\	    R_ack(b) => Some(R(b))"

srch_actions_def "srch_actions (akt) ==                      \
\	    case akt of   \
\	    Next    =>  None |          \
\           S_msg(m) => None |         \
\	    R_msg(m) => None |         \
\           S_pkt(p) => Some(S(p)) |   \
\	    R_pkt(p) => Some(R(p)) |   \
\	    S_ack(b) => None |         \
\	    R_ack(b) => None"


end