[isabelle-dev] [isabelle] Relaxing type class constraints on interval multiplication (HOL-Library.Interval)

[Lawrence Paulson]

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>