--- a/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 18:23:50 2008 +0200
+++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 21:25:51 2008 +0200
@@ -15,31 +15,22 @@
= "'m list * bool multiset * 'm packet multiset * bool * bool"
(* messages #replies #received header mode *)
-consts
-
- 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"
- rsent :: "'m receiver_state => bool multiset"
- rrcvd :: "'m receiver_state => 'm packet multiset"
- rbit :: "'m receiver_state => bool"
- rsending :: "'m receiver_state => bool"
-
-defs
+definition rq :: "'m receiver_state => 'm list" where "rq == fst"
+definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd"
+definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd"
+definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd"
+definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd"
-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"
+definition
+ receiver_asig :: "'m action signature" where
+ "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_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 ==
+definition
+ receiver_trans:: "('m action, 'm receiver_state)transition set" where
+"receiver_trans =
{tr. let s = fst(tr);
t = snd(snd(tr))
in
@@ -83,9 +74,10 @@
~rsending(s) &
rsending(t)}"
-
-receiver_ioa_def: "receiver_ioa ==
- (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
+definition
+ receiver_ioa :: "('m action, 'm receiver_state)ioa" where
+ "receiver_ioa =
+ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
lemma in_receiver_asig:
"S_msg(m) ~: actions(receiver_asig)"