Re: [isabelle] Dependencies on constants

On 23/06/10 20:24, Jasmin Blanchette wrote:
Am 23.06.2010 um 10:13 schrieb Rafal Kolanski:

That's amazing. I think it may be exactly what I've been looking
for! I really should have asked the list sooner rather than banging
my head against the wall for hours.

The advantage of Spec_Rules is that it returns simplification
rules for recursive functions rather than the raw definition,
intro rules for (co)inductive predicates, etc.

Is there any disadvantage you know of? For example, non-bizarre
ways of introducing constants that don't show up in this list?

I don't know for sure. I haven't ported my "Defs"-based code to
"Spec_Rules" yet. Lukas uses "Spec_Rules" for the predicate compiler;
maybe he has some insights to share.

I would definitely suggest you try with "Spec_Rules" first and use
"Defs" as a fallback.

I've investigated Spec_Rules. It works as advertised for "definition" and "constdefs", however the primrec/recdef/function/fun sadly do not register their constants in this manner. I'll take a look at Defs now, to see if those are workable.

Perhaps one day all packages will register with Spec_Rules? Who knows. Still, for definitions and constdefs, this is already a step forward.


Rafal Kolanski.

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