isabelle: src/HOLCF/IOA/NTP/Spec.thy@9da1cf997e79 (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/Spec.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: 6468 diff changeset	5	The specification of reliable transmission.
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	Spec = List + IOA + Action +
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	consts
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
6468 a7b1669f5365 put types into "" because of signature clash; mueller parents: 3523 diff changeset	12	spec_sig :: "'m action signature"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	spec_trans :: ('m action, 'm list)transition set
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	spec_ioa :: ('m action, 'm list)ioa
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	defs
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	sig_def "spec_sig == (UN m.{S_msg(m)},
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	UN m.{R_msg(m)},
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	{})"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	trans_def "spec_trans ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	{tr. let s = fst(tr);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24	t = snd(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	in
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	case fst(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	of
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	S_msg(m) => t = s@[m] \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	R_msg(m) => s = (m#t) \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	S_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	R_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	S_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	R_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	C_m_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	C_m_r => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	C_r_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	C_r_r(m) => False}"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	39	ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"
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	end

author	wenzelm
	Sat, 11 Jun 2005 23:24:33 +0200
changeset 16377	9da1cf997e79
parent 14981	e73f8140af78
child 17244	0b2ff9541727
permissions	-rw-r--r--