Stream: Beginner Questions

Topic: Strong Induction


view this post on Zulip 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

view this post on Zulip 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