Re: [isabelle] Difference between primrec and fun

Thanks for your answers.

So, as an executive summary of the executive summary (including Manuel's answer), we could say: There are cases where primrec works and fun doesn't and vice versa. And if both work, use primrec because it's faster and some things might be easier later.

Please correct me if that rule of thumb is wrong.

I think it might be useful to cover primrec in the function definition tutorial.

Best wishes,

On 10/2/19 10:57 AM, Traytel Dmitriy wrote:
Hi Dominique,

this is a recurring topic on this mailing list. See e.g.:

The executive summary is: Reasons fo using the more low-level but also light-weight primrec include:

- primrec works for infinitely branching or mutually recursive datatypes, cases in which fun frequently fails (e.g., due to lack of a size function) and function requires manual termination proofs - documentation purposes (primrec means structural induction can be used when proving things about the functions; whereas fun may require structural or computational induction)
- speed


On 2 Oct 2019, at 08:32, Dominique Unruh <unruh at <mailto:unruh at>> wrote:

Dear all,

Isabelle has different commands for introducing recursive functions: fun, function, primrec.

The relationship between fun and function is clear to me: fun is just a convenience command that invokes function with some useful defaults.

But I cannot figure out what primrec is meant for. From the documentation (isar-ref), primrec does the same as fun, except that it imposes additional limitations on the structure of the recursive function. (And in contrast to the fun/function difference, it is not easier/more compact to write.)

So my question is: Is there any difference between primrec and fun in cases when both can be used? In that case: which command tends to be preferable? Why does primrec exist?

Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.