Re: [isabelle] Looking up Constants (ML-level)

Hi Moa,

> On the ML level, given a set of Isabelle Constants and a context/theory, I'd like to look up
> - If the constant is a datatype-constructor

src/HOL/Tools/refute.ML exports a function "is_IDT_constructor" that does just that. It relies on
src/HOL/Tools/Datatype/datatype.ML, which has some functions for querying the datatype package.

> - or, if it is a function
> - if it is a function, I'd also like to look up its defining equations. Is there a more programatic way of doing this than relying on @thms{'f.simps'}?
> Could someone please point me to the relevant bit of Isabelle where I can find some functions that does this?

To find the defining equations, there's src/Pure/Isar/spec_rules.ML. There's a rough classification in the following categories:

  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive

"simp" rules correspond to "Equational".

Tools like Nitpick and the Predicate Compiler use these APIs. You can grep their code to see examples of how they can be used.

I hope this helps.



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