Re: [isabelle] Fun vs Primrec: difference?
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
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,
simplifier will use automatically. In addition, datatype and fun
plicitly declare some simplification rules: datatype the distinctness
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:
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