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