[isabelle] Induction over n for a proposition ALL k <= n



I'd like to prove a theorem which looks like that:

theorem "P i (i+k) ⟹ Q i (i+k)"

I use induction over `k` for an arbitrary `i` which works fine for case
`0`. However, in `Suc`, I get some assumptions:

P ?i (?i + k) ⟹ Q ?i (?i + k)
P ?i (?i + Suc k)

This is useless so far. What I'd like to have is:

P ?i (?i + ?k) ⟹ ?k < k ⟹ Q ?i (?i + ?k)

At the moment, I am using

theorem
  "(⋀k. ⟦ k < n; P i (i+k) ⟧ ⟹ Q i (i+k)) ⟹ P i (i+n) ⟹ Q i (i+n)"

This seems to be rather convoluted, though. What is the usual approach here?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.