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

user_694001 0
Viewed 71

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?

isabelle typeclass
2 Answers

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! :)

user_21442270

The above answer gives me what I practically need, however, the /literal/ answer to the question turns out to be that you can change notation for a type class globally using notation:

notation plus (infixl "⊕" 65)

You probably won't want to do that for plus, because if you do, arithmetic takes on your new look:

term "(2 :: nat) + 3"

--> "2 ⊕ 3"
  :: "nat"
user_6940010
Related