author | wenzelm |
Fri, 26 Apr 2024 13:25:44 +0200 | |
changeset 80150 | 96f60533ec1d |
parent 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
(* Title: HOL/HOLCF/IOA/NTP/Packet.thy Author: Tobias Nipkow & Konrad Slind *) theory Packet imports Multiset begin type_synonym 'msg packet = "bool * 'msg" definition hdr :: "'msg packet \<Rightarrow> bool" where "hdr \<equiv> fst" definition msg :: "'msg packet \<Rightarrow> 'msg" where "msg \<equiv> snd" text \<open>Instantiation of a tautology?\<close> lemma eq_packet_imp_eq_hdr: "\<forall>x. x = packet \<longrightarrow> hdr(x) = hdr(packet)" by simp declare hdr_def [simp] msg_def [simp] end