# HG changeset patch # User desharna # Date 1656156881 -7200 # Node ID 8d56461f85ecf65ff3fa5941507fe38103d63582 # Parent a4b47c684445539380e018ed8b23f4ddd52d92a0 moved antimono to Fun and redefined it as an abbreviation diff -r a4b47c684445 -r 8d56461f85ec NEWS --- a/NEWS Sat Jun 25 13:21:27 2022 +0200 +++ b/NEWS Sat Jun 25 13:34:41 2022 +0200 @@ -57,10 +57,11 @@ of monotone_of. Lemmas mono_on_def and strict_mono_on_def are explicitly provided for backward compatibility but their usage is discouraged. INCOMPATIBILITY. - - Move mono, strict_mono, and relevant lemmas to Fun theory. Also change - them to be abbreviations of mono_on and strict_mono_on. Lemmas - mono_def and strict_mono_def, are explicitly provided for backward - compatibility but their usage is discouraged. Minor INCOMPATIBILITY. + - Move mono, strict_mono, antimono, and relevant lemmas to Fun theory. + Also change them to be abbreviations of mono_on, strict_mono_on, + and monotone, respectively. Lemmas mono_def, strict_mono_def, and + antimono_def are explicitly provided for backward compatibility but + their usage is discouraged. Minor INCOMPATIBILITY. - Added lemmas. monotone_onD monotone_onI diff -r a4b47c684445 -r 8d56461f85ec src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/Doc/Main/Main_Doc.thy Sat Jun 25 13:34:41 2022 +0200 @@ -156,6 +156,7 @@ \<^const>\Fun.mono\ & \<^typeof>\Fun.mono\\\ \<^const>\Fun.strict_mono_on\ & \<^typeof>\Fun.strict_mono_on\\\ \<^const>\Fun.strict_mono\ & \<^typeof>\Fun.strict_mono\\\ +\<^const>\Fun.antimono\ & \<^typeof>\Fun.antimono\\\ \<^const>\Fun.fun_upd\ & \<^typeof>\Fun.fun_upd\\\ \end{tabular} diff -r a4b47c684445 -r 8d56461f85ec src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sat Jun 25 13:34:41 2022 +0200 @@ -1383,7 +1383,7 @@ lemma nn_integral_monotone_convergence_INF_decseq: assumes f: "decseq f" and *: "\i. f i \ borel_measurable M" "(\\<^sup>+ x. f i x \M) < \" shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" - using nn_integral_monotone_convergence_INF_AE[of f M i, OF _ *] f by (auto simp: decseq_Suc_iff le_fun_def) + using nn_integral_monotone_convergence_INF_AE[of f M i, OF _ *] f by (simp add: decseq_SucD le_funD) theorem nn_integral_liminf: fixes u :: "nat \ 'a \ ennreal" @@ -1464,7 +1464,7 @@ fix C :: "nat \ 'b" assume C: "decseq C" then show "(\\<^sup>+ y. f y (Inf (C ` UNIV)) \M) = (INF i. \\<^sup>+ y. f y (C i) \M)" using inf_continuous_mono[OF f] bnd - by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top + by (auto simp add: inf_continuousD[OF f C] fun_eq_iff monotone_def le_fun_def less_top intro!: nn_integral_monotone_convergence_INF_decseq) qed diff -r a4b47c684445 -r 8d56461f85ec src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/HOL/Fun.thy Sat Jun 25 13:34:41 2022 +0200 @@ -1035,14 +1035,20 @@ abbreviation strict_mono :: "('a \ 'b::order) \ bool" where "strict_mono \ strict_mono_on UNIV" +abbreviation antimono :: "('a \ 'b::order) \ bool" + where "antimono \ monotone (\) (\x y. y \ x)" + lemma mono_def[no_atp]: "mono f \ (\x y. x \ y \ f x \ f y)" by (simp add: monotone_on_def) lemma strict_mono_def[no_atp]: "strict_mono f \ (\x y. x < y \ f x < f y)" by (simp add: monotone_on_def) -text \Lemmas @{thm [source] mono_def} and @{thm [source] strict_mono_def} are provided for backward -compatibility.\ +lemma antimono_def[no_atp]: "antimono f \ (\x y. x \ y \ f x \ f y)" + by (simp add: monotone_on_def) + +text \Lemmas @{thm [source] mono_def}, @{thm [source] strict_mono_def}, and +@{thm [source] antimono_def} are provided for backward compatibility.\ lemma monoI [intro?]: "(\x y. x \ y \ f x \ f y) \ mono f" by (rule monotoneI) @@ -1050,12 +1056,18 @@ lemma strict_monoI [intro?]: "(\x y. x < y \ f x < f y) \ strict_mono f" by (rule monotoneI) +lemma antimonoI [intro?]: "(\x y. x \ y \ f x \ f y) \ antimono f" + by (rule monotoneI) + lemma monoD [dest?]: "mono f \ x \ y \ f x \ f y" by (rule monotoneD) lemma strict_monoD [dest?]: "strict_mono f \ x < y \ f x < f y" by (rule monotoneD) +lemma antimonoD [dest?]: "antimono f \ x \ y \ f x \ f y" + by (rule monotoneD) + lemma monoE: assumes "mono f" assumes "x \ y" @@ -1064,6 +1076,15 @@ from assms show "f x \ f y" by (simp add: mono_def) qed +lemma antimonoE: + fixes f :: "'a \ 'b::order" + assumes "antimono f" + assumes "x \ y" + obtains "f x \ f y" +proof + from assms show "f x \ f y" by (simp add: antimono_def) +qed + lemma mono_imp_mono_on: "mono f \ mono_on A f" by (rule monotone_on_subset[OF _ subset_UNIV]) @@ -1219,6 +1240,11 @@ lemma (in linorder) max_of_mono: "mono f \ max (f m) (f n) = f (max m n)" by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) +lemma (in linorder) + max_of_antimono: "antimono f \ max (f x) (f y) = f (min x y)" and + min_of_antimono: "antimono f \ min (f x) (f y) = f (max x y)" + by (auto simp: antimono_def Orderings.max_def max_def Orderings.min_def min_def intro!: antisym) + lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \ inj_on f A" by (auto intro!: inj_onI dest: strict_mono_eq) diff -r a4b47c684445 -r 8d56461f85ec src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/HOL/Lattices.thy Sat Jun 25 13:34:41 2022 +0200 @@ -606,11 +606,6 @@ end -lemma max_of_antimono: "antimono f \ max (f x) (f y) = f (min x y)" - and min_of_antimono: "antimono f \ min (f x) (f y) = f (max x y)" - for f::"'a::linorder \ 'b::linorder" - by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym) - lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \ 'a \ 'a)" by (auto intro: antisym simp add: min_def fun_eq_iff) diff -r a4b47c684445 -r 8d56461f85ec src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/HOL/Orderings.thy Sat Jun 25 13:34:41 2022 +0200 @@ -1058,36 +1058,6 @@ *) -subsection \Monotonicity\ - -context order -begin - -definition antimono :: "('a \ 'b::order) \ bool" where - "antimono f \ (\x y. x \ y \ f x \ f y)" - -lemma antimonoI [intro?]: - fixes f :: "'a \ 'b::order" - shows "(\x y. x \ y \ f x \ f y) \ antimono f" - unfolding antimono_def by iprover - -lemma antimonoD [dest?]: - fixes f :: "'a \ 'b::order" - shows "antimono f \ x \ y \ f x \ f y" - unfolding antimono_def by iprover - -lemma antimonoE: - fixes f :: "'a \ 'b::order" - assumes "antimono f" - assumes "x \ y" - obtains "f x \ f y" -proof - from assms show "f x \ f y" by (simp add: antimono_def) -qed - -end - - subsection \min and max -- fundamental\ definition (in ord) min :: "'a \ 'a \ 'a" where diff -r a4b47c684445 -r 8d56461f85ec src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Sat Jun 25 13:21:27 2022 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Sat Jun 25 13:34:41 2022 +0200 @@ -2154,7 +2154,7 @@ for n x y by metis have "antimono P" - using P(4) unfolding decseq_Suc_iff le_fun_def by blast + using P(4) by (rule decseq_SucI) obtain X where X: "P n (X n)" for n using P(1)[THEN eventually_happens'[OF \F \ bot\]] by metis