*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Induction over n for a proposition ALL k <= n*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 27 Dec 2011 20:34:17 +0100*In-reply-to*: <jdd284$3mo$1@dough.gmane.org>*References*: <jdd284$3mo$1@dough.gmane.org>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0

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? >

**Follow-Ups**:**Re: [isabelle] Induction over n for a proposition ALL k <= n***From:*Lars Hupel

**References**:**[isabelle] Induction over n for a proposition ALL k <= n***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Next by Date: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Previous by Thread: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Next by Thread: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list