isabelle: src/HOL/HOLCF/IOA/NTP/Packet.thy@b5f3d1051b13 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Packet.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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	theory Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	imports Multiset
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8
41476 0fa9629aa399 types -> type_synonym huffman parents: 40774 diff changeset	9	type_synonym
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	'msg packet = "bool * 'msg"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	12	definition
67613 ce654b0e6d69 more symbols; wenzelm parents: 62002 diff changeset	13	hdr :: "'msg packet \<Rightarrow> bool" where
ce654b0e6d69 more symbols; wenzelm parents: 62002 diff changeset	14	"hdr \<equiv> fst"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	16	definition
67613 ce654b0e6d69 more symbols; wenzelm parents: 62002 diff changeset	17	msg :: "'msg packet \<Rightarrow> 'msg" where
ce654b0e6d69 more symbols; wenzelm parents: 62002 diff changeset	18	"msg \<equiv> snd"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	20
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 42151 diff changeset	21	text \<open>Instantiation of a tautology?\<close>
67613 ce654b0e6d69 more symbols; wenzelm parents: 62002 diff changeset	22	lemma eq_packet_imp_eq_hdr: "\<forall>x. x = packet \<longrightarrow> hdr(x) = hdr(packet)"
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	23	by simp
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	24
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	25	declare hdr_def [simp] msg_def [simp]
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	end

author	wenzelm
	Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659	b5f3d1051b13
parent 67613	ce654b0e6d69
permissions	-rw-r--r--