Re: [isabelle] Difference between primrec and fun



Hi Dominique,

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

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00032.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html

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

Dmitriy

On 2 Oct 2019, at 08:32, Dominique Unruh <unruh at ut.ee<mailto:unruh at ut.ee>> 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,
Dominique.




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