[isabelle-dev] [isabelle] Relaxing type class constraints on interval multiplication (HOL-Library.Interval)
Lawrence Paulson
lp15 at cam.ac.uk
Fri Jan 26 13:33:19 CET 2024
Okay it is done now
Larry
On 25 Jan 2024 at 21:09 +0000, Fabian Immler <fabian.immler at gmail.com>, wrote:
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
On Mon, Jan 22, 2024 at 11:34 Achim D. Brucker <adbrucker at 0x5f.org<mailto:adbrucker at 0x5f.org>> wrote:
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240126/26c0b26f/attachment.htm>
More information about the isabelle-dev
mailing list