Wolfgang Jeltsch (Nov 24 2021 at 15:27): Wolfgang Jeltsch (Nov 24 2021 at 15:27):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?
Kevin Kappelmann (Nov 24 2021 at 15:37):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
Wolfgang Jeltsch (Nov 24 2021 at 19:06):Thanks a lot for the hint. I didn’t know about this search website. Is there a link to it on the Isabelle website?
Kevin Kappelmann (Nov 24 2021 at 22:16):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 :)
Manuel Eberl (Nov 25 2021 at 09:25):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.
Wolfgang Jeltsch (Nov 25 2021 at 11:58):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.
Wolfgang Jeltsch (Nov 25 2021 at 12:02):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
realand 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.
Lukas Stevens (Nov 25 2021 at 12:20):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
realand 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.
Lukas Stevens (Nov 25 2021 at 12:20):Something like deriving via in Haskell.
Lukas Stevens (Nov 25 2021 at 12:22):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.
Manuel Eberl (Nov 25 2021 at 12:26):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.
Manuel Eberl (Nov 25 2021 at 12:26):deriving in Haskell is great, but it doesn't have to prove theorems.
Manuel Eberl (Nov 25 2021 at 12:27):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.
Lukas Stevens (Nov 25 2021 at 12:28):Manuel Eberl said:
Well, there is
lift_definitionandtransferthat 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.
Notification Bot (Nov 28 2021 at 21:05):Wolfgang Jeltsch has marked this topic as resolved.
Last updated: Dec 21 2024 at 12:33 UTC