isabelle: src/HOLCF/IOA/NTP/Impl.thy@e73f8140af78 (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/Impl.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
12218 6597093b77e7 GPLed; wenzelm parents: 3852 diff changeset	5	The implementation.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	Impl = Sender + Receiver + Abschannel +
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	types
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	'm impl_state
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	(* sender_state * receiver_state * srch_state * rsch_state *)
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	consts
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	impl_ioa :: ('m action, 'm impl_state)ioa
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	sen :: 'm impl_state => 'm sender_state
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	rec :: 'm impl_state => 'm receiver_state
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21	srch :: 'm impl_state => 'm packet multiset
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	rsch :: 'm impl_state => bool multiset
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	inv1, inv2,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24	inv3, inv4 :: 'm impl_state => bool
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	hdr_sum :: 'm packet multiset => bool => nat
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	impl_def
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	"impl_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_ioa \|\| rsch_ioa)"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	sen_def "sen == fst"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	rec_def "rec == fst o snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	srch_def "srch == fst o snd o snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	rsch_def "rsch == snd o snd o snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	hdr_sum_def
3852 e694c660055b fixed dots; wenzelm parents: 3073 diff changeset	38	"hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	39
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40	(* Lemma 5.1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41	inv1_def
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42	"inv1(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	43	(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	44	& (!b. count (ssent(sen s)) b
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	45	= hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	46
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	47	(* Lemma 5.2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	48	inv2_def "inv2(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	49	(rbit(rec(s)) = sbit(sen(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	50	ssending(sen(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	51	count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	52	count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	53	\|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	54	(rbit(rec(s)) = (~sbit(sen(s))) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	55	rsending(rec(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	56	count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	57	count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	58
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	59	(* Lemma 5.3 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	60	inv3_def "inv3(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	61	rbit(rec(s)) = sbit(sen(s))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	62	--> (!m. sq(sen(s))=[] \| m ~= hd(sq(sen(s)))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	63	--> count (rrcvd(rec s)) (sbit(sen(s)),m)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	64	+ count (srch s) (sbit(sen(s)),m)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	65	<= count (rsent(rec s)) (~sbit(sen s)))"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	66
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	67	(* Lemma 5.4 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	68	inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	69
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	70	end

author	kleing
	Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981	e73f8140af78
parent 12218	6597093b77e7
child 17244	0b2ff9541727
permissions	-rw-r--r--