Email Gateway (Aug 06 2022 at 11:01): Email Gateway (Aug 06 2022 at 11:01):From: Jørgen Villadsen <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Asta Halkjær From and I find the following "backwards induction" useful:
lemma distinct_back_induct [case_names Full Distinct Drop]:
assumes ‹P xs› ‹distinct xs› ‹⋀x xs. P (x # xs) ⟹ distinct (x # xs) ⟹ P xs›
shows ‹P []›
using assms by (induct xs) (fast, metis distinct.simps(2))
Is it already in the distribution, perhaps generalized to properties other than distinct?
Regards, Jørgen
Email Gateway (Aug 08 2022 at 10:45):From: Lawrence Paulson <lp15@cam.ac.uk>
Somewhat to my surprise, I can’t find any sort of backwards induction for lists in the List theory. If we decided to add one, I would simplify it to something like
lemma back_induct [case_names Base Step]:
assumes ‹P xs› ‹⋀x xs. P (x # xs) ⟹ P xs›
shows ‹P []›
using assms by (induct xs) auto
There are lots of properties you could conjoin with P, not just distinct.
Larry
Email Gateway (Aug 08 2022 at 11:56):From: Tjark Weber <tjark.weber@it.uu.se>
Note that the conclusion ‹P []› could be generalized:
lemma:
assumes ‹P xs› ‹⋀x xs. P (x # xs) ⟹ P xs›
shows ‹P (drop n xs)›
using assms
by (induct xs arbitrary: n,
metis drop_Nil,
metis drop0 drop_Suc_Cons nat.exhaust)
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 08 2022 at 13:13):From: Thomas Sewell <tals4@cam.ac.uk>
It might be worth mentioning another way to do this.
You can state the property "P (drop i xs)" and show it by induction on i. This gives the same proof steps, give or take some fiddling with theorems like drop_Suc and tl_drop.
Of course, it's not as neat as the custom induction in this particular problem, but it generalises to a few others as well.
Cheers,
Thomas.
Last updated: Jan 04 2025 at 20:18 UTC