isabelle: src/HOL/HOLCF/IOA/NTP/Sender.thy@528bad46f29e (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Sender.thy
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* The implementation: sender *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Sender
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports IOA Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
41476 0fa9629aa399 types -> type_synonym huffman parents: 40774 diff changeset	11	type_synonym
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	(* messages #sent #received header mode *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	15	definition sq :: "'m sender_state => 'm list" where "sq = fst"
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	16	definition ssent :: "'m sender_state => bool multiset" where "ssent = fst o snd"
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	17	definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst o snd o snd"
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	18	definition sbit :: "'m sender_state => bool" where "sbit = fst o snd o snd o snd"
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	19	definition ssending :: "'m sender_state => bool" where "ssending = snd o snd o snd o snd"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	21	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	22	sender_asig :: "'m action signature" where
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	23	"sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	24	UN pkt. {S_pkt(pkt)},
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	25	{C_m_s,C_r_s})"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	27	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	28	sender_trans :: "('m action, 'm sender_state)transition set" where
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	29	"sender_trans =
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	30	{tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	31	t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	of
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34	S_msg(m) => sq(t)=sq(s)@[m] &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	ssent(t)=ssent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	36	srcvd(t)=srcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	37	sbit(t)=sbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	38	ssending(t)=ssending(s) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39	R_msg(m) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	40	S_pkt(pkt) => hdr(pkt) = sbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	41	(? Q. sq(s) = (msg(pkt)#Q)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	42	sq(t) = sq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	43	ssent(t) = addm (ssent s) (sbit s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	44	srcvd(t) = srcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	45	sbit(t) = sbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	46	ssending(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	47	ssending(t) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	48	R_pkt(pkt) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	49	S_ack(b) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	50	R_ack(b) => sq(t)=sq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	51	ssent(t)=ssent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	52	srcvd(t) = addm (srcvd s) b &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	53	sbit(t)=sbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	54	ssending(t)=ssending(s) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	55	C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	56	sq(t)=sq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	57	ssent(t)=ssent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	58	srcvd(t)=srcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	59	sbit(t)=sbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	60	ssending(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	61	~ssending(t) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	62	C_m_r => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	63	C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	64	sq(t)=tl(sq(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	65	ssent(t)=ssent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	66	srcvd(t)=srcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	67	sbit(t) = (~sbit(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	68	~ssending(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	69	ssending(t) \|
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	70	C_r_r(m) => False}"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	71
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	72	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	73	sender_ioa :: "('m action, 'm sender_state)ioa" where
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	74	"sender_ioa =
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	75	(sender_asig, {([],{\|},{\|},False,True)}, sender_trans,{},{})"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	76
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	77	lemma in_sender_asig:
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	78	"S_msg(m) : actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	79	"R_msg(m) ~: actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	80	"S_pkt(pkt) : actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	81	"R_pkt(pkt) ~: actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	82	"S_ack(b) ~: actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	83	"R_ack(b) : actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	84	"C_m_s : actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	85	"C_m_r ~: actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	86	"C_r_s : actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	87	"C_r_r(m) ~: actions(sender_asig)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	88	by (simp_all add: sender_asig_def actions_def asig_projections)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	89
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	90	lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	91
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	92	end

author	huffman
	Thu, 17 Nov 2011 05:27:45 +0100
changeset 45531	528bad46f29e
parent 42151	4da4fc77664b
child 58880	0baae4311a9f
permissions	-rw-r--r--