*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 23:12:23 +0100*In-reply-to*: <4EFA1DB9.9010604@in.tum.de>*References*: <jdd284$3mo$1@dough.gmane.org> <4EFA1DB9.9010604@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:9.0) Gecko/20111224 Thunderbird/9.0.1

> 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). Thanks, that worked. Now I have a question regarding the recommended style: Is it better to make a proof without `less_induct` but rather with an explicit premise and then prove the proposition as a corollary using by (induct n arbitrary: i nt rule: less_induct) (fact cyk_correct_helper) or by stating it as a single theorem, where the structure would look like proof (induct n arbitrary: i nt rule: less_induct) case (less n' i nt) thus ?case proof (cases n') case 0 thus ?thesis sorry next case (Suc n) thus ?thesis sorry qed qed The more general question is whether it is good style to nest case distinction proofs.

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

**References**:**[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] 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