isabelle: src/HOLCF/IOA/NTP/Spec.thy@efd626efcb04 (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	*)
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 specification of reliable transmission *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Spec
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports IOA Action
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	consts
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
6468 a7b1669f5365 put types into "" because of signature clash; mueller parents: 3523 diff changeset	14	spec_sig :: "'m action signature"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	spec_trans :: "('m action, 'm list)transition set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	spec_ioa :: "('m action, 'm list)ioa"
3073 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	defs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	20	sig_def: "spec_sig == (UN m.{S_msg(m)},
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21	UN m.{R_msg(m)},
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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	trans_def: "spec_trans ==
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	{tr. let s = fst(tr);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	t = snd(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	in
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	case fst(snd(tr))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	of
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	S_msg(m) => t = s@[m] \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	R_msg(m) => s = (m#t) \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	S_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	R_pkt(pkt) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	S_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	R_ack(b) => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	C_m_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	C_m_r => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	C_r_s => False \|
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	39	C_r_r(m) => False}"
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	ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	42
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	43	end

author	wenzelm
	Mon, 23 Jun 2008 16:01:03 +0200
changeset 27327	efd626efcb04
parent 19739	c58ef2aa5430
child 27361	24ec32bee347
permissions	-rw-r--r--