isabelle: src/HOLCF/IOA/NTP/Impl.thy@0b2ff9541727 (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	*)
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 *}
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Impl
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Sender Receiver Abschannel
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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	types
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	'm impl_state
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	= "'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	16	(* 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	17
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	consts
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	20	impl_ioa :: "('m action, 'm impl_state)ioa"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	sen :: "'m impl_state => 'm sender_state"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	rec :: "'m impl_state => 'm receiver_state"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	srch :: "'m impl_state => 'm packet multiset"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	rsch :: "'m impl_state => bool multiset"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	inv1 :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	inv2 :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	inv3 :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	28	inv4 :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	29	hdr_sum :: "'m packet multiset => bool => nat"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	defs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	impl_def:
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	"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	35
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	36	sen_def: "sen == fst"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	37	rec_def: "rec == fst o snd"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	38	srch_def: "srch == fst o snd o snd"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39	rsch_def: "rsch == snd o snd o snd"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	41	hdr_sum_def:
3852 e694c660055b fixed dots; wenzelm parents: 3073 diff changeset	42	"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	43
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	44	(* Lemma 5.1 *)
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	45	inv1_def:
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	46	"inv1(s) ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	47	(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	48	& (!b. count (ssent(sen s)) b
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	49	= 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	50
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	51	(* Lemma 5.2 *)
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	52	inv2_def: "inv2(s) ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	53	(rbit(rec(s)) = sbit(sen(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	54	ssending(sen(s)) &
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	55	count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	56	count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	57	\|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	58	(rbit(rec(s)) = (~sbit(sen(s))) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	59	rsending(rec(s)) &
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	60	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	61	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	62
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	63	(* Lemma 5.3 *)
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	64	inv3_def: "inv3(s) ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	65	rbit(rec(s)) = sbit(sen(s))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	66	--> (!m. sq(sen(s))=[] \| m ~= hd(sq(sen(s)))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	67	--> count (rrcvd(rec s)) (sbit(sen(s)),m)
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	68	+ count (srch s) (sbit(sen(s)),m)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	69	<= 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	70
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	71	(* Lemma 5.4 *)
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	72	inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	73
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	74	ML {* use_legacy_bindings (the_context ()) *}
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	75
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	76	end

author	wenzelm
	Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244	0b2ff9541727
parent 14981	e73f8140af78
child 19739	c58ef2aa5430
permissions	-rw-r--r--