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`

.

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

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

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

Thanks a lot. That was of great help.

Wolfgang Jeltsch has marked this topic as resolved.

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]$.

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.

You could enable `show_sorts`

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

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).

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.

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.

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: Dec 07 2023 at 08:19 UTC