Re: [isabelle] primrec

Hi all,

> That's precisely the point. There are very few reasons to prefer primrec to fun.

well, it's a matter of taste, but there are:

a) didactic: markup primitive recursive functions as such
b) efficiency: primrec is faster than fun
c) automation: the primrec construction always works, whereas for
function you rely on a huge stack of layers, where borderline cases you
have not foreseen could break down the whole matter (important when you
write packages with themselves define recursive functions)
d) generality: in datatypes involving higher-order arguments for
constructors, primrec may succeed, whereas function is stumbling over
those function arguments.

What I see most critical nowadays is

> The latter will also give you an induction rule exactly tailored to your function, and other benefits.

e) simplicity: if you have a primitive recursive function specification
and define it by means of primrec, the reader of your theory *sees* that
the corresponding proof principle is structural induction on the
corresponding datatype, whereas function would suggest that a special
induction rule should apply.

None of these is a reason to artificially bend a straightforward
non-primrec specification to a primrec one.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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