IOA/example/Channels.thy

Added headers and made various small mods.

(*  Title:      HOL/IOA/example/Channels.thy
    ID:         $Id$
    Author:     Tobias Nipkow & Konrad Slind
    Copyright   1994  TU Muenchen

The (faulty) transmission channels (both directions)
*)

Channels = IOA + Action + Multiset +

consts

srch_asig, 
rsch_asig  :: "'m action signature"

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

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

defs

srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    \
\                            UN pkt. {R_pkt(pkt)},    \
\                            {}>"

rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \
\                            UN b. {R_ack(b)}, \
\                            {}>"

srch_trans_def "srch_trans ==                                       \
\ {tr. let s = fst(tr);                                             \
\          t = snd(snd(tr))                                         \
\      in                                                           \
\      case fst(snd(tr))                                            \
\        of S_msg(m) => False |                                     \
\           R_msg(m) => False |                                     \
\           S_pkt(pkt) => t = addm(s, pkt) |                        \
\           R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) |   \
\           S_ack(b) => False |                                     \
\           R_ack(b) => False |                                     \
\           C_m_s => False |                                        \
\           C_m_r => False |                                        \
\           C_r_s => False |                                        \
\           C_r_r(m) => False}"

rsch_trans_def "rsch_trans ==                         \
\ {tr. let s = fst(tr);                               \
\          t = snd(snd(tr))                           \
\      in                                             \
\      case fst(snd(tr))                              \
\      of                                             \
\      S_msg(m) => False |                            \
\      R_msg(m) => False |                            \
\      S_pkt(pkt) => False |                          \
\      R_pkt(pkt) => False |                          \
\      S_ack(b) => t = addm(s,b) |                    \
\      R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) |  \
\      C_m_s => False |                               \
\      C_m_r => False |                               \
\      C_r_s => False |                               \
\      C_r_r(m) => False}"


srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>"

end