# HG changeset patch
# User haftmann
# Date 1311016551 -7200
# Node ID 935359fd8210c5d418a1b66981fff0ea76cbc04e
# Parent  f3e75541cb7833950defa401f0d7e31015983025
moved lemmas to appropriate theory

diff -r f3e75541cb78 -r 935359fd8210 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 18:52:52 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:15:51 2011 +0200
@@ -397,14 +397,6 @@
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   unfolding SUP_def less_Sup_iff by auto
 
--- "FIXME move"
-
-lemma image_ident [simp]: "(%x. x) ` Y = Y"
-  by blast
-
-lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
-  by blast
-
 class complete_boolean_algebra = boolean_algebra + complete_lattice
 begin
 
diff -r f3e75541cb78 -r 935359fd8210 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jul 18 18:52:52 2011 +0200
+++ b/src/HOL/Set.thy	Mon Jul 18 21:15:51 2011 +0200
@@ -880,6 +880,9 @@
   \medskip Range of a function -- just a translation for image!
 *}
 
+lemma image_ident [simp]: "(%x. x) ` Y = Y"
+  by blast
+
 lemma range_eqI: "b = f x ==> b \<in> range f"
   by simp
 
@@ -1163,6 +1166,12 @@
 lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
   by (simp add: image_def)
 
+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
+
 
 text {* \medskip @{text range}. *}
 
@@ -1673,11 +1682,8 @@
   "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
   by auto
 
-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 vimage_ident [simp]: "(%x. x) -` Y = Y"
+  by blast
 
 
 subsubsection {* Getting the Contents of a Singleton Set *}