*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Induction over n for a proposition ALL k <= n*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 27 Dec 2011 19:19:48 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:9.0) Gecko/20111224 Thunderbird/9.0.1

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

**Re: [isabelle] Induction over n for a proposition ALL k <= n***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Introducing a variable from a constant
- Next by Date: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Previous by Thread: Re: [isabelle] Introducing a variable from a constant
- 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