Re: [isabelle] Difference between primrec and fun

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.