Gergely Buday (Sep 28 2023 at 15:38): Gergely Buday (Sep 28 2023 at 15:38):Section 6.5.3 Declaring rules of the Isabelle/Isar Reference Manual says that one can define custom cases, induction and coinduction rules.
Is there any checking that they satisfy the properties of cases, induction and coinduction?
And, when can I say that a rule is a cases, induction or coinduction rule? Where can I read about this?
Wolfgang Jeltsch (Sep 28 2023 at 16:41):You can pass elimination, induction, and coinduction rules to the cases, induction, and coinduction methods respectively via a rule argument (that is, after a rule:). If a rule so passed doesn’t have the right structure, the method will find out upon invocation.
At least for cases and induction, this should be mentioned in the prog-prove tutorial, and in general this should also be discussed in the section of the Isabelle/Isar Reference Manual that discusses cases, induction, and coinduction.
Last updated: May 02 2024 at 04:18 UTC