Theory Adhoc_Overloading_Examples

(*  Title:      HOL/Examples/Adhoc_Overloading_Examples.thy
    Author:     Christian Sternagel

section ‹Ad Hoc Overloading›

theory Adhoc_Overloading_Examples

text ‹Adhoc overloading allows to overload a constant depending on
its type. Typically this involves to introduce an uninterpreted
constant (used for input and output) and then add some variants (used

subsection ‹Plain Ad Hoc Overloading›

text ‹Consider the type of first-order terms.›
datatype ('a, 'b) "term" =
  Var 'b |
  Fun 'a "('a, 'b) term list"

text ‹The set of variables of a term might be computed as follows.›
fun term_vars :: "('a, 'b) term  'b set" where
  "term_vars (Var x) = {x}" |
  "term_vars (Fun f ts) = (set (map term_vars ts))"

text ‹However, also for \emph{rules} (i.e., pairs of terms) and term
rewrite systems (i.e., sets of rules), the set of variables makes
sense. Thus we introduce an unspecified constant vars›.›

consts vars :: "'a  'b set"

text ‹Which is then overloaded with variants for terms, rules, and TRSs.›
  vars term_vars

value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"

fun rule_vars :: "('a, 'b) term × ('a, 'b) term  'b set" where
  "rule_vars (l, r) = vars l  vars r"

  vars rule_vars

value [nbe] "vars (Var 1, Var 0)"

definition trs_vars :: "(('a, 'b) term × ('a, 'b) term) set  'b set" where
  "trs_vars R = (rule_vars ` R)"

  vars trs_vars

value [nbe] "vars {(Var 1, Var 0)}"

text ‹Sometimes it is necessary to add explicit type constraints
before a variant can be determined.›
(*value "vars R" (*has multiple instances*)*)
value "vars (R :: (('a, 'b) term × ('a, 'b) term) set)"

text ‹It is also possible to remove variants.›
  vars term_vars rule_vars 

(*value "vars (Var 1)" (*does not have an instance*)*)

text ‹As stated earlier, the overloaded constant is only used for
input and output. Internally, always a variant is used, as can be
observed by the configuration option show_variants›.›

  vars term_vars

declare [[show_variants]]

term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)

subsection ‹Adhoc Overloading inside Locales›

text ‹As example we use permutations that are parametrized over an
atom type typ'a.›

definition perms :: "('a  'a) set" where
  "perms = {f. bij f  finite {x. f x  x}}"

typedef 'a perm = "perms :: ('a  'a) set"
  by standard (auto simp: perms_def)

text ‹First we need some auxiliary lemmas.›
lemma permsI [Pure.intro]:
  assumes "bij f" and "MOST x. f x = x"
  shows "f  perms"
  using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)

lemma perms_imp_bij:
  "f  perms  bij f"
  by (simp add: perms_def)

lemma perms_imp_MOST_eq:
  "f  perms  MOST x. f x = x"
  by (simp add: perms_def) (metis MOST_iff_finiteNeg)

lemma id_perms [simp]:
  "id  perms"
  "(λx. x)  perms"
  by (auto simp: perms_def bij_def)

lemma perms_comp [simp]:
  assumes f: "f  perms" and g: "g  perms"
  shows "(f  g)  perms"
  apply (intro permsI bij_comp)
  apply (rule perms_imp_bij [OF g])
  apply (rule perms_imp_bij [OF f])
  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
  by simp

lemma perms_inv:
  assumes f: "f  perms"
  shows "inv f  perms"
  apply (rule permsI)
  apply (rule bij_imp_bij_inv)
  apply (rule perms_imp_bij [OF f])
  apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
  apply (erule subst, rule inv_f_f)
  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])

lemma bij_Rep_perm: "bij (Rep_perm p)"
  using Rep_perm [of p] unfolding perms_def by simp

instantiation perm :: (type) group_add

definition "0 = Abs_perm id"
definition "- p = Abs_perm (inv (Rep_perm p))"
definition "p + q = Abs_perm (Rep_perm p  Rep_perm q)"
definition "(p1::'a perm) - p2 = p1 + - p2"

lemma Rep_perm_0: "Rep_perm 0 = id"
  unfolding zero_perm_def by (simp add: Abs_perm_inverse)

lemma Rep_perm_add:
  "Rep_perm (p1 + p2) = Rep_perm p1  Rep_perm p2"
  unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)

lemma Rep_perm_uminus:
  "Rep_perm (- p) = inv (Rep_perm p)"
  unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)

  apply standard
  unfolding Rep_perm_inject [symmetric]
  unfolding minus_perm_def
  unfolding Rep_perm_add
  unfolding Rep_perm_uminus
  unfolding Rep_perm_0
  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])


lemmas Rep_perm_simps =

section ‹Permutation Types›

text ‹We want to be able to apply permutations to arbitrary types. To
this end we introduce a constant PERMUTE› together with
convenient infix syntax.›

consts PERMUTE :: "'a perm  'b  'b" (infixr "" 75)

text ‹Then we add a locale for types typ'b that support
appliciation of permutations.›
locale permute =
  fixes permute :: "'a perm  'b  'b"
  assumes permute_zero [simp]: "permute 0 x = x"
    and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"

  PERMUTE permute


text ‹Permuting atoms.›
definition permute_atom :: "'a perm  'a  'a" where
  "permute_atom p a = (Rep_perm p) a"

  PERMUTE permute_atom

interpretation atom_permute: permute permute_atom
  by standard (simp_all add: permute_atom_def Rep_perm_simps)

text ‹Permuting permutations.›
definition permute_perm :: "'a perm  'a perm  'a perm" where
  "permute_perm p q = p + q - p"

  PERMUTE permute_perm

interpretation perm_permute: permute permute_perm
  apply standard
  unfolding permute_perm_def
  apply simp
  apply (simp only: diff_conv_add_uminus minus_add add.assoc)

text ‹Permuting functions.›
locale fun_permute =
  dom: permute perm1 + ran: permute perm2
  for perm1 :: "'a perm  'b  'b"
  and perm2 :: "'a perm  'c  'c"

  PERMUTE perm1 perm2

definition permute_fun :: "'a perm  ('b  'c)  ('b  'c)" where
  "permute_fun p f = (λx. p  (f (-p  x)))"

  PERMUTE permute_fun


sublocale fun_permute  permute permute_fun
  by (unfold_locales, auto simp: permute_fun_def)
     (metis dom.permute_plus minus_add)

lemma "(Abs_perm id :: nat perm)  Suc 0 = Suc 0"
  unfolding permute_atom_def
  by (metis Rep_perm_0 id_apply zero_perm_def)

interpretation atom_fun_permute: fun_permute permute_atom permute_atom
  by (unfold_locales)

  PERMUTE atom_fun_permute.permute_fun

lemma "(Abs_perm id :: 'a perm)  id = id"
  unfolding atom_fun_permute.permute_fun_def
  unfolding permute_atom_def
  by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)