Re: [isabelle] well-founded induction on the length of a list
Thank you all for your help.
I have some follow up questions for my own learning purposes.
Is it possible to use wf_induct directly? Would I need to re-state my
lemma to do so?
What is the format of induction rules? In other words, what kind of
rules can I use with "apply (induct ... rule: ...)"? Does induct simply
just specify the way assumptions and conclusions are matched with the
current goal to produce new subgoals like rule, erule, ...?
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.
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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and