# HG changeset patch
# User desharna
# Date 1656156087 -7200
# Node ID a4b47c684445539380e018ed8b23f4ddd52d92a0
# Parent  6d4fb57eb66c80f87f60b7c51ae584cc240833e1
moved mono and strict_mono to Fun and redefined them as abbreviations

diff -r 6d4fb57eb66c -r a4b47c684445 NEWS
--- a/NEWS	Tue Jul 05 09:44:38 2022 +0200
+++ b/NEWS	Sat Jun 25 13:21:27 2022 +0200
@@ -53,8 +53,14 @@
     compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
   - Changed argument order of mono_on and strict_mono_on to uniformize
     with monotone_on and the general "characterizing set at the beginning
-    of predicates" preference. Also change them to be abbreviation of
-    monotone_of. Minor INCOMPATIBILITY
+    of predicates" preference. Also change them to be abbreviations
+    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.
   - Added lemmas.
       monotone_onD
       monotone_onI
diff -r 6d4fb57eb66c -r a4b47c684445 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -58,8 +58,6 @@
 \<^const>\<open>Orderings.max\<close> & \<^typeof>\<open>Orderings.max\<close>\\
 @{const[source] top} & \<^typeof>\<open>Orderings.top\<close>\\
 @{const[source] bot} & \<^typeof>\<open>Orderings.bot\<close>\\
-\<^const>\<open>Orderings.mono\<close> & \<^typeof>\<open>Orderings.mono\<close>\\
-\<^const>\<open>Orderings.strict_mono\<close> & \<^typeof>\<open>Orderings.strict_mono\<close>\\
 \end{tabular}
 
 \subsubsection*{Syntax}
@@ -152,6 +150,12 @@
 \<^const>\<open>Fun.surj\<close> & \<^typeof>\<open>Fun.surj\<close>\\
 \<^const>\<open>Fun.bij\<close> & \<^typeof>\<open>Fun.bij\<close>\\
 \<^const>\<open>Fun.bij_betw\<close> & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
+\<^const>\<open>Fun.monotone_on\<close> & \<^typeof>\<open>Fun.monotone_on\<close>\\
+\<^const>\<open>Fun.monotone\<close> & \<^typeof>\<open>Fun.monotone\<close>\\
+\<^const>\<open>Fun.mono_on\<close> & \<^typeof>\<open>Fun.mono_on\<close>\\
+\<^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.fun_upd\<close> & \<^typeof>\<open>Fun.fun_upd\<close>\\
 \end{tabular}
 
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Fun.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -590,9 +590,6 @@
 lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
   by (auto intro!: inj_onI)
 
-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)
-
 lemma bij_betw_byWitness:
   assumes left: "\<forall>a \<in> A. f' (f a) = a"
     and right: "\<forall>a' \<in> A'. f (f' a') = a'"
@@ -931,7 +928,7 @@
 qed
 
 
-subsection \<open>Monotonic functions over a set\<close>
+subsection \<open>Monotonicity\<close>
 
 definition monotone_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "monotone_on A orda ordb f \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. orda x y \<longrightarrow> ordb (f x) (f y))"
@@ -980,39 +977,45 @@
     using mono_f[THEN monotone_onD] by simp
 qed
 
-abbreviation mono_on :: "('a :: ord) set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+
+subsubsection \<open>Specializations For @{class ord} Type Class And More\<close>
+
+context ord begin
+
+abbreviation mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
   where "mono_on A \<equiv> monotone_on A (\<le>) (\<le>)"
 
-lemma mono_on_def: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
+abbreviation strict_mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+  where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
+
+lemma mono_on_def[no_atp]: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
   by (auto simp add: monotone_on_def)
 
+lemma strict_mono_on_def[no_atp]:
+  "strict_mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s)"
+  by (auto simp add: monotone_on_def)
+
+text \<open>Lemmas @{thm [source] mono_on_def} and @{thm [source] strict_mono_on_def} are provided for
+backward compatibility.\<close>
+
 lemma mono_onI:
   "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on A f"
   by (rule monotone_onI)
 
-lemma mono_onD:
-  "\<lbrakk>mono_on A f; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
+lemma strict_mono_onI:
+  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on A f"
+  by (rule monotone_onI)
+
+lemma mono_onD: "\<lbrakk>mono_on A f; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
   by (rule monotone_onD)
 
-lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
-  unfolding mono_def mono_on_def by auto
+lemma strict_mono_onD: "\<lbrakk>strict_mono_on A f; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
+  by (rule monotone_onD)
 
 lemma mono_on_subset: "mono_on A f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on B f"
   by (rule monotone_on_subset)
 
-abbreviation strict_mono_on :: "('a :: ord) set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
-  where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
-
-lemma strict_mono_on_def: "strict_mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s)"
-  by (auto simp add: monotone_on_def)
-
-lemma strict_mono_onI:
-  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on A f"
-  by (rule monotone_onI)
-
-lemma strict_mono_onD:
-  "\<lbrakk>strict_mono_on A f; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
-  by (rule monotone_onD)
+end
 
 lemma mono_on_greaterD:
   assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
@@ -1024,6 +1027,136 @@
   with assms(4) show False by simp
 qed
 
+context order begin
+
+abbreviation mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
+  where "mono \<equiv> mono_on UNIV"
+
+abbreviation strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
+  where "strict_mono \<equiv> strict_mono_on UNIV"
+
+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 monoI [intro?]: "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
+  by (rule monotoneI)
+
+lemma strict_monoI [intro?]: "(\<And>x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> strict_mono 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 monoE:
+  assumes "mono f"
+  assumes "x \<le> y"
+  obtains "f x \<le> f y"
+proof
+  from assms show "f x \<le> f y" by (simp add: mono_def)
+qed
+
+lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
+  by (rule monotone_on_subset[OF _ subset_UNIV])
+
+lemma strict_mono_mono [dest?]:
+  assumes "strict_mono f"
+  shows "mono f"
+proof (rule monoI)
+  fix x y
+  assume "x \<le> y"
+  show "f x \<le> f y"
+  proof (cases "x = y")
+    case True then show ?thesis by simp
+  next
+    case False with \<open>x \<le> y\<close> have "x < y" by simp
+    with assms strict_monoD have "f x < f y" by auto
+    then show ?thesis by simp
+
+  qed
+qed
+
+end
+
+context linorder begin
+
+lemma mono_invE:
+  fixes f :: "'a \<Rightarrow> 'b::order"
+  assumes "mono f"
+  assumes "f x < f y"
+  obtains "x \<le> y"
+proof
+  show "x \<le> y"
+  proof (rule ccontr)
+    assume "\<not> x \<le> y"
+    then have "y \<le> x" by simp
+    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+    with \<open>f x < f y\<close> show False by simp
+  qed
+qed
+
+lemma mono_strict_invE:
+  fixes f :: "'a \<Rightarrow> 'b::order"
+  assumes "mono f"
+  assumes "f x < f y"
+  obtains "x < y"
+proof
+  show "x < y"
+  proof (rule ccontr)
+    assume "\<not> x < y"
+    then have "y \<le> x" by simp
+    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+    with \<open>f x < f y\<close> show False by simp
+  qed
+qed
+
+lemma strict_mono_eq:
+  assumes "strict_mono f"
+  shows "f x = f y \<longleftrightarrow> x = y"
+proof
+  assume "f x = f y"
+  show "x = y" proof (cases x y rule: linorder_cases)
+    case less with assms strict_monoD have "f x < f y" by auto
+    with \<open>f x = f y\<close> show ?thesis by simp
+  next
+    case equal then show ?thesis .
+  next
+    case greater with assms strict_monoD have "f y < f x" by auto
+    with \<open>f x = f y\<close> show ?thesis by simp
+  qed
+qed simp
+
+lemma strict_mono_less_eq:
+  assumes "strict_mono f"
+  shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
+proof
+  assume "x \<le> y"
+  with assms strict_mono_mono monoD show "f x \<le> f y" by auto
+next
+  assume "f x \<le> f y"
+  show "x \<le> y" proof (rule ccontr)
+    assume "\<not> x \<le> y" then have "y < x" by simp
+    with assms strict_monoD have "f y < f x" by auto
+    with \<open>f x \<le> f y\<close> show False by simp
+  qed
+qed
+
+lemma strict_mono_less:
+  assumes "strict_mono f"
+  shows "f x < f y \<longleftrightarrow> x < y"
+  using assms
+    by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
+
+end
+
 lemma strict_mono_inv:
   fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
   assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
@@ -1064,6 +1197,50 @@
   "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
   by (rule mono_onI, rule strict_mono_on_leD)
 
+lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
+  unfolding mono_def le_fun_def by auto
+
+lemma mono_add:
+  fixes a :: "'a::ordered_ab_semigroup_add" 
+  shows "mono ((+) a)"
+  by (simp add: add_left_mono monoI)
+
+lemma (in semilattice_inf) mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B"
+  for f :: "'a \<Rightarrow> 'b::semilattice_inf"
+  by (auto simp add: mono_def intro: Lattices.inf_greatest)
+
+lemma (in semilattice_sup) mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)"
+  for f :: "'a \<Rightarrow> 'b::semilattice_sup"
+  by (auto simp add: mono_def intro: Lattices.sup_least)
+
+lemma (in linorder) min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
+  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
+
+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) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
+  by (auto intro!: inj_onI dest: strict_mono_eq)
+
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+  by (fact mono_inf)
+
+lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
+  by (fact mono_sup)
+
+
+subsubsection \<open>Least value operator\<close>
+
+lemma Least_mono: "mono f \<Longrightarrow> \<exists>x\<in>S. \<forall>y\<in>S. x \<le> y \<Longrightarrow> (LEAST y. y \<in> f ` S) = f (LEAST x. x \<in> S)"
+  for f :: "'a::order \<Rightarrow> 'b::order"
+  \<comment> \<open>Courtesy of Stephan Merz\<close>
+  apply clarify
+  apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
+   apply fast
+  apply (rule LeastI2_order)
+    apply (auto elim: monoD intro!: order_antisym)
+  done
+
 
 subsection \<open>Setup\<close>
 
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Groups.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -639,11 +639,6 @@
 
 end
 
-lemma mono_add:
-  fixes a :: "'a::ordered_ab_semigroup_add" 
-  shows "mono ((+) a)"
-  by (simp add: add_left_mono monoI)
-
 text \<open>Strict monotonicity in both arguments\<close>
 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Lattices.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -220,9 +220,6 @@
 lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
   by (fast intro: inf_greatest le_infI1 le_infI2)
 
-lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
-  by (auto simp add: mono_def intro: Lattices.inf_greatest)
-
 end
 
 context semilattice_sup
@@ -249,9 +246,6 @@
 lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
   by (fast intro: sup_least le_supI1 le_supI2)
 
-lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
-  by (auto simp add: mono_def intro: Lattices.sup_least)
-
 end
 
 
@@ -610,12 +604,6 @@
   \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
   by (cases a b rule: linorder_cases) auto
 
-lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
-  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
-
-lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder"
-  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
-
 end
 
 lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)"
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Orderings.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -1063,28 +1063,6 @@
 context order
 begin
 
-definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
-  "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
-
-lemma monoI [intro?]:
-  fixes f :: "'a \<Rightarrow> 'b::order"
-  shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
-  unfolding mono_def by iprover
-
-lemma monoD [dest?]:
-  fixes f :: "'a \<Rightarrow> 'b::order"
-  shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
-  unfolding mono_def by iprover
-
-lemma monoE:
-  fixes f :: "'a \<Rightarrow> 'b::order"
-  assumes "mono f"
-  assumes "x \<le> y"
-  obtains "f x \<le> f y"
-proof
-  from assms show "f x \<le> f y" by (simp add: mono_def)
-qed
-
 definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
   "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
 
@@ -1107,107 +1085,6 @@
   from assms show "f x \<ge> f y" by (simp add: antimono_def)
 qed
 
-definition strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
-  "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
-
-lemma strict_monoI [intro?]:
-  assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
-  shows "strict_mono f"
-  using assms unfolding strict_mono_def by auto
-
-lemma strict_monoD [dest?]:
-  "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
-  unfolding strict_mono_def by auto
-
-lemma strict_mono_mono [dest?]:
-  assumes "strict_mono f"
-  shows "mono f"
-proof (rule monoI)
-  fix x y
-  assume "x \<le> y"
-  show "f x \<le> f y"
-  proof (cases "x = y")
-    case True then show ?thesis by simp
-  next
-    case False with \<open>x \<le> y\<close> have "x < y" by simp
-    with assms strict_monoD have "f x < f y" by auto
-    then show ?thesis by simp
-
-  qed
-qed
-
-end
-
-context linorder
-begin
-
-lemma mono_invE:
-  fixes f :: "'a \<Rightarrow> 'b::order"
-  assumes "mono f"
-  assumes "f x < f y"
-  obtains "x \<le> y"
-proof
-  show "x \<le> y"
-  proof (rule ccontr)
-    assume "\<not> x \<le> y"
-    then have "y \<le> x" by simp
-    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
-    with \<open>f x < f y\<close> show False by simp
-  qed
-qed
-
-lemma mono_strict_invE:
-  fixes f :: "'a \<Rightarrow> 'b::order"
-  assumes "mono f"
-  assumes "f x < f y"
-  obtains "x < y"
-proof
-  show "x < y"
-  proof (rule ccontr)
-    assume "\<not> x < y"
-    then have "y \<le> x" by simp
-    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
-    with \<open>f x < f y\<close> show False by simp
-  qed
-qed
-
-lemma strict_mono_eq:
-  assumes "strict_mono f"
-  shows "f x = f y \<longleftrightarrow> x = y"
-proof
-  assume "f x = f y"
-  show "x = y" proof (cases x y rule: linorder_cases)
-    case less with assms strict_monoD have "f x < f y" by auto
-    with \<open>f x = f y\<close> show ?thesis by simp
-  next
-    case equal then show ?thesis .
-  next
-    case greater with assms strict_monoD have "f y < f x" by auto
-    with \<open>f x = f y\<close> show ?thesis by simp
-  qed
-qed simp
-
-lemma strict_mono_less_eq:
-  assumes "strict_mono f"
-  shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
-proof
-  assume "x \<le> y"
-  with assms strict_mono_mono monoD show "f x \<le> f y" by auto
-next
-  assume "f x \<le> f y"
-  show "x \<le> y" proof (rule ccontr)
-    assume "\<not> x \<le> y" then have "y < x" by simp
-    with assms strict_monoD have "f y < f x" by auto
-    with \<open>f x \<le> f y\<close> show False by simp
-  qed
-qed
-
-lemma strict_mono_less:
-  assumes "strict_mono f"
-  shows "f x < f y \<longleftrightarrow> x < y"
-  using assms
-    by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
-
 end
 
 
@@ -1614,9 +1491,6 @@
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   by (rule le_funE)
 
-lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
-  unfolding mono_def le_fun_def by auto
-
 
 subsection \<open>Order on unary and binary predicates\<close>
 
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Set.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -666,9 +666,6 @@
 lemma IntE [elim!]: "c \<in> A \<inter> B \<Longrightarrow> (c \<in> A \<Longrightarrow> c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
-lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
-  by (fact mono_inf)
-
 
 subsubsection \<open>Binary union\<close>
 
@@ -700,9 +697,6 @@
 lemma insert_def: "insert a B = {x. x = a} \<union> B"
   by (simp add: insert_compr Un_def)
 
-lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
-  by (fact mono_sup)
-
 
 subsubsection \<open>Set difference\<close>
 
@@ -1808,19 +1802,6 @@
 qed
 
 
-subsubsection \<open>Least value operator\<close>
-
-lemma Least_mono: "mono f \<Longrightarrow> \<exists>x\<in>S. \<forall>y\<in>S. x \<le> y \<Longrightarrow> (LEAST y. y \<in> f ` S) = f (LEAST x. x \<in> S)"
-  for f :: "'a::order \<Rightarrow> 'b::order"
-  \<comment> \<open>Courtesy of Stephan Merz\<close>
-  apply clarify
-  apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
-   apply fast
-  apply (rule LeastI2_order)
-    apply (auto elim: monoD intro!: order_antisym)
-  done
-
-
 subsubsection \<open>Monad operation\<close>
 
 definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
diff -r 6d4fb57eb66c -r a4b47c684445 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Jun 25 13:21:27 2022 +0200
@@ -399,7 +399,8 @@
   (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
     [] []
     (HOLogic.mk_Trueprop
-      (Const (\<^const_name>\<open>Orderings.mono\<close>, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
+      (\<^Const>\<open>monotone_on predT predT for
+          \<^Const>\<open>top \<^Type>\<open>set predT\<close>\<close> \<^Const>\<open>less_eq predT\<close> \<^Const>\<open>less_eq predT\<close> fp_fun\<close>))
     (fn _ => EVERY [resolve_tac ctxt @{thms monoI} 1,
       REPEAT (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST