Email Gateway (Aug 22 2022 at 11:49): Email Gateway (Aug 22 2022 at 11:49):From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
is it possible to have two class instantiations with two different relations for the same type? For example having (set, \subset) p.o. and also having (set, \supset) p.o. ? For the moment it seems not, but how do I proceed if I need both orders in a theorem? Thank you!
Email Gateway (Aug 22 2022 at 11:49):From: Lars Hupel <hupel@in.tum.de>
Hi Jonathan,
is it possible to have two class instantiations with two different
relations for the same type? For example having (set, \subset) p.o.
and also having (set, \supset) p.o. ? For the moment it seems not,
it is impossible to do so in Isabelle. Type class instantiations must
be unique. It is possible to have two identical instantiations in two
different theories, but then these two theories cannot be merged
together (that is, you can't import from both).
but how do I proceed if I need both orders in a theorem? Thank you!
There are two solutions here:
1) The standard Haskell trick to introduce a new type, e.g.
datatype 'a reverse = Reverse (get_reverse: 'a)
... and then writing an instance
instance reverse :: (po) po where
2) Use locales instead of type classes, as in e.g. HOL-Algebra. For
reference, see the locale manual, especially §7.1 which specifically
deals with your use case.
Cheers
Lars
Last updated: Apr 25 2024 at 20:15 UTC