Hi, I am working in Isabelle/ZF but my guess is that the question is also relevant for Isabelle/HOL.

When I make a datatype, there are definitions and lemmas generated by ML code. From the examples, I can see that they have names like list.defs and list.bnd_mono etc. How can I get a list of them (for a particular datatype) and how can I access their definition. There is a similar question in https://stackoverflow.com/questions/65556815/how-to-show-the-defintion-of-functions-in-isabelle and there they indicate a way to print definitions by accessing the ML level. If this is the way to do it, can someone help me how to do it in jedit, by showing me the exact command (and in what window) for the example of lists defined in List.thy.

Thanks

Dan

You can try doing a `print_consts`

for definitions and a `print_theorems`

for theorems, to be placed after the datatype command

Another thing you can do is something like `find_theorems name:"foo."`

if your datatype is called "foo".

And `find_consts`

for definitions.

Or: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/datatypes.pdf, Section 2.4

Note however that neither the `print_*`

nor `find_*`

commands will show you all the definitions and theorems that exist – some of them are hidden by default because they are considered internals. There are ways to get the datatype package to expose them, but that should normally not be necessary.

For instance, the `fun`

package does not expose the raw definition of the function, only the simplification rules. And the `datatype`

packages also hides the definitions of the datatype constructors.

Mathias Fleury, I am not sure, but I think the ZF datatype package does not refer to the new implementation that this document refers to, but to an old package whose implementation is in the ZF/Tools directory. I am unsure of how much of it I can use, but I will certainly try!

Last updated: Dec 07 2023 at 20:16 UTC