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