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.

  - Johannes

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