--- a/src/HOL/Finite_Set.thy Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jun 04 19:44:06 2009 +0200
@@ -457,6 +457,18 @@
by(blast intro: finite_subset[OF subset_Pow_Union])
+lemma finite_subset_image:
+ assumes "finite B"
+ shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
+using assms proof(induct)
+ case empty thus ?case by simp
+next
+ case insert thus ?case
+ by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
+ blast
+qed
+
+
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
--- a/src/HOL/Set.thy Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Set.thy Thu Jun 04 19:44:06 2009 +0200
@@ -1344,13 +1344,16 @@
by auto
lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
- by blast
+by blast
lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
- by blast
+by blast
lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
- by blast
+by blast
+
+lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
+by blast
lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"