Can I change the notation in a built-in Isabelle type-class

Question

I have made a type of mine an instance of monoid_add:

instantiation "marking_ext" :: (monoid_add) monoid_add  
begin
  definition
    marking_add_def:
    "M + N = 
    ...
end

I can now use the familiar + notation between values of type ('a :: monoid_add) marking_ext, e.g., write M + N. But I would rather use \<oplus>, writing M \<oplus> N.

Can I change the notation of the typeclass instance, yet stay within the built-in hierarchy of type-classes?

Answer 1

You can add additional notation for + on your type, e.g. by introducing an abbreviation:

abbreviation marking_add' :: "marking_ext ⇒ marking_ext ⇒ marking_ext" (infixl "⊕" 65)
  where "(⊕) ≡ (+)"

You can tweak the operator precedence as needed (65 is the one that the normal + has).

Note, however, that introducing additional notation can be problematic if it clashes with notation in other theories. If someone wants to use your development in the future together with some other libraries that also define a notation ⊕, there will be syntax clashes and those can make life a bit harder for that person. There's usually a way to get around it (especially for simple notation like this one), but still: I would usually suggest not to use unnecessary extra notation unless there is a real benefit. In this particular case, I don't really see what the benefit would be. But that's just my advice, feel free to ignore it, of course! :)