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?
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:
f (x#xs) (y#ys) = …
or f n = (if n = 0 then … else …)
.x # xs
, but not x # y # xs
)f (Node l r) = … f l … f r …
, but not f (Node l r) = … f (Node r l) …
.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
.