Does the Isabelle standard library (the `HOL`

session or one of the other session that are part of the Isabelle distribution) contain definitions of the type of all non-negative reals and the type of all positive reals?

Maybe here's something you can use?

https://search.isabelle.in.tum.de/#search/default_Isabelle2021_AFP2021?page=%5B%5D&q=%7B%22term%22%3A%22%E2%84%9D%22%2C%22fields%22%3A%5B%7B%22field%22%3A%22Name%22%2C%22match%22%3A%22OneOf%22%2C%22terms%22%3A%5B%22nonneg%22%5D%7D%5D%2C%22facets%22%3A%7B%22Kind%22%3A%5B%22Constant%22%5D%7D%7D

Thanks a lot for the hint. I didn’t know about this search website. Is there a link to it on the Isabelle website?

There's no link on the isabelle download page. Here's a website of useful links for isabelle: isabelle.systems

maybe there's something else for you to discover :)

As far as I know, there is only the set of non-negative reals (written as $\mathbb{R}_{\geq 0}$) and the type of extended non-negative reals `ennreal`

(which is very important in measure theory).

Subtype definitions like that are kind of tedious because of all the type coercions you need and lemmas you have to re-prove for the new type. It's usually better to just use `real`

and carry around the non-negativity information separately.

Kevin Kappelmann said:

There's no link on the isabelle download page. Here's a website of useful links for isabelle: isabelle.systems

Interesting. Is this a collection of links to Isabelle-related services that aren’t considered “official” enough to be mentioned on the Isabelle website? So far, I’ve always turned to the Isabelle website when looking for Isabelle-related things. I’ve never expected there to be another, more information-rich website on Isabelle.

Manuel Eberl said:

Subtype definitions like that are kind of tedious because of all the type coercions you need and lemmas you have to re-prove for the new type. It's usually better to just use

`real`

and carry around the non-negativity information separately.

I see. However, in my context, which is testing a particular proof method I’ve developed, this is not an option, as such extra conditions cannot be handled by said proof method. So I’ll go for a custom subtype.

Wolfgang Jeltsch said:

Manuel Eberl said:

Subtype definitions like that are kind of tedious because of all the type coercions you need and lemmas you have to re-prove for the new type. It's usually better to just use

`real`

and carry around the non-negativity information separately.I see. However, in my context, which is testing a particular proof method I’ve developed, this is not an option, as such extra conditions cannot be handled by said proof method. So I’ll go for a custom subtype.

What we would really need here is a more automated lifting package that lets us lift all the theorems and typeclass instances we want more automatically.

Something like deriving via in Haskell.

This would also be convenient for the prod type headache where if you import one instance of linorder for prod, you will never be able to get rid of it again.

Well, there *is* `lift_definition`

and `transfer`

that sort of do this. But you still have to say what definitions and theorems you want, and sometimes there are still things to prove. I don't think it can be automated fully.

`deriving`

in Haskell is great, but it doesn't have to prove theorems.

Wolfgang Jeltsch said:

Kevin Kappelmann said:

There's no link on the isabelle download page. Here's a website of useful links for isabelle: isabelle.systems

Interesting. Is this a collection of links to Isabelle-related services that aren’t considered “official” enough to be mentioned on the Isabelle website? So far, I’ve always turned to the Isabelle website when looking for Isabelle-related things. I’ve never expected there to be another, more information-rich website on Isabelle.

Yes, if I recall correctly, @Lars Hupel made that website for precisely that reason.

Manuel Eberl said:

Well, there

is`lift_definition`

and`transfer`

that sort of do this. But you still have to say what definitions and theorems you want, and sometimes there are still things to prove. I don't think it can be automated fully.

True. I was thinking of the case where you do a type copy but here we have a proper subtype. The proper subtype wouldn't have additive inverses any more for example.

Wolfgang Jeltsch has marked this topic as resolved.

Last updated: Sep 11 2024 at 16:22 UTC