Re: [isabelle] Difference between primrec and fun
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)
On 2 Oct 2019, at 08:32, Dominique Unruh <unruh at ut.ee<mailto:unruh at ut.ee>> wrote:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and