# HG changeset patch
# User Andreas Lochbihler
# Date 1341300342 -7200
# Node ID fea68365c9757298f83f572eab4432e74dfbf869
# Parent  d07a0b9601aaeb922e0b4c093fff86fcf05ba57d
add finiteness lemmas for 'a * 'b and 'a set

diff -r d07a0b9601aa -r fea68365c975 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jun 28 09:18:58 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 03 09:25:42 2012 +0200
@@ -404,6 +404,11 @@
     by (auto simp add: finite_conv_nat_seg_image)
 qed
 
+lemma finite_prod: 
+  "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
+by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV 
+   dest: finite_cartesian_productD1 finite_cartesian_productD2)
+
 lemma finite_Pow_iff [iff]:
   "finite (Pow A) \<longleftrightarrow> finite A"
 proof
@@ -420,6 +425,9 @@
   "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
   by (simp add: Pow_def [symmetric])
 
+lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)"
+by(simp only: finite_Pow_iff Pow_UNIV[symmetric])
+
 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   by (blast intro: finite_subset [OF subset_Pow_Union])