# HG changeset patch
# User haftmann
# Date 1394989744 -3600
# Node ID 9a241bc276cddb9c40dac2b59bead5489fdde197
# Parent  dd89ce51d2c82ae1c98e0532bab826e5d46c895d
normalising simp rules for compound operators

diff -r dd89ce51d2c8 -r 9a241bc276cd NEWS
--- a/NEWS	Sat Mar 15 16:54:32 2014 +0100
+++ b/NEWS	Sun Mar 16 18:09:04 2014 +0100
@@ -98,6 +98,12 @@
 
 *** HOL ***
 
+* More aggressive normalization of expressions involving INF and Inf
+or SUP and Sup. INCOMPATIBILITY.
+
+* INF_image and SUP_image do not unfold composition.
+INCOMPATIBILITY.
+
 * Swapped orientation of facts image_comp and vimage_comp:
   image_compose ~> image_comp [symmetric]
   image_comp ~> image_comp [symmetric]
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -25,7 +25,7 @@
     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
     gset_bd: "\<And>x. |gset x| \<le>o gbd"
   shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
-apply (subst sym[OF SUP_def])
+apply simp
 apply (rule ordLeq_transitive)
 apply (rule card_of_UNION_Sigma)
 apply (subst SIGMA_CSUM)
@@ -69,7 +69,7 @@
 by blast
 
 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold comp_apply collect_def SUP_def)
+by (unfold comp_apply collect_def) simp
 
 lemma wpull_cong:
 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -1,4 +1,4 @@
- (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
 
 header {* Complete lattices *}
 
@@ -20,10 +20,24 @@
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   INF_def: "INFI A f = \<Sqinter>(f ` A)"
 
-lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
-  by (simp add: INF_def image_image)
+lemma Inf_image_eq [simp]:
+  "\<Sqinter>(f ` A) = INFI A f"
+  by (simp add: INF_def)
+
+lemma INF_image [simp]:
+  "INFI (f ` A) g = INFI A (g \<circ> f)"
+  by (simp only: INF_def image_comp)
 
-lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
+lemma INF_identity_eq [simp]:
+  "INFI A (\<lambda>x. x) = \<Sqinter>A"
+  by (simp add: INF_def)
+
+lemma INF_id_eq [simp]:
+  "INFI A id = \<Sqinter>A"
+  by (simp add: id_def)
+
+lemma INF_cong:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
   by (simp add: INF_def image_def)
 
 end
@@ -35,10 +49,24 @@
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   SUP_def: "SUPR A f = \<Squnion>(f ` A)"
 
-lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
-  by (simp add: SUP_def image_image)
+lemma Sup_image_eq [simp]:
+  "\<Squnion>(f ` A) = SUPR A f"
+  by (simp add: SUP_def)
+
+lemma SUP_image [simp]:
+  "SUPR (f ` A) g = SUPR A (g \<circ> f)"
+  by (simp only: SUP_def image_comp)
 
-lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
+lemma SUP_identity_eq [simp]:
+  "SUPR A (\<lambda>x. x) = \<Squnion>A"
+  by (simp add: SUP_def)
+
+lemma SUP_id_eq [simp]:
+  "SUPR A id = \<Squnion>A"
+  by (simp add: id_def)
+
+lemma SUP_cong:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
   by (simp add: SUP_def image_def)
 
 end
@@ -112,10 +140,11 @@
 
 lemma INF_foundation_dual:
   "Sup.SUPR Inf = INFI"
-  by (simp add: fun_eq_iff INF_def Sup.SUP_def)
+  by (simp add: fun_eq_iff Sup.SUP_def)
 
 lemma SUP_foundation_dual:
-  "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
+  "Inf.INFI Sup = SUPR"
+  by (simp add: fun_eq_iff Inf.INF_def)
 
 lemma Sup_eqI:
   "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
@@ -127,23 +156,23 @@
 
 lemma SUP_eqI:
   "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x"
-  unfolding SUP_def by (rule Sup_eqI) auto
+  using Sup_eqI [of "f ` A" x] by auto
 
 lemma INF_eqI:
   "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
-  unfolding INF_def by (rule Inf_eqI) auto
+  using Inf_eqI [of "f ` A" x] by auto
 
 lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
-  by (auto simp add: INF_def intro: Inf_lower)
+  using Inf_lower [of _ "f ` A"] by simp
 
 lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
-  by (auto simp add: INF_def intro: Inf_greatest)
+  using Inf_greatest [of "f ` A"] by auto
 
 lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
-  by (auto simp add: SUP_def intro: Sup_upper)
+  using Sup_upper [of _ "f ` A"] by simp
 
 lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
-  by (auto simp add: SUP_def intro: Sup_least)
+  using Sup_least [of "f ` A"] by auto
 
 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   using Inf_lower [of u A] by auto
@@ -161,25 +190,25 @@
   by (auto intro: Inf_greatest dest: Inf_lower)
 
 lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
-  by (auto simp add: INF_def le_Inf_iff)
+  using le_Inf_iff [of _ "f ` A"] by simp
 
 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   by (auto intro: Sup_least dest: Sup_upper)
 
 lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
-  by (auto simp add: SUP_def Sup_le_iff)
+  using Sup_le_iff [of "f ` A"] by simp
 
 lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
-lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
-  by (simp add: INF_def)
+lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+  unfolding INF_def Inf_insert by simp
 
 lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
-lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
-  by (simp add: SUP_def)
+lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+  unfolding SUP_def Sup_insert by simp
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   by (simp add: INF_def)
@@ -219,7 +248,7 @@
 
 lemma INF_mono:
   "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
-  unfolding INF_def by (rule Inf_mono) fast
+  using Inf_mono [of "g ` B" "f ` A"] by auto
 
 lemma Sup_mono:
   assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
@@ -233,7 +262,7 @@
 
 lemma SUP_mono:
   "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
-  unfolding SUP_def by (rule Sup_mono) fast
+  using Sup_mono [of "f ` A" "g ` B"] by auto
 
 lemma INF_superset_mono:
   "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
@@ -267,13 +296,13 @@
 lemma SUPR_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
   assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
-  shows "(SUP i:A. f i) = (SUP j:B. g j)"
+  shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
   by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
 
 lemma INFI_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
   assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
-  shows "(INF i:A. f i) = (INF j:B. g j)"
+  shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
   by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
 
 lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
@@ -329,9 +358,9 @@
 qed
 
 lemma INF_top_conv [simp]:
- "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
-  by (auto simp add: INF_def)
+  "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+  using Inf_top_conv [of "B ` A"] by simp_all
 
 lemma Sup_bot_conv [simp]:
   "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
@@ -342,7 +371,7 @@
 lemma SUP_bot_conv [simp]:
  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
  "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
-  by (auto simp add: SUP_def)
+  using Sup_bot_conv [of "B ` A"] by simp_all
 
 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   by (auto intro: antisym INF_lower INF_greatest)
@@ -367,7 +396,7 @@
   shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
 proof -
   from assms obtain J where "I = insert k J" by blast
-  then show ?thesis by (simp add: INF_insert)
+  then show ?thesis by simp
 qed
 
 lemma SUP_absorb:
@@ -375,7 +404,7 @@
   shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
 proof -
   from assms obtain J where "I = insert k J" by blast
-  then show ?thesis by (simp add: SUP_insert)
+  then show ?thesis by simp
 qed
 
 lemma INF_constant:
@@ -406,17 +435,17 @@
 
 lemma INF_UNIV_bool_expand:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
-  by (simp add: UNIV_bool INF_insert inf_commute)
+  by (simp add: UNIV_bool inf_commute)
 
 lemma SUP_UNIV_bool_expand:
   "(\<Squnion>b. A b) = A True \<squnion> A False"
-  by (simp add: UNIV_bool SUP_insert sup_commute)
+  by (simp add: UNIV_bool sup_commute)
 
 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
 
 lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
-  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+  using Inf_le_Sup [of "f ` A"] by simp
 
 lemma SUP_eq_const:
   "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
@@ -443,11 +472,11 @@
 
 lemma sup_INF:
   "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
-  by (simp add: INF_def sup_Inf image_image)
+  by (simp only: INF_def sup_Inf image_image)
 
 lemma inf_SUP:
   "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
-  by (simp add: SUP_def inf_Sup image_image)
+  by (simp only: SUP_def inf_Sup image_image)
 
 lemma dual_complete_distrib_lattice:
   "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
@@ -529,17 +558,17 @@
 qed
 
 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
-  by (simp add: INF_def SUP_def uminus_Inf image_image)
+  by (simp only: INF_def SUP_def uminus_Inf image_image)
 
 lemma uminus_Sup:
   "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
 proof -
-  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
+  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
   then show ?thesis by simp
 qed
   
 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
-  by (simp add: INF_def SUP_def uminus_Sup image_image)
+  by (simp only: INF_def SUP_def uminus_Sup image_image)
 
 end
 
@@ -562,7 +591,7 @@
 
 lemma INF_less_iff:
   "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
-  unfolding INF_def Inf_less_iff by auto
+  using Inf_less_iff [of "f ` A"] by simp
 
 lemma less_Sup_iff:
   "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
@@ -570,7 +599,7 @@
 
 lemma less_SUP_iff:
   "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
+  using less_Sup_iff [of _ "f ` A"] by simp
 
 lemma Sup_eq_top_iff [simp]:
   "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -596,7 +625,7 @@
 
 lemma SUP_eq_top_iff [simp]:
   "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
-  unfolding SUP_def by auto
+  using Sup_eq_top_iff [of "f ` A"] by simp
 
 lemma Inf_eq_bot_iff [simp]:
   "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
@@ -605,18 +634,7 @@
 
 lemma INF_eq_bot_iff [simp]:
   "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
-  unfolding INF_def by auto
-
-lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
-proof safe
-  fix y assume "x \<le> \<Squnion>A" "y < x"
-  then have "y < \<Squnion>A" by auto
-  then show "\<exists>a\<in>A. y < a"
-    unfolding less_Sup_iff .
-qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
-
-lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
-  unfolding le_Sup_iff SUP_def by simp
+  using Inf_eq_bot_iff [of "f ` A"] by simp
 
 lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
 proof safe
@@ -628,7 +646,18 @@
 
 lemma INF_le_iff:
   "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
-  unfolding Inf_le_iff INF_def by simp
+  using Inf_le_iff [of "f ` A"] by simp
+
+lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+  fix y assume "x \<le> \<Squnion>A" "y < x"
+  then have "y < \<Squnion>A" by auto
+  then show "\<exists>a\<in>A. y < a"
+    unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+  using le_Sup_iff [of _ "f ` A"] by simp
 
 subclass complete_distrib_lattice
 proof
@@ -704,14 +733,15 @@
 
 lemma INF_apply [simp]:
   "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
+  using Inf_apply [of "f ` A"] by (simp add: comp_def)
 
 lemma SUP_apply [simp]:
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
+  using Sup_apply [of "f ` A"] by (simp add: comp_def)
 
 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
+qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image
+  simp del: Inf_image_eq Sup_image_eq)
 
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
@@ -888,14 +918,14 @@
 
 lemma INTER_eq:
   "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
-  by (auto simp add: INF_def)
+  by (auto intro!: INF_eqI)
 
-lemma Inter_image_eq [simp]:
-  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
-  by (rule sym) (fact INF_def)
+lemma Inter_image_eq:
+  "\<Inter>(B ` A) = (\<Inter>x\<in>A. B x)"
+  by (fact Inf_image_eq)
 
 lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
-  by (auto simp add: INF_def image_def)
+  using Inter_iff [of _ "B ` A"] by simp
 
 lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   by (auto simp add: INF_def image_def)
@@ -1077,7 +1107,7 @@
 
 lemma UNION_eq:
   "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
-  by (auto simp add: SUP_def)
+  by (auto intro!: SUP_eqI)
 
 lemma bind_UNION [code]:
   "Set.bind A f = UNION A f"
@@ -1087,12 +1117,12 @@
   "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   by (simp add: bind_UNION)
 
-lemma Union_image_eq [simp]:
+lemma Union_image_eq:
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
-  by (rule sym) (fact SUP_def)
+  by (fact Sup_image_eq)
 
 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
-  by (auto simp add: SUP_def image_def)
+  using Union_iff [of _ "B ` A"] by simp
 
 lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   -- {* The order of the premises presupposes that @{term A} is rigid;
@@ -1214,13 +1244,13 @@
 lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
   by (rule sym) (rule SUP_sup_distrib)
 
-lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
-  by (simp only: INT_Int_distrib INF_def)
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" -- {* FIXME drop *}
+  by (simp add: INT_Int_distrib)
 
-lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" -- {* FIXME drop *}
   -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
   -- {* Union of a family of unions *}
-  by (simp only: UN_Un_distrib SUP_def)
+  by (simp add: UN_Un_distrib)
 
 lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
   by (fact sup_INF)
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -275,16 +275,16 @@
   by (auto intro!: cInf_eq_minimum)
 
 lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
-  unfolding INF_def by (rule cInf_lower) auto
+  using cInf_lower [of _ "f ` A"] by simp
 
 lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
-  unfolding INF_def by (rule cInf_greatest) auto
+  using cInf_greatest [of "f ` A"] by auto
 
 lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
-  unfolding SUP_def by (rule cSup_upper) auto
+  using cSup_upper [of _ "f ` A"] by simp
 
 lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
-  unfolding SUP_def by (rule cSup_least) auto
+  using cSup_least [of "f ` A"] by auto
 
 lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
   by (auto intro: cINF_lower assms order_trans)
@@ -311,16 +311,16 @@
   by (metis cSUP_upper le_less_trans)
 
 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
-  by (metis INF_def cInf_insert assms empty_is_image image_insert)
+  by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
 
 lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
-  by (metis SUP_def cSup_insert assms empty_is_image image_insert)
+  by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
 
 lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFI A f \<le> INFI B g"
-  unfolding INF_def by (auto intro: cInf_mono)
+  using cInf_mono [of "g ` B" "f ` A"] by auto
 
 lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPR A f \<le> SUPR B g"
-  unfolding SUP_def by (auto intro: cSup_mono)
+  using cSup_mono [of "f ` A" "g ` B"] by auto
 
 lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFI B g \<le> INFI A f"
   by (rule cINF_mono) auto
@@ -338,13 +338,13 @@
   by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
 
 lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFI (A \<union> B) f = inf (INFI A f) (INFI B f)"
-  unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib)
+  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
 
 lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
   by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
 
 lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPR (A \<union> B) f = sup (SUPR A f) (SUPR B f)"
-  unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib)
+  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
 
 lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))"
   by (intro antisym le_infI cINF_greatest cINF_lower2)
@@ -388,10 +388,10 @@
   by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
 
 lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
-  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
+  using cInf_less_iff[of "f`A"] by auto
 
 lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
-  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
+  using less_cSup_iff[of "f`A"] by auto
 
 lemma less_cSupE:
   assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -1041,7 +1041,7 @@
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?inf"
     by (induct A arbitrary: B)
-      (simp_all add: INF_def inf_left_commute)
+      (simp_all add: inf_left_commute)
 qed
 
 lemma sup_SUP_fold_sup:
@@ -1052,7 +1052,7 @@
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?sup"
     by (induct A arbitrary: B)
-      (simp_all add: SUP_def sup_left_commute)
+      (simp_all add: sup_left_commute)
 qed
 
 lemma INF_fold_inf:
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/GCD.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -1581,6 +1581,9 @@
   from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
 qed
 
+declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
+declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
+
 lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
   by (fact Lcm_nat_empty)
 
@@ -1736,11 +1739,11 @@
 
 lemma Lcm_set_int [code, code_unfold]:
   "Lcm (set xs) = fold lcm xs (1::int)"
-  by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
+  by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
 
 lemma Gcd_set_int [code, code_unfold]:
   "Gcd (set xs) = fold gcd xs (0::int)"
-  by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
+  by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
 
 end
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Groups_Big.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -162,8 +162,7 @@
 proof cases
   assume "finite C"
   from UNION_disjoint [OF this assms]
-  show ?thesis
-    by (simp add: SUP_def)
+  show ?thesis by simp
 qed (auto dest: finite_UnionD intro: infinite)
 
 lemma distrib:
@@ -1020,7 +1019,7 @@
    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    ==> card (Union C) = setsum card C"
 apply (frule card_UN_disjoint [of C id])
-apply (simp_all add: SUP_def id_def)
+apply simp_all
 done
 
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -1389,16 +1389,26 @@
 qed
 
 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
-  by (auto intro!: Sup_eqI
+  by (auto intro!: SUP_eqI
            simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
            intro!: complete_lattice_class.Inf_lower2)
 
+lemma ereal_SUP_uminus_eq:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
+  using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+
 lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
   by (auto intro!: inj_onI)
 
 lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
   using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
 
+lemma ereal_INF_uminus_eq:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
+  using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+
 lemma ereal_SUP_not_infty:
   fixes f :: "_ \<Rightarrow> ereal"
   shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPR A f\<bar> \<noteq> \<infinity>"
@@ -1415,7 +1425,7 @@
   fixes f :: "'a \<Rightarrow> ereal"
   shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
   using ereal_Sup_uminus_image_eq[of "f`R"]
-  by (simp add: SUP_def INF_def image_image)
+  by (simp add: image_image)
 
 lemma ereal_INFI_uminus:
   fixes f :: "'a \<Rightarrow> ereal"
@@ -1763,7 +1773,7 @@
 lemma SUPR_countable_SUPR:
   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
   using Sup_countable_SUPR[of "g`A"]
-  by (auto simp: SUP_def)
+  by auto
 
 lemma Sup_ereal_cadd:
   fixes A :: "ereal set"
@@ -1772,7 +1782,7 @@
   shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
 proof (rule antisym)
   have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
-    by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
+    by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
   then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
   show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
   proof (cases a)
@@ -1794,8 +1804,8 @@
   assumes "A \<noteq> {}"
     and "a \<noteq> -\<infinity>"
   shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
-  using Sup_ereal_cadd[of "uminus ` A" a] assms
-  by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
+  using Sup_ereal_cadd [of "uminus ` A" a] assms
+  unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
 
 lemma SUPR_ereal_cminus:
   fixes f :: "'i \<Rightarrow> ereal"
@@ -1820,8 +1830,8 @@
   then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
     by (auto simp: image_image)
   with * show ?thesis
-    using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
-    by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
+    using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
+    by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
 qed
 
 lemma INFI_ereal_cminus:
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -143,7 +143,7 @@
 lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
   parametric right_total_Compl_transfer Compl_transfer by simp
 
-instance by (default, simp_all only: INF_def SUP_def) (transfer, auto)+
+instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
 
 end
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Option_ord.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -292,11 +292,11 @@
 
 lemma Some_INF:
   "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
-  by (simp add: INF_def Some_Inf image_image)
+  using Some_Inf [of "f ` A"] by (simp add: comp_def)
 
 lemma Some_SUP:
   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
-  by (simp add: SUP_def Some_Sup image_image)
+  using Some_Sup [of "f ` A"] by (simp add: comp_def)
 
 instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
 begin
@@ -319,7 +319,7 @@
       case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
       from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
       then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
-        by (simp add: Some_INF Some_Inf)
+        by (simp add: Some_INF Some_Inf comp_def)
       with Some B show ?thesis by (simp add: Some_image_these_eq)
     qed
   qed
@@ -332,7 +332,7 @@
     show ?thesis
     proof (cases "B = {} \<or> B = {None}")
       case True
-      then show ?thesis by (auto simp add: SUP_def)
+      then show ?thesis by auto
     next
       have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
         by auto
@@ -347,7 +347,7 @@
       moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
         by simp
       ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
-        by (simp add: Some_SUP Some_Sup)
+        by (simp add: Some_SUP Some_Sup comp_def)
       with Some show ?thesis
         by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
     qed
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -178,7 +178,7 @@
 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     conditionally_complete_lattice
   by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
-    INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
+    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
 
 instance prod :: (complete_lattice, complete_lattice) complete_lattice
   by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
@@ -197,46 +197,46 @@
   unfolding Inf_prod_def by simp
 
 lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
-  by (simp add: SUP_def fst_Sup image_image)
+  using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
 
 lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
-  by (simp add: SUP_def snd_Sup image_image)
+  using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
 
 lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
-  by (simp add: INF_def fst_Inf image_image)
+  using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
 
 lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
-  by (simp add: INF_def snd_Inf image_image)
+  using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
 
 lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
-  by (simp add: SUP_def Sup_prod_def image_image)
+  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
 
 lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
-  by (simp add: INF_def Inf_prod_def image_image)
+  unfolding INF_def Inf_prod_def by (simp add: comp_def)
 
 
 text {* Alternative formulations for set infima and suprema over the product
 of two complete lattices: *}
 
 lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
-by (auto simp: Inf_prod_def INF_def)
+by (auto simp: Inf_prod_def)
 
 lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
-by (auto simp: Sup_prod_def SUP_def)
+by (auto simp: Sup_prod_def)
 
 lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_comp)
+  unfolding INF_def Inf_prod_def by simp
 
 lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_comp)
+  unfolding SUP_def Sup_prod_def by simp
 
 lemma INF_prod_alt_def:
   "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
-by (metis fst_INF snd_INF surjective_pairing)
+  by (simp add: INFI_prod_alt_def comp_def)
 
 lemma SUP_prod_alt_def:
   "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
-by (metis fst_SUP snd_SUP surjective_pairing)
+  by (simp add: SUPR_prod_alt_def comp_def)
 
 
 subsection {* Complete distributive lattices *}
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Lifting_Set.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -125,7 +125,7 @@
 
 lemma UNION_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
-  unfolding SUP_def [abs_def] by transfer_prover
+  unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
 
 lemma Ball_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/List.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -2877,13 +2877,13 @@
 
 lemma (in complete_lattice) INF_set_fold:
   "INFI (set xs) f = fold (inf \<circ> f) xs top"
-  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
+  using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
 
 declare INF_set_fold [code]
 
 lemma (in complete_lattice) SUP_set_fold:
   "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
-  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
+  using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
 
 declare SUP_set_fold [code]
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -917,8 +917,8 @@
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
-  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
-  by (auto intro: complete_lattice_class.Sup_upper)
+  unfolding suminf_ereal_eq_SUPR[OF assms]
+  by (auto intro: complete_lattice_class.SUP_upper)
 
 lemma suminf_0_le:
   fixes f :: "nat \<Rightarrow> ereal"
@@ -1215,8 +1215,9 @@
   apply (subst SUP_inf)
   apply (intro SUP_cong[OF refl])
   apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
-  apply (simp add: INF_def del: inf_ereal_def)
-  done
+  apply (drule sym)
+  apply auto
+  by (metis INF_absorb centre_in_ball)
 
 
 subsection {* monoset *}
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -18,7 +18,7 @@
 lemma cInf_abs_ge: (* TODO: is this really needed? *)
   fixes S :: "real set"
   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
-  by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
+  by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto)
 
 lemma cSup_asclose: (* TODO: is this really needed? *)
   fixes S :: "real set"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -2709,7 +2709,7 @@
 lemma infnorm_Max:
   fixes x :: "'a::euclidean_space"
   shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
-  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
+  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
 
 lemma infnorm_set_lemma:
   fixes x :: "'a::euclidean_space"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -39,10 +39,12 @@
   hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
   thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
     by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
+      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
       intro!: cInf_greatest cSup_least)
 qed (force intro!: cInf_lower cSup_upper
       simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
-        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
+        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
+      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
 
 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
   and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
@@ -51,7 +53,7 @@
 
 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
   and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
-  by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
+  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
 
 lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
   by (auto simp: eucl_abs)
@@ -87,7 +89,7 @@
   shows "Sup s = X"
   using assms
   unfolding eucl_Sup euclidean_representation_setsum
-  by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
+  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
 
 lemma Inf_eq_minimum_componentwise:
   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
@@ -96,7 +98,7 @@
   shows "Inf s = X"
   using assms
   unfolding eucl_Inf euclidean_representation_setsum
-  by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
+  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
 
 end
 
@@ -115,10 +117,11 @@
       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
     by auto
   hence "Inf ?proj = x \<bullet> b"
-    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
+    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
   hence "x \<bullet> b = Inf X \<bullet> b"
-    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
-      setsum_delta cong: if_cong)
+    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
+      simp del: Inf_class.Inf_image_eq
+      cong: if_cong)
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
 qed
 
@@ -137,10 +140,10 @@
       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
     by auto
   hence "Sup ?proj = x \<bullet> b"
-    by (auto intro!: cSup_eq_maximum)
+    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
   hence "x \<bullet> b = Sup X \<bullet> b"
-    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
-      setsum_delta cong: if_cong)
+    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
+      simp del: Sup_image_eq cong: if_cong)
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
 qed
 
@@ -715,7 +718,7 @@
 lemma diameter_closed_interval:
   fixes a b::"'a::ordered_euclidean_space"
   shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
-  by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono
+  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
      simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
 
 text {* Intervals in general, including infinite and mixtures of open and closed. *}
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -1548,7 +1548,7 @@
       fix y
       assume "y \<in> {x<..} \<inter> I"
       with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
-        by (auto intro!: cInf_lower bdd_belowI2)
+        by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
       with a have "a < f y"
         by (blast intro: less_le_trans)
     }
@@ -3116,7 +3116,7 @@
     fix X
     assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
     then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
-      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD)
+      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
     with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
       by auto
     with B show False
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Predicate.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -85,11 +85,11 @@
 
 lemma eval_INFI [simp]:
   "eval (INFI A f) = INFI A (eval \<circ> f)"
-  by (simp only: INF_def eval_Inf image_comp)
+  using eval_Inf [of "f ` A"] by simp
 
 lemma eval_SUPR [simp]:
   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
-  by (simp only: SUP_def eval_Sup image_comp)
+  using eval_Sup [of "f ` A"] by simp
 
 instantiation pred :: (type) complete_boolean_algebra
 begin
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -975,7 +975,7 @@
     have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
       using C' A'
       by (subst volume_finite_additive[symmetric, OF V(1)])
-         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq
+         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
                intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
                intro: generated_ringI_Basic)
     also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
@@ -987,7 +987,7 @@
     also have "\<dots> = \<mu>_r (\<Union>C')"
       using C' Un_A
       by (subst volume_finite_additive[symmetric, OF V(1)])
-         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq 
+         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
                intro: generated_ringI_Basic)
     finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
       using C' by simp
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -936,7 +936,7 @@
           by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
         also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
         finally obtain i where "a * u x < f i x" unfolding SUP_def
-          by (auto simp add: less_Sup_iff)
+          by (auto simp add: less_SUP_iff)
         hence "a * u x \<le> f i x" by auto
         thus ?thesis using `x \<in> space M` by auto
       qed
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -159,7 +159,7 @@
   moreover
   { fix y assume y: "y \<in> I"
     with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
-      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
+      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) }
   ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
     by simp
   also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -386,7 +386,7 @@
   also have "\<dots> = ?y"
   proof (rule antisym)
     show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
-      using g_in_G by (auto intro: Sup_mono simp: SUP_def)
+      using g_in_G by (auto intro: SUP_mono)
     show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   qed
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Regularity.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -319,8 +319,8 @@
       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
     also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
         (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
-      by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
-         (rule INF_cong, auto simp add: sU intro!: INF_cong)
+      by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
+        (rule INF_cong, auto simp add: sU intro!: INF_cong)
     finally have
       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
     moreover have
@@ -335,7 +335,7 @@
     also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
       by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
-      by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
+      by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
          (rule SUP_cong, auto simp: sU)
     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
     proof (safe intro!: antisym SUP_least)
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -31,13 +31,13 @@
   using open_Union [of "{S, T}"] by simp
 
 lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
-  unfolding SUP_def by (rule open_Union) auto
+  using open_Union [of "B ` A"] by simp
 
 lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
   by (induct set: finite) auto
 
 lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
-  unfolding INF_def by (rule open_Inter) auto
+  using open_Inter [of "B ` A"] by simp
 
 lemma openI:
   assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
@@ -70,7 +70,7 @@
   by (induct set: finite) auto
 
 lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
-  unfolding SUP_def by (rule closed_Union) auto
+  using closed_Union [of "B ` A"] by simp
 
 lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
   unfolding closed_def by simp
@@ -169,7 +169,7 @@
 
 lemma generate_topology_Union: 
   "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
-  unfolding SUP_def by (intro generate_topology.UN) auto
+  using generate_topology.UN [of "K ` I"] by auto
 
 lemma topological_space_generate_topology:
   "class.topological_space (generate_topology S)"
@@ -1952,10 +1952,25 @@
   unfolding compact_fip by auto
 
 lemma compact_imp_fip_image:
-  "compact s \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> closed (f i)) \<Longrightarrow> (\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})) \<Longrightarrow>
-    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
-  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
-  by (metis image_iff)
+  assumes "compact s"
+    and P: "\<And>i. i \<in> I \<Longrightarrow> closed (f i)"
+    and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})"
+  shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
+proof -
+  note `compact s`
+  moreover from P have "\<forall>i \<in> f ` I. closed i" by blast
+  moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})"
+  proof (rule, rule, erule conjE)
+    fix A :: "'a set set"
+    assume "finite A"
+    moreover assume "A \<subseteq> f ` I"
+    ultimately obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B"
+      using finite_subset_image [of A f I] by blast
+    with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp
+  qed
+  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip)
+  then show ?thesis by simp
+qed
 
 end
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -257,7 +257,7 @@
  apply (simp add: progress_induction_step) 
 txt{*Disjunctive case*}
 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
- apply (simp add: Int_Union) 
+ apply simp 
 apply (blast intro: UN_in_lattice) 
 done
 
diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -306,7 +306,7 @@
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   |] ==> wf(Union R)"
-  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
+  using wf_UN[of R "\<lambda>i. i"] by simp
 
 (*Intuition: we find an (R u S)-min element of a nonempty subset A
              by case distinction.