Ahmed B (Apr 28 2021 at 13:28): Ahmed B (Apr 28 2021 at 13:28):If I carry out induction in Isabelle on a natural number, Isabelle automatically uses standard induction (in the Suc x case, the induction hypothesis is that the predicate holds for x). Is there a way to force Isabelle to carry out strong induction (in the Suc x case, the induction hypothesis is that the predicate holds for all n < Suc x)? Thanks
Manuel Eberl (Apr 28 2021 at 13:43):You can use the induction rule less_induct (i.e. (induction n rule: less_induct)) to perform strong induction. That will not give you 0 and Suc as cases though, but only a single induction case less where you get as an induction hypothesis that the property holds for all k < n. If you want to distinguish between e.g: zero and non-zero, you have to do an additional case split (or prove a custom induction rule that does this, e.g. with induction_schema).
Last updated: Dec 21 2024 at 16:20 UTC