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.
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".
find_consts for definitions.
Or: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/datatypes.pdf, Section 2.4
Note however that neither the
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: Aug 15 2022 at 02:13 UTC