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