Re: [isabelle] primrec or fun



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

That difference is indeed significant for more than theoretical reasons.

Your ultimate aim is not to specify something but to actually prove
properties about it.  Specifications mechanisms indicate what proof
principle is likely most suitable to derive fundamental properties:

	definition -> unfolding
	inductive -> induction using specific induct rule
	function -> induction using specific induct rule
	primrec -> structural induction over a datatype

Hence primrec can be seen as a codified comment in that respect.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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