# HG changeset patch # User haftmann # Date 1395251242 -3600 # Node ID 1c3f1f2431f909084b6569c92e79b82ecd61f9cd # Parent dc429a5b13c497e7f9d63c303fe5068c584b0af3 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION diff -r dc429a5b13c4 -r 1c3f1f2431f9 NEWS --- a/NEWS Wed Mar 19 17:06:02 2014 +0000 +++ b/NEWS Wed Mar 19 18:47:22 2014 +0100 @@ -98,6 +98,9 @@ *** HOL *** +* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. +INCOMPATIBILITY. + * Consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly. INCOMPATIBILITY. diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Complete_Lattices.thy Wed Mar 19 18:47:22 2014 +0100 @@ -17,27 +17,27 @@ fixes Inf :: "'a set \ 'a" ("\_" [900] 900) begin -definition INFI :: "'b set \ ('b \ 'a) \ 'a" where - INF_def: "INFI A f = \(f ` A)" +definition INFIMUM :: "'b set \ ('b \ 'a) \ 'a" where + INF_def: "INFIMUM A f = \(f ` A)" lemma Inf_image_eq [simp]: - "\(f ` A) = INFI A f" + "\(f ` A) = INFIMUM A f" by (simp add: INF_def) lemma INF_image [simp]: - "INFI (f ` A) g = INFI A (g \ f)" + "INFIMUM (f ` A) g = INFIMUM A (g \ f)" by (simp only: INF_def image_comp) lemma INF_identity_eq [simp]: - "INFI A (\x. x) = \A" + "INFIMUM A (\x. x) = \A" by (simp add: INF_def) lemma INF_id_eq [simp]: - "INFI A id = \A" + "INFIMUM A id = \A" by (simp add: id_def) lemma INF_cong: - "A = B \ (\x. x \ B \ C x = D x) \ INFI A C = INFI B D" + "A = B \ (\x. x \ B \ C x = D x) \ INFIMUM A C = INFIMUM B D" by (simp add: INF_def image_def) end @@ -46,33 +46,33 @@ fixes Sup :: "'a set \ 'a" ("\_" [900] 900) begin -definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where - SUP_def: "SUPR A f = \(f ` A)" +definition SUPREMUM :: "'b set \ ('b \ 'a) \ 'a" where + SUP_def: "SUPREMUM A f = \(f ` A)" lemma Sup_image_eq [simp]: - "\(f ` A) = SUPR A f" + "\(f ` A) = SUPREMUM A f" by (simp add: SUP_def) lemma SUP_image [simp]: - "SUPR (f ` A) g = SUPR A (g \ f)" + "SUPREMUM (f ` A) g = SUPREMUM A (g \ f)" by (simp only: SUP_def image_comp) lemma SUP_identity_eq [simp]: - "SUPR A (\x. x) = \A" + "SUPREMUM A (\x. x) = \A" by (simp add: SUP_def) lemma SUP_id_eq [simp]: - "SUPR A id = \A" + "SUPREMUM A id = \A" by (simp add: id_def) lemma SUP_cong: - "A = B \ (\x. x \ B \ C x = D x) \ SUPR A C = SUPR B D" + "A = B \ (\x. x \ B \ C x = D x) \ SUPREMUM A C = SUPREMUM B D" by (simp add: SUP_def image_def) end text {* - Note: must use names @{const INFI} and @{const SUPR} here instead of + Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of @{text INF} and @{text SUP} to allow the following syntax coexist with the plain constant names. *} @@ -91,17 +91,17 @@ translations "INF x y. B" == "INF x. INF y. B" - "INF x. B" == "CONST INFI CONST UNIV (%x. B)" + "INF x. B" == "CONST INFIMUM CONST UNIV (%x. B)" "INF x. B" == "INF x:CONST UNIV. B" - "INF x:A. B" == "CONST INFI A (%x. B)" + "INF x:A. B" == "CONST INFIMUM A (%x. B)" "SUP x y. B" == "SUP x. SUP y. B" - "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)" + "SUP x. B" == "CONST SUPREMUM CONST UNIV (%x. B)" "SUP x. B" == "SUP x:CONST UNIV. B" - "SUP x:A. B" == "CONST SUPR A (%x. B)" + "SUP x:A. B" == "CONST SUPREMUM A (%x. B)" print_translation {* - [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, - Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}] *} -- {* to avoid eta-contraction of body *} subsection {* Abstract complete lattices *} @@ -139,11 +139,11 @@ begin lemma INF_foundation_dual: - "Sup.SUPR Inf = INFI" + "Sup.SUPREMUM Inf = INFIMUM" by (simp add: fun_eq_iff Sup.SUP_def) lemma SUP_foundation_dual: - "Inf.INFI Sup = SUPR" + "Inf.INFIMUM Sup = SUPREMUM" by (simp add: fun_eq_iff Inf.INF_def) lemma Sup_eqI: @@ -201,13 +201,13 @@ lemma Inf_insert [simp]: "\insert a A = a \ \A" by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) -lemma INF_insert [simp]: "(\x\insert a A. f x) = f a \ INFI A f" +lemma INF_insert [simp]: "(\x\insert a A. f x) = f a \ INFIMUM A f" unfolding INF_def Inf_insert by simp lemma Sup_insert [simp]: "\insert a A = a \ \A" by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) -lemma SUP_insert [simp]: "(\x\insert a A. f x) = f a \ SUPR A f" +lemma SUP_insert [simp]: "(\x\insert a A. f x) = f a \ SUPREMUM A f" unfolding SUP_def Sup_insert by simp lemma INF_empty [simp]: "(\x\{}. f x) = \" @@ -444,23 +444,23 @@ lemma Inf_le_Sup: "A \ {} \ Inf A \ Sup A" by (blast intro: Sup_upper2 Inf_lower ex_in_conv) -lemma INF_le_SUP: "A \ {} \ INFI A f \ SUPR A f" +lemma INF_le_SUP: "A \ {} \ INFIMUM A f \ SUPREMUM A f" using Inf_le_Sup [of "f ` A"] by simp lemma SUP_eq_const: - "I \ {} \ (\i. i \ I \ f i = x) \ SUPR I f = x" + "I \ {} \ (\i. i \ I \ f i = x) \ SUPREMUM I f = x" by (auto intro: SUP_eqI) lemma INF_eq_const: - "I \ {} \ (\i. i \ I \ f i = x) \ INFI I f = x" + "I \ {} \ (\i. i \ I \ f i = x) \ INFIMUM I f = x" by (auto intro: INF_eqI) lemma SUP_eq_iff: - "I \ {} \ (\i. i \ I \ c \ f i) \ (SUPR I f = c) \ (\i\I. f i = c)" + "I \ {} \ (\i. i \ I \ c \ f i) \ (SUPREMUM I f = c) \ (\i\I. f i = c)" using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym) lemma INF_eq_iff: - "I \ {} \ (\i. i \ I \ f i \ c) \ (INFI I f = c) \ (\i\I. f i = c)" + "I \ {} \ (\i. i \ I \ f i \ c) \ (INFIMUM I f = c) \ (\i\I. f i = c)" using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym) end @@ -645,7 +645,7 @@ qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Inf_lower) lemma INF_le_iff: - "INFI A f \ x \ (\y>x. \i\A. y > f i)" + "INFIMUM A f \ x \ (\y>x. \i\A. y > f i)" using Inf_le_iff [of "f ` A"] by simp lemma le_Sup_iff: "x \ \A \ (\ya\A. y < a)" @@ -656,7 +656,7 @@ unfolding less_Sup_iff . qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Sup_upper) -lemma le_SUP_iff: "x \ SUPR A f \ (\yi\A. y < f i)" +lemma le_SUP_iff: "x \ SUPREMUM A f \ (\yi\A. y < f i)" using le_Sup_iff [of _ "f ` A"] by simp subclass complete_distrib_lattice @@ -696,11 +696,11 @@ by auto lemma INF_bool_eq [simp]: - "INFI = Ball" + "INFIMUM = Ball" by (simp add: fun_eq_iff INF_def) lemma SUP_bool_eq [simp]: - "SUPR = Bex" + "SUPREMUM = Bex" by (simp add: fun_eq_iff SUP_def) instance bool :: complete_boolean_algebra proof @@ -887,7 +887,7 @@ subsubsection {* Intersections of families *} abbreviation INTER :: "'a set \ ('a \ 'b set) \ 'b set" where - "INTER \ INFI" + "INTER \ INFIMUM" text {* Note: must use name @{const INTER} here instead of @{text INT} @@ -1067,7 +1067,7 @@ subsubsection {* Unions of families *} abbreviation UNION :: "'a set \ ('a \ 'b set) \ 'b set" where - "UNION \ SUPR" + "UNION \ SUPREMUM" text {* Note: must use name @{const UNION} here instead of @{text UN} diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Mar 19 18:47:22 2014 +0100 @@ -274,22 +274,22 @@ lemma cInf_atLeastAtMost[simp]: "y \ x \ Inf {y..x} = y" by (auto intro!: cInf_eq_minimum) -lemma cINF_lower: "bdd_below (f ` A) \ x \ A \ INFI A f \ f x" +lemma cINF_lower: "bdd_below (f ` A) \ x \ A \ INFIMUM A f \ f x" using cInf_lower [of _ "f ` A"] by simp -lemma cINF_greatest: "A \ {} \ (\x. x \ A \ m \ f x) \ m \ INFI A f" +lemma cINF_greatest: "A \ {} \ (\x. x \ A \ m \ f x) \ m \ INFIMUM A f" using cInf_greatest [of "f ` A"] by auto -lemma cSUP_upper: "x \ A \ bdd_above (f ` A) \ f x \ SUPR A f" +lemma cSUP_upper: "x \ A \ bdd_above (f ` A) \ f x \ SUPREMUM A f" using cSup_upper [of _ "f ` A"] by simp -lemma cSUP_least: "A \ {} \ (\x. x \ A \ f x \ M) \ SUPR A f \ M" +lemma cSUP_least: "A \ {} \ (\x. x \ A \ f x \ M) \ SUPREMUM A f \ M" using cSup_least [of "f ` A"] by auto -lemma cINF_lower2: "bdd_below (f ` A) \ x \ A \ f x \ u \ INFI A f \ u" +lemma cINF_lower2: "bdd_below (f ` A) \ x \ A \ f x \ u \ INFIMUM A f \ u" by (auto intro: cINF_lower assms order_trans) -lemma cSUP_upper2: "bdd_above (f ` A) \ x \ A \ u \ f x \ u \ SUPR A f" +lemma cSUP_upper2: "bdd_above (f ` A) \ x \ A \ u \ f x \ u \ SUPREMUM A f" by (auto intro: cSUP_upper assms order_trans) lemma cSUP_const: "A \ {} \ (SUP x:A. c) = c" @@ -298,10 +298,10 @@ lemma cINF_const: "A \ {} \ (INF x:A. c) = c" by (intro antisym cINF_greatest) (auto intro: cINF_lower) -lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ INFI A f \ (\x\A. u \ f x)" +lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ INFIMUM A f \ (\x\A. u \ f x)" by (metis cINF_greatest cINF_lower assms order_trans) -lemma cSUP_le_iff: "A \ {} \ bdd_above (f ` A) \ SUPR A f \ u \ (\x\A. f x \ u)" +lemma cSUP_le_iff: "A \ {} \ bdd_above (f ` A) \ SUPREMUM A f \ u \ (\x\A. f x \ u)" by (metis cSUP_least cSUP_upper assms order_trans) lemma less_cINF_D: "bdd_below (f`A) \ y < (INF i:A. f i) \ i \ A \ y < f i" @@ -310,22 +310,22 @@ lemma cSUP_lessD: "bdd_above (f`A) \ (SUP i:A. f i) < y \ i \ A \ f i < y" by (metis cSUP_upper le_less_trans) -lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFI (insert a A) f = inf (f a) (INFI A f)" +lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)" by (metis cInf_insert Inf_image_eq image_insert image_is_empty) -lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ SUPR (insert a A) f = sup (f a) (SUPR A f)" +lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)" by (metis cSup_insert Sup_image_eq image_insert image_is_empty) -lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ INFI A f \ INFI B g" +lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ INFIMUM A f \ INFIMUM B g" using cInf_mono [of "g ` B" "f ` A"] by auto -lemma cSUP_mono: "A \ {} \ bdd_above (g ` B) \ (\n. n \ A \ \m\B. f n \ g m) \ SUPR A f \ SUPR B g" +lemma cSUP_mono: "A \ {} \ bdd_above (g ` B) \ (\n. n \ A \ \m\B. f n \ g m) \ SUPREMUM A f \ SUPREMUM B g" using cSup_mono [of "f ` A" "g ` B"] by auto -lemma cINF_superset_mono: "A \ {} \ bdd_below (g ` B) \ A \ B \ (\x. x \ B \ g x \ f x) \ INFI B g \ INFI A f" +lemma cINF_superset_mono: "A \ {} \ bdd_below (g ` B) \ A \ B \ (\x. x \ B \ g x \ f x) \ INFIMUM B g \ INFIMUM A f" by (rule cINF_mono) auto -lemma cSUP_subset_mono: "A \ {} \ bdd_above (g ` B) \ A \ B \ (\x. x \ B \ f x \ g x) \ SUPR A f \ SUPR B g" +lemma cSUP_subset_mono: "A \ {} \ bdd_above (g ` B) \ A \ B \ (\x. x \ B \ f x \ g x) \ SUPREMUM A f \ SUPREMUM B g" by (rule cSUP_mono) auto lemma less_eq_cInf_inter: "bdd_below A \ bdd_below B \ A \ B \ {} \ inf (Inf A) (Inf B) \ Inf (A \ B)" @@ -337,20 +337,20 @@ lemma cInf_union_distrib: "A \ {} \ bdd_below A \ B \ {} \ bdd_below B \ Inf (A \ B) = inf (Inf A) (Inf B)" by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower) -lemma cINF_union: "A \ {} \ bdd_below (f`A) \ B \ {} \ bdd_below (f`B) \ INFI (A \ B) f = inf (INFI A f) (INFI B f)" +lemma cINF_union: "A \ {} \ bdd_below (f`A) \ B \ {} \ bdd_below (f`B) \ INFIMUM (A \ B) f = inf (INFIMUM A f) (INFIMUM B f)" using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) lemma cSup_union_distrib: "A \ {} \ bdd_above A \ B \ {} \ bdd_above B \ Sup (A \ B) = sup (Sup A) (Sup B)" by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper) -lemma cSUP_union: "A \ {} \ bdd_above (f`A) \ B \ {} \ bdd_above (f`B) \ SUPR (A \ B) f = sup (SUPR A f) (SUPR B f)" +lemma cSUP_union: "A \ {} \ bdd_above (f`A) \ B \ {} \ bdd_above (f`B) \ SUPREMUM (A \ B) f = sup (SUPREMUM A f) (SUPREMUM B f)" using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) -lemma cINF_inf_distrib: "A \ {} \ bdd_below (f`A) \ bdd_below (g`A) \ inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))" +lemma cINF_inf_distrib: "A \ {} \ bdd_below (f`A) \ bdd_below (g`A) \ inf (INFIMUM A f) (INFIMUM A g) = (INF a:A. inf (f a) (g a))" by (intro antisym le_infI cINF_greatest cINF_lower2) (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI) -lemma SUP_sup_distrib: "A \ {} \ bdd_above (f`A) \ bdd_above (g`A) \ sup (SUPR A f) (SUPR A g) = (SUP a:A. sup (f a) (g a))" +lemma SUP_sup_distrib: "A \ {} \ bdd_above (f`A) \ bdd_above (g`A) \ sup (SUPREMUM A f) (SUPREMUM A g) = (SUP a:A. sup (f a) (g a))" by (intro antisym le_supI cSUP_least cSUP_upper2) (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI) diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Finite_Set.thy Wed Mar 19 18:47:22 2014 +0100 @@ -1035,7 +1035,7 @@ lemma inf_INF_fold_inf: assumes "finite A" - shows "inf B (INFI A f) = fold (inf \ f) B A" (is "?inf = ?fold") + shows "inf B (INFIMUM A f) = fold (inf \ f) B A" (is "?inf = ?fold") proof (rule sym) interpret comp_fun_idem inf by (fact comp_fun_idem_inf) interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem) @@ -1046,7 +1046,7 @@ lemma sup_SUP_fold_sup: assumes "finite A" - shows "sup B (SUPR A f) = fold (sup \ f) B A" (is "?sup = ?fold") + shows "sup B (SUPREMUM A f) = fold (sup \ f) B A" (is "?sup = ?fold") proof (rule sym) interpret comp_fun_idem sup by (fact comp_fun_idem_sup) interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem) @@ -1057,12 +1057,12 @@ lemma INF_fold_inf: assumes "finite A" - shows "INFI A f = fold (inf \ f) top A" + shows "INFIMUM A f = fold (inf \ f) top A" using assms inf_INF_fold_inf [of A top] by simp lemma SUP_fold_sup: assumes "finite A" - shows "SUPR A f = fold (sup \ f) bot A" + shows "SUPREMUM A f = fold (sup \ f) bot A" using assms sup_SUP_fold_sup [of A bot] by simp end diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/GCD.thy Wed Mar 19 18:47:22 2014 +0100 @@ -1558,8 +1558,8 @@ interpretation gcd_lcm_complete_lattice_nat: complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" where - "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)" - and "Sup.SUPR Lcm A f = Lcm (f ` A)" + "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)" + and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" proof - show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\m n. m dvd n \ \ n dvd m) lcm 1 (0::nat)" proof @@ -1577,8 +1577,8 @@ qed then interpret gcd_lcm_complete_lattice_nat: complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" . - from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" . - from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" . + from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" . + from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" . qed declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del] diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/Extended_Real.thy Wed Mar 19 18:47:22 2014 +0100 @@ -1411,15 +1411,15 @@ lemma ereal_SUP_not_infty: fixes f :: "_ \ ereal" - shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \SUPR A f\ \ \" + shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \SUPREMUM A f\ \ \" using SUP_upper2[of _ A l f] SUP_least[of A f u] - by (cases "SUPR A f") auto + by (cases "SUPREMUM A f") auto lemma ereal_INF_not_infty: fixes f :: "_ \ ereal" - shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \INFI A f\ \ \" + shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \INFIMUM A f\ \ \" using INF_lower2[of _ A f u] INF_greatest[of A l f] - by (cases "INFI A f") auto + by (cases "INFIMUM A f") auto lemma ereal_SUP_uminus: fixes f :: "'a \ ereal" @@ -1528,12 +1528,12 @@ fixes f :: "'i \ ereal" assumes "\i. f i + y \ z" and "y \ -\" - shows "SUPR UNIV f + y \ z" + shows "SUPREMUM UNIV f + y \ z" proof (cases y) case (real r) then have "\i. f i \ z - y" using assms by (simp add: ereal_le_minus_iff) - then have "SUPR UNIV f \ z - y" + then have "SUPREMUM UNIV f \ z - y" by (rule SUP_least) then show ?thesis using real by (simp add: ereal_le_minus_iff) @@ -1544,11 +1544,11 @@ assumes "incseq f" and "incseq g" and pos: "\i. f i \ -\" "\i. g i \ -\" - shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g" + shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g" proof (rule SUP_eqI) fix y assume *: "\i. i \ UNIV \ f i + g i \ y" - have f: "SUPR UNIV f \ -\" + have f: "SUPREMUM UNIV f \ -\" using pos unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD) @@ -1565,13 +1565,13 @@ also have "\ \ y" using * by auto finally have "f i + g j \ y" . } - then have "SUPR UNIV f + g j \ y" + then have "SUPREMUM UNIV f + g j \ y" using assms(4)[of j] by (intro SUP_ereal_le_addI) auto - then have "g j + SUPR UNIV f \ y" by (simp add: ac_simps) + then have "g j + SUPREMUM UNIV f \ y" by (simp add: ac_simps) } - then have "SUPR UNIV g + SUPR UNIV f \ y" + then have "SUPREMUM UNIV g + SUPREMUM UNIV f \ y" using f by (rule SUP_ereal_le_addI) - then show "SUPR UNIV f + SUPR UNIV g \ y" + then show "SUPREMUM UNIV f + SUPREMUM UNIV g \ y" by (simp add: ac_simps) qed (auto intro!: add_mono SUP_upper) @@ -1579,7 +1579,7 @@ fixes f g :: "nat \ ereal" assumes inc: "incseq f" "incseq g" and pos: "\i. 0 \ f i" "\i. 0 \ g i" - shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g" + shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g" proof (intro SUP_ereal_add inc) fix i show "f i \ -\" "g i \ -\" @@ -1590,7 +1590,7 @@ fixes f g :: "'a \ nat \ ereal" assumes "\n. n \ A \ incseq (f n)" and pos: "\n i. n \ A \ 0 \ f n i" - shows "(SUP i. \n\A. f n i) = (\n\A. SUPR UNIV (f n))" + shows "(SUP i. \n\A. f n i) = (\n\A. SUPREMUM UNIV (f n))" proof (cases "finite A") case True then show ?thesis using assms @@ -1604,20 +1604,20 @@ fixes f :: "nat \ ereal" assumes "\i. 0 \ f i" and "0 \ c" - shows "(SUP i. c * f i) = c * SUPR UNIV f" + shows "(SUP i. c * f i) = c * SUPREMUM UNIV f" proof (rule SUP_eqI) fix i - have "f i \ SUPR UNIV f" + have "f i \ SUPREMUM UNIV f" by (rule SUP_upper) auto - then show "c * f i \ c * SUPR UNIV f" + then show "c * f i \ c * SUPREMUM UNIV f" using `0 \ c` by (rule ereal_mult_left_mono) next fix y assume *: "\i. i \ UNIV \ c * f i \ y" - show "c * SUPR UNIV f \ y" + show "c * SUPREMUM UNIV f \ y" proof (cases "0 < c \ c \ \") case True - with * have "SUPR UNIV f \ y / c" + with * have "SUPREMUM UNIV f \ y / c" by (intro SUP_least) (auto simp: ereal_le_divide_pos) with True show ?thesis by (auto simp: ereal_le_divide_pos) @@ -1630,7 +1630,7 @@ case True then have "range f = {0}" by auto - with True show "c * SUPR UNIV f \ y" + with True show "c * SUPREMUM UNIV f \ y" using * by (auto simp: SUP_def max.absorb1) next case False @@ -1677,7 +1677,7 @@ lemma Sup_countable_SUP: assumes "A \ {}" - shows "\f::nat \ ereal. range f \ A \ Sup A = SUPR UNIV f" + shows "\f::nat \ ereal. range f \ A \ Sup A = SUPREMUM UNIV f" proof (cases "Sup A") case (real r) have "\n::nat. \x. x \ A \ Sup A < x + 1 / ereal (real n)" @@ -1691,7 +1691,7 @@ qed from choice[OF this] obtain f :: "nat \ ereal" where f: "\x. f x \ A \ Sup A < f x + 1 / ereal (real x)" .. - have "SUPR UNIV f = Sup A" + have "SUPREMUM UNIV f = Sup A" proof (rule SUP_eqI) fix i show "f i \ Sup A" @@ -1752,7 +1752,7 @@ qed from choice[OF this] obtain f :: "nat \ ereal" where f: "\z. f z \ A \ x + ereal (real z) \ f z" .. - have "SUPR UNIV f = \" + have "SUPREMUM UNIV f = \" proof (rule SUP_PInfty) fix n :: nat show "\i\UNIV. ereal (real n) \ f i" @@ -1771,7 +1771,7 @@ qed lemma SUP_countable_SUP: - "A \ {} \ \f::nat \ ereal. range f \ g`A \ SUPR A g = SUPR UNIV f" + "A \ {} \ \f::nat \ ereal. range f \ g`A \ SUPREMUM A g = SUPREMUM UNIV f" using Sup_countable_SUP [of "g`A"] by auto @@ -1852,7 +1852,7 @@ fixes f :: "nat \ ereal" assumes "decseq f" "decseq g" and fin: "\i. f i \ \" "\i. g i \ \" - shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g" + shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g" proof - have INF_less: "(INF i. f i) < \" "(INF i. g i) < \" using assms unfolding INF_less_iff by auto @@ -1863,7 +1863,7 @@ } then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))" by simp - also have "\ = INFI UNIV f + INFI UNIV g" + also have "\ = INFIMUM UNIV f + INFIMUM UNIV g" unfolding ereal_INF_uminus using assms INF_less by (subst SUP_ereal_add) diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Kleene_Algebra.thy --- a/src/HOL/Library/Kleene_Algebra.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/Kleene_Algebra.thy Wed Mar 19 18:47:22 2014 +0100 @@ -367,7 +367,7 @@ class kleene_by_complete_lattice = pre_kleene + complete_lattice + power + star + - assumes star_cont: "a * star b * c = SUPR UNIV (\n. a * b ^ n * c)" + assumes star_cont: "a * star b * c = SUPREMUM UNIV (\n. a * b ^ n * c)" begin subclass kleene diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Mar 19 18:47:22 2014 +0100 @@ -43,13 +43,13 @@ abbreviation "limsup \ Limsup sequentially" lemma Liminf_eqI: - "(\P. eventually P F \ INFI (Collect P) f \ x) \ - (\y. (\P. eventually P F \ INFI (Collect P) f \ y) \ x \ y) \ Liminf F f = x" + "(\P. eventually P F \ INFIMUM (Collect P) f \ x) \ + (\y. (\P. eventually P F \ INFIMUM (Collect P) f \ y) \ x \ y) \ Liminf F f = x" unfolding Liminf_def by (auto intro!: SUP_eqI) lemma Limsup_eqI: - "(\P. eventually P F \ x \ SUPR (Collect P) f) \ - (\y. (\P. eventually P F \ y \ SUPR (Collect P) f) \ y \ x) \ Limsup F f = x" + "(\P. eventually P F \ x \ SUPREMUM (Collect P) f) \ + (\y. (\P. eventually P F \ y \ SUPREMUM (Collect P) f) \ y \ x) \ Limsup F f = x" unfolding Limsup_def by (auto intro!: INF_eqI) lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)" @@ -93,7 +93,7 @@ proof (safe intro!: SUP_mono) fix P assume "eventually P F" with ev have "eventually (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\Q\{P. eventually P F}. INFI (Collect P) f \ INFI (Collect Q) g" + then show "\Q\{P. eventually P F}. INFIMUM (Collect P) f \ INFIMUM (Collect Q) g" by (intro bexI[of _ ?Q]) (auto intro!: INF_mono) qed @@ -109,7 +109,7 @@ proof (safe intro!: INF_mono) fix P assume "eventually P F" with ev have "eventually (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\Q\{P. eventually P F}. SUPR (Collect Q) f \ SUPR (Collect P) g" + then show "\Q\{P. eventually P F}. SUPREMUM (Collect Q) f \ SUPREMUM (Collect P) g" by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono) qed @@ -129,13 +129,13 @@ then have "eventually (\x. P x \ Q x) F" (is "eventually ?C F") by (rule eventually_conj) then have not_False: "(\x. P x \ Q x) \ (\x. False)" using ntriv by (auto simp add: eventually_False) - have "INFI (Collect P) f \ INFI (Collect ?C) f" + have "INFIMUM (Collect P) f \ INFIMUM (Collect ?C) f" by (rule INF_mono) auto - also have "\ \ SUPR (Collect ?C) f" + also have "\ \ SUPREMUM (Collect ?C) f" using not_False by (intro INF_le_SUP) auto - also have "\ \ SUPR (Collect Q) f" + also have "\ \ SUPREMUM (Collect Q) f" by (rule SUP_mono) auto - finally show "INFI (Collect P) f \ SUPR (Collect Q) f" . + finally show "INFIMUM (Collect P) f \ SUPREMUM (Collect Q) f" . qed lemma Liminf_bounded: @@ -154,22 +154,22 @@ fixes X :: "_ \ _ :: complete_linorder" shows "C \ Liminf F X \ (\yx. y < X x) F)" proof - - { fix y P assume "eventually P F" "y < INFI (Collect P) X" + { fix y P assume "eventually P F" "y < INFIMUM (Collect P) X" then have "eventually (\x. y < X x) F" by (auto elim!: eventually_elim1 dest: less_INF_D) } moreover { fix y P assume "y < C" and y: "\yx. y < X x) F" - have "\P. eventually P F \ y < INFI (Collect P) X" + have "\P. eventually P F \ y < INFIMUM (Collect P) X" proof (cases "\z. y < z \ z < C") case True then obtain z where z: "y < z \ z < C" .. - moreover from z have "z \ INFI {x. z < X x} X" + moreover from z have "z \ INFIMUM {x. z < X x} X" by (auto intro!: INF_greatest) ultimately show ?thesis using y by (intro exI[of _ "\x. z < X x"]) auto next case False - then have "C \ INFI {x. y < X x} X" + then have "C \ INFIMUM {x. y < X x} X" by (intro INF_greatest) auto with `y < C` show ?thesis using y by (intro exI[of _ "\x. y < X x"]) auto @@ -185,17 +185,17 @@ shows "Liminf F f = f0" proof (intro Liminf_eqI) fix P assume P: "eventually P F" - then have "eventually (\x. INFI (Collect P) f \ f x) F" + then have "eventually (\x. INFIMUM (Collect P) f \ f x) F" by eventually_elim (auto intro!: INF_lower) - then show "INFI (Collect P) f \ f0" + then show "INFIMUM (Collect P) f \ f0" by (rule tendsto_le[OF ntriv lim tendsto_const]) next - fix y assume upper: "\P. eventually P F \ INFI (Collect P) f \ y" + fix y assume upper: "\P. eventually P F \ INFIMUM (Collect P) f \ y" show "f0 \ y" proof cases assume "\z. y < z \ z < f0" then obtain z where "y < z \ z < f0" .. - moreover have "z \ INFI {x. z < f x} f" + moreover have "z \ INFIMUM {x. z < f x} f" by (rule INF_greatest) simp ultimately show ?thesis using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto @@ -208,9 +208,9 @@ using lim[THEN topological_tendstoD, of "{y <..}"] by auto then have "eventually (\x. f0 \ f x) F" using discrete by (auto elim!: eventually_elim1) - then have "INFI {x. f0 \ f x} f \ y" + then have "INFIMUM {x. f0 \ f x} f \ y" by (rule upper) - moreover have "f0 \ INFI {x. f0 \ f x} f" + moreover have "f0 \ INFIMUM {x. f0 \ f x} f" by (intro INF_greatest) simp ultimately show "f0 \ y" by simp qed @@ -224,17 +224,17 @@ shows "Limsup F f = f0" proof (intro Limsup_eqI) fix P assume P: "eventually P F" - then have "eventually (\x. f x \ SUPR (Collect P) f) F" + then have "eventually (\x. f x \ SUPREMUM (Collect P) f) F" by eventually_elim (auto intro!: SUP_upper) - then show "f0 \ SUPR (Collect P) f" + then show "f0 \ SUPREMUM (Collect P) f" by (rule tendsto_le[OF ntriv tendsto_const lim]) next - fix y assume lower: "\P. eventually P F \ y \ SUPR (Collect P) f" + fix y assume lower: "\P. eventually P F \ y \ SUPREMUM (Collect P) f" show "y \ f0" proof (cases "\z. f0 < z \ z < y") case True then obtain z where "f0 < z \ z < y" .. - moreover have "SUPR {x. f x < z} f \ z" + moreover have "SUPREMUM {x. f x < z} f \ z" by (rule SUP_least) simp ultimately show ?thesis using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto @@ -247,9 +247,9 @@ using lim[THEN topological_tendstoD, of "{..< y}"] by auto then have "eventually (\x. f x \ f0) F" using False by (auto elim!: eventually_elim1 simp: not_less) - then have "y \ SUPR {x. f x \ f0} f" + then have "y \ SUPREMUM {x. f x \ f0} f" by (rule lower) - moreover have "SUPR {x. f x \ f0} f \ f0" + moreover have "SUPREMUM {x. f x \ f0} f \ f0" by (intro SUP_least) simp ultimately show "y \ f0" by simp qed @@ -264,14 +264,14 @@ proof (rule order_tendstoI) fix a assume "f0 < a" with assms have "Limsup F f < a" by simp - then obtain P where "eventually P F" "SUPR (Collect P) f < a" + then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a" unfolding Limsup_def INF_less_iff by auto then show "eventually (\x. f x < a) F" by (auto elim!: eventually_elim1 dest: SUP_lessD) next fix a assume "a < f0" with assms have "a < Liminf F f" by simp - then obtain P where "eventually P F" "a < INFI (Collect P) f" + then obtain P where "eventually P F" "a < INFIMUM (Collect P) f" unfolding Liminf_def less_SUP_iff by auto then show "eventually (\x. a < f x) F" by (auto elim!: eventually_elim1 dest: less_INF_D) diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/Product_Order.thy Wed Mar 19 18:47:22 2014 +0100 @@ -219,11 +219,11 @@ of two complete lattices: *} lemma INF_prod_alt_def: - "INFI A f = (INFI A (fst o f), INFI A (snd o f))" + "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))" unfolding INF_def Inf_prod_def by simp lemma SUP_prod_alt_def: - "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))" + "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))" unfolding SUP_def Sup_prod_def by simp diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/RBT_Set.thy Wed Mar 19 18:47:22 2014 +0100 @@ -112,7 +112,7 @@ "Inf_fin = Inf_fin" .. lemma [code, code del]: - "INFI = INFI" .. + "INFIMUM = INFIMUM" .. lemma [code, code del]: "Max = Max" .. @@ -121,7 +121,7 @@ "Sup_fin = Sup_fin" .. lemma [code, code del]: - "SUPR = SUPR" .. + "SUPREMUM = SUPREMUM" .. lemma [code, code del]: "(Inf :: 'a set set \ 'a set) = Inf" .. @@ -759,7 +759,7 @@ lemma INF_Set_fold [code]: fixes f :: "_ \ 'a::complete_lattice" - shows "INFI (Set t) f = fold_keys (inf \ f) t top" + shows "INFIMUM (Set t) f = fold_keys (inf \ f) t top" proof - have "comp_fun_commute ((inf :: 'a \ 'a \ 'a) \ f)" by default (auto simp add: fun_eq_iff ac_simps) @@ -800,7 +800,7 @@ lemma SUP_Set_fold [code]: fixes f :: "_ \ 'a::complete_lattice" - shows "SUPR (Set t) f = fold_keys (sup \ f) t bot" + shows "SUPREMUM (Set t) f = fold_keys (sup \ f) t bot" proof - have "comp_fun_commute ((sup :: 'a \ 'a \ 'a) \ f)" by default (auto simp add: fun_eq_iff ac_simps) diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Lifting_Set.thy Wed Mar 19 18:47:22 2014 +0100 @@ -150,12 +150,12 @@ unfolding rel_fun_def rel_set_def by fast lemma SUP_parametric [transfer_rule]: - "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \ _ \ _::complete_lattice)" + "(rel_set R ===> (R ===> op =) ===> op =) SUPREMUM (SUPREMUM :: _ \ _ \ _::complete_lattice)" proof(rule rel_funI)+ fix A B f and g :: "'b \ 'c" assume AB: "rel_set R A B" and fg: "(R ===> op =) f g" - show "SUPR A f = SUPR B g" + show "SUPREMUM A f = SUPREMUM B g" by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI) qed diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/List.thy --- a/src/HOL/List.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/List.thy Wed Mar 19 18:47:22 2014 +0100 @@ -2876,13 +2876,13 @@ declare Sup_set_fold [where 'a = "'a set", code] lemma (in complete_lattice) INF_set_fold: - "INFI (set xs) f = fold (inf \ f) xs top" + "INFIMUM (set xs) f = fold (inf \ f) xs top" using Inf_set_fold [of "map f xs "] by (simp add: fold_map) declare INF_set_fold [code] lemma (in complete_lattice) SUP_set_fold: - "SUPR (set xs) f = fold (sup \ f) xs bot" + "SUPREMUM (set xs) f = fold (sup \ f) xs bot" using Sup_set_fold [of "map f xs "] by (simp add: fold_map) declare SUP_set_fold [code] diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Mar 19 18:47:22 2014 +0100 @@ -1166,13 +1166,13 @@ assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) - then show "\r>0. INFI (Collect P) f \ INFI (S \ ball x r - {x}) f" + then show "\r>0. INFIMUM (Collect P) f \ INFIMUM (S \ ball x r - {x}) f" by (intro exI[of _ d] INF_mono conjI `0 < d`) auto next fix d :: real assume "0 < d" then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \ - INFI (S \ ball x d - {x}) f \ INFI (Collect P) f" + INFIMUM (S \ ball x d - {x}) f \ INFIMUM (Collect P) f" by (intro exI[of _ "\y. y \ S \ ball x d - {x}"]) (auto intro!: INF_mono exI[of _ d] simp: dist_commute) qed @@ -1186,13 +1186,13 @@ assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) - then show "\r>0. SUPR (S \ ball x r - {x}) f \ SUPR (Collect P) f" + then show "\r>0. SUPREMUM (S \ ball x r - {x}) f \ SUPREMUM (Collect P) f" by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto next fix d :: real assume "0 < d" then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \ - SUPR (Collect P) f \ SUPR (S \ ball x d - {x}) f" + SUPREMUM (Collect P) f \ SUPREMUM (S \ ball x d - {x}) f" by (intro exI[of _ "\y. y \ S \ ball x d - {x}"]) (auto intro!: SUP_mono exI[of _ d] simp: dist_commute) qed @@ -1285,11 +1285,11 @@ fix P assume P: "eventually P net" fix S - assume S: "mono_set S" "INFI (Collect P) f \ S" + assume S: "mono_set S" "INFIMUM (Collect P) f \ S" { fix x assume "P x" - then have "INFI (Collect P) f \ f x" + then have "INFIMUM (Collect P) f \ f x" by (intro complete_lattice_class.INF_lower) simp with S have "f x \ S" by (simp add: mono_set) @@ -1299,16 +1299,16 @@ next fix y l assume S: "\S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net" - assume P: "\P. eventually P net \ INFI (Collect P) f \ y" + assume P: "\P. eventually P net \ INFIMUM (Collect P) f \ y" show "l \ y" proof (rule dense_le) fix B assume "B < l" then have "eventually (\x. f x \ {B <..}) net" by (intro S[rule_format]) auto - then have "INFI {x. B < f x} f \ y" + then have "INFIMUM {x. B < f x} f \ y" using P by auto - moreover have "B \ INFI {x. B < f x} f" + moreover have "B \ INFIMUM {x. B < f x} f" by (intro INF_greatest) auto ultimately show "B \ y" by simp @@ -1324,13 +1324,13 @@ fix P assume P: "eventually P net" fix S - assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \ S" + assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \ S" { fix x assume "P x" - then have "f x \ SUPR (Collect P) f" + then have "f x \ SUPREMUM (Collect P) f" by (intro complete_lattice_class.SUP_upper) simp - with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2) + with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2) have "f x \ S" by (simp add: inj_image_mem_iff) } with P show "eventually (\x. f x \ S) net" @@ -1338,16 +1338,16 @@ next fix y l assume S: "\S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net" - assume P: "\P. eventually P net \ y \ SUPR (Collect P) f" + assume P: "\P. eventually P net \ y \ SUPREMUM (Collect P) f" show "y \ l" proof (rule dense_ge) fix B assume "l < B" then have "eventually (\x. f x \ {..< B}) net" by (intro S[rule_format]) auto - then have "y \ SUPR {x. f x < B} f" + then have "y \ SUPREMUM {x. f x < B} f" using P by auto - moreover have "SUPR {x. f x < B} f \ B" + moreover have "SUPREMUM {x. f x < B} f \ B" by (intro SUP_least) auto ultimately show "y \ B" by simp diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 19 18:47:22 2014 +0100 @@ -11842,7 +11842,7 @@ using goal2 by auto qed then obtain K where *: "\x\{d. d division_of \d}. K = (\k\x. norm (integral k f))" - "SUPR {d. d division_of \d} (setsum (\k. norm (integral k f))) - e < K" + "SUPREMUM {d. d division_of \d} (setsum (\k. norm (integral k f))) - e < K" by (auto simp add: image_iff not_le) from this(1) obtain d where "d division_of \d" and "K = (\k\d. norm (integral k f))" diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Predicate.thy Wed Mar 19 18:47:22 2014 +0100 @@ -65,17 +65,17 @@ by (simp add: sup_pred_def) definition - "\A = Pred (INFI A eval)" + "\A = Pred (INFIMUM A eval)" lemma eval_Inf [simp]: - "eval (\A) = INFI A eval" + "eval (\A) = INFIMUM A eval" by (simp add: Inf_pred_def) definition - "\A = Pred (SUPR A eval)" + "\A = Pred (SUPREMUM A eval)" lemma eval_Sup [simp]: - "eval (\A) = SUPR A eval" + "eval (\A) = SUPREMUM A eval" by (simp add: Sup_pred_def) instance proof @@ -84,11 +84,11 @@ end lemma eval_INF [simp]: - "eval (INFI A f) = INFI A (eval \ f)" + "eval (INFIMUM A f) = INFIMUM A (eval \ f)" using eval_Inf [of "f ` A"] by simp lemma eval_SUP [simp]: - "eval (SUPR A f) = SUPR A (eval \ f)" + "eval (SUPREMUM A f) = SUPREMUM A (eval \ f)" using eval_Sup [of "f ` A"] by simp instantiation pred :: (type) complete_boolean_algebra @@ -121,10 +121,10 @@ by (simp add: single_def) definition bind :: "'a pred \ ('a \ 'b pred) \ 'b pred" (infixl "\=" 70) where - "P \= f = (SUPR {x. eval P x} f)" + "P \= f = (SUPREMUM {x. eval P x} f)" lemma eval_bind [simp]: - "eval (P \= f) = eval (SUPR {x. eval P x} f)" + "eval (P \= f) = eval (SUPREMUM {x. eval P x} f)" by (simp add: bind_def) lemma bind_bind: diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Mar 19 18:47:22 2014 +0100 @@ -781,7 +781,7 @@ lemma positive_integral_def_finite: "integral\<^sup>P M f = (SUP g : {g. simple_function M g \ g \ max 0 \ f \ range g \ {0 ..< \}}. integral\<^sup>S M g)" - (is "_ = SUPR ?A ?f") + (is "_ = SUPREMUM ?A ?f") unfolding positive_integral_def proof (safe intro!: antisym SUP_least) fix g assume g: "simple_function M g" "g \ max 0 \ f" @@ -793,7 +793,7 @@ apply (safe intro!: simple_function_max simple_function_If) apply (force simp: max_def le_fun_def split: split_if_asm)+ done - show "integral\<^sup>S M g \ SUPR ?A ?f" + show "integral\<^sup>S M g \ SUPREMUM ?A ?f" proof cases have g0: "?g 0 \ ?A" by (intro g_in_A) auto assume "(emeasure M) ?G = 0" @@ -804,7 +804,7 @@ (auto simp: max_def intro!: simple_function_If) next assume \_G: "(emeasure M) ?G \ 0" - have "SUPR ?A (integral\<^sup>S M) = \" + have "SUPREMUM ?A (integral\<^sup>S M) = \" proof (intro SUP_PInfty) fix n :: nat let ?y = "ereal (real n) / (if (emeasure M) ?G = \ then 1 else (emeasure M) ?G)" @@ -1029,7 +1029,7 @@ using N(1) by auto } qed also have "\ = (SUP i. (\\<^sup>+ x. f i x \M))" - using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext) + using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext) finally show ?thesis . qed @@ -1045,7 +1045,7 @@ shows "(SUP i. integral\<^sup>S M (f i)) = (\\<^sup>+x. (SUP i. f i x) \M)" using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1) f(3)[THEN borel_measurable_simple_function] f(2)] - by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext) + by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext) lemma positive_integral_max_0: "(\\<^sup>+x. max 0 (f x) \M) = integral\<^sup>P M f" @@ -1069,7 +1069,7 @@ and g: "incseq g" "\i x. 0 \ g i x" "\i. simple_function M (g i)" and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" - (is "SUPR _ ?F = SUPR _ ?G") + (is "SUPREMUM _ ?F = SUPREMUM _ ?G") proof - have "(SUP i. integral\<^sup>S M (f i)) = (\\<^sup>+x. (SUP i. f i x) \M)" using f by (rule positive_integral_monotone_convergence_simple) @@ -1128,7 +1128,7 @@ by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg) qed also have "\ = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))" - using u(2, 6) v(2, 6) `0 \ a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext) + using u(2, 6) v(2, 6) `0 \ a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext) finally have "(\\<^sup>+ x. max 0 (a * f x + g x) \M) = a * (\\<^sup>+x. max 0 (f x) \M) + (\\<^sup>+x. max 0 (g x) \M)" unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric] unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric] diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 19 18:47:22 2014 +0100 @@ -169,7 +169,7 @@ by (auto intro!: SUP_upper2 integral_nonneg) next show "(SUP n. \i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))" - proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2]) + proof (intro arg_cong[where f="SUPREMUM UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2]) fix n have "\m. (UNION {.. sets lebesgue" using rA by auto from lebesgueD[OF this] diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Product_Type.thy Wed Mar 19 18:47:22 2014 +0100 @@ -342,8 +342,8 @@ in [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}, - Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, - Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}] |> map (fn (Q, tr) => (Q, contract Q tr)) end *} diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Relation.thy Wed Mar 19 18:47:22 2014 +0100 @@ -281,7 +281,7 @@ by (fast intro: symI elim: symE) lemma symp_INF: - "\x\S. symp (r x) \ symp (INFI S r)" + "\x\S. symp (r x) \ symp (INFIMUM S r)" by (fact sym_INTER [to_pred]) lemma sym_UNION: @@ -289,7 +289,7 @@ by (fast intro: symI elim: symE) lemma symp_SUP: - "\x\S. symp (r x) \ symp (SUPR S r)" + "\x\S. symp (r x) \ symp (SUPREMUM S r)" by (fact sym_UNION [to_pred]) diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Mar 19 18:47:22 2014 +0100 @@ -393,7 +393,7 @@ fun mk_UNION X f = let val (T, U) = dest_funT (fastype_of f); - in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end; + in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end; fun mk_Union T = Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T); diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Wellfounded.thy Wed Mar 19 18:47:22 2014 +0100 @@ -297,7 +297,7 @@ done lemma wfP_SUP: - "\i. wfP (r i) \ \i j. r i \ r j \ inf (DomainP (r i)) (RangeP (r j)) = bot \ wfP (SUPR UNIV r)" + "\i. wfP (r i) \ \i j. r i \ r j \ inf (DomainP (r i)) (RangeP (r j)) = bot \ wfP (SUPREMUM UNIV r)" apply (rule wf_UN[to_pred]) apply simp_all done