Re: [isabelle] Dependencies on constants




On 23/06/10 18:05, Jasmin Blanchette wrote:
What I want is some way of discovering (even really slowly) "this
is the first occurrence of a given constant; before this theorem it
did not exist before". In the case of "False" this would be
HOL.False_def.

You might find the "Defs" table useful. E.g. try:

ML {* Defs.all_specifications_of (Theory.defs_of @{theory}) *}

Most if not all constants get registered in this table when they are
defined (or introduced with the "axiomatization" command).

A more recent and in many ways more powerful approach is to use

ML {* Spec_Rules.get @{context} *}

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 hope this helps.

Yes, it definitely does, thank you, Jasmin!

Rafal Kolanski.





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