src/HOL/Finite_Set.thy
changeset 57025 e7fd64f82876
parent 56218 1c3f1f2431f9
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Finite_Set.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -415,10 +415,13 @@
     1.4      by (auto simp add: finite_conv_nat_seg_image)
     1.5  qed
     1.6  
     1.7 +lemma finite_cartesian_product_iff:
     1.8 +  "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
     1.9 +  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
    1.10 +
    1.11  lemma finite_prod: 
    1.12    "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
    1.13 -by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV 
    1.14 -   dest: finite_cartesian_productD1 finite_cartesian_productD2)
    1.15 +  using finite_cartesian_product_iff[of UNIV UNIV] by simp
    1.16  
    1.17  lemma finite_Pow_iff [iff]:
    1.18    "finite (Pow A) \<longleftrightarrow> finite A"