normalising simp rules for compound operators
authorhaftmann
Sun Mar 16 18:09:04 2014 +0100 (2014-03-16)
changeset 561669a241bc276cd
parent 56165 dd89ce51d2c8
child 56167 ac8098b0e458
normalising simp rules for compound operators
NEWS
src/HOL/BNF_Comp.thy
src/HOL/Complete_Lattices.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Product_Order.thy
src/HOL/Lifting_Set.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Predicate.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
src/HOL/Topological_Spaces.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/NEWS	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -98,6 +98,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* More aggressive normalization of expressions involving INF and Inf
     1.8 +or SUP and Sup. INCOMPATIBILITY.
     1.9 +
    1.10 +* INF_image and SUP_image do not unfold composition.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13  * Swapped orientation of facts image_comp and vimage_comp:
    1.14    image_compose ~> image_comp [symmetric]
    1.15    image_comp ~> image_comp [symmetric]
     2.1 --- a/src/HOL/BNF_Comp.thy	Sat Mar 15 16:54:32 2014 +0100
     2.2 +++ b/src/HOL/BNF_Comp.thy	Sun Mar 16 18:09:04 2014 +0100
     2.3 @@ -25,7 +25,7 @@
     2.4      fset_bd: "\<And>x. |fset x| \<le>o fbd" and
     2.5      gset_bd: "\<And>x. |gset x| \<le>o gbd"
     2.6    shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
     2.7 -apply (subst sym[OF SUP_def])
     2.8 +apply simp
     2.9  apply (rule ordLeq_transitive)
    2.10  apply (rule card_of_UNION_Sigma)
    2.11  apply (subst SIGMA_CSUM)
    2.12 @@ -69,7 +69,7 @@
    2.13  by blast
    2.14  
    2.15  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"
    2.16 -by (unfold comp_apply collect_def SUP_def)
    2.17 +by (unfold comp_apply collect_def) simp
    2.18  
    2.19  lemma wpull_cong:
    2.20  "\<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"
     3.1 --- a/src/HOL/Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 - (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     3.5 +(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     3.6  
     3.7  header {* Complete lattices *}
     3.8  
     3.9 @@ -20,10 +20,24 @@
    3.10  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    3.11    INF_def: "INFI A f = \<Sqinter>(f ` A)"
    3.12  
    3.13 -lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
    3.14 -  by (simp add: INF_def image_image)
    3.15 +lemma Inf_image_eq [simp]:
    3.16 +  "\<Sqinter>(f ` A) = INFI A f"
    3.17 +  by (simp add: INF_def)
    3.18 +
    3.19 +lemma INF_image [simp]:
    3.20 +  "INFI (f ` A) g = INFI A (g \<circ> f)"
    3.21 +  by (simp only: INF_def image_comp)
    3.22  
    3.23 -lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
    3.24 +lemma INF_identity_eq [simp]:
    3.25 +  "INFI A (\<lambda>x. x) = \<Sqinter>A"
    3.26 +  by (simp add: INF_def)
    3.27 +
    3.28 +lemma INF_id_eq [simp]:
    3.29 +  "INFI A id = \<Sqinter>A"
    3.30 +  by (simp add: id_def)
    3.31 +
    3.32 +lemma INF_cong:
    3.33 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
    3.34    by (simp add: INF_def image_def)
    3.35  
    3.36  end
    3.37 @@ -35,10 +49,24 @@
    3.38  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    3.39    SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    3.40  
    3.41 -lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
    3.42 -  by (simp add: SUP_def image_image)
    3.43 +lemma Sup_image_eq [simp]:
    3.44 +  "\<Squnion>(f ` A) = SUPR A f"
    3.45 +  by (simp add: SUP_def)
    3.46 +
    3.47 +lemma SUP_image [simp]:
    3.48 +  "SUPR (f ` A) g = SUPR A (g \<circ> f)"
    3.49 +  by (simp only: SUP_def image_comp)
    3.50  
    3.51 -lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
    3.52 +lemma SUP_identity_eq [simp]:
    3.53 +  "SUPR A (\<lambda>x. x) = \<Squnion>A"
    3.54 +  by (simp add: SUP_def)
    3.55 +
    3.56 +lemma SUP_id_eq [simp]:
    3.57 +  "SUPR A id = \<Squnion>A"
    3.58 +  by (simp add: id_def)
    3.59 +
    3.60 +lemma SUP_cong:
    3.61 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
    3.62    by (simp add: SUP_def image_def)
    3.63  
    3.64  end
    3.65 @@ -112,10 +140,11 @@
    3.66  
    3.67  lemma INF_foundation_dual:
    3.68    "Sup.SUPR Inf = INFI"
    3.69 -  by (simp add: fun_eq_iff INF_def Sup.SUP_def)
    3.70 +  by (simp add: fun_eq_iff Sup.SUP_def)
    3.71  
    3.72  lemma SUP_foundation_dual:
    3.73 -  "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
    3.74 +  "Inf.INFI Sup = SUPR"
    3.75 +  by (simp add: fun_eq_iff Inf.INF_def)
    3.76  
    3.77  lemma Sup_eqI:
    3.78    "(\<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"
    3.79 @@ -127,23 +156,23 @@
    3.80  
    3.81  lemma SUP_eqI:
    3.82    "(\<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"
    3.83 -  unfolding SUP_def by (rule Sup_eqI) auto
    3.84 +  using Sup_eqI [of "f ` A" x] by auto
    3.85  
    3.86  lemma INF_eqI:
    3.87    "(\<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"
    3.88 -  unfolding INF_def by (rule Inf_eqI) auto
    3.89 +  using Inf_eqI [of "f ` A" x] by auto
    3.90  
    3.91  lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    3.92 -  by (auto simp add: INF_def intro: Inf_lower)
    3.93 +  using Inf_lower [of _ "f ` A"] by simp
    3.94  
    3.95  lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    3.96 -  by (auto simp add: INF_def intro: Inf_greatest)
    3.97 +  using Inf_greatest [of "f ` A"] by auto
    3.98  
    3.99  lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   3.100 -  by (auto simp add: SUP_def intro: Sup_upper)
   3.101 +  using Sup_upper [of _ "f ` A"] by simp
   3.102  
   3.103  lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
   3.104 -  by (auto simp add: SUP_def intro: Sup_least)
   3.105 +  using Sup_least [of "f ` A"] by auto
   3.106  
   3.107  lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   3.108    using Inf_lower [of u A] by auto
   3.109 @@ -161,25 +190,25 @@
   3.110    by (auto intro: Inf_greatest dest: Inf_lower)
   3.111  
   3.112  lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
   3.113 -  by (auto simp add: INF_def le_Inf_iff)
   3.114 +  using le_Inf_iff [of _ "f ` A"] by simp
   3.115  
   3.116  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   3.117    by (auto intro: Sup_least dest: Sup_upper)
   3.118  
   3.119  lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   3.120 -  by (auto simp add: SUP_def Sup_le_iff)
   3.121 +  using Sup_le_iff [of "f ` A"] by simp
   3.122  
   3.123  lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   3.124    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   3.125  
   3.126 -lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   3.127 -  by (simp add: INF_def)
   3.128 +lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   3.129 +  unfolding INF_def Inf_insert by simp
   3.130  
   3.131  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   3.132    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   3.133  
   3.134 -lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   3.135 -  by (simp add: SUP_def)
   3.136 +lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   3.137 +  unfolding SUP_def Sup_insert by simp
   3.138  
   3.139  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   3.140    by (simp add: INF_def)
   3.141 @@ -219,7 +248,7 @@
   3.142  
   3.143  lemma INF_mono:
   3.144    "(\<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)"
   3.145 -  unfolding INF_def by (rule Inf_mono) fast
   3.146 +  using Inf_mono [of "g ` B" "f ` A"] by auto
   3.147  
   3.148  lemma Sup_mono:
   3.149    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
   3.150 @@ -233,7 +262,7 @@
   3.151  
   3.152  lemma SUP_mono:
   3.153    "(\<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)"
   3.154 -  unfolding SUP_def by (rule Sup_mono) fast
   3.155 +  using Sup_mono [of "f ` A" "g ` B"] by auto
   3.156  
   3.157  lemma INF_superset_mono:
   3.158    "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)"
   3.159 @@ -267,13 +296,13 @@
   3.160  lemma SUPR_eq:
   3.161    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
   3.162    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   3.163 -  shows "(SUP i:A. f i) = (SUP j:B. g j)"
   3.164 +  shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
   3.165    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
   3.166  
   3.167  lemma INFI_eq:
   3.168    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
   3.169    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   3.170 -  shows "(INF i:A. f i) = (INF j:B. g j)"
   3.171 +  shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
   3.172    by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
   3.173  
   3.174  lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   3.175 @@ -329,9 +358,9 @@
   3.176  qed
   3.177  
   3.178  lemma INF_top_conv [simp]:
   3.179 - "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   3.180 - "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   3.181 -  by (auto simp add: INF_def)
   3.182 +  "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   3.183 +  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   3.184 +  using Inf_top_conv [of "B ` A"] by simp_all
   3.185  
   3.186  lemma Sup_bot_conv [simp]:
   3.187    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   3.188 @@ -342,7 +371,7 @@
   3.189  lemma SUP_bot_conv [simp]:
   3.190   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   3.191   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   3.192 -  by (auto simp add: SUP_def)
   3.193 +  using Sup_bot_conv [of "B ` A"] by simp_all
   3.194  
   3.195  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   3.196    by (auto intro: antisym INF_lower INF_greatest)
   3.197 @@ -367,7 +396,7 @@
   3.198    shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
   3.199  proof -
   3.200    from assms obtain J where "I = insert k J" by blast
   3.201 -  then show ?thesis by (simp add: INF_insert)
   3.202 +  then show ?thesis by simp
   3.203  qed
   3.204  
   3.205  lemma SUP_absorb:
   3.206 @@ -375,7 +404,7 @@
   3.207    shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
   3.208  proof -
   3.209    from assms obtain J where "I = insert k J" by blast
   3.210 -  then show ?thesis by (simp add: SUP_insert)
   3.211 +  then show ?thesis by simp
   3.212  qed
   3.213  
   3.214  lemma INF_constant:
   3.215 @@ -406,17 +435,17 @@
   3.216  
   3.217  lemma INF_UNIV_bool_expand:
   3.218    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   3.219 -  by (simp add: UNIV_bool INF_insert inf_commute)
   3.220 +  by (simp add: UNIV_bool inf_commute)
   3.221  
   3.222  lemma SUP_UNIV_bool_expand:
   3.223    "(\<Squnion>b. A b) = A True \<squnion> A False"
   3.224 -  by (simp add: UNIV_bool SUP_insert sup_commute)
   3.225 +  by (simp add: UNIV_bool sup_commute)
   3.226  
   3.227  lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   3.228    by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
   3.229  
   3.230  lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
   3.231 -  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
   3.232 +  using Inf_le_Sup [of "f ` A"] by simp
   3.233  
   3.234  lemma SUP_eq_const:
   3.235    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
   3.236 @@ -443,11 +472,11 @@
   3.237  
   3.238  lemma sup_INF:
   3.239    "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   3.240 -  by (simp add: INF_def sup_Inf image_image)
   3.241 +  by (simp only: INF_def sup_Inf image_image)
   3.242  
   3.243  lemma inf_SUP:
   3.244    "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   3.245 -  by (simp add: SUP_def inf_Sup image_image)
   3.246 +  by (simp only: SUP_def inf_Sup image_image)
   3.247  
   3.248  lemma dual_complete_distrib_lattice:
   3.249    "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   3.250 @@ -529,17 +558,17 @@
   3.251  qed
   3.252  
   3.253  lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   3.254 -  by (simp add: INF_def SUP_def uminus_Inf image_image)
   3.255 +  by (simp only: INF_def SUP_def uminus_Inf image_image)
   3.256  
   3.257  lemma uminus_Sup:
   3.258    "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   3.259  proof -
   3.260 -  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
   3.261 +  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
   3.262    then show ?thesis by simp
   3.263  qed
   3.264    
   3.265  lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   3.266 -  by (simp add: INF_def SUP_def uminus_Sup image_image)
   3.267 +  by (simp only: INF_def SUP_def uminus_Sup image_image)
   3.268  
   3.269  end
   3.270  
   3.271 @@ -562,7 +591,7 @@
   3.272  
   3.273  lemma INF_less_iff:
   3.274    "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   3.275 -  unfolding INF_def Inf_less_iff by auto
   3.276 +  using Inf_less_iff [of "f ` A"] by simp
   3.277  
   3.278  lemma less_Sup_iff:
   3.279    "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   3.280 @@ -570,7 +599,7 @@
   3.281  
   3.282  lemma less_SUP_iff:
   3.283    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   3.284 -  unfolding SUP_def less_Sup_iff by auto
   3.285 +  using less_Sup_iff [of _ "f ` A"] by simp
   3.286  
   3.287  lemma Sup_eq_top_iff [simp]:
   3.288    "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   3.289 @@ -596,7 +625,7 @@
   3.290  
   3.291  lemma SUP_eq_top_iff [simp]:
   3.292    "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   3.293 -  unfolding SUP_def by auto
   3.294 +  using Sup_eq_top_iff [of "f ` A"] by simp
   3.295  
   3.296  lemma Inf_eq_bot_iff [simp]:
   3.297    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   3.298 @@ -605,18 +634,7 @@
   3.299  
   3.300  lemma INF_eq_bot_iff [simp]:
   3.301    "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   3.302 -  unfolding INF_def by auto
   3.303 -
   3.304 -lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   3.305 -proof safe
   3.306 -  fix y assume "x \<le> \<Squnion>A" "y < x"
   3.307 -  then have "y < \<Squnion>A" by auto
   3.308 -  then show "\<exists>a\<in>A. y < a"
   3.309 -    unfolding less_Sup_iff .
   3.310 -qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
   3.311 -
   3.312 -lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   3.313 -  unfolding le_Sup_iff SUP_def by simp
   3.314 +  using Inf_eq_bot_iff [of "f ` A"] by simp
   3.315  
   3.316  lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
   3.317  proof safe
   3.318 @@ -628,7 +646,18 @@
   3.319  
   3.320  lemma INF_le_iff:
   3.321    "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   3.322 -  unfolding Inf_le_iff INF_def by simp
   3.323 +  using Inf_le_iff [of "f ` A"] by simp
   3.324 +
   3.325 +lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   3.326 +proof safe
   3.327 +  fix y assume "x \<le> \<Squnion>A" "y < x"
   3.328 +  then have "y < \<Squnion>A" by auto
   3.329 +  then show "\<exists>a\<in>A. y < a"
   3.330 +    unfolding less_Sup_iff .
   3.331 +qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
   3.332 +
   3.333 +lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   3.334 +  using le_Sup_iff [of _ "f ` A"] by simp
   3.335  
   3.336  subclass complete_distrib_lattice
   3.337  proof
   3.338 @@ -704,14 +733,15 @@
   3.339  
   3.340  lemma INF_apply [simp]:
   3.341    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   3.342 -  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
   3.343 +  using Inf_apply [of "f ` A"] by (simp add: comp_def)
   3.344  
   3.345  lemma SUP_apply [simp]:
   3.346    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   3.347 -  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
   3.348 +  using Sup_apply [of "f ` A"] by (simp add: comp_def)
   3.349  
   3.350  instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
   3.351 -qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
   3.352 +qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image
   3.353 +  simp del: Inf_image_eq Sup_image_eq)
   3.354  
   3.355  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   3.356  
   3.357 @@ -888,14 +918,14 @@
   3.358  
   3.359  lemma INTER_eq:
   3.360    "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   3.361 -  by (auto simp add: INF_def)
   3.362 +  by (auto intro!: INF_eqI)
   3.363  
   3.364 -lemma Inter_image_eq [simp]:
   3.365 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   3.366 -  by (rule sym) (fact INF_def)
   3.367 +lemma Inter_image_eq:
   3.368 +  "\<Inter>(B ` A) = (\<Inter>x\<in>A. B x)"
   3.369 +  by (fact Inf_image_eq)
   3.370  
   3.371  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   3.372 -  by (auto simp add: INF_def image_def)
   3.373 +  using Inter_iff [of _ "B ` A"] by simp
   3.374  
   3.375  lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   3.376    by (auto simp add: INF_def image_def)
   3.377 @@ -1077,7 +1107,7 @@
   3.378  
   3.379  lemma UNION_eq:
   3.380    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   3.381 -  by (auto simp add: SUP_def)
   3.382 +  by (auto intro!: SUP_eqI)
   3.383  
   3.384  lemma bind_UNION [code]:
   3.385    "Set.bind A f = UNION A f"
   3.386 @@ -1087,12 +1117,12 @@
   3.387    "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   3.388    by (simp add: bind_UNION)
   3.389  
   3.390 -lemma Union_image_eq [simp]:
   3.391 +lemma Union_image_eq:
   3.392    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   3.393 -  by (rule sym) (fact SUP_def)
   3.394 +  by (fact Sup_image_eq)
   3.395  
   3.396  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   3.397 -  by (auto simp add: SUP_def image_def)
   3.398 +  using Union_iff [of _ "B ` A"] by simp
   3.399  
   3.400  lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   3.401    -- {* The order of the premises presupposes that @{term A} is rigid;
   3.402 @@ -1214,13 +1244,13 @@
   3.403  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)"
   3.404    by (rule sym) (rule SUP_sup_distrib)
   3.405  
   3.406 -lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
   3.407 -  by (simp only: INT_Int_distrib INF_def)
   3.408 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" -- {* FIXME drop *}
   3.409 +  by (simp add: INT_Int_distrib)
   3.410  
   3.411 -lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
   3.412 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" -- {* FIXME drop *}
   3.413    -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
   3.414    -- {* Union of a family of unions *}
   3.415 -  by (simp only: UN_Un_distrib SUP_def)
   3.416 +  by (simp add: UN_Un_distrib)
   3.417  
   3.418  lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
   3.419    by (fact sup_INF)
     4.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
     4.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
     4.3 @@ -275,16 +275,16 @@
     4.4    by (auto intro!: cInf_eq_minimum)
     4.5  
     4.6  lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
     4.7 -  unfolding INF_def by (rule cInf_lower) auto
     4.8 +  using cInf_lower [of _ "f ` A"] by simp
     4.9  
    4.10  lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
    4.11 -  unfolding INF_def by (rule cInf_greatest) auto
    4.12 +  using cInf_greatest [of "f ` A"] by auto
    4.13  
    4.14  lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
    4.15 -  unfolding SUP_def by (rule cSup_upper) auto
    4.16 +  using cSup_upper [of _ "f ` A"] by simp
    4.17  
    4.18  lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
    4.19 -  unfolding SUP_def by (rule cSup_least) auto
    4.20 +  using cSup_least [of "f ` A"] by auto
    4.21  
    4.22  lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
    4.23    by (auto intro: cINF_lower assms order_trans)
    4.24 @@ -311,16 +311,16 @@
    4.25    by (metis cSUP_upper le_less_trans)
    4.26  
    4.27  lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
    4.28 -  by (metis INF_def cInf_insert assms empty_is_image image_insert)
    4.29 +  by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
    4.30  
    4.31  lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
    4.32 -  by (metis SUP_def cSup_insert assms empty_is_image image_insert)
    4.33 +  by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
    4.34  
    4.35  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"
    4.36 -  unfolding INF_def by (auto intro: cInf_mono)
    4.37 +  using cInf_mono [of "g ` B" "f ` A"] by auto
    4.38  
    4.39  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"
    4.40 -  unfolding SUP_def by (auto intro: cSup_mono)
    4.41 +  using cSup_mono [of "f ` A" "g ` B"] by auto
    4.42  
    4.43  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"
    4.44    by (rule cINF_mono) auto
    4.45 @@ -338,13 +338,13 @@
    4.46    by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
    4.47  
    4.48  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)"
    4.49 -  unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib)
    4.50 +  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    4.51  
    4.52  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)"
    4.53    by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
    4.54  
    4.55  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)"
    4.56 -  unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib)
    4.57 +  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    4.58  
    4.59  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))"
    4.60    by (intro antisym le_infI cINF_greatest cINF_lower2)
    4.61 @@ -388,10 +388,10 @@
    4.62    by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
    4.63  
    4.64  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)"
    4.65 -  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
    4.66 +  using cInf_less_iff[of "f`A"] by auto
    4.67  
    4.68  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)"
    4.69 -  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
    4.70 +  using less_cSup_iff[of "f`A"] by auto
    4.71  
    4.72  lemma less_cSupE:
    4.73    assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
     5.1 --- a/src/HOL/Finite_Set.thy	Sat Mar 15 16:54:32 2014 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Sun Mar 16 18:09:04 2014 +0100
     5.3 @@ -1041,7 +1041,7 @@
     5.4    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
     5.5    from `finite A` show "?fold = ?inf"
     5.6      by (induct A arbitrary: B)
     5.7 -      (simp_all add: INF_def inf_left_commute)
     5.8 +      (simp_all add: inf_left_commute)
     5.9  qed
    5.10  
    5.11  lemma sup_SUP_fold_sup:
    5.12 @@ -1052,7 +1052,7 @@
    5.13    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    5.14    from `finite A` show "?fold = ?sup"
    5.15      by (induct A arbitrary: B)
    5.16 -      (simp_all add: SUP_def sup_left_commute)
    5.17 +      (simp_all add: sup_left_commute)
    5.18  qed
    5.19  
    5.20  lemma INF_fold_inf:
     6.1 --- a/src/HOL/GCD.thy	Sat Mar 15 16:54:32 2014 +0100
     6.2 +++ b/src/HOL/GCD.thy	Sun Mar 16 18:09:04 2014 +0100
     6.3 @@ -1581,6 +1581,9 @@
     6.4    from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
     6.5  qed
     6.6  
     6.7 +declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
     6.8 +declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
     6.9 +
    6.10  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
    6.11    by (fact Lcm_nat_empty)
    6.12  
    6.13 @@ -1736,11 +1739,11 @@
    6.14  
    6.15  lemma Lcm_set_int [code, code_unfold]:
    6.16    "Lcm (set xs) = fold lcm xs (1::int)"
    6.17 -  by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
    6.18 +  by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
    6.19  
    6.20  lemma Gcd_set_int [code, code_unfold]:
    6.21    "Gcd (set xs) = fold gcd xs (0::int)"
    6.22 -  by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
    6.23 +  by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
    6.24  
    6.25  end
    6.26  
     7.1 --- a/src/HOL/Groups_Big.thy	Sat Mar 15 16:54:32 2014 +0100
     7.2 +++ b/src/HOL/Groups_Big.thy	Sun Mar 16 18:09:04 2014 +0100
     7.3 @@ -162,8 +162,7 @@
     7.4  proof cases
     7.5    assume "finite C"
     7.6    from UNION_disjoint [OF this assms]
     7.7 -  show ?thesis
     7.8 -    by (simp add: SUP_def)
     7.9 +  show ?thesis by simp
    7.10  qed (auto dest: finite_UnionD intro: infinite)
    7.11  
    7.12  lemma distrib:
    7.13 @@ -1020,7 +1019,7 @@
    7.14     (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    7.15     ==> card (Union C) = setsum card C"
    7.16  apply (frule card_UN_disjoint [of C id])
    7.17 -apply (simp_all add: SUP_def id_def)
    7.18 +apply simp_all
    7.19  done
    7.20  
    7.21  
     8.1 --- a/src/HOL/Library/Extended_Real.thy	Sat Mar 15 16:54:32 2014 +0100
     8.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Mar 16 18:09:04 2014 +0100
     8.3 @@ -1389,16 +1389,26 @@
     8.4  qed
     8.5  
     8.6  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
     8.7 -  by (auto intro!: Sup_eqI
     8.8 +  by (auto intro!: SUP_eqI
     8.9             simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
    8.10             intro!: complete_lattice_class.Inf_lower2)
    8.11  
    8.12 +lemma ereal_SUP_uminus_eq:
    8.13 +  fixes f :: "'a \<Rightarrow> ereal"
    8.14 +  shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
    8.15 +  using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
    8.16 +
    8.17  lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
    8.18    by (auto intro!: inj_onI)
    8.19  
    8.20  lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
    8.21    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
    8.22  
    8.23 +lemma ereal_INF_uminus_eq:
    8.24 +  fixes f :: "'a \<Rightarrow> ereal"
    8.25 +  shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
    8.26 +  using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
    8.27 +
    8.28  lemma ereal_SUP_not_infty:
    8.29    fixes f :: "_ \<Rightarrow> ereal"
    8.30    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>"
    8.31 @@ -1415,7 +1425,7 @@
    8.32    fixes f :: "'a \<Rightarrow> ereal"
    8.33    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
    8.34    using ereal_Sup_uminus_image_eq[of "f`R"]
    8.35 -  by (simp add: SUP_def INF_def image_image)
    8.36 +  by (simp add: image_image)
    8.37  
    8.38  lemma ereal_INFI_uminus:
    8.39    fixes f :: "'a \<Rightarrow> ereal"
    8.40 @@ -1763,7 +1773,7 @@
    8.41  lemma SUPR_countable_SUPR:
    8.42    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
    8.43    using Sup_countable_SUPR[of "g`A"]
    8.44 -  by (auto simp: SUP_def)
    8.45 +  by auto
    8.46  
    8.47  lemma Sup_ereal_cadd:
    8.48    fixes A :: "ereal set"
    8.49 @@ -1772,7 +1782,7 @@
    8.50    shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
    8.51  proof (rule antisym)
    8.52    have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
    8.53 -    by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
    8.54 +    by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
    8.55    then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
    8.56    show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
    8.57    proof (cases a)
    8.58 @@ -1794,8 +1804,8 @@
    8.59    assumes "A \<noteq> {}"
    8.60      and "a \<noteq> -\<infinity>"
    8.61    shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
    8.62 -  using Sup_ereal_cadd[of "uminus ` A" a] assms
    8.63 -  by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
    8.64 +  using Sup_ereal_cadd [of "uminus ` A" a] assms
    8.65 +  unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
    8.66  
    8.67  lemma SUPR_ereal_cminus:
    8.68    fixes f :: "'i \<Rightarrow> ereal"
    8.69 @@ -1820,8 +1830,8 @@
    8.70    then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
    8.71      by (auto simp: image_image)
    8.72    with * show ?thesis
    8.73 -    using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
    8.74 -    by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
    8.75 +    using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
    8.76 +    by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
    8.77  qed
    8.78  
    8.79  lemma INFI_ereal_cminus:
     9.1 --- a/src/HOL/Library/FSet.thy	Sat Mar 15 16:54:32 2014 +0100
     9.2 +++ b/src/HOL/Library/FSet.thy	Sun Mar 16 18:09:04 2014 +0100
     9.3 @@ -143,7 +143,7 @@
     9.4  lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
     9.5    parametric right_total_Compl_transfer Compl_transfer by simp
     9.6  
     9.7 -instance by (default, simp_all only: INF_def SUP_def) (transfer, auto)+
     9.8 +instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
     9.9  
    9.10  end
    9.11  
    10.1 --- a/src/HOL/Library/Option_ord.thy	Sat Mar 15 16:54:32 2014 +0100
    10.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Mar 16 18:09:04 2014 +0100
    10.3 @@ -292,11 +292,11 @@
    10.4  
    10.5  lemma Some_INF:
    10.6    "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
    10.7 -  by (simp add: INF_def Some_Inf image_image)
    10.8 +  using Some_Inf [of "f ` A"] by (simp add: comp_def)
    10.9  
   10.10  lemma Some_SUP:
   10.11    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   10.12 -  by (simp add: SUP_def Some_Sup image_image)
   10.13 +  using Some_Sup [of "f ` A"] by (simp add: comp_def)
   10.14  
   10.15  instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
   10.16  begin
   10.17 @@ -319,7 +319,7 @@
   10.18        case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
   10.19        from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
   10.20        then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
   10.21 -        by (simp add: Some_INF Some_Inf)
   10.22 +        by (simp add: Some_INF Some_Inf comp_def)
   10.23        with Some B show ?thesis by (simp add: Some_image_these_eq)
   10.24      qed
   10.25    qed
   10.26 @@ -332,7 +332,7 @@
   10.27      show ?thesis
   10.28      proof (cases "B = {} \<or> B = {None}")
   10.29        case True
   10.30 -      then show ?thesis by (auto simp add: SUP_def)
   10.31 +      then show ?thesis by auto
   10.32      next
   10.33        have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
   10.34          by auto
   10.35 @@ -347,7 +347,7 @@
   10.36        moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
   10.37          by simp
   10.38        ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
   10.39 -        by (simp add: Some_SUP Some_Sup)
   10.40 +        by (simp add: Some_SUP Some_Sup comp_def)
   10.41        with Some show ?thesis
   10.42          by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
   10.43      qed
    11.1 --- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 16:54:32 2014 +0100
    11.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Mar 16 18:09:04 2014 +0100
    11.3 @@ -178,7 +178,7 @@
    11.4  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
    11.5      conditionally_complete_lattice
    11.6    by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
    11.7 -    INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
    11.8 +    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
    11.9  
   11.10  instance prod :: (complete_lattice, complete_lattice) complete_lattice
   11.11    by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   11.12 @@ -197,46 +197,46 @@
   11.13    unfolding Inf_prod_def by simp
   11.14  
   11.15  lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
   11.16 -  by (simp add: SUP_def fst_Sup image_image)
   11.17 +  using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
   11.18  
   11.19  lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
   11.20 -  by (simp add: SUP_def snd_Sup image_image)
   11.21 +  using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
   11.22  
   11.23  lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
   11.24 -  by (simp add: INF_def fst_Inf image_image)
   11.25 +  using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
   11.26  
   11.27  lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
   11.28 -  by (simp add: INF_def snd_Inf image_image)
   11.29 +  using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
   11.30  
   11.31  lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   11.32 -  by (simp add: SUP_def Sup_prod_def image_image)
   11.33 +  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
   11.34  
   11.35  lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   11.36 -  by (simp add: INF_def Inf_prod_def image_image)
   11.37 +  unfolding INF_def Inf_prod_def by (simp add: comp_def)
   11.38  
   11.39  
   11.40  text {* Alternative formulations for set infima and suprema over the product
   11.41  of two complete lattices: *}
   11.42  
   11.43  lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
   11.44 -by (auto simp: Inf_prod_def INF_def)
   11.45 +by (auto simp: Inf_prod_def)
   11.46  
   11.47  lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
   11.48 -by (auto simp: Sup_prod_def SUP_def)
   11.49 +by (auto simp: Sup_prod_def)
   11.50  
   11.51  lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
   11.52 -by (auto simp: INF_def Inf_prod_def image_comp)
   11.53 +  unfolding INF_def Inf_prod_def by simp
   11.54  
   11.55  lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
   11.56 -by (auto simp: SUP_def Sup_prod_def image_comp)
   11.57 +  unfolding SUP_def Sup_prod_def by simp
   11.58  
   11.59  lemma INF_prod_alt_def:
   11.60    "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
   11.61 -by (metis fst_INF snd_INF surjective_pairing)
   11.62 +  by (simp add: INFI_prod_alt_def comp_def)
   11.63  
   11.64  lemma SUP_prod_alt_def:
   11.65    "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
   11.66 -by (metis fst_SUP snd_SUP surjective_pairing)
   11.67 +  by (simp add: SUPR_prod_alt_def comp_def)
   11.68  
   11.69  
   11.70  subsection {* Complete distributive lattices *}
    12.1 --- a/src/HOL/Lifting_Set.thy	Sat Mar 15 16:54:32 2014 +0100
    12.2 +++ b/src/HOL/Lifting_Set.thy	Sun Mar 16 18:09:04 2014 +0100
    12.3 @@ -125,7 +125,7 @@
    12.4  
    12.5  lemma UNION_transfer [transfer_rule]:
    12.6    "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
    12.7 -  unfolding SUP_def [abs_def] by transfer_prover
    12.8 +  unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
    12.9  
   12.10  lemma Ball_transfer [transfer_rule]:
   12.11    "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
    13.1 --- a/src/HOL/List.thy	Sat Mar 15 16:54:32 2014 +0100
    13.2 +++ b/src/HOL/List.thy	Sun Mar 16 18:09:04 2014 +0100
    13.3 @@ -2877,13 +2877,13 @@
    13.4  
    13.5  lemma (in complete_lattice) INF_set_fold:
    13.6    "INFI (set xs) f = fold (inf \<circ> f) xs top"
    13.7 -  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
    13.8 +  using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
    13.9  
   13.10  declare INF_set_fold [code]
   13.11  
   13.12  lemma (in complete_lattice) SUP_set_fold:
   13.13    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   13.14 -  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   13.15 +  using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
   13.16  
   13.17  declare SUP_set_fold [code]
   13.18  
    14.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sat Mar 15 16:54:32 2014 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Mar 16 18:09:04 2014 +0100
    14.3 @@ -917,8 +917,8 @@
    14.4    fixes f :: "nat \<Rightarrow> ereal"
    14.5    assumes "\<And>n. 0 \<le> f n"
    14.6    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
    14.7 -  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
    14.8 -  by (auto intro: complete_lattice_class.Sup_upper)
    14.9 +  unfolding suminf_ereal_eq_SUPR[OF assms]
   14.10 +  by (auto intro: complete_lattice_class.SUP_upper)
   14.11  
   14.12  lemma suminf_0_le:
   14.13    fixes f :: "nat \<Rightarrow> ereal"
   14.14 @@ -1215,8 +1215,9 @@
   14.15    apply (subst SUP_inf)
   14.16    apply (intro SUP_cong[OF refl])
   14.17    apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
   14.18 -  apply (simp add: INF_def del: inf_ereal_def)
   14.19 -  done
   14.20 +  apply (drule sym)
   14.21 +  apply auto
   14.22 +  by (metis INF_absorb centre_in_ball)
   14.23  
   14.24  
   14.25  subsection {* monoset *}
    15.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Mar 15 16:54:32 2014 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Mar 16 18:09:04 2014 +0100
    15.3 @@ -18,7 +18,7 @@
    15.4  lemma cInf_abs_ge: (* TODO: is this really needed? *)
    15.5    fixes S :: "real set"
    15.6    shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
    15.7 -  by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
    15.8 +  by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto)
    15.9  
   15.10  lemma cSup_asclose: (* TODO: is this really needed? *)
   15.11    fixes S :: "real set"
    16.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Mar 15 16:54:32 2014 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Mar 16 18:09:04 2014 +0100
    16.3 @@ -2709,7 +2709,7 @@
    16.4  lemma infnorm_Max:
    16.5    fixes x :: "'a::euclidean_space"
    16.6    shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
    16.7 -  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
    16.8 +  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
    16.9  
   16.10  lemma infnorm_set_lemma:
   16.11    fixes x :: "'a::euclidean_space"
    17.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
    17.3 @@ -39,10 +39,12 @@
    17.4    hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
    17.5    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"
    17.6      by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
    17.7 +      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
    17.8        intro!: cInf_greatest cSup_least)
    17.9  qed (force intro!: cInf_lower cSup_upper
   17.10        simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
   17.11 -        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
   17.12 +        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
   17.13 +      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
   17.14  
   17.15  lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
   17.16    and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
   17.17 @@ -51,7 +53,7 @@
   17.18  
   17.19  lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
   17.20    and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
   17.21 -  by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
   17.22 +  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
   17.23  
   17.24  lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
   17.25    by (auto simp: eucl_abs)
   17.26 @@ -87,7 +89,7 @@
   17.27    shows "Sup s = X"
   17.28    using assms
   17.29    unfolding eucl_Sup euclidean_representation_setsum
   17.30 -  by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
   17.31 +  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
   17.32  
   17.33  lemma Inf_eq_minimum_componentwise:
   17.34    assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
   17.35 @@ -96,7 +98,7 @@
   17.36    shows "Inf s = X"
   17.37    using assms
   17.38    unfolding eucl_Inf euclidean_representation_setsum
   17.39 -  by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   17.40 +  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   17.41  
   17.42  end
   17.43  
   17.44 @@ -115,10 +117,11 @@
   17.45        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
   17.46      by auto
   17.47    hence "Inf ?proj = x \<bullet> b"
   17.48 -    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   17.49 +    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
   17.50    hence "x \<bullet> b = Inf X \<bullet> b"
   17.51 -    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
   17.52 -      setsum_delta cong: if_cong)
   17.53 +    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
   17.54 +      simp del: Inf_class.Inf_image_eq
   17.55 +      cong: if_cong)
   17.56    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
   17.57  qed
   17.58  
   17.59 @@ -137,10 +140,10 @@
   17.60        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
   17.61      by auto
   17.62    hence "Sup ?proj = x \<bullet> b"
   17.63 -    by (auto intro!: cSup_eq_maximum)
   17.64 +    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
   17.65    hence "x \<bullet> b = Sup X \<bullet> b"
   17.66 -    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
   17.67 -      setsum_delta cong: if_cong)
   17.68 +    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
   17.69 +      simp del: Sup_image_eq cong: if_cong)
   17.70    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
   17.71  qed
   17.72  
   17.73 @@ -715,7 +718,7 @@
   17.74  lemma diameter_closed_interval:
   17.75    fixes a b::"'a::ordered_euclidean_space"
   17.76    shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
   17.77 -  by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono
   17.78 +  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
   17.79       simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
   17.80  
   17.81  text {* Intervals in general, including infinite and mixtures of open and closed. *}
    18.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
    18.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
    18.3 @@ -1548,7 +1548,7 @@
    18.4        fix y
    18.5        assume "y \<in> {x<..} \<inter> I"
    18.6        with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
    18.7 -        by (auto intro!: cInf_lower bdd_belowI2)
    18.8 +        by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
    18.9        with a have "a < f y"
   18.10          by (blast intro: less_le_trans)
   18.11      }
   18.12 @@ -3116,7 +3116,7 @@
   18.13      fix X
   18.14      assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
   18.15      then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
   18.16 -      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD)
   18.17 +      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
   18.18      with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
   18.19        by auto
   18.20      with B show False
    19.1 --- a/src/HOL/Predicate.thy	Sat Mar 15 16:54:32 2014 +0100
    19.2 +++ b/src/HOL/Predicate.thy	Sun Mar 16 18:09:04 2014 +0100
    19.3 @@ -85,11 +85,11 @@
    19.4  
    19.5  lemma eval_INFI [simp]:
    19.6    "eval (INFI A f) = INFI A (eval \<circ> f)"
    19.7 -  by (simp only: INF_def eval_Inf image_comp)
    19.8 +  using eval_Inf [of "f ` A"] by simp
    19.9  
   19.10  lemma eval_SUPR [simp]:
   19.11    "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   19.12 -  by (simp only: SUP_def eval_Sup image_comp)
   19.13 +  using eval_Sup [of "f ` A"] by simp
   19.14  
   19.15  instantiation pred :: (type) complete_boolean_algebra
   19.16  begin
    20.1 --- a/src/HOL/Probability/Caratheodory.thy	Sat Mar 15 16:54:32 2014 +0100
    20.2 +++ b/src/HOL/Probability/Caratheodory.thy	Sun Mar 16 18:09:04 2014 +0100
    20.3 @@ -975,7 +975,7 @@
    20.4      have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
    20.5        using C' A'
    20.6        by (subst volume_finite_additive[symmetric, OF V(1)])
    20.7 -         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq
    20.8 +         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
    20.9                 intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
   20.10                 intro: generated_ringI_Basic)
   20.11      also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
   20.12 @@ -987,7 +987,7 @@
   20.13      also have "\<dots> = \<mu>_r (\<Union>C')"
   20.14        using C' Un_A
   20.15        by (subst volume_finite_additive[symmetric, OF V(1)])
   20.16 -         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq 
   20.17 +         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
   20.18                 intro: generated_ringI_Basic)
   20.19      finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
   20.20        using C' by simp
    21.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 16:54:32 2014 +0100
    21.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Mar 16 18:09:04 2014 +0100
    21.3 @@ -936,7 +936,7 @@
    21.4            by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
    21.5          also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
    21.6          finally obtain i where "a * u x < f i x" unfolding SUP_def
    21.7 -          by (auto simp add: less_Sup_iff)
    21.8 +          by (auto simp add: less_SUP_iff)
    21.9          hence "a * u x \<le> f i x" by auto
   21.10          thus ?thesis using `x \<in> space M` by auto
   21.11        qed
    22.1 --- a/src/HOL/Probability/Probability_Measure.thy	Sat Mar 15 16:54:32 2014 +0100
    22.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Sun Mar 16 18:09:04 2014 +0100
    22.3 @@ -159,7 +159,7 @@
    22.4    moreover
    22.5    { fix y assume y: "y \<in> I"
    22.6      with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
    22.7 -      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
    22.8 +      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) }
    22.9    ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
   22.10      by simp
   22.11    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
    23.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Mar 15 16:54:32 2014 +0100
    23.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Mar 16 18:09:04 2014 +0100
    23.3 @@ -386,7 +386,7 @@
    23.4    also have "\<dots> = ?y"
    23.5    proof (rule antisym)
    23.6      show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
    23.7 -      using g_in_G by (auto intro: Sup_mono simp: SUP_def)
    23.8 +      using g_in_G by (auto intro: SUP_mono)
    23.9      show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
   23.10        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   23.11    qed
    24.1 --- a/src/HOL/Probability/Regularity.thy	Sat Mar 15 16:54:32 2014 +0100
    24.2 +++ b/src/HOL/Probability/Regularity.thy	Sun Mar 16 18:09:04 2014 +0100
    24.3 @@ -319,8 +319,8 @@
    24.4        by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
    24.5      also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
    24.6          (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
    24.7 -      by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
    24.8 -         (rule INF_cong, auto simp add: sU intro!: INF_cong)
    24.9 +      by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
   24.10 +        (rule INF_cong, auto simp add: sU intro!: INF_cong)
   24.11      finally have
   24.12        "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
   24.13      moreover have
   24.14 @@ -335,7 +335,7 @@
   24.15      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   24.16        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   24.17      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
   24.18 -      by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
   24.19 +      by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
   24.20           (rule SUP_cong, auto simp: sU)
   24.21      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   24.22      proof (safe intro!: antisym SUP_least)
    25.1 --- a/src/HOL/Topological_Spaces.thy	Sat Mar 15 16:54:32 2014 +0100
    25.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Mar 16 18:09:04 2014 +0100
    25.3 @@ -31,13 +31,13 @@
    25.4    using open_Union [of "{S, T}"] by simp
    25.5  
    25.6  lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
    25.7 -  unfolding SUP_def by (rule open_Union) auto
    25.8 +  using open_Union [of "B ` A"] by simp
    25.9  
   25.10  lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
   25.11    by (induct set: finite) auto
   25.12  
   25.13  lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
   25.14 -  unfolding INF_def by (rule open_Inter) auto
   25.15 +  using open_Inter [of "B ` A"] by simp
   25.16  
   25.17  lemma openI:
   25.18    assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
   25.19 @@ -70,7 +70,7 @@
   25.20    by (induct set: finite) auto
   25.21  
   25.22  lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
   25.23 -  unfolding SUP_def by (rule closed_Union) auto
   25.24 +  using closed_Union [of "B ` A"] by simp
   25.25  
   25.26  lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
   25.27    unfolding closed_def by simp
   25.28 @@ -169,7 +169,7 @@
   25.29  
   25.30  lemma generate_topology_Union: 
   25.31    "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
   25.32 -  unfolding SUP_def by (intro generate_topology.UN) auto
   25.33 +  using generate_topology.UN [of "K ` I"] by auto
   25.34  
   25.35  lemma topological_space_generate_topology:
   25.36    "class.topological_space (generate_topology S)"
   25.37 @@ -1952,10 +1952,25 @@
   25.38    unfolding compact_fip by auto
   25.39  
   25.40  lemma compact_imp_fip_image:
   25.41 -  "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>
   25.42 -    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
   25.43 -  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
   25.44 -  by (metis image_iff)
   25.45 +  assumes "compact s"
   25.46 +    and P: "\<And>i. i \<in> I \<Longrightarrow> closed (f i)"
   25.47 +    and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})"
   25.48 +  shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
   25.49 +proof -
   25.50 +  note `compact s`
   25.51 +  moreover from P have "\<forall>i \<in> f ` I. closed i" by blast
   25.52 +  moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})"
   25.53 +  proof (rule, rule, erule conjE)
   25.54 +    fix A :: "'a set set"
   25.55 +    assume "finite A"
   25.56 +    moreover assume "A \<subseteq> f ` I"
   25.57 +    ultimately obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B"
   25.58 +      using finite_subset_image [of A f I] by blast
   25.59 +    with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp
   25.60 +  qed
   25.61 +  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip)
   25.62 +  then show ?thesis by simp
   25.63 +qed
   25.64  
   25.65  end
   25.66  
    26.1 --- a/src/HOL/UNITY/ProgressSets.thy	Sat Mar 15 16:54:32 2014 +0100
    26.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Sun Mar 16 18:09:04 2014 +0100
    26.3 @@ -257,7 +257,7 @@
    26.4   apply (simp add: progress_induction_step) 
    26.5  txt{*Disjunctive case*}
    26.6  apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
    26.7 - apply (simp add: Int_Union) 
    26.8 + apply simp 
    26.9  apply (blast intro: UN_in_lattice) 
   26.10  done
   26.11  
    27.1 --- a/src/HOL/Wellfounded.thy	Sat Mar 15 16:54:32 2014 +0100
    27.2 +++ b/src/HOL/Wellfounded.thy	Sun Mar 16 18:09:04 2014 +0100
    27.3 @@ -306,7 +306,7 @@
    27.4   "[| ALL r:R. wf r;  
    27.5       ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
    27.6    |] ==> wf(Union R)"
    27.7 -  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
    27.8 +  using wf_UN[of R "\<lambda>i. i"] by simp
    27.9  
   27.10  (*Intuition: we find an (R u S)-min element of a nonempty subset A
   27.11               by case distinction.