*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] well-founded induction on the length of a list*From*: Amarin Phaosawasdi <phaosaw2 at illinois.edu>*Date*: Tue, 17 Mar 2015 13:58:02 -0500*In-reply-to*: <1426502485.10949.9.camel@lapnipkow5>*References*: <5505C347.7030100@illinois.edu> <5505C647.1020604@in.tum.de> <1426502485.10949.9.camel@lapnipkow5>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.5.0

Thank you all for your help. I have some follow up questions for my own learning purposes.

Amarin On 03/16/2015 05:41 AM, Johannes HÃlzl wrote:

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

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

**Re: [isabelle] well-founded induction on the length of a list***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Work on a new theorem prover
- Next by Date: [isabelle] Antiquotations
- Previous by Thread: Re: [isabelle] well-founded induction on the length of a list
- Next by Thread: [isabelle] LSFA 2015 - Second Call for Papers
- 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