--- a/src/HOLCF/IOA/ABP/Sender.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Sender.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,41 +12,45 @@
types
'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *}
-constdefs
-sq :: "'m sender_state => 'm list"
-"sq == fst"
+definition
+ sq :: "'m sender_state => 'm list" where
+ "sq = fst"
-sbit :: "'m sender_state => bool"
-"sbit == snd"
+definition
+ sbit :: "'m sender_state => bool" where
+ "sbit = snd"
-sender_asig :: "'m action signature"
-"sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
- UN pkt. {S_pkt(pkt)},
- {})"
+definition
+ sender_asig :: "'m action signature" where
+ "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+ UN pkt. {S_pkt(pkt)},
+ {})"
-sender_trans :: "('m action, 'm sender_state)transition set"
-"sender_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- Next => if sq(s)=[] then t=s else False |
- S_msg(m) => sq(t)=sq(s)@[m] &
- sbit(t)=sbit(s) |
- R_msg(m) => False |
- S_pkt(pkt) => sq(s) ~= [] &
- hdr(pkt) = sbit(s) &
- msg(pkt) = hd(sq(s)) &
- sq(t) = sq(s) &
- sbit(t) = sbit(s) |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => if b = sbit(s) then
- sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
- sq(t)=sq(s) & sbit(t)=sbit(s)}"
-
-sender_ioa :: "('m action, 'm sender_state)ioa"
-"sender_ioa ==
- (sender_asig, {([],True)}, sender_trans,{},{})"
+definition
+ sender_trans :: "('m action, 'm sender_state)transition set" where
+ "sender_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => if sq(s)=[] then t=s else False |
+ S_msg(m) => sq(t)=sq(s)@[m] &
+ sbit(t)=sbit(s) |
+ R_msg(m) => False |
+ S_pkt(pkt) => sq(s) ~= [] &
+ hdr(pkt) = sbit(s) &
+ msg(pkt) = hd(sq(s)) &
+ sq(t) = sq(s) &
+ sbit(t) = sbit(s) |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => if b = sbit(s) then
+ sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
+ sq(t)=sq(s) & sbit(t)=sbit(s)}"
+
+definition
+ sender_ioa :: "('m action, 'm sender_state)ioa" where
+ "sender_ioa =
+ (sender_asig, {([],True)}, sender_trans,{},{})"
end