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

section ‹Ad Hoc Overloading›

theory Adhoc_Overloading
imports
  Main
  "HOL-Library.Infinite_Set"
begin

text ‹Adhoc overloading allows to overload a constant depending on
  type. Typically this involves to introduce an uninterpreted
  (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
  systems (i.e., sets of rules), the set of variables makes
 . Thus we introduce an unspecified constant ‹vars›.›

consts vars :: "'a → 'b set"

text ‹Which is then overloaded with variants for terms, rules, and TRSs.›
adhoc_overloading
  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"

adhoc_overloading
  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)"

adhoc_overloading
  vars ⇌ trs_vars

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

text ‹Sometimes it is necessary to add explicit type constraints
  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.›
no_adhoc_overloading
  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
  and output. Internally, always a variant is used, as can be
  by the configuration option ‹show_variants›.›

adhoc_overloading
  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
  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]])
  done

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

instantiation perm :: (type) group_add
begin

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)

instance
  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]])
  done

end

lemmas Rep_perm_simps =
  Rep_perm_0
  Rep_perm_add
  Rep_perm_uminus


section ‹Permutation Types›

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

consts PERMUTE :: "'a perm → 'b → 'b" (infixr ‹∙› 75)

text ‹Then we add a locale for types typ‹'b› that support
  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)"
begin

adhoc_overloading
  PERMUTE ⇌ permute

end

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

adhoc_overloading
  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"

adhoc_overloading
  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)
  done

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

adhoc_overloading
  PERMUTE ⇌ perm1 perm2

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

adhoc_overloading
  PERMUTE ⇌ permute_fun

end

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)

adhoc_overloading
  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)

end