# HG changeset patch
# User nipkow
# Date 1244137446 -7200
# Node ID 428e4caf22994d3b276d55157c15dfaf89659ff7
# Parent  ee1d5bec4ce3ea4fcc3b5c35294421e09769f902
finite lemmas

diff -r ee1d5bec4ce3 -r 428e4caf2299 src/HOL/Finite_Set.thy
--- 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*}
diff -r ee1d5bec4ce3 -r 428e4caf2299 src/HOL/Set.thy
--- 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}"