Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 17:24):

From: Moa Johansson <moakristin.johansson@univr.it>
Hi,

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
• 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?

Thanks,
Moa

Email Gateway (Aug 18 2022 at 17:24):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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.

Regards,

Jasmin

Last updated: Apr 23 2024 at 12:29 UTC