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