Email Gateway (Jan 22 2024 at 10:34): Email Gateway (Jan 22 2024 at 10:34):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
In the theory HOL-Library.Interval, the type "'a interval" uses the
following instantiation for the type class "times":
instantiation "interval" :: (linordered_semiring) times
This prevents, for instance, using interval multiplication with the
instance "ereal interval".
It seems to be possible to "relax" the instantiation for
times/multiplication-related type classes to "{times, linorder}",
which is supported by ereal (and, hence, allows for using interval
multiplication over extended reals).
I did locally change the instantiations in HOL-Library.Interval and
rebuilt HOL-Library without any problems. HOL-Library.Interval is not
used a lot. Still, given that this change makes the interval type
applicable in more situation, I do not expect any major problems with
this change.
My changes are described in the attached patch (relative to the
Isabelle development tip 79579:57ceacd4a17b).
Is this a change that could make it into the Isabelle distribution?
Best,
Achim
relaxing_interval_type_classes.patch
Email Gateway (Jan 25 2024 at 21:09):From: Fabian Immler <fabian.immler@gmail.com>
Hi Achim,
Thank you for these suggestions. From my point of view (as one of the
authors of HOL-Library.Interval), these changes are reasonable and could go
to the Isabelle distribution (after testing with the AFP).
Unfortunately I currently don’t have access to the development repository.
Would somebody reading this volunteer to bring these changes to
isabelle-dev?
Best wishes,
Fabian
Last updated: Apr 29 2024 at 01:08 UTC