# HG changeset patch
# User nipkow
# Date 1234636035 -3600
# Node ID f24137b42d9b69d7c9746aaa960b068690689562
# Parent  2c0046b26f80811f19ecb239a560ed21be6c69e9
more finiteness

diff -r 2c0046b26f80 -r f24137b42d9b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Feb 14 08:45:16 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Feb 14 19:27:15 2009 +0100
@@ -176,7 +176,7 @@
 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
 
-lemma finite_disjI[simp]:
+lemma finite_Collect_disjI[simp]:
   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
 by(simp add:Collect_disj_eq)
 
@@ -184,7 +184,7 @@
   -- {* The converse obviously fails. *}
 by (blast intro: finite_subset)
 
-lemma finite_conjI [simp, intro]:
+lemma finite_Collect_conjI [simp, intro]:
   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
   -- {* The converse obviously fails. *}
 by(simp add:Collect_conj_eq)
@@ -247,7 +247,7 @@
   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
 by(simp add:Compl_eq_Diff_UNIV)
 
-lemma finite_not[simp]:
+lemma finite_Collect_not[simp]:
   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
 by(simp add:Collect_neg_eq)
 
@@ -393,6 +393,8 @@
     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
 qed
 
+lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
+by(simp add: Pow_def[symmetric])
 
 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
 by(blast intro: finite_subset[OF subset_Pow_Union])