Re: [isabelle] Dependencies on constants

Hi Rafal,

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

it depends what you actually aiming it.  The Defs module represents the
proof theoretic aspect of definitions, i.e. constants which depend on
other constants.  The Spec_Rules represent more the end-user view of
"initial specification".

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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