Re: [isabelle] a little problem



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é

Am 07.07.2011 um 07:11 schrieb 游珍:

> 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
> 

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.