I'm trying to prove the following induction scheme:

If there is a range of integers and a proposition holds for the bounds, and for the neighbors of any n, it holds for any n in the bounds.

I am trying to prove this by induction over the range, as for the case of only one inner element in the range it trivially holds, and if the range increases by one element, the proposition still holds if either l is decreased or m is increased. However, I struggle to tell Isabelle. How would I formulate the proof in the best way?

can you just do induction on `n-l`

?

my first intuition is however that it does not hold, because proving the case `l+1`

does not work without proving `m-1`

and vice-versa

Okay nitpick agrees for natural numbers that it does not hold:

```
Nitpicking formula...
Nitpick found a counterexample:
Free variables:
P = (λx. _)(0 := True, 1 := False, 2 := False, 3 := True)
l = 0
m = 3
n = 2
```

Note that there is also `dec_induct`

, which might be helpful in your case.

Last updated: Feb 27 2024 at 08:17 UTC