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



I think you need less_induct, induction where you can assume the
property holds for all smaller values. It is used like this:
(induction k arbitrary: i rule: less_induct).

Regards
Tobias Nipkow


Am 27/12/2011 19:19, schrieb Lars Hupel:
> 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.