## Stream: Beginner Questions

### Topic: Strong Induction

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