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

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: Sep 25 2021 at 09:17 UTC