# 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>\<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}
 
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 *: "\<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
 
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 \<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)
 
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 \<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)
 
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 \<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
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 \<open>F \<noteq> bot\<close>]] by metis