isabelle: src/HOL/HOLCF/IOA/NTP/Spec.thy@99a720d3ed8f (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Spec.thy
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 61032 diff changeset	5	section \<open>The specification of reliable transmission\<close>
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Spec
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 62009 diff changeset	8	imports IOA.IOA Action
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	11	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	12	spec_sig :: "'m action signature" where
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	13	sig_def: "spec_sig = (\<Union>m.{S_msg(m)},
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	14	\<Union>m.{R_msg(m)},
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	15	{})"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	17	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	18	spec_trans :: "('m action, 'm list)transition set" where
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	19	trans_def: "spec_trans =
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	20	{tr. let s = fst(tr);
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	21	t = snd(snd(tr))
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	22	in
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	23	case fst(snd(tr))
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	24	of
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	25	S_msg(m) \<Rightarrow> t = s@[m] \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	26	R_msg(m) \<Rightarrow> s = (m#t) \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	27	S_pkt(pkt) \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	28	R_pkt(pkt) \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	29	S_ack(b) \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	30	R_ack(b) \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	31	C_m_s \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	32	C_m_r \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	33	C_r_s \<Rightarrow> False \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	34	C_r_r(m) \<Rightarrow> False}"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35
27361 24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	36	definition
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	37	spec_ioa :: "('m action, 'm list)ioa" where
24ec32bee347 modernized specifications; wenzelm parents: 19739 diff changeset	38	ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40	end

author	haftmann
	Thu, 24 Jul 2025 17:46:29 +0200
changeset 82902	99a720d3ed8f
parent 67613	ce654b0e6d69
permissions	-rw-r--r--