*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Induction over n for a proposition ALL k <= n*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 27 Dec 2011 19:26:08 +0100*In-reply-to*: <jdd284$3mo$1@dough.gmane.org>*References*: <jdd284$3mo$1@dough.gmane.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:9.0) Gecko/20111224 Thunderbird/9.0.1

> 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? I should add that I have no idea whether this works, as I'm still in the process of figuring out how my proof should look like.

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

- Previous by Date: [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: [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