Re: [isabelle] Difference between primrec and fun



Dear Dominique,

It’s important to remember that Isabelle/HOL is based on higher-order logic and that most of its extensions, including recursive functions, types and predicates, are derived from first principles. So there is a bootstrapping process. A general well-founded recursion theorem is proved and the recursive data type definition package makes use of that to make primrec available on the types it introduces.

If you look at these session graph at https://isabelle.in.tum.de/dist/library/HOL/HOL/session_graph.pdf

it turns out that primrec is already available in theory Nat, where it provides primitive recursion on natural numbers, well before the function definition package in Fun_Def.

The specific advantages described by others on this list are possible because primrec maps straightforwardly to internal recursion combinators with no need to check termination or deal with pattern matching.

Larry Paulson



> On 2 Oct 2019, at 07:32, Dominique Unruh <unruh at ut.ee> wrote:
> 
> 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 MHonArc.