Email Gateway (Aug 19 2022 at 11:01): Email Gateway (Aug 19 2022 at 11:01):From: "Roger H." <s57076@hotmail.com>
Hello!
how can i prove this result:
lemma "set (tl L) ⊆ set L"
Thank you!
Email Gateway (Aug 19 2022 at 11:01):From: Ramana Kumar <rk436@cam.ac.uk>
That statement may not be true, unless you add an hypothesis that L is not
empty. (It depends on how tl is defined.)
The result should then follow easily by induction on L.
Email Gateway (Aug 19 2022 at 11:01):From: Ondřej Kunčar <kuncar@in.tum.de>
by (induction L) auto
Email Gateway (Aug 19 2022 at 11:01):From: Lars Noschinski <noschinl@in.tum.de>
Properties of functions defined by pattern matching can usually be
proved by induction. "tl" is not recursive, so case analysis suffices.
See the "induct" and "cases" methods.
-- Lars
Email Gateway (Aug 19 2022 at 11:02):From: Tobias Nipkow <nipkow@in.tum.de>
By calling sledgehammer, which gave me
by (metis (lifting) append_in_lists_conv dual_order.refl lists_eq_set
mem_Collect_eq rotate1_hd_tl set_rotate1 tl.simps(1))
Not a pretty proof, but I got it w/o having to post anything.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC