Email Gateway (Aug 19 2022 at 14:57): Email Gateway (Aug 19 2022 at 14:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I'll take a look after it.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:58):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/reports/Isabelle/rev/e848a17d9dee
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:15):From: René Neumann <rene.neumann@in.tum.de>
Hi,
I noticed that though there is "list_nonempty_induct" and "rev_induct",
there is no variant for reverse induction on an nonempty list. Would
this be worth adding (modulo renaming)?
lemma rev_nonempty_induct[consumes 1, case_names single snoc]:
assumes ne: "xs ≠ []"
and single: "⋀x. P [x]"
and snoc': "⋀x xs. xs ≠ [] ⟹ P xs ⟹ P (xs@[x])"
shows "P xs"
using ne
proof (induct xs rule: rev_induct)
case (snoc x xs) thus ?case
proof (cases xs)
case Nil thus ?thesis by (simp add: single)
next
case Cons with snoc show ?thesis by (fastforce intro!: snoc')
qed
qed simp
Email Gateway (Aug 19 2022 at 15:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I am personally in favour of it. Further comments?
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:20):From: Tobias Nipkow <nipkow@in.tum.de>
I am happy to see it go in.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC