Dan Synek (Feb 07 2022 at 16:49): Dan Synek (Feb 07 2022 at 16:49):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
Manuel Eberl (Feb 07 2022 at 16:52):You can try doing a print_consts for definitions and a print_theorems for theorems, to be placed after the datatype command
Manuel Eberl (Feb 07 2022 at 16:52):Another thing you can do is something like find_theorems name:"foo." if your datatype is called "foo".
Manuel Eberl (Feb 07 2022 at 16:52):And find_consts for definitions.
Mathias Fleury (Feb 07 2022 at 16:52):Or: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/datatypes.pdf, Section 2.4
Manuel Eberl (Feb 07 2022 at 16:53):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.
Manuel Eberl (Feb 07 2022 at 16:55):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.
Dan Synek (Feb 07 2022 at 21:17):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: Apr 19 2024 at 12:27 UTC