isabelle: src/HOLCF/IOA/NTP/Spec.thy@23eae933c2d9 (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	Copyright 1994 TU Muenchen
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	The specification of reliable transmission
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	Spec = List + IOA + Action +
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	consts
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	spec_sig :: 'm action signature
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	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	15	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	16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	defs
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	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	20	UN m.{R_msg(m)},
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	trans_def "spec_trans ==
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24	{tr. let s = fst(tr);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	t = snd(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	in
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	case fst(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	of
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	S_msg(m) => t = s@[m] \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	R_msg(m) => s = (m#t) \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	S_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	R_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	S_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	R_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	C_m_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	C_m_r => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	C_r_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	C_r_r(m) => False}"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	39
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	40	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	41
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42	end

author	mueller
	Thu, 17 Jul 1997 12:44:58 +0200
changeset 3523	23eae933c2d9
parent 3073	88366253a09a
child 6468	a7b1669f5365
permissions	-rw-r--r--