--- a/IOA/example/Channels.thy Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* 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