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.
Am Sonntag, den 15.03.2015, 18:49 +0100 schrieb Tobias Nipkow:
> (induction xs rule: length_induct)
> 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