# HG changeset patch
# User haftmann
# Date 1204054695 -3600
# Node ID f6bd8686b71e44a52b623146ef022da9a8f91ded
# Parent  6094349a4de92ab873322bf8b844e1eb6641bb5b
moved some set lemmas from Set.thy here

diff -r 6094349a4de9 -r f6bd8686b71e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 26 20:38:14 2008 +0100
+++ b/src/HOL/Set.thy	Tue Feb 26 20:38:15 2008 +0100
@@ -645,6 +645,9 @@
 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
   by (simp add: Bex_def)
 
+lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
+  by auto
+
 
 subsubsection {* The empty set *}
 
@@ -953,6 +956,9 @@
 lemma image_Un: "f`(A Un B) = f`A Un f`B"
   by blast
 
+lemma image_eq_UN: "f`A = (UN x:A. {f x})"
+  by blast
+
 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   by blast
 
@@ -2110,6 +2116,24 @@
   -- {* monotonicity *}
   by blast
 
+lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+by (blast intro: sym)
+
+lemma image_vimage_subset: "f ` (f -` A) <= A"
+by blast
+
+lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
+by blast
+
+lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
+by blast
+
+lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
+by blast
+
+lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
+by blast
+
 
 subsection {* Getting the Contents of a Singleton Set *}