diff -r 535789c26230 -r 40b44cb20c8c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Nov 09 11:34:22 2009 +0100
+++ b/src/HOL/Set.thy	Mon Nov 09 15:50:15 2009 +0000
@@ -1645,6 +1645,14 @@
 lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
 by blast
 
+lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
+  by auto
+
+lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) = 
+   (if c \<in> A then (if d \<in> A then UNIV else B)
+    else if d \<in> A then -B else {})"  
+  by (auto simp add: vimage_def) 
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast