Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] prove set (tl L) ⊆ set L


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Email Gateway (Aug 19 2022 at 11:01):

From: Ondřej Kunčar <kuncar@in.tum.de>
by (induction L) auto

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC