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
On 10/2/19 10:57 AM, Traytel Dmitriy wrote:
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