1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory GenericTag 8imports 9 HOL.HOL 10begin 11 12text \<open> 13 Generic annotation constant. 14 15 @{typ 'ns} is a namespace parameter and should be a different 16 type or constant for each distinct use of this constant. 17 18 @{typ 'tag} is an arbitrary annotation associated with the actual 19 value @{term x}. 20\<close> 21definition generic_tag :: "'ns \<Rightarrow> 'tag \<Rightarrow> 'a \<Rightarrow> 'a" 22 where remove_generic_tag[code del]: "generic_tag _ _ x \<equiv> x" 23 24text \<open>Often the tagged value is a proposition to be proved.\<close> 25lemma generic_tagP_I: 26 "P \<Longrightarrow> generic_tag ns tag P" 27 by (simp add: remove_generic_tag) 28 29lemma generic_tag_True: 30 "generic_tag ns tag True" 31 by (simp add: remove_generic_tag) 32 33text \<open>We often want to avoid rewriting under annotations.\<close> 34lemma generic_tag_cong: 35 "x = x' \<Longrightarrow> generic_tag ns tag x = generic_tag ns tag x'" 36 by simp 37 38end