src/HOL/Set.thy
changeset 43898 935359fd8210
parent 43866 8a50dc70cbff
child 43967 610efb6bda1f
     1.1 --- a/src/HOL/Set.thy	Mon Jul 18 18:52:52 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Jul 18 21:15:51 2011 +0200
     1.3 @@ -880,6 +880,9 @@
     1.4    \medskip Range of a function -- just a translation for image!
     1.5  *}
     1.6  
     1.7 +lemma image_ident [simp]: "(%x. x) ` Y = Y"
     1.8 +  by blast
     1.9 +
    1.10  lemma range_eqI: "b = f x ==> b \<in> range f"
    1.11    by simp
    1.12  
    1.13 @@ -1163,6 +1166,12 @@
    1.14  lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
    1.15    by (simp add: image_def)
    1.16  
    1.17 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    1.18 +by blast
    1.19 +
    1.20 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
    1.21 +by blast
    1.22 +
    1.23  
    1.24  text {* \medskip @{text range}. *}
    1.25  
    1.26 @@ -1673,11 +1682,8 @@
    1.27    "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
    1.28    by auto
    1.29  
    1.30 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    1.31 -by blast
    1.32 -
    1.33 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
    1.34 -by blast
    1.35 +lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    1.36 +  by blast
    1.37  
    1.38  
    1.39  subsubsection {* Getting the Contents of a Singleton Set *}