Stream: General

Topic: ✔ Logarithms

Wolfgang Jeltsch (Nov 28 2021 at 21:08):

What logarithm functions are provided by standard sessions like HOL, HOL-Library, and HOL-Analysis? There’s log, but I can’t even get ln.

And, more generally, how could I find this out myself? Search by browsing through https://isabelle.in.tum.de/library/HOL/index.html needs quite some good guessing to be efficient, and automated search with https://search.isabelle.in.tum.de/ shows 920 hits when entering log.

Kevin Kappelmann (Nov 28 2021 at 21:25):

On search.isabelle.in.tum.de you should use the filters to narrow down the search results (cf the examples page on the website)
In your case, you could start with a search for "semantic entitty name" of "log" or "ln": https://search.isabelle.in.tum.de/#search/default_Isabelle2021_AFP2021?page=%5B%5D&q=%7B%22fields%22%3A%5B%7B%22field%22%3A%22Name%22%2C%22match%22%3A%22OneOf%22%2C%22terms%22%3A%5B%22ln%22%2C%22log%22%5D%7D%5D%2C%22facets%22%3A%7B%22Kind%22%3A%5B%22Constant%22%5D%7D%7D

Kevin Kappelmann (Nov 28 2021 at 21:26):

and if that's still too much, further refine based on the type, removing one of "ln" or "log" etc.

Kevin Kappelmann (Nov 28 2021 at 21:28):

or maybe a concept-based search on serapis works better for you if you have some further context.

Wolfgang Jeltsch (Nov 28 2021 at 22:17):

Thanks a lot. That was of great help.

Notification Bot (Nov 28 2021 at 22:17):

Wolfgang Jeltsch has marked this topic as resolved.

Manuel Eberl (Nov 29 2021 at 08:50):

Wolfgang Jeltsch said:

What logarithm functions are provided by standard sessions like HOL, HOL-Library, and HOL-Analysis? There’s log, but I can’t even get ln.

And, more generally, how could I find this out myself? Search by browsing through https://isabelle.in.tum.de/library/HOL/index.html needs quite some good guessing to be efficient, and automated search with https://search.isabelle.in.tum.de/ shows 920 hits when entering log.

Wait, what do you mean you ‘can't get ln’? The ln function is defined in HOL. The log function is even defined in terms of ln. You just have to remember to import Complex_Main instead of Main if you want to use it. (but if you use HOL-Analysis, that imports Complex_Main anyway).

ln is defined in its own type class ln. There is an instantiation for real where ln x is undefined for non-positive x in the sense that ∀x<0. ln x = c for some constant c that we know nothing about. And there is an instantiation for complex in HOL-Analysis, where ln 0 is undefined and otherwise ln z is the principal branch of the logarithm, i.e. the unique w such that $e^w = z$ and $\text{Im}(w)\in(-\pi,\pi]$.

Wolfgang Jeltsch (Nov 30 2021 at 00:47):

Manuel Eberl said:

Wait, what do you mean you ‘can't get ln’?

I got this wrong. For checking whether a constant of a certain name is available, I typically write term ⟨name⟩, and when Isabelle shows ⟨name⟩ :: 'a, I know it’s not available (of course, this isn’t entirely safe, as in particular undefined does have type 'a). In the case of ln, Isabelle showed me ln :: 'a ⇒ 'a, and I just saw the type variable and immediately thought ln doesn’t exist. A problem here is that Isabelle doesn’t show a type like 'a::⟨some_class⟩ ⇒ 'a in such cases.

Kevin Kappelmann (Nov 30 2021 at 08:15):

You could enable show_sorts for that: https://isabelle.in.tum.de/doc/isar-ref.pdf#attribute.show-sorts

Lukas Stevens (Nov 30 2021 at 09:31):

There is also find_consts. And if the variable is shown in black (instead of blue), then it is not free so you know that it is already defined (you can then also Ctrl+Click to go to the definition).

Wolfgang Jeltsch (Nov 30 2021 at 15:49):

Well, find_consts isn’t about showing sorts for given constants, but about finding constants by type, right? How would you find ln by type? There are zillions of functions that have the same type, and maybe you would even have to know its most general type, which would require to know a fair bit of the class structure of the standard library.

The constant being shown in black vs. blue is, of course, a viable solution.

Fabian Huch (Nov 30 2021 at 15:53):

You can find ln by name with find_consts:

find_consts name: "ln"

Of course you have to have it imported somewhere for that to work.

Wolfgang Jeltsch (Nov 30 2021 at 16:10):

Sure. However, that was not my point. My point was that, as I assumed, find_consts could search by type only. I just didn’t know about the name: argument. Thanks for showing me that.

Last updated: Apr 24 2024 at 16:18 UTC