Dan Synek (Feb 12 2022 at 16:55): Dan Synek (Feb 12 2022 at 16:55):Hi, I am using Isabelle/ZF which has an older implementation of inductive definitions. In the document "Isabelle’s Logics: FOL and ZF" they have the following tip: "If the package fails when trying to prove your introduction rules, then set the flag trace_induct to true and try again."
I couldn't find any other mention of this flag in any documentation. So how do I set this flag? I looked for other flags and guessed [[declare trace_induct =true]], but that didn't work.
Thanks!
Wolfgang Jeltsch (Feb 12 2022 at 18:41):Dan Synek said:
I couldn't find any other mention of this flag in any documentation. So how do I set this flag? I looked for other flags and guessed [[declare trace_induct =true]], but that didn't work.
Thanks!
The declare keyword must be outside the brackets. I think declare [[trace_induct=true]] will work.
Simon Roßkopf (Feb 12 2022 at 18:54):You can show the available attributes using the print_attributes command. trace_induct does not appear in there. The document mentions in its abstract that it predates Isar and comes from a time when you interacted using ML (but was rewritten).
Searching the Isabelle repo for trace_induct showed that this flag was introduced in file ~~/src/ZF/indrule.ML in 02b7c759159b (Back in 1998). It is just a copy of Ind_Syntax.trace in ~~/src/ZF/ind_syntax.ML, introduced in the same commit. indrule.ML was deleted in 8a1059aa01f0 but ind_syntax.ML still remains to this day, so you could probably use that one. You can set it on the ML level, using for example ML‹Ind_Syntax.trace := true›. I have no idea about Isabelle/ZF so take all of this with a grain of salt.
Last updated: Apr 19 2024 at 08:19 UTC