Re: [isabelle] Difference between primrec and fun



There are also some things like parametricity and measurability that are
fairly easy to prove for primitive-recursive functions but can become
quite tedious for functions defined with ‘fun’.

Manuel


On 02/10/2019 09:57, Traytel Dmitriy wrote:
> 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.