--- a/src/HOLCF/IOA/ABP/Receiver.thy Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/ABP/Receiver.thy Sat Sep 03 16:50:22 2005 +0200
@@ -1,58 +1,56 @@
(* Title: HOLCF/IOA/ABP/Receiver.thy
ID: $Id$
Author: Olaf Müller
-
-The implementation: receiver.
*)
-Receiver = List + IOA + Action + Lemmas +
-
-types
+header {* The implementation: receiver *}
-'m receiver_state
-= "'m list * bool"
-(* messages mode *)
+theory Receiver
+imports IOA Action Lemmas
+begin
-consts
+types
+ 'm receiver_state = "'m list * bool" -- {* messages, mode *}
- receiver_asig :: "'m action signature"
- receiver_trans:: ('m action, 'm receiver_state)transition set
- receiver_ioa :: ('m action, 'm receiver_state)ioa
- rq :: 'm receiver_state => 'm list
- rbit :: 'm receiver_state => bool
+constdefs
+ rq :: "'m receiver_state => 'm list"
+ "rq == fst"
-defs
+ rbit :: "'m receiver_state => bool"
+ "rbit == snd"
-rq_def "rq == fst"
-rbit_def "rbit == snd"
-
-receiver_asig_def "receiver_asig ==
- (UN pkt. {R_pkt(pkt)},
- (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+receiver_asig :: "'m action signature"
+"receiver_asig ==
+ (UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
{})"
-receiver_trans_def "receiver_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- Next => False |
- S_msg(m) => False |
- R_msg(m) => (rq(s) ~= []) &
- m = hd(rq(s)) &
- rq(t) = tl(rq(s)) &
- rbit(t)=rbit(s) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
- rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
- rq(t) =rq(s) & rbit(t)=rbit(s) |
- S_ack(b) => b = rbit(s) &
- rq(t) = rq(s) &
- rbit(t)=rbit(s) |
+receiver_trans :: "('m action, 'm receiver_state)transition set"
+"receiver_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ Next => False |
+ S_msg(m) => False |
+ R_msg(m) => (rq(s) ~= []) &
+ m = hd(rq(s)) &
+ rq(t) = tl(rq(s)) &
+ rbit(t)=rbit(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
+ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
+ rq(t) =rq(s) & rbit(t)=rbit(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rbit(t)=rbit(s) |
R_ack(b) => False}"
-receiver_ioa_def "receiver_ioa ==
+receiver_ioa :: "('m action, 'm receiver_state)ioa"
+"receiver_ioa ==
(receiver_asig, {([],False)}, receiver_trans,{},{})"
+ML {* use_legacy_bindings (the_context ()) *}
+
end