--- a/src/HOL/Finite_Set.thy Sat Feb 14 06:53:28 2009 -0800
+++ b/src/HOL/Finite_Set.thy Sat Feb 14 19:27:26 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])