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

  print_theorems

(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").

cheers

chris

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 jaist.ac.jp> 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
remain:

Search for "fun primrec" here:

   https://lists.cam.ac.uk/pipermail/cl-isabelle-users/









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