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

imports
Main
"HOL-Library.Infinite_Set"
begin

its type. Typically this involves to introduce an uninterpreted
constant (used for input and output) and then add some variants (used
internally).›

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

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"

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

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)

"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_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_uminus

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

PERMUTE permute

end

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

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

end

sublocale fun_permute ⊆ permute permute_fun
by (unfold_locales, auto simp: permute_fun_def)

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)

`