Re: [isabelle] primrec or fun



Dear Rusi,

Am Mittwoch, den 11.05.2016, 16:18 +0530 schrieb Rustom Mody:
> In
> http://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol
> the general advice seems to be:
> 
> > 
> > *From a practitionerâs point of view, primrec is a lower-level tool that
> > you usually do not need to worry about, and simply always use fun.*
> > 
> 
> However when I see examples anywhere I see mostly primrec and not fun

Iâm not sure about the history of primrec and fun, but some of the
examples might be from times when fun was not around, or not as good as
it is now. Also, some tutorials/classes/courses might deliberately use
primrec to force the student to be aware of the differences between
primitive recursion and general recursion.

> Also I remember seeing somewhere that primrec is preferable since functions
> in IsabelleÂÂmust be terminating and with fun that proof obligation needs
> to be separately dealt with

"fun" always proves termination (or gives up). If it cannot, you have
to use "function" and prove termination yourself.

There are only a few (obscure?) cases where fun cannot do what primrec
can, as Andreas writes on SO: When a data type does not have a size
function.

Greetings,
Joachim

 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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