IOA/example/Receiver.thy

-Receiver = List + IOA + Action + Multiset + "Lemmas" +
+(*  Title:      HOL/IOA/example/Receiver.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The implementation: receiver
+*)
+
+Receiver = List + IOA + Action + Multiset +
 
 types 
 
 'm receiver_state
 = "'m list * bool multiset * 'm packet multiset * bool * bool"

   rsent         :: "'m receiver_state => bool multiset"
   rrcvd         :: "'m receiver_state => 'm packet multiset"
   rbit          :: "'m receiver_state => bool"
   rsending      :: "'m receiver_state => bool"
 
-rules
+defs
 
 rq_def       "rq == fst"
 rsent_def    "rsent == fst o snd"
 rrcvd_def    "rrcvd == fst o snd o snd"
 rbit_def     "rbit == fst o snd o snd o snd"
 rsending_def "rsending == snd o snd o snd o snd"
 
-receiver_asig_def "receiver_asig ==                                      \
-\ <UN pkt. {R_pkt(pkt)},                                              \
-\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),                          \
+receiver_asig_def "receiver_asig ==            \
+\ <UN pkt. {R_pkt(pkt)},                       \
+\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
 \  insert(C_m_r, UN m. {C_r_r(m)})>"
 
 receiver_trans_def "receiver_trans ==                                    \
 \ {tr. let s = fst(tr);                                                  \
 \          t = snd(snd(tr))                                              \

 \                     rsent(t) = addm(rsent(s),rbit(s))  &               \
 \                     rrcvd(t) = rrcvd(s)                &               \
 \                     rbit(t)=rbit(s)                    &               \
 \                     rsending(s)                        &               \
 \                     rsending(t) |                                      \
-\R_ack(b) => False |                                                  \
+\      R_ack(b) => False |                                                  \
 \      C_m_s => False |                                                  \
 \ C_m_r => count(rsent(s),~rbit(s)) < countm(rrcvd(s),%y.hdr(y)=rbit(s)) & \
 \             rq(t) = rq(s)                        &                     \
 \             rsent(t)=rsent(s)                    &                     \
 \             rrcvd(t)=rrcvd(s)                    &                     \