What is the difference between primrec and fun in Isabelle/HOL?

Question

I'm reading the Isabelle tutorial and been trying to clear my concept on use of primrec and fun. With what I've searched so far, including the answer here; I understand that constructor inside primrec can have only one equation and primrec has [simp] by default whereas fun can have multiple equations and the automation tactics need to be specified explicitly. However, I still struggle to understand it clearly.

Anyone kind enough to explain with some examples?

Answer 1

primrec does primitive recursion on an algebraic datatype (or something that has been set up to look like one, like the natural numbers; I don't know much about the internals of it). This means that you have a lot of restrictions in the kind of recursion schemes that you can have:

• You can only have exactly one non-variable argument on the left-hand side (i.e. only one parameter on which you can do pattern matching). You cannot do something like f (x#xs) (y#ys) = … or f n = (if n = 0 then … else …).
• You can only pattern match on a single constructor (i.e. x # xs, but not x # y # xs)
• You can only call the function recursively on exactly the variables that you matched on the left-hand side, i.e. f (Node l r) = … f l … f r …, but not f (Node l r) = … f (Node r l) ….
• Nested recursion is only possible if it mirrors the definition of the datatype.

fun comes from the function package and is a simplified version of function that tries to prove exhaustiveness, non-overlappedness of patterns, and termination automatically. This works for most functions that arise in practice; when it does not, one has to use function and prove these things by hand. Termination is usually the one tricky one.

The main difference between fun and primrec is that fun has none of the restrictions I listed above for primrec. With fun, pretty much everything goes. As far as I know, everything primrec can do, fun can do as well.

function can also do a lot of other things such as mutually-recursive functions, partial functions (i.e. functions that do not terminate on all inputs), conditional function equations, etc. Refer to the function package manual for more information on this.

Another feature of the function command is that it generates a number of helpful rules for each function defined with it, such as the cases rule, the induction rule, the elims rules, etc. Also, you can automatically derive specialised elimination rules with the fun_cases command. This, too, is described in the manual.

TL;DR: what Joachim said. fun is usually what you want to use. If it is not enough, use function. You can use primrec for very simple functions, but there is no real advantage to do so. Another alternative that may be interesting for possibly non-terminating functions is inductive.