Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] a little problem

Email Gateway (Aug 18 2022 at 18:02):

From: 游珍 <yucy0405@163.com>
Dear friends,

I have a promble about verifying the next lemma.

lemma add_finite : "finite A \<and> A \<noteq> {} \<Longrightarrow> finite {(x::nat) + m |m. m \<in> A}"

Need your help! Thanks.

yucy

Email Gateway (Aug 18 2022 at 18:02):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear yucy,

perhaps you want to use finite_imageI:

lemma add_finite : "finite A \<Longrightarrow> finite {(x::nat) + m |m. m \<in> A}"
proof -
assume f: "finite A"
have id: "{x + m | m. m \<in> A} = (\<lambda>m. x + m) ` A" by auto
from finite_imageI[OF f]
show ?thesis unfolding id .
qed

Cheers,
René

Email Gateway (Aug 18 2022 at 18:02):

From: Tobias Nipkow <nipkow@in.tum.de>
The trick is that {e | m. m : A} is equivalent to (%m. e) A. Now you can use the lemma finite_imageI: finite ?F ==> finite (?h ?F)

lemma add_finite : "finite A ==> finite {(x::nat) + m |m. m : A}"
using finite_imageI[of A "%m. x+m"]
by(simp add: image_def)

Note that A ~= {} is unnecessary.

Tobias

Last updated: Nov 21 2024 at 12:39 UTC