Re: [isabelle] Fun vs Primrec: difference?
Answer is at “isar-ref.pdf”/10.3 (page 204 and 205)
primrec defines primitive recursive functions over datatypes
(see also datatype and rep datatype). The given equations
specify reduction rules […] At most one reduction rule for
each constructor can be given. […] The reduction rules are
declared as simp by default […]
function defines functions by general well‑founded recursion.
[…] The function is specified by a set of (possibly conditional)
recursive equations with arbitrary pattern matching. The command
generates proof obligations for the completeness and the compatibility
of patterns. […] The termination command can then be used to establish
that the function is total.
fun is a shorthand notation for “function (sequential ), followed
by automated proof attempts regarding pattern matching and
That's nearly all the basics one needs to know :-) After that, I feel it's
better to use Function only when Primrec is not enough and to use Fun only
when Function is not enough (especially if one wish to avoid to rely on
implicit automated proofs).
Le Sat, 28 Jul 2012 20:33:49 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> a écrit:
Hi people out there,
New beginner here, and so beginner's questions :-P
My first one: what's the difference between “fun” and “primrec” please ?
Both looks similar or synonymous, but surprisingly, when Main is not
imported (yes, I know it should, but that's for testing), “fun” seems
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and