Christian Zimmerer (Jun 23 2023 at 13:27): Christian Zimmerer (Jun 23 2023 at 13:27):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?
Mathias Fleury (Jun 23 2023 at 14:01):can you just do induction on n-l?
Mathias Fleury (Jun 23 2023 at 14:03):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
Mathias Fleury (Jun 23 2023 at 14:08):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: Apr 28 2024 at 04:17 UTC