Re: [isabelle] Fun vs Primrec: difference?

Dear Yannick,

a very useful command to find out what theorems are newly added as part of some previous command (e.g., datatype, primrec, fun) is


(Just type it in your *.thy file directly after the command you are interested in).

It will give a list of all the new theorems. So you will see that when defining a function f via primrec or via fun, both times you will get g.simps (of course it is a different matter whether those new theorems are already included in automatic tools like 'simp', which is the case for g.simps from "fun" and "primrec").



On 07/30/2012 12:59 AM, Yannick Duchêne (Hibou57) wrote:
Additionally, “isabelle2012/doc/prog-prove.pdf” also says on page 18

   The attribute simp declares theorems to be simplification rules,
which the
   simplifier will use automatically. In addition, datatype and fun
commands im-
   plicitly declare some simplification rules: datatype the distinctness
and injec-
   tivity rules, fun the defining equations.

But this does not implies primrec don't too. Will check a later day.

Le Sun, 29 Jul 2012 07:11:59 +0200, Christian Sternagel
<c-sterna at> a écrit:

Dear Yannick,

this is not the first time this question is asked. Maybe it is best to
read through the previous discussions and come back if still questions

Search for "fun primrec" here:

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