src/HOL/Set.thy
changeset 33533 40b44cb20c8c
parent 33045 2b3694001c48
child 33935 b94b4587106a
     1.1 --- a/src/HOL/Set.thy	Mon Nov 09 11:34:22 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Nov 09 15:50:15 2009 +0000
     1.3 @@ -1645,6 +1645,14 @@
     1.4  lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
     1.5  by blast
     1.6  
     1.7 +lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
     1.8 +  by auto
     1.9 +
    1.10 +lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) = 
    1.11 +   (if c \<in> A then (if d \<in> A then UNIV else B)
    1.12 +    else if d \<in> A then -B else {})"  
    1.13 +  by (auto simp add: vimage_def) 
    1.14 +
    1.15  lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    1.16  by blast
    1.17