--- a/src/HOL/Finite_Set.thy Tue Jun 23 10:22:11 2009 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jun 23 11:32:12 2009 +0200
@@ -285,6 +285,10 @@
-- {* The image of a finite set is finite. *}
by (induct set: finite) simp_all
+lemma finite_image_set [simp]:
+ "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
+ by (simp add: image_Collect [symmetric])
+
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
apply (frule finite_imageI)
apply (erule finite_subset, assumption)
--- a/src/HOL/Library/FuncSet.thy Tue Jun 23 10:22:11 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Jun 23 11:32:12 2009 +0200
@@ -67,6 +67,9 @@
"f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by(auto simp: Pi_def)
+lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
+ by (auto intro: Pi_I)
+
lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
by (simp add: Pi_def)