1(*  Title:      HOL/HOLCF/IOA/NTP/Packet.thy
2    Author:     Tobias Nipkow & Konrad Slind
3*)
4
5theory Packet
6imports Multiset
7begin
8
9type_synonym
10  'msg packet = "bool * 'msg"
11
12definition
13  hdr :: "'msg packet \<Rightarrow> bool" where
14  "hdr \<equiv> fst"
15
16definition
17  msg :: "'msg packet \<Rightarrow> 'msg" where
18  "msg \<equiv> snd"
19
20
21text \<open>Instantiation of a tautology?\<close>
22lemma eq_packet_imp_eq_hdr: "\<forall>x. x = packet \<longrightarrow> hdr(x) = hdr(packet)"
23  by simp
24
25declare hdr_def [simp] msg_def [simp]
26
27end
28