# HG changeset patch
# User haftmann
# Date 1245749532 -7200
# Node ID ba52fcfaec289c661a68d4b07677b6b19b2cda04
# Parent  3585bebe49a87887a08b7d28185006423bd5b002# Parent  d5f39775edd26f3fbfc59e65f2197eb7eb8043dd
merged

diff -r 3585bebe49a8 -r ba52fcfaec28 src/HOL/Finite_Set.thy
--- 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)
diff -r 3585bebe49a8 -r ba52fcfaec28 src/HOL/Library/FuncSet.thy
--- 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)