1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 18:52:52 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:15:51 2011 +0200
     1.3 @@ -397,14 +397,6 @@
     1.4    shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
     1.5    unfolding SUP_def less_Sup_iff by auto
     1.6  
     1.7 --- "FIXME move"
     1.8 -
     1.9 -lemma image_ident [simp]: "(%x. x) ` Y = Y"
    1.10 -  by blast
    1.11 -
    1.12 -lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    1.13 -  by blast
    1.14 -
    1.15  class complete_boolean_algebra = boolean_algebra + complete_lattice
    1.16  begin
    1.17  

     2.1 --- a/src/HOL/Set.thy	Mon Jul 18 18:52:52 2011 +0200
     2.2 +++ b/src/HOL/Set.thy	Mon Jul 18 21:15:51 2011 +0200
     2.3 @@ -880,6 +880,9 @@
     2.4    \medskip Range of a function -- just a translation for image!
     2.5  *}
     2.6  
     2.7 +lemma image_ident [simp]: "(%x. x) ` Y = Y"
     2.8 +  by blast
     2.9 +
    2.10  lemma range_eqI: "b = f x ==> b \<in> range f"
    2.11    by simp
    2.12  
    2.13 @@ -1163,6 +1166,12 @@
    2.14  lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
    2.15    by (simp add: image_def)
    2.16  
    2.17 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    2.18 +by blast
    2.19 +
    2.20 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
    2.21 +by blast
    2.22 +
    2.23  
    2.24  text {* \medskip @{text range}. *}
    2.25  
    2.26 @@ -1673,11 +1682,8 @@
    2.27    "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
    2.28    by auto
    2.29  
    2.30 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    2.31 -by blast
    2.32 -
    2.33 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
    2.34 -by blast
    2.35 +lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    2.36 +  by blast
    2.37  
    2.38  
    2.39  subsubsection {* Getting the Contents of a Singleton Set *}