Re: [isabelle] a little problem



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

Am 07/07/2011 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






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