--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy Thu Feb 15 12:11:00 2018 +0100
@@ -31,41 +31,41 @@
t = snd(snd(tr))
in case fst(snd(tr))
of
- S_msg(m) => sq(t)=sq(s)@[m] &
- ssent(t)=ssent(s) &
- srcvd(t)=srcvd(s) &
- sbit(t)=sbit(s) &
+ S_msg(m) => sq(t)=sq(s)@[m] \<and>
+ ssent(t)=ssent(s) \<and>
+ srcvd(t)=srcvd(s) \<and>
+ sbit(t)=sbit(s) \<and>
ssending(t)=ssending(s) |
R_msg(m) => False |
- S_pkt(pkt) => hdr(pkt) = sbit(s) &
- (? Q. sq(s) = (msg(pkt)#Q)) &
- sq(t) = sq(s) &
- ssent(t) = addm (ssent s) (sbit s) &
- srcvd(t) = srcvd(s) &
- sbit(t) = sbit(s) &
- ssending(s) &
+ S_pkt(pkt) => hdr(pkt) = sbit(s) \<and>
+ (\<exists>Q. sq(s) = (msg(pkt)#Q)) \<and>
+ sq(t) = sq(s) \<and>
+ ssent(t) = addm (ssent s) (sbit s) \<and>
+ srcvd(t) = srcvd(s) \<and>
+ sbit(t) = sbit(s) \<and>
+ ssending(s) \<and>
ssending(t) |
R_pkt(pkt) => False |
S_ack(b) => False |
- R_ack(b) => sq(t)=sq(s) &
- ssent(t)=ssent(s) &
- srcvd(t) = addm (srcvd s) b &
- sbit(t)=sbit(s) &
+ R_ack(b) => sq(t)=sq(s) \<and>
+ ssent(t)=ssent(s) \<and>
+ srcvd(t) = addm (srcvd s) b \<and>
+ sbit(t)=sbit(s) \<and>
ssending(t)=ssending(s) |
- C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
- sq(t)=sq(s) &
- ssent(t)=ssent(s) &
- srcvd(t)=srcvd(s) &
- sbit(t)=sbit(s) &
- ssending(s) &
+ C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) \<and>
+ sq(t)=sq(s) \<and>
+ ssent(t)=ssent(s) \<and>
+ srcvd(t)=srcvd(s) \<and>
+ sbit(t)=sbit(s) \<and>
+ ssending(s) \<and>
~ssending(t) |
C_m_r => False |
- C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
- sq(t)=tl(sq(s)) &
- ssent(t)=ssent(s) &
- srcvd(t)=srcvd(s) &
- sbit(t) = (~sbit(s)) &
- ~ssending(s) &
+ C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) \<and>
+ sq(t)=tl(sq(s)) \<and>
+ ssent(t)=ssent(s) \<and>
+ srcvd(t)=srcvd(s) \<and>
+ sbit(t) = (~sbit(s)) \<and>
+ ~ssending(s) \<and>
ssending(t) |
C_r_r(m) => False}"
@@ -74,17 +74,17 @@
"sender_ioa =
(sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
-lemma in_sender_asig:
- "S_msg(m) : actions(sender_asig)"
- "R_msg(m) ~: actions(sender_asig)"
- "S_pkt(pkt) : actions(sender_asig)"
- "R_pkt(pkt) ~: actions(sender_asig)"
- "S_ack(b) ~: actions(sender_asig)"
- "R_ack(b) : actions(sender_asig)"
- "C_m_s : actions(sender_asig)"
- "C_m_r ~: actions(sender_asig)"
- "C_r_s : actions(sender_asig)"
- "C_r_r(m) ~: actions(sender_asig)"
+lemma in_sender_asig:
+ "S_msg(m) \<in> actions(sender_asig)"
+ "R_msg(m) \<notin> actions(sender_asig)"
+ "S_pkt(pkt) \<in> actions(sender_asig)"
+ "R_pkt(pkt) \<notin> actions(sender_asig)"
+ "S_ack(b) \<notin> actions(sender_asig)"
+ "R_ack(b) \<in> actions(sender_asig)"
+ "C_m_s \<in> actions(sender_asig)"
+ "C_m_r \<notin> actions(sender_asig)"
+ "C_r_s \<in> actions(sender_asig)"
+ "C_r_r(m) \<notin> actions(sender_asig)"
by (simp_all add: sender_asig_def actions_def asig_projections)
lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def