How to show the defintion of functions in Isabelle

Is there a way in Isabelle proof assistant (2020) to check the definition of a predefined function, such as div (or abbreviation and other definitions)?

While learning about Isabelle, I find it helpful to understand how a function like div is defined. I know you can Print or Check in Coq, but couldn't get to the definition in Isabelle.

I tried to hover the mouse over and the context menu in Isabelle/jEdit, but couldn't find anything. Searching on the internet does not seem to render anything relevant either.

Solution

Ctrl+Click on the constant usually takes you to its definition (no matter by what means the constant was defined, be it definition or inductive or fun). This works for types and theorems as well!

However, for things like div that are defined in a type class, this takes you to the declaration instead. There are some other instances (e.g. constants that come out of locale interpretations, like sum) where you also don't end up where you wanted to.

I am not aware of any unified mechanism to access definitions (at least not without diving into Isabelle's ML interfaces).

However, the typical cases are the following (assuming your constant is called foo):

For ‘normal’ definitions (using the definition command) the theorem is simply called foo_def. For some other tools like primrec, the _def theorem is also accessible.
For constants from typeclasses like (+), (*), (-), (div), (mod), gcd, size, the name is foo_type_def, where type is the type in question. See for instance plus_nat_def, size_list_def.
For functions defined with fun/function/etc., the _def theorem is hidden because it comes out of a complicated internal construction, would just be confusing to the user, and is pretty useless. I think it internally builds some kind of call graph and then defines the function through that – I am not sure about the details. In any case, for fun, you should see the foo.simps lemmas as definitions (or foo.psimps if the function does not terminate everywhere).
(Co-)inductive predicates (defined with inductive/coinductive) are characterised by their foo.intros rules. They also have foo.simps though.
Some constants (such as datatype constructors) do not have visible definitions at all. I suggest you just treat them like magically they drop out of the sky with the properties that characterise them (injectivity, exhaustiveness, etc). ;)

For functions with fancy syntax like (+), you can find out the name of the underlying constant either by Ctrl+hovering over it with your mouse, or (in most cases) Ctrl+clicking on it.

If all else fails, you can also look at the internal representation of the constant like this:

ML_val ‹@{term "(+)"}›

This outputs the following:

val it = Const ("Groups.plus_class.plus", "'a ⇒ 'a ⇒ 'a"): term

And so you can see that the constant's name is plus (and its full name is Groups.plus_class.plus). And indeed, plus_nat_def gives you the definition of addition on natural numbers.

Lastly, note that sometimes people will define things one way and then add additional ‘alternative’ definitions later on by just showing the equality, e.g. is_singleton_def vs. is_singleton_altdef. In many cases, it is also better to work with derived properties rather than expanding the definitions all the time. Definitions can sometimes contain technical details such as ‘what does the function behave like on bad inputs’ (e.g. division by zero or logarithm of a negative number), and it is usually a good idea to avoid any dependence of your proof on such details whenever possible.