isabelle: src/HOLCF/IOA/NTP/Sender.thy@9116dc6842e1 (annotated)

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

author	paulson
	Thu, 21 Sep 2006 17:39:57 +0200
changeset 20662	9116dc6842e1
parent 19739	c58ef2aa5430
child 27361	24ec32bee347
permissions	-rw-r--r--