--- 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
--- 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>\<open>Fun.mono\<close> & \<^typeof>\<open>Fun.mono\<close>\\
\<^const>\<open>Fun.strict_mono_on\<close> & \<^typeof>\<open>Fun.strict_mono_on\<close>\\
\<^const>\<open>Fun.strict_mono\<close> & \<^typeof>\<open>Fun.strict_mono\<close>\\
+\<^const>\<open>Fun.antimono\<close> & \<^typeof>\<open>Fun.antimono\<close>\\
\<^const>\<open>Fun.fun_upd\<close> & \<^typeof>\<open>Fun.fun_upd\<close>\\
\end{tabular}
--- 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 *: "\<And>i. f i \<in> borel_measurable M" "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>"
shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>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 \<Rightarrow> 'a \<Rightarrow> ennreal"
@@ -1464,7 +1464,7 @@
fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C"
then show "(\<integral>\<^sup>+ y. f y (Inf (C ` UNIV)) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>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
--- 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 \<Rightarrow> 'b::order) \<Rightarrow> bool"
where "strict_mono \<equiv> strict_mono_on UNIV"
+abbreviation antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
+ where "antimono \<equiv> monotone (\<le>) (\<lambda>x y. y \<le> x)"
+
lemma mono_def[no_atp]: "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
by (simp add: monotone_on_def)
lemma strict_mono_def[no_atp]: "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
by (simp add: monotone_on_def)
-text \<open>Lemmas @{thm [source] mono_def} and @{thm [source] strict_mono_def} are provided for backward
-compatibility.\<close>
+lemma antimono_def[no_atp]: "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
+ by (simp add: monotone_on_def)
+
+text \<open>Lemmas @{thm [source] mono_def}, @{thm [source] strict_mono_def}, and
+@{thm [source] antimono_def} are provided for backward compatibility.\<close>
lemma monoI [intro?]: "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
by (rule monotoneI)
@@ -1050,12 +1056,18 @@
lemma strict_monoI [intro?]: "(\<And>x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> strict_mono f"
by (rule monotoneI)
+lemma antimonoI [intro?]: "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
+ by (rule monotoneI)
+
lemma monoD [dest?]: "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
by (rule monotoneD)
lemma strict_monoD [dest?]: "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
by (rule monotoneD)
+lemma antimonoD [dest?]: "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
+ by (rule monotoneD)
+
lemma monoE:
assumes "mono f"
assumes "x \<le> y"
@@ -1064,6 +1076,15 @@
from assms show "f x \<le> f y" by (simp add: mono_def)
qed
+lemma antimonoE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "antimono f"
+ assumes "x \<le> y"
+ obtains "f x \<ge> f y"
+proof
+ from assms show "f x \<ge> f y" by (simp add: antimono_def)
+qed
+
lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
by (rule monotone_on_subset[OF _ subset_UNIV])
@@ -1219,6 +1240,11 @@
lemma (in linorder) max_of_mono: "mono f \<Longrightarrow> 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 \<Longrightarrow> max (f x) (f y) = f (min x y)" and
+ min_of_antimono: "antimono f \<Longrightarrow> 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 \<Longrightarrow> inj_on f A"
by (auto intro!: inj_onI dest: strict_mono_eq)
--- 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 \<Longrightarrow> max (f x) (f y) = f (min x y)"
- and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)"
- for f::"'a::linorder \<Rightarrow> 'b::linorder"
- by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym)
-
lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
by (auto intro: antisym simp add: min_def fun_eq_iff)
--- 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 \<open>Monotonicity\<close>
-
-context order
-begin
-
-definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
- "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
-
-lemma antimonoI [intro?]:
- fixes f :: "'a \<Rightarrow> 'b::order"
- shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
- unfolding antimono_def by iprover
-
-lemma antimonoD [dest?]:
- fixes f :: "'a \<Rightarrow> 'b::order"
- shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
- unfolding antimono_def by iprover
-
-lemma antimonoE:
- fixes f :: "'a \<Rightarrow> 'b::order"
- assumes "antimono f"
- assumes "x \<le> y"
- obtains "f x \<ge> f y"
-proof
- from assms show "f x \<ge> f y" by (simp add: antimono_def)
-qed
-
-end
-
-
subsection \<open>min and max -- fundamental\<close>
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
--- 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 \<open>F \<noteq> bot\<close>]] by metis