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