Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] pred ... (map ... x) = pred ... x


view this post on Zulip Email Gateway (Aug 22 2022 at 13:02):

From: Lars Hupel <hupel@in.tum.de>
Dear BNF developers,

may I suggest theorems of the following form to be generated by the
datatype package?

theorem list_all_map:
fixes P :: "'a ⇒ bool"
and f :: "'b ⇒ 'a"
and xs :: "'b list"
shows "list_all P (map f xs) = list_all (λx. P (f x)) xs"

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 13:02):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,

in a recent repository version (e.g. c4fad0569a24) you get list.pred_map:

theorem
fixes Q :: "'a ⇒ bool"
and f :: "'b ⇒ 'a"
and x :: "'b list"
shows "list_all Q (map f x) = list_all (Q o f) x”

Additionally unfolding o_def will give you what you want.

Dmitriy


Last updated: Mar 29 2024 at 08:18 UTC