--- a/IOA/example/Channels.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Channels.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Channels = IOA + Action + Multiset + "Lemmas" + Packet +
+(* 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
@@ -11,7 +19,7 @@
srch_ioa :: "('m action, 'm packet multiset)ioa"
rsch_ioa :: "('m action, bool multiset)ioa"
-rules
+defs
srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \
\ UN pkt. {R_pkt(pkt)}, \
@@ -21,37 +29,37 @@
\ 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 | \
+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_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 | \
+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_m_s => False | \
+\ C_m_r => False | \
+\ C_r_s => False | \
\ C_r_r(m) => False}"