Bob Rubbens (May 06 2023 at 10:17): Bob Rubbens (May 06 2023 at 10:17):Hi all, I noticed it is possible to reuse isabelle's unary minus syntax by instantiating the uminus typeclass for my type. Is something similar possible for the set contains (∈) syntax? It seems that in Set.thy the syntax is not separated out into a separate typeclass, so I'm suspecting it's not possible
Manuel Eberl (May 06 2023 at 18:38):It's not possible in a way that I would recommend.
If you really want to do it there is one option: you can remove the existing notation for ∈ and introduce a new one using a mechanism like adhoc_overloading. There are two reasons why this is a bad idea:
adhoc_overloading does not always work that well; in particular, it often leads to very incomprehensible error messages when there is a type error (and type checking can fail due to syntactic ambiguities)Note that the type class approach that you mentioned does not work here, since the type of a ‘contains’ operation is typically something like 'a ⇒ 'a my_type ⇒ bool and type classes cannot handle something like this. The raw overloading mechanism that is underneath type classes can handle this in principle, but then you would have to specify the operation as 'a ⇒ 'b ⇒ bool and that would lead to you having to annotate a lot of types in practice.
Manuel Eberl (May 06 2023 at 18:38):What I would recommend is that you either define a function set_my_type :: 'a my_type ⇒ 'a set and then simply write foo ∈ set_my_type bar instead of the foo ∈ bar that you wanted.
Manuel Eberl (May 06 2023 at 18:39):You could also define some custom syntax like a ∈ with some extra symbol/letter in the index. That is completely unproblematic and is almost exactly the thing you wanted, save for the extra symbol/letter. This is what is e.g. done for multisets, where we write x ∈# A.
Manuel Eberl (May 06 2023 at 18:40):(and x ∈# A is just an abbreviation for x ∈ set_mset A)
Bob Rubbens (May 06 2023 at 19:49):Thanks! I wound up using the subscript workaround, works like a charm.
Wolfgang Jeltsch (May 06 2023 at 22:25):@Manuel Eberl, what is the difference between overloading and adhoc_overloading? Unfortunately, the documentation of adhoc_overloading in The Isabelle/Isar Reference Manual is very terse; so I can’t surely tell. From the theory Adhoc_Overloading_Examples, I get the impression that both overloading and adhoc_overloading use the same underlying overloading mechanism and the difference is just that overloading lets you define the constants to overload with in a local context while adhoc_overloading allows overloading with already existing constants. Is that correct?
Last updated: Apr 27 2024 at 12:25 UTC