1(* Title: HOL/ex/Adhoc_Overloading_Examples.thy 2 Author: Christian Sternagel 3*) 4 5section \<open>Ad Hoc Overloading\<close> 6 7theory Adhoc_Overloading_Examples 8imports 9 Main 10 "HOL-Library.Infinite_Set" 11 "HOL-Library.Adhoc_Overloading" 12begin 13 14text \<open>Adhoc overloading allows to overload a constant depending on 15its type. Typically this involves to introduce an uninterpreted 16constant (used for input and output) and then add some variants (used 17internally).\<close> 18 19subsection \<open>Plain Ad Hoc Overloading\<close> 20 21text \<open>Consider the type of first-order terms.\<close> 22datatype ('a, 'b) "term" = 23 Var 'b | 24 Fun 'a "('a, 'b) term list" 25 26text \<open>The set of variables of a term might be computed as follows.\<close> 27fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where 28 "term_vars (Var x) = {x}" | 29 "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))" 30 31text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term 32rewrite systems (i.e., sets of rules), the set of variables makes 33sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close> 34 35consts vars :: "'a \<Rightarrow> 'b set" 36 37text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close> 38adhoc_overloading 39 vars term_vars 40 41value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" 42 43fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where 44 "rule_vars (l, r) = vars l \<union> vars r" 45 46adhoc_overloading 47 vars rule_vars 48 49value [nbe] "vars (Var 1, Var 0)" 50 51definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where 52 "trs_vars R = \<Union>(rule_vars ` R)" 53 54adhoc_overloading 55 vars trs_vars 56 57value [nbe] "vars {(Var 1, Var 0)}" 58 59text \<open>Sometimes it is necessary to add explicit type constraints 60before a variant can be determined.\<close> 61(*value "vars R" (*has multiple instances*)*) 62value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)" 63 64text \<open>It is also possible to remove variants.\<close> 65no_adhoc_overloading 66 vars term_vars rule_vars 67 68(*value "vars (Var 1)" (*does not have an instance*)*) 69 70text \<open>As stated earlier, the overloaded constant is only used for 71input and output. Internally, always a variant is used, as can be 72observed by the configuration option \<open>show_variants\<close>.\<close> 73 74adhoc_overloading 75 vars term_vars 76 77declare [[show_variants]] 78 79term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) 80 81 82subsection \<open>Adhoc Overloading inside Locales\<close> 83 84text \<open>As example we use permutations that are parametrized over an 85atom type \<^typ>\<open>'a\<close>.\<close> 86 87definition perms :: "('a \<Rightarrow> 'a) set" where 88 "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}" 89 90typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set" 91 by standard (auto simp: perms_def) 92 93text \<open>First we need some auxiliary lemmas.\<close> 94lemma permsI [Pure.intro]: 95 assumes "bij f" and "MOST x. f x = x" 96 shows "f \<in> perms" 97 using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) 98 99lemma perms_imp_bij: 100 "f \<in> perms \<Longrightarrow> bij f" 101 by (simp add: perms_def) 102 103lemma perms_imp_MOST_eq: 104 "f \<in> perms \<Longrightarrow> MOST x. f x = x" 105 by (simp add: perms_def) (metis MOST_iff_finiteNeg) 106 107lemma id_perms [simp]: 108 "id \<in> perms" 109 "(\<lambda>x. x) \<in> perms" 110 by (auto simp: perms_def bij_def) 111 112lemma perms_comp [simp]: 113 assumes f: "f \<in> perms" and g: "g \<in> perms" 114 shows "(f \<circ> g) \<in> perms" 115 apply (intro permsI bij_comp) 116 apply (rule perms_imp_bij [OF g]) 117 apply (rule perms_imp_bij [OF f]) 118 apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]]) 119 apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]]) 120 by simp 121 122lemma perms_inv: 123 assumes f: "f \<in> perms" 124 shows "inv f \<in> perms" 125 apply (rule permsI) 126 apply (rule bij_imp_bij_inv) 127 apply (rule perms_imp_bij [OF f]) 128 apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]]) 129 apply (erule subst, rule inv_f_f) 130 apply (rule bij_is_inj [OF perms_imp_bij [OF f]]) 131 done 132 133lemma bij_Rep_perm: "bij (Rep_perm p)" 134 using Rep_perm [of p] unfolding perms_def by simp 135 136instantiation perm :: (type) group_add 137begin 138 139definition "0 = Abs_perm id" 140definition "- p = Abs_perm (inv (Rep_perm p))" 141definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)" 142definition "(p1::'a perm) - p2 = p1 + - p2" 143 144lemma Rep_perm_0: "Rep_perm 0 = id" 145 unfolding zero_perm_def by (simp add: Abs_perm_inverse) 146 147lemma Rep_perm_add: 148 "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2" 149 unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm) 150 151lemma Rep_perm_uminus: 152 "Rep_perm (- p) = inv (Rep_perm p)" 153 unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm) 154 155instance 156 apply standard 157 unfolding Rep_perm_inject [symmetric] 158 unfolding minus_perm_def 159 unfolding Rep_perm_add 160 unfolding Rep_perm_uminus 161 unfolding Rep_perm_0 162 apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) 163 done 164 165end 166 167lemmas Rep_perm_simps = 168 Rep_perm_0 169 Rep_perm_add 170 Rep_perm_uminus 171 172 173section \<open>Permutation Types\<close> 174 175text \<open>We want to be able to apply permutations to arbitrary types. To 176this end we introduce a constant \<open>PERMUTE\<close> together with 177convenient infix syntax.\<close> 178 179consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75) 180 181text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support 182appliciation of permutations.\<close> 183locale permute = 184 fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" 185 assumes permute_zero [simp]: "permute 0 x = x" 186 and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)" 187begin 188 189adhoc_overloading 190 PERMUTE permute 191 192end 193 194text \<open>Permuting atoms.\<close> 195definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where 196 "permute_atom p a = (Rep_perm p) a" 197 198adhoc_overloading 199 PERMUTE permute_atom 200 201interpretation atom_permute: permute permute_atom 202 by standard (simp_all add: permute_atom_def Rep_perm_simps) 203 204text \<open>Permuting permutations.\<close> 205definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where 206 "permute_perm p q = p + q - p" 207 208adhoc_overloading 209 PERMUTE permute_perm 210 211interpretation perm_permute: permute permute_perm 212 apply standard 213 unfolding permute_perm_def 214 apply simp 215 apply (simp only: diff_conv_add_uminus minus_add add.assoc) 216 done 217 218text \<open>Permuting functions.\<close> 219locale fun_permute = 220 dom: permute perm1 + ran: permute perm2 221 for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" 222 and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c" 223begin 224 225adhoc_overloading 226 PERMUTE perm1 perm2 227 228definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where 229 "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))" 230 231adhoc_overloading 232 PERMUTE permute_fun 233 234end 235 236sublocale fun_permute \<subseteq> permute permute_fun 237 by (unfold_locales, auto simp: permute_fun_def) 238 (metis dom.permute_plus minus_add) 239 240lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0" 241 unfolding permute_atom_def 242 by (metis Rep_perm_0 id_apply zero_perm_def) 243 244interpretation atom_fun_permute: fun_permute permute_atom permute_atom 245 by (unfold_locales) 246 247adhoc_overloading 248 PERMUTE atom_fun_permute.permute_fun 249 250lemma "(Abs_perm id :: 'a perm) \<bullet> id = id" 251 unfolding atom_fun_permute.permute_fun_def 252 unfolding permute_atom_def 253 by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def) 254 255end 256 257