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> 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 not available.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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