Re: [isabelle] Two orders / class instantiations

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.