*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] well-founded induction on the length of a list*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 16 Mar 2015 11:41:25 +0100*In-reply-to*: <5505C647.1020604@in.tum.de>*Organization*: TU München*References*: <5505C347.7030100@illinois.edu> <5505C647.1020604@in.tum.de>

The induction method is quite flexible and allows you to construct such a proof quite easily: - the rule for well-founded induction on < is less_induct - you are allows to do induction over terms (not only variables) - the arbitrary-option allows you to quantify over variables So you can write: lemma "P (xs::'a list)" apply (induction "length xs" arbitrary: xs rule: less_induct) and get the desired result without needing a special induction rule. - Johannes Am Sonntag, den 15.03.2015, 18:49 +0100 schrieb Tobias Nipkow: > (induction xs rule: length_induct) > > Tobias > > On 15/03/2015 18:37, Amarin Phaosawasdi wrote: > > Hi, > > > > When trying to prove > > > > lemma "property_1 (xs::'a list) â property_2 xs" > > > > how do I apply well-founded induction on the length of xs using the relation > > less_than? > > > > Amarin > > >

**Follow-Ups**:**Re: [isabelle] well-founded induction on the length of a list***From:*Amarin Phaosawasdi

**References**:**[isabelle] well-founded induction on the length of a list***From:*Amarin Phaosawasdi

**Re: [isabelle] well-founded induction on the length of a list***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] well-founded induction on the length of a list
- Next by Date: Re: [isabelle] Reddit over, or in conjunction, with Stackoverflow?
- Previous by Thread: Re: [isabelle] well-founded induction on the length of a list
- Next by Thread: Re: [isabelle] well-founded induction on the length of a list
- Cl-isabelle-users March 2015 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