Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 17:22):

From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
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

Email Gateway (Aug 19 2022 at 17:22):

From: Joachim Breitner <breitner@kit.edu>
Hi,

I have used
proof(induction xs rule: measure_induct_rule[where f = length])

Greetings,
Joachim
signature.asc

Email Gateway (Aug 19 2022 at 17:22):

From: Tobias Nipkow <nipkow@in.tum.de>
(induction xs rule: length_induct)

Tobias
smime.p7s

Email Gateway (Aug 19 2022 at 17:22):

From: Johannes Hölzl <hoelzl@in.tum.de>
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

Email Gateway (Aug 19 2022 at 17:23):

From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
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, ...?

Amarin

Last updated: Nov 21 2024 at 12:39 UTC