isabelle: src/HOLCF/IOA/NTP/Impl.thy@3f475e54875c (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
12218 6597093b77e7 GPLed; wenzelm parents: 3852 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 3852 diff changeset	6	The implementation.
3073 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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9	Impl = Sender + Receiver + Abschannel +
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	types
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	'm impl_state
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	= "'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	15	(* 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	16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	consts
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	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	20	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	21	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	22	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	23	rsch :: 'm impl_state => bool multiset
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24	inv1, inv2,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	inv3, inv4 :: 'm impl_state => bool
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	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	27
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	defs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	impl_def
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	"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	32
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	sen_def "sen == fst"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	rec_def "rec == fst o snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	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	36	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	37
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	hdr_sum_def
3852 e694c660055b fixed dots; wenzelm parents: 3073 diff changeset	39	"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	40
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41	(* Lemma 5.1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42	inv1_def
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	43	"inv1(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	44	(!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	45	& (!b. count (ssent(sen s)) b
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	46	= 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	47
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	48	(* Lemma 5.2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	49	inv2_def "inv2(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	50	(rbit(rec(s)) = sbit(sen(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	51	ssending(sen(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	52	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	53	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	54	\|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	55	(rbit(rec(s)) = (~sbit(sen(s))) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	56	rsending(rec(s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	57	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	58	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	59
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	60	(* Lemma 5.3 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	61	inv3_def "inv3(s) ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	62	rbit(rec(s)) = sbit(sen(s))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	63	--> (!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	64	--> 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	65	+ 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	66	<= 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	67
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	68	(* Lemma 5.4 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	69	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	70
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	71	end

author	paulson
	Tue, 09 Jul 2002 10:44:41 +0200
changeset 13318	3f475e54875c
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--