elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
authorhaftmann
Wed Mar 19 18:47:22 2014 +0100 (2014-03-19)
changeset 562181c3f1f2431f9
parent 56217 dc429a5b13c4
child 56219 bf80d125406b
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
NEWS
src/HOL/Complete_Lattices.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/RBT_Set.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/Predicate.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Wed Mar 19 17:06:02 2014 +0000
     1.2 +++ b/NEWS	Wed Mar 19 18:47:22 2014 +0100
     1.3 @@ -98,6 +98,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Consolidated theorem names containing INFI and SUPR: have INF
    1.11  and SUP instead uniformly.  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Complete_Lattices.thy	Wed Mar 19 17:06:02 2014 +0000
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Mar 19 18:47:22 2014 +0100
     2.3 @@ -17,27 +17,27 @@
     2.4    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     2.5  begin
     2.6  
     2.7 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
     2.8 -  INF_def: "INFI A f = \<Sqinter>(f ` A)"
     2.9 +definition INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.10 +  INF_def: "INFIMUM A f = \<Sqinter>(f ` A)"
    2.11  
    2.12  lemma Inf_image_eq [simp]:
    2.13 -  "\<Sqinter>(f ` A) = INFI A f"
    2.14 +  "\<Sqinter>(f ` A) = INFIMUM A f"
    2.15    by (simp add: INF_def)
    2.16  
    2.17  lemma INF_image [simp]:
    2.18 -  "INFI (f ` A) g = INFI A (g \<circ> f)"
    2.19 +  "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
    2.20    by (simp only: INF_def image_comp)
    2.21  
    2.22  lemma INF_identity_eq [simp]:
    2.23 -  "INFI A (\<lambda>x. x) = \<Sqinter>A"
    2.24 +  "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
    2.25    by (simp add: INF_def)
    2.26  
    2.27  lemma INF_id_eq [simp]:
    2.28 -  "INFI A id = \<Sqinter>A"
    2.29 +  "INFIMUM A id = \<Sqinter>A"
    2.30    by (simp add: id_def)
    2.31  
    2.32  lemma INF_cong:
    2.33 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
    2.34 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
    2.35    by (simp add: INF_def image_def)
    2.36  
    2.37  end
    2.38 @@ -46,33 +46,33 @@
    2.39    fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    2.40  begin
    2.41  
    2.42 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.43 -  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    2.44 +definition SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.45 +  SUP_def: "SUPREMUM A f = \<Squnion>(f ` A)"
    2.46  
    2.47  lemma Sup_image_eq [simp]:
    2.48 -  "\<Squnion>(f ` A) = SUPR A f"
    2.49 +  "\<Squnion>(f ` A) = SUPREMUM A f"
    2.50    by (simp add: SUP_def)
    2.51  
    2.52  lemma SUP_image [simp]:
    2.53 -  "SUPR (f ` A) g = SUPR A (g \<circ> f)"
    2.54 +  "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
    2.55    by (simp only: SUP_def image_comp)
    2.56  
    2.57  lemma SUP_identity_eq [simp]:
    2.58 -  "SUPR A (\<lambda>x. x) = \<Squnion>A"
    2.59 +  "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
    2.60    by (simp add: SUP_def)
    2.61  
    2.62  lemma SUP_id_eq [simp]:
    2.63 -  "SUPR A id = \<Squnion>A"
    2.64 +  "SUPREMUM A id = \<Squnion>A"
    2.65    by (simp add: id_def)
    2.66  
    2.67  lemma SUP_cong:
    2.68 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
    2.69 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    2.70    by (simp add: SUP_def image_def)
    2.71  
    2.72  end
    2.73  
    2.74  text {*
    2.75 -  Note: must use names @{const INFI} and @{const SUPR} here instead of
    2.76 +  Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of
    2.77    @{text INF} and @{text SUP} to allow the following syntax coexist
    2.78    with the plain constant names.
    2.79  *}
    2.80 @@ -91,17 +91,17 @@
    2.81  
    2.82  translations
    2.83    "INF x y. B"   == "INF x. INF y. B"
    2.84 -  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
    2.85 +  "INF x. B"     == "CONST INFIMUM CONST UNIV (%x. B)"
    2.86    "INF x. B"     == "INF x:CONST UNIV. B"
    2.87 -  "INF x:A. B"   == "CONST INFI A (%x. B)"
    2.88 +  "INF x:A. B"   == "CONST INFIMUM A (%x. B)"
    2.89    "SUP x y. B"   == "SUP x. SUP y. B"
    2.90 -  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
    2.91 +  "SUP x. B"     == "CONST SUPREMUM CONST UNIV (%x. B)"
    2.92    "SUP x. B"     == "SUP x:CONST UNIV. B"
    2.93 -  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    2.94 +  "SUP x:A. B"   == "CONST SUPREMUM A (%x. B)"
    2.95  
    2.96  print_translation {*
    2.97 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    2.98 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    2.99 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
   2.100 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
   2.101  *} -- {* to avoid eta-contraction of body *}
   2.102  
   2.103  subsection {* Abstract complete lattices *}
   2.104 @@ -139,11 +139,11 @@
   2.105  begin
   2.106  
   2.107  lemma INF_foundation_dual:
   2.108 -  "Sup.SUPR Inf = INFI"
   2.109 +  "Sup.SUPREMUM Inf = INFIMUM"
   2.110    by (simp add: fun_eq_iff Sup.SUP_def)
   2.111  
   2.112  lemma SUP_foundation_dual:
   2.113 -  "Inf.INFI Sup = SUPR"
   2.114 +  "Inf.INFIMUM Sup = SUPREMUM"
   2.115    by (simp add: fun_eq_iff Inf.INF_def)
   2.116  
   2.117  lemma Sup_eqI:
   2.118 @@ -201,13 +201,13 @@
   2.119  lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   2.120    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   2.121  
   2.122 -lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   2.123 +lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
   2.124    unfolding INF_def Inf_insert by simp
   2.125  
   2.126  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   2.127    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   2.128  
   2.129 -lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   2.130 +lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
   2.131    unfolding SUP_def Sup_insert by simp
   2.132  
   2.133  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   2.134 @@ -444,23 +444,23 @@
   2.135  lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   2.136    by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
   2.137  
   2.138 -lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
   2.139 +lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
   2.140    using Inf_le_Sup [of "f ` A"] by simp
   2.141  
   2.142  lemma SUP_eq_const:
   2.143 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
   2.144 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
   2.145    by (auto intro: SUP_eqI)
   2.146  
   2.147  lemma INF_eq_const:
   2.148 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFI I f = x"
   2.149 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
   2.150    by (auto intro: INF_eqI)
   2.151  
   2.152  lemma SUP_eq_iff:
   2.153 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPR I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   2.154 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   2.155    using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
   2.156  
   2.157  lemma INF_eq_iff:
   2.158 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFI I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   2.159 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   2.160    using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
   2.161  
   2.162  end
   2.163 @@ -645,7 +645,7 @@
   2.164  qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
   2.165  
   2.166  lemma INF_le_iff:
   2.167 -  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   2.168 +  "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   2.169    using Inf_le_iff [of "f ` A"] by simp
   2.170  
   2.171  lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   2.172 @@ -656,7 +656,7 @@
   2.173      unfolding less_Sup_iff .
   2.174  qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
   2.175  
   2.176 -lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   2.177 +lemma le_SUP_iff: "x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   2.178    using le_Sup_iff [of _ "f ` A"] by simp
   2.179  
   2.180  subclass complete_distrib_lattice
   2.181 @@ -696,11 +696,11 @@
   2.182    by auto
   2.183  
   2.184  lemma INF_bool_eq [simp]:
   2.185 -  "INFI = Ball"
   2.186 +  "INFIMUM = Ball"
   2.187    by (simp add: fun_eq_iff INF_def)
   2.188  
   2.189  lemma SUP_bool_eq [simp]:
   2.190 -  "SUPR = Bex"
   2.191 +  "SUPREMUM = Bex"
   2.192    by (simp add: fun_eq_iff SUP_def)
   2.193  
   2.194  instance bool :: complete_boolean_algebra proof
   2.195 @@ -887,7 +887,7 @@
   2.196  subsubsection {* Intersections of families *}
   2.197  
   2.198  abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.199 -  "INTER \<equiv> INFI"
   2.200 +  "INTER \<equiv> INFIMUM"
   2.201  
   2.202  text {*
   2.203    Note: must use name @{const INTER} here instead of @{text INT}
   2.204 @@ -1067,7 +1067,7 @@
   2.205  subsubsection {* Unions of families *}
   2.206  
   2.207  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.208 -  "UNION \<equiv> SUPR"
   2.209 +  "UNION \<equiv> SUPREMUM"
   2.210  
   2.211  text {*
   2.212    Note: must use name @{const UNION} here instead of @{text UN}
     3.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 19 17:06:02 2014 +0000
     3.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 19 18:47:22 2014 +0100
     3.3 @@ -274,22 +274,22 @@
     3.4  lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
     3.5    by (auto intro!: cInf_eq_minimum)
     3.6  
     3.7 -lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
     3.8 +lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFIMUM A f \<le> f x"
     3.9    using cInf_lower [of _ "f ` A"] by simp
    3.10  
    3.11 -lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
    3.12 +lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFIMUM A f"
    3.13    using cInf_greatest [of "f ` A"] by auto
    3.14  
    3.15 -lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
    3.16 +lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPREMUM A f"
    3.17    using cSup_upper [of _ "f ` A"] by simp
    3.18  
    3.19 -lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
    3.20 +lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPREMUM A f \<le> M"
    3.21    using cSup_least [of "f ` A"] by auto
    3.22  
    3.23 -lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
    3.24 +lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
    3.25    by (auto intro: cINF_lower assms order_trans)
    3.26  
    3.27 -lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f"
    3.28 +lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
    3.29    by (auto intro: cSUP_upper assms order_trans)
    3.30  
    3.31  lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
    3.32 @@ -298,10 +298,10 @@
    3.33  lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
    3.34    by (intro antisym cINF_greatest) (auto intro: cINF_lower)
    3.35  
    3.36 -lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
    3.37 +lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
    3.38    by (metis cINF_greatest cINF_lower assms order_trans)
    3.39  
    3.40 -lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
    3.41 +lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
    3.42    by (metis cSUP_least cSUP_upper assms order_trans)
    3.43  
    3.44  lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
    3.45 @@ -310,22 +310,22 @@
    3.46  lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
    3.47    by (metis cSUP_upper le_less_trans)
    3.48  
    3.49 -lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
    3.50 +lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)"
    3.51    by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
    3.52  
    3.53 -lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
    3.54 +lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)"
    3.55    by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
    3.56  
    3.57 -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"
    3.58 +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> INFIMUM A f \<le> INFIMUM B g"
    3.59    using cInf_mono [of "g ` B" "f ` A"] by auto
    3.60  
    3.61 -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"
    3.62 +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> SUPREMUM A f \<le> SUPREMUM B g"
    3.63    using cSup_mono [of "f ` A" "g ` B"] by auto
    3.64  
    3.65 -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"
    3.66 +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> INFIMUM B g \<le> INFIMUM A f"
    3.67    by (rule cINF_mono) auto
    3.68  
    3.69 -lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPR A f \<le> SUPR B g"
    3.70 +lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
    3.71    by (rule cSUP_mono) auto
    3.72  
    3.73  lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
    3.74 @@ -337,20 +337,20 @@
    3.75  lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
    3.76    by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
    3.77  
    3.78 -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)"
    3.79 +lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFIMUM (A \<union> B) f = inf (INFIMUM A f) (INFIMUM B f)"
    3.80    using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    3.81  
    3.82  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)"
    3.83    by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
    3.84  
    3.85 -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)"
    3.86 +lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPREMUM (A \<union> B) f = sup (SUPREMUM A f) (SUPREMUM B f)"
    3.87    using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    3.88  
    3.89 -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))"
    3.90 +lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFIMUM A f) (INFIMUM A g) = (INF a:A. inf (f a) (g a))"
    3.91    by (intro antisym le_infI cINF_greatest cINF_lower2)
    3.92       (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)
    3.93  
    3.94 -lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPR A f) (SUPR A g) = (SUP a:A. sup (f a) (g a))"
    3.95 +lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPREMUM A f) (SUPREMUM A g) = (SUP a:A. sup (f a) (g a))"
    3.96    by (intro antisym le_supI cSUP_least cSUP_upper2)
    3.97       (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
    3.98  
     4.1 --- a/src/HOL/Finite_Set.thy	Wed Mar 19 17:06:02 2014 +0000
     4.2 +++ b/src/HOL/Finite_Set.thy	Wed Mar 19 18:47:22 2014 +0100
     4.3 @@ -1035,7 +1035,7 @@
     4.4  
     4.5  lemma inf_INF_fold_inf:
     4.6    assumes "finite A"
     4.7 -  shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
     4.8 +  shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
     4.9  proof (rule sym)
    4.10    interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
    4.11    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
    4.12 @@ -1046,7 +1046,7 @@
    4.13  
    4.14  lemma sup_SUP_fold_sup:
    4.15    assumes "finite A"
    4.16 -  shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
    4.17 +  shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
    4.18  proof (rule sym)
    4.19    interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
    4.20    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    4.21 @@ -1057,12 +1057,12 @@
    4.22  
    4.23  lemma INF_fold_inf:
    4.24    assumes "finite A"
    4.25 -  shows "INFI A f = fold (inf \<circ> f) top A"
    4.26 +  shows "INFIMUM A f = fold (inf \<circ> f) top A"
    4.27    using assms inf_INF_fold_inf [of A top] by simp
    4.28  
    4.29  lemma SUP_fold_sup:
    4.30    assumes "finite A"
    4.31 -  shows "SUPR A f = fold (sup \<circ> f) bot A"
    4.32 +  shows "SUPREMUM A f = fold (sup \<circ> f) bot A"
    4.33    using assms sup_SUP_fold_sup [of A bot] by simp
    4.34  
    4.35  end
     5.1 --- a/src/HOL/GCD.thy	Wed Mar 19 17:06:02 2014 +0000
     5.2 +++ b/src/HOL/GCD.thy	Wed Mar 19 18:47:22 2014 +0100
     5.3 @@ -1558,8 +1558,8 @@
     5.4  interpretation gcd_lcm_complete_lattice_nat:
     5.5    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
     5.6  where
     5.7 -  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
     5.8 -  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
     5.9 +  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    5.10 +  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    5.11  proof -
    5.12    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    5.13    proof
    5.14 @@ -1577,8 +1577,8 @@
    5.15    qed
    5.16    then interpret gcd_lcm_complete_lattice_nat:
    5.17      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
    5.18 -  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
    5.19 -  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
    5.20 +  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
    5.21 +  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
    5.22  qed
    5.23  
    5.24  declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Mar 19 17:06:02 2014 +0000
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 19 18:47:22 2014 +0100
     6.3 @@ -1411,15 +1411,15 @@
     6.4  
     6.5  lemma ereal_SUP_not_infty:
     6.6    fixes f :: "_ \<Rightarrow> ereal"
     6.7 -  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>"
     6.8 +  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>SUPREMUM A f\<bar> \<noteq> \<infinity>"
     6.9    using SUP_upper2[of _ A l f] SUP_least[of A f u]
    6.10 -  by (cases "SUPR A f") auto
    6.11 +  by (cases "SUPREMUM A f") auto
    6.12  
    6.13  lemma ereal_INF_not_infty:
    6.14    fixes f :: "_ \<Rightarrow> ereal"
    6.15 -  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>INFI A f\<bar> \<noteq> \<infinity>"
    6.16 +  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>INFIMUM A f\<bar> \<noteq> \<infinity>"
    6.17    using INF_lower2[of _ A f u] INF_greatest[of A l f]
    6.18 -  by (cases "INFI A f") auto
    6.19 +  by (cases "INFIMUM A f") auto
    6.20  
    6.21  lemma ereal_SUP_uminus:
    6.22    fixes f :: "'a \<Rightarrow> ereal"
    6.23 @@ -1528,12 +1528,12 @@
    6.24    fixes f :: "'i \<Rightarrow> ereal"
    6.25    assumes "\<And>i. f i + y \<le> z"
    6.26      and "y \<noteq> -\<infinity>"
    6.27 -  shows "SUPR UNIV f + y \<le> z"
    6.28 +  shows "SUPREMUM UNIV f + y \<le> z"
    6.29  proof (cases y)
    6.30    case (real r)
    6.31    then have "\<And>i. f i \<le> z - y"
    6.32      using assms by (simp add: ereal_le_minus_iff)
    6.33 -  then have "SUPR UNIV f \<le> z - y"
    6.34 +  then have "SUPREMUM UNIV f \<le> z - y"
    6.35      by (rule SUP_least)
    6.36    then show ?thesis
    6.37      using real by (simp add: ereal_le_minus_iff)
    6.38 @@ -1544,11 +1544,11 @@
    6.39    assumes "incseq f"
    6.40      and "incseq g"
    6.41      and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
    6.42 -  shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
    6.43 +  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
    6.44  proof (rule SUP_eqI)
    6.45    fix y
    6.46    assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
    6.47 -  have f: "SUPR UNIV f \<noteq> -\<infinity>"
    6.48 +  have f: "SUPREMUM UNIV f \<noteq> -\<infinity>"
    6.49      using pos
    6.50      unfolding SUP_def Sup_eq_MInfty
    6.51      by (auto dest: image_eqD)
    6.52 @@ -1565,13 +1565,13 @@
    6.53        also have "\<dots> \<le> y" using * by auto
    6.54        finally have "f i + g j \<le> y" .
    6.55      }
    6.56 -    then have "SUPR UNIV f + g j \<le> y"
    6.57 +    then have "SUPREMUM UNIV f + g j \<le> y"
    6.58        using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
    6.59 -    then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps)
    6.60 +    then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
    6.61    }
    6.62 -  then have "SUPR UNIV g + SUPR UNIV f \<le> y"
    6.63 +  then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
    6.64      using f by (rule SUP_ereal_le_addI)
    6.65 -  then show "SUPR UNIV f + SUPR UNIV g \<le> y"
    6.66 +  then show "SUPREMUM UNIV f + SUPREMUM UNIV g \<le> y"
    6.67      by (simp add: ac_simps)
    6.68  qed (auto intro!: add_mono SUP_upper)
    6.69  
    6.70 @@ -1579,7 +1579,7 @@
    6.71    fixes f g :: "nat \<Rightarrow> ereal"
    6.72    assumes inc: "incseq f" "incseq g"
    6.73      and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
    6.74 -  shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
    6.75 +  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
    6.76  proof (intro SUP_ereal_add inc)
    6.77    fix i
    6.78    show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
    6.79 @@ -1590,7 +1590,7 @@
    6.80    fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
    6.81    assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
    6.82      and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
    6.83 -  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPR UNIV (f n))"
    6.84 +  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPREMUM UNIV (f n))"
    6.85  proof (cases "finite A")
    6.86    case True
    6.87    then show ?thesis using assms
    6.88 @@ -1604,20 +1604,20 @@
    6.89    fixes f :: "nat \<Rightarrow> ereal"
    6.90    assumes "\<And>i. 0 \<le> f i"
    6.91      and "0 \<le> c"
    6.92 -  shows "(SUP i. c * f i) = c * SUPR UNIV f"
    6.93 +  shows "(SUP i. c * f i) = c * SUPREMUM UNIV f"
    6.94  proof (rule SUP_eqI)
    6.95    fix i
    6.96 -  have "f i \<le> SUPR UNIV f"
    6.97 +  have "f i \<le> SUPREMUM UNIV f"
    6.98      by (rule SUP_upper) auto
    6.99 -  then show "c * f i \<le> c * SUPR UNIV f"
   6.100 +  then show "c * f i \<le> c * SUPREMUM UNIV f"
   6.101      using `0 \<le> c` by (rule ereal_mult_left_mono)
   6.102  next
   6.103    fix y
   6.104    assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
   6.105 -  show "c * SUPR UNIV f \<le> y"
   6.106 +  show "c * SUPREMUM UNIV f \<le> y"
   6.107    proof (cases "0 < c \<and> c \<noteq> \<infinity>")
   6.108      case True
   6.109 -    with * have "SUPR UNIV f \<le> y / c"
   6.110 +    with * have "SUPREMUM UNIV f \<le> y / c"
   6.111        by (intro SUP_least) (auto simp: ereal_le_divide_pos)
   6.112      with True show ?thesis
   6.113        by (auto simp: ereal_le_divide_pos)
   6.114 @@ -1630,7 +1630,7 @@
   6.115          case True
   6.116          then have "range f = {0}"
   6.117            by auto
   6.118 -        with True show "c * SUPR UNIV f \<le> y"
   6.119 +        with True show "c * SUPREMUM UNIV f \<le> y"
   6.120            using * by (auto simp: SUP_def max.absorb1)
   6.121        next
   6.122          case False
   6.123 @@ -1677,7 +1677,7 @@
   6.124  
   6.125  lemma Sup_countable_SUP:
   6.126    assumes "A \<noteq> {}"
   6.127 -  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
   6.128 +  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
   6.129  proof (cases "Sup A")
   6.130    case (real r)
   6.131    have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
   6.132 @@ -1691,7 +1691,7 @@
   6.133    qed
   6.134    from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
   6.135      where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
   6.136 -  have "SUPR UNIV f = Sup A"
   6.137 +  have "SUPREMUM UNIV f = Sup A"
   6.138    proof (rule SUP_eqI)
   6.139      fix i
   6.140      show "f i \<le> Sup A"
   6.141 @@ -1752,7 +1752,7 @@
   6.142      qed
   6.143      from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
   6.144        where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
   6.145 -    have "SUPR UNIV f = \<infinity>"
   6.146 +    have "SUPREMUM UNIV f = \<infinity>"
   6.147      proof (rule SUP_PInfty)
   6.148        fix n :: nat
   6.149        show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
   6.150 @@ -1771,7 +1771,7 @@
   6.151  qed
   6.152  
   6.153  lemma SUP_countable_SUP:
   6.154 -  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
   6.155 +  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
   6.156    using Sup_countable_SUP [of "g`A"]
   6.157    by auto
   6.158  
   6.159 @@ -1852,7 +1852,7 @@
   6.160    fixes f :: "nat \<Rightarrow> ereal"
   6.161    assumes "decseq f" "decseq g"
   6.162      and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   6.163 -  shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
   6.164 +  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
   6.165  proof -
   6.166    have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
   6.167      using assms unfolding INF_less_iff by auto
   6.168 @@ -1863,7 +1863,7 @@
   6.169    }
   6.170    then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   6.171      by simp
   6.172 -  also have "\<dots> = INFI UNIV f + INFI UNIV g"
   6.173 +  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
   6.174      unfolding ereal_INF_uminus
   6.175      using assms INF_less
   6.176      by (subst SUP_ereal_add)
     7.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 17:06:02 2014 +0000
     7.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 18:47:22 2014 +0100
     7.3 @@ -367,7 +367,7 @@
     7.4  
     7.5  class kleene_by_complete_lattice = pre_kleene
     7.6    + complete_lattice + power + star +
     7.7 -  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
     7.8 +  assumes star_cont: "a * star b * c = SUPREMUM UNIV (\<lambda>n. a * b ^ n * c)"
     7.9  begin
    7.10  
    7.11  subclass kleene
     8.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 19 17:06:02 2014 +0000
     8.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 19 18:47:22 2014 +0100
     8.3 @@ -43,13 +43,13 @@
     8.4  abbreviation "limsup \<equiv> Limsup sequentially"
     8.5  
     8.6  lemma Liminf_eqI:
     8.7 -  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
     8.8 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
     8.9 +  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>  
    8.10 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    8.11    unfolding Liminf_def by (auto intro!: SUP_eqI)
    8.12  
    8.13  lemma Limsup_eqI:
    8.14 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    8.15 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    8.16 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>  
    8.17 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    8.18    unfolding Limsup_def by (auto intro!: INF_eqI)
    8.19  
    8.20  lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
    8.21 @@ -93,7 +93,7 @@
    8.22  proof (safe intro!: SUP_mono)
    8.23    fix P assume "eventually P F"
    8.24    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    8.25 -  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
    8.26 +  then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
    8.27      by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
    8.28  qed
    8.29  
    8.30 @@ -109,7 +109,7 @@
    8.31  proof (safe intro!: INF_mono)
    8.32    fix P assume "eventually P F"
    8.33    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    8.34 -  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
    8.35 +  then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
    8.36      by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
    8.37  qed
    8.38  
    8.39 @@ -129,13 +129,13 @@
    8.40    then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
    8.41    then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
    8.42      using ntriv by (auto simp add: eventually_False)
    8.43 -  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
    8.44 +  have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
    8.45      by (rule INF_mono) auto
    8.46 -  also have "\<dots> \<le> SUPR (Collect ?C) f"
    8.47 +  also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
    8.48      using not_False by (intro INF_le_SUP) auto
    8.49 -  also have "\<dots> \<le> SUPR (Collect Q) f"
    8.50 +  also have "\<dots> \<le> SUPREMUM (Collect Q) f"
    8.51      by (rule SUP_mono) auto
    8.52 -  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
    8.53 +  finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
    8.54  qed
    8.55  
    8.56  lemma Liminf_bounded:
    8.57 @@ -154,22 +154,22 @@
    8.58    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
    8.59    shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
    8.60  proof -
    8.61 -  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
    8.62 +  { fix y P assume "eventually P F" "y < INFIMUM (Collect P) X"
    8.63      then have "eventually (\<lambda>x. y < X x) F"
    8.64        by (auto elim!: eventually_elim1 dest: less_INF_D) }
    8.65    moreover
    8.66    { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
    8.67 -    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
    8.68 +    have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
    8.69      proof (cases "\<exists>z. y < z \<and> z < C")
    8.70        case True
    8.71        then obtain z where z: "y < z \<and> z < C" ..
    8.72 -      moreover from z have "z \<le> INFI {x. z < X x} X"
    8.73 +      moreover from z have "z \<le> INFIMUM {x. z < X x} X"
    8.74          by (auto intro!: INF_greatest)
    8.75        ultimately show ?thesis
    8.76          using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
    8.77      next
    8.78        case False
    8.79 -      then have "C \<le> INFI {x. y < X x} X"
    8.80 +      then have "C \<le> INFIMUM {x. y < X x} X"
    8.81          by (intro INF_greatest) auto
    8.82        with `y < C` show ?thesis
    8.83          using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
    8.84 @@ -185,17 +185,17 @@
    8.85    shows "Liminf F f = f0"
    8.86  proof (intro Liminf_eqI)
    8.87    fix P assume P: "eventually P F"
    8.88 -  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
    8.89 +  then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
    8.90      by eventually_elim (auto intro!: INF_lower)
    8.91 -  then show "INFI (Collect P) f \<le> f0"
    8.92 +  then show "INFIMUM (Collect P) f \<le> f0"
    8.93      by (rule tendsto_le[OF ntriv lim tendsto_const])
    8.94  next
    8.95 -  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
    8.96 +  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
    8.97    show "f0 \<le> y"
    8.98    proof cases
    8.99      assume "\<exists>z. y < z \<and> z < f0"
   8.100      then obtain z where "y < z \<and> z < f0" ..
   8.101 -    moreover have "z \<le> INFI {x. z < f x} f"
   8.102 +    moreover have "z \<le> INFIMUM {x. z < f x} f"
   8.103        by (rule INF_greatest) simp
   8.104      ultimately show ?thesis
   8.105        using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   8.106 @@ -208,9 +208,9 @@
   8.107          using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   8.108        then have "eventually (\<lambda>x. f0 \<le> f x) F"
   8.109          using discrete by (auto elim!: eventually_elim1)
   8.110 -      then have "INFI {x. f0 \<le> f x} f \<le> y"
   8.111 +      then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
   8.112          by (rule upper)
   8.113 -      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
   8.114 +      moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
   8.115          by (intro INF_greatest) simp
   8.116        ultimately show "f0 \<le> y" by simp
   8.117      qed
   8.118 @@ -224,17 +224,17 @@
   8.119    shows "Limsup F f = f0"
   8.120  proof (intro Limsup_eqI)
   8.121    fix P assume P: "eventually P F"
   8.122 -  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
   8.123 +  then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
   8.124      by eventually_elim (auto intro!: SUP_upper)
   8.125 -  then show "f0 \<le> SUPR (Collect P) f"
   8.126 +  then show "f0 \<le> SUPREMUM (Collect P) f"
   8.127      by (rule tendsto_le[OF ntriv tendsto_const lim])
   8.128  next
   8.129 -  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   8.130 +  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
   8.131    show "y \<le> f0"
   8.132    proof (cases "\<exists>z. f0 < z \<and> z < y")
   8.133      case True
   8.134      then obtain z where "f0 < z \<and> z < y" ..
   8.135 -    moreover have "SUPR {x. f x < z} f \<le> z"
   8.136 +    moreover have "SUPREMUM {x. f x < z} f \<le> z"
   8.137        by (rule SUP_least) simp
   8.138      ultimately show ?thesis
   8.139        using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   8.140 @@ -247,9 +247,9 @@
   8.141          using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   8.142        then have "eventually (\<lambda>x. f x \<le> f0) F"
   8.143          using False by (auto elim!: eventually_elim1 simp: not_less)
   8.144 -      then have "y \<le> SUPR {x. f x \<le> f0} f"
   8.145 +      then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
   8.146          by (rule lower)
   8.147 -      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
   8.148 +      moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
   8.149          by (intro SUP_least) simp
   8.150        ultimately show "y \<le> f0" by simp
   8.151      qed
   8.152 @@ -264,14 +264,14 @@
   8.153  proof (rule order_tendstoI)
   8.154    fix a assume "f0 < a"
   8.155    with assms have "Limsup F f < a" by simp
   8.156 -  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
   8.157 +  then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
   8.158      unfolding Limsup_def INF_less_iff by auto
   8.159    then show "eventually (\<lambda>x. f x < a) F"
   8.160      by (auto elim!: eventually_elim1 dest: SUP_lessD)
   8.161  next
   8.162    fix a assume "a < f0"
   8.163    with assms have "a < Liminf F f" by simp
   8.164 -  then obtain P where "eventually P F" "a < INFI (Collect P) f"
   8.165 +  then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
   8.166      unfolding Liminf_def less_SUP_iff by auto
   8.167    then show "eventually (\<lambda>x. a < f x) F"
   8.168      by (auto elim!: eventually_elim1 dest: less_INF_D)
     9.1 --- a/src/HOL/Library/Product_Order.thy	Wed Mar 19 17:06:02 2014 +0000
     9.2 +++ b/src/HOL/Library/Product_Order.thy	Wed Mar 19 18:47:22 2014 +0100
     9.3 @@ -219,11 +219,11 @@
     9.4  of two complete lattices: *}
     9.5  
     9.6  lemma INF_prod_alt_def:
     9.7 -  "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
     9.8 +  "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
     9.9    unfolding INF_def Inf_prod_def by simp
    9.10  
    9.11  lemma SUP_prod_alt_def:
    9.12 -  "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
    9.13 +  "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
    9.14    unfolding SUP_def Sup_prod_def by simp
    9.15  
    9.16  
    10.1 --- a/src/HOL/Library/RBT_Set.thy	Wed Mar 19 17:06:02 2014 +0000
    10.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Mar 19 18:47:22 2014 +0100
    10.3 @@ -112,7 +112,7 @@
    10.4    "Inf_fin = Inf_fin" ..
    10.5  
    10.6  lemma [code, code del]:
    10.7 -  "INFI = INFI" ..
    10.8 +  "INFIMUM = INFIMUM" ..
    10.9  
   10.10  lemma [code, code del]:
   10.11    "Max = Max" ..
   10.12 @@ -121,7 +121,7 @@
   10.13    "Sup_fin = Sup_fin" ..
   10.14  
   10.15  lemma [code, code del]:
   10.16 -  "SUPR = SUPR" ..
   10.17 +  "SUPREMUM = SUPREMUM" ..
   10.18  
   10.19  lemma [code, code del]:
   10.20    "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
   10.21 @@ -759,7 +759,7 @@
   10.22  
   10.23  lemma INF_Set_fold [code]:
   10.24    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   10.25 -  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
   10.26 +  shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
   10.27  proof -
   10.28    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   10.29      by default (auto simp add: fun_eq_iff ac_simps)
   10.30 @@ -800,7 +800,7 @@
   10.31  
   10.32  lemma SUP_Set_fold [code]:
   10.33    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   10.34 -  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
   10.35 +  shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
   10.36  proof -
   10.37    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   10.38      by default (auto simp add: fun_eq_iff ac_simps)
    11.1 --- a/src/HOL/Lifting_Set.thy	Wed Mar 19 17:06:02 2014 +0000
    11.2 +++ b/src/HOL/Lifting_Set.thy	Wed Mar 19 18:47:22 2014 +0100
    11.3 @@ -150,12 +150,12 @@
    11.4    unfolding rel_fun_def rel_set_def by fast
    11.5  
    11.6  lemma SUP_parametric [transfer_rule]:
    11.7 -  "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
    11.8 +  "(rel_set R ===> (R ===> op =) ===> op =) SUPREMUM (SUPREMUM :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
    11.9  proof(rule rel_funI)+
   11.10    fix A B f and g :: "'b \<Rightarrow> 'c"
   11.11    assume AB: "rel_set R A B"
   11.12      and fg: "(R ===> op =) f g"
   11.13 -  show "SUPR A f = SUPR B g"
   11.14 +  show "SUPREMUM A f = SUPREMUM B g"
   11.15      by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
   11.16  qed
   11.17  
    12.1 --- a/src/HOL/List.thy	Wed Mar 19 17:06:02 2014 +0000
    12.2 +++ b/src/HOL/List.thy	Wed Mar 19 18:47:22 2014 +0100
    12.3 @@ -2876,13 +2876,13 @@
    12.4  declare Sup_set_fold [where 'a = "'a set", code]
    12.5  
    12.6  lemma (in complete_lattice) INF_set_fold:
    12.7 -  "INFI (set xs) f = fold (inf \<circ> f) xs top"
    12.8 +  "INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
    12.9    using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
   12.10  
   12.11  declare INF_set_fold [code]
   12.12  
   12.13  lemma (in complete_lattice) SUP_set_fold:
   12.14 -  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   12.15 +  "SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
   12.16    using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
   12.17  
   12.18  declare SUP_set_fold [code]
    13.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Mar 19 17:06:02 2014 +0000
    13.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Mar 19 18:47:22 2014 +0100
    13.3 @@ -1166,13 +1166,13 @@
    13.4    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    13.5    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
    13.6      by (auto simp: zero_less_dist_iff dist_commute)
    13.7 -  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
    13.8 +  then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f"
    13.9      by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   13.10  next
   13.11    fix d :: real
   13.12    assume "0 < d"
   13.13    then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   13.14 -    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   13.15 +    INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f"
   13.16      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   13.17         (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   13.18  qed
   13.19 @@ -1186,13 +1186,13 @@
   13.20    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   13.21    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   13.22      by (auto simp: zero_less_dist_iff dist_commute)
   13.23 -  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   13.24 +  then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f"
   13.25      by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   13.26  next
   13.27    fix d :: real
   13.28    assume "0 < d"
   13.29    then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   13.30 -    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   13.31 +    SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f"
   13.32      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   13.33         (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   13.34  qed
   13.35 @@ -1285,11 +1285,11 @@
   13.36    fix P
   13.37    assume P: "eventually P net"
   13.38    fix S
   13.39 -  assume S: "mono_set S" "INFI (Collect P) f \<in> S"
   13.40 +  assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S"
   13.41    {
   13.42      fix x
   13.43      assume "P x"
   13.44 -    then have "INFI (Collect P) f \<le> f x"
   13.45 +    then have "INFIMUM (Collect P) f \<le> f x"
   13.46        by (intro complete_lattice_class.INF_lower) simp
   13.47      with S have "f x \<in> S"
   13.48        by (simp add: mono_set)
   13.49 @@ -1299,16 +1299,16 @@
   13.50  next
   13.51    fix y l
   13.52    assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   13.53 -  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
   13.54 +  assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y"
   13.55    show "l \<le> y"
   13.56    proof (rule dense_le)
   13.57      fix B
   13.58      assume "B < l"
   13.59      then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
   13.60        by (intro S[rule_format]) auto
   13.61 -    then have "INFI {x. B < f x} f \<le> y"
   13.62 +    then have "INFIMUM {x. B < f x} f \<le> y"
   13.63        using P by auto
   13.64 -    moreover have "B \<le> INFI {x. B < f x} f"
   13.65 +    moreover have "B \<le> INFIMUM {x. B < f x} f"
   13.66        by (intro INF_greatest) auto
   13.67      ultimately show "B \<le> y"
   13.68        by simp
   13.69 @@ -1324,13 +1324,13 @@
   13.70    fix P
   13.71    assume P: "eventually P net"
   13.72    fix S
   13.73 -  assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
   13.74 +  assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S"
   13.75    {
   13.76      fix x
   13.77      assume "P x"
   13.78 -    then have "f x \<le> SUPR (Collect P) f"
   13.79 +    then have "f x \<le> SUPREMUM (Collect P) f"
   13.80        by (intro complete_lattice_class.SUP_upper) simp
   13.81 -    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   13.82 +    with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
   13.83      have "f x \<in> S"
   13.84        by (simp add: inj_image_mem_iff) }
   13.85    with P show "eventually (\<lambda>x. f x \<in> S) net"
   13.86 @@ -1338,16 +1338,16 @@
   13.87  next
   13.88    fix y l
   13.89    assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   13.90 -  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   13.91 +  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f"
   13.92    show "y \<le> l"
   13.93    proof (rule dense_ge)
   13.94      fix B
   13.95      assume "l < B"
   13.96      then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   13.97        by (intro S[rule_format]) auto
   13.98 -    then have "y \<le> SUPR {x. f x < B} f"
   13.99 +    then have "y \<le> SUPREMUM {x. f x < B} f"
  13.100        using P by auto
  13.101 -    moreover have "SUPR {x. f x < B} f \<le> B"
  13.102 +    moreover have "SUPREMUM {x. f x < B} f \<le> B"
  13.103        by (intro SUP_least) auto
  13.104      ultimately show "y \<le> B"
  13.105        by simp
    14.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 19 17:06:02 2014 +0000
    14.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 19 18:47:22 2014 +0100
    14.3 @@ -11842,7 +11842,7 @@
    14.4          using goal2 by auto
    14.5      qed
    14.6      then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
    14.7 -      "SUPR {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
    14.8 +      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
    14.9        by (auto simp add: image_iff not_le)
   14.10      from this(1) obtain d where "d division_of \<Union>d"
   14.11        and "K = (\<Sum>k\<in>d. norm (integral k f))"
    15.1 --- a/src/HOL/Predicate.thy	Wed Mar 19 17:06:02 2014 +0000
    15.2 +++ b/src/HOL/Predicate.thy	Wed Mar 19 18:47:22 2014 +0100
    15.3 @@ -65,17 +65,17 @@
    15.4    by (simp add: sup_pred_def)
    15.5  
    15.6  definition
    15.7 -  "\<Sqinter>A = Pred (INFI A eval)"
    15.8 +  "\<Sqinter>A = Pred (INFIMUM A eval)"
    15.9  
   15.10  lemma eval_Inf [simp]:
   15.11 -  "eval (\<Sqinter>A) = INFI A eval"
   15.12 +  "eval (\<Sqinter>A) = INFIMUM A eval"
   15.13    by (simp add: Inf_pred_def)
   15.14  
   15.15  definition
   15.16 -  "\<Squnion>A = Pred (SUPR A eval)"
   15.17 +  "\<Squnion>A = Pred (SUPREMUM A eval)"
   15.18  
   15.19  lemma eval_Sup [simp]:
   15.20 -  "eval (\<Squnion>A) = SUPR A eval"
   15.21 +  "eval (\<Squnion>A) = SUPREMUM A eval"
   15.22    by (simp add: Sup_pred_def)
   15.23  
   15.24  instance proof
   15.25 @@ -84,11 +84,11 @@
   15.26  end
   15.27  
   15.28  lemma eval_INF [simp]:
   15.29 -  "eval (INFI A f) = INFI A (eval \<circ> f)"
   15.30 +  "eval (INFIMUM A f) = INFIMUM A (eval \<circ> f)"
   15.31    using eval_Inf [of "f ` A"] by simp
   15.32  
   15.33  lemma eval_SUP [simp]:
   15.34 -  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   15.35 +  "eval (SUPREMUM A f) = SUPREMUM A (eval \<circ> f)"
   15.36    using eval_Sup [of "f ` A"] by simp
   15.37  
   15.38  instantiation pred :: (type) complete_boolean_algebra
   15.39 @@ -121,10 +121,10 @@
   15.40    by (simp add: single_def)
   15.41  
   15.42  definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   15.43 -  "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
   15.44 +  "P \<guillemotright>= f = (SUPREMUM {x. eval P x} f)"
   15.45  
   15.46  lemma eval_bind [simp]:
   15.47 -  "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   15.48 +  "eval (P \<guillemotright>= f) = eval (SUPREMUM {x. eval P x} f)"
   15.49    by (simp add: bind_def)
   15.50  
   15.51  lemma bind_bind:
    16.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 17:06:02 2014 +0000
    16.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 18:47:22 2014 +0100
    16.3 @@ -781,7 +781,7 @@
    16.4  
    16.5  lemma positive_integral_def_finite:
    16.6    "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
    16.7 -    (is "_ = SUPR ?A ?f")
    16.8 +    (is "_ = SUPREMUM ?A ?f")
    16.9    unfolding positive_integral_def
   16.10  proof (safe intro!: antisym SUP_least)
   16.11    fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
   16.12 @@ -793,7 +793,7 @@
   16.13      apply (safe intro!: simple_function_max simple_function_If)
   16.14      apply (force simp: max_def le_fun_def split: split_if_asm)+
   16.15      done
   16.16 -  show "integral\<^sup>S M g \<le> SUPR ?A ?f"
   16.17 +  show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
   16.18    proof cases
   16.19      have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto
   16.20      assume "(emeasure M) ?G = 0"
   16.21 @@ -804,7 +804,7 @@
   16.22           (auto simp: max_def intro!: simple_function_If)
   16.23    next
   16.24      assume \<mu>_G: "(emeasure M) ?G \<noteq> 0"
   16.25 -    have "SUPR ?A (integral\<^sup>S M) = \<infinity>"
   16.26 +    have "SUPREMUM ?A (integral\<^sup>S M) = \<infinity>"
   16.27      proof (intro SUP_PInfty)
   16.28        fix n :: nat
   16.29        let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)"
   16.30 @@ -1029,7 +1029,7 @@
   16.31          using N(1) by auto }
   16.32    qed
   16.33    also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
   16.34 -    using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext)
   16.35 +    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
   16.36    finally show ?thesis .
   16.37  qed
   16.38  
   16.39 @@ -1045,7 +1045,7 @@
   16.40    shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   16.41    using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
   16.42      f(3)[THEN borel_measurable_simple_function] f(2)]
   16.43 -  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext)
   16.44 +  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
   16.45  
   16.46  lemma positive_integral_max_0:
   16.47    "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
   16.48 @@ -1069,7 +1069,7 @@
   16.49    and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)"
   16.50    and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
   16.51    shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
   16.52 -    (is "SUPR _ ?F = SUPR _ ?G")
   16.53 +    (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
   16.54  proof -
   16.55    have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   16.56      using f by (rule positive_integral_monotone_convergence_simple)
   16.57 @@ -1128,7 +1128,7 @@
   16.58        by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg)
   16.59    qed
   16.60    also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
   16.61 -    using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext)
   16.62 +    using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext)
   16.63    finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
   16.64      unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
   16.65      unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
    17.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 19 17:06:02 2014 +0000
    17.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 19 18:47:22 2014 +0100
    17.3 @@ -169,7 +169,7 @@
    17.4          by (auto intro!: SUP_upper2 integral_nonneg)
    17.5      next
    17.6        show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))"
    17.7 -      proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
    17.8 +      proof (intro arg_cong[where f="SUPREMUM UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
    17.9          fix n
   17.10          have "\<And>m. (UNION {..<m} A) \<in> sets lebesgue" using rA by auto
   17.11          from lebesgueD[OF this]
    18.1 --- a/src/HOL/Product_Type.thy	Wed Mar 19 17:06:02 2014 +0000
    18.2 +++ b/src/HOL/Product_Type.thy	Wed Mar 19 18:47:22 2014 +0100
    18.3 @@ -342,8 +342,8 @@
    18.4    in
    18.5      [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
    18.6       Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
    18.7 -     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    18.8 -     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    18.9 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
   18.10 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
   18.11      |> map (fn (Q, tr) => (Q, contract Q tr))
   18.12    end
   18.13  *}
    19.1 --- a/src/HOL/Relation.thy	Wed Mar 19 17:06:02 2014 +0000
    19.2 +++ b/src/HOL/Relation.thy	Wed Mar 19 18:47:22 2014 +0100
    19.3 @@ -281,7 +281,7 @@
    19.4    by (fast intro: symI elim: symE)
    19.5  
    19.6  lemma symp_INF:
    19.7 -  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
    19.8 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
    19.9    by (fact sym_INTER [to_pred])
   19.10  
   19.11  lemma sym_UNION:
   19.12 @@ -289,7 +289,7 @@
   19.13    by (fast intro: symI elim: symE)
   19.14  
   19.15  lemma symp_SUP:
   19.16 -  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
   19.17 +  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
   19.18    by (fact sym_UNION [to_pred])
   19.19  
   19.20  
    20.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Mar 19 17:06:02 2014 +0000
    20.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Mar 19 18:47:22 2014 +0100
    20.3 @@ -393,7 +393,7 @@
    20.4  
    20.5  fun mk_UNION X f =
    20.6    let val (T, U) = dest_funT (fastype_of f);
    20.7 -  in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end;
    20.8 +  in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end;
    20.9  
   20.10  fun mk_Union T =
   20.11    Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
    21.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 19 17:06:02 2014 +0000
    21.2 +++ b/src/HOL/Wellfounded.thy	Wed Mar 19 18:47:22 2014 +0100
    21.3 @@ -297,7 +297,7 @@
    21.4  done
    21.5  
    21.6  lemma wfP_SUP:
    21.7 -  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
    21.8 +  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)"
    21.9    apply (rule wf_UN[to_pred])
   21.10    apply simp_all
   21.11    done