Re: [isabelle] well-founded induction on the length of a list



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.