# HG changeset patch
# User desharna
# Date 1656098255 -7200
# Node ID da901dcafc2952be3709c60f102b1567c3f28daf
# Parent  19ec8f844e08fc0d8baf71512249399e67268d57# Parent  0f7cb6cd08fe6d1eaa695794e76f0e576c13660e
merged

diff -r 0f7cb6cd08fe -r da901dcafc29 NEWS
--- a/NEWS	Thu Jun 23 23:42:47 2022 +0200
+++ b/NEWS	Fri Jun 24 21:17:35 2022 +0200
@@ -47,10 +47,15 @@
   - Added predicate monotone_on and redefined monotone to be an
     abbreviation. Lemma monotone_def is explicitly provided for backward
     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
   - Added lemmas.
       monotone_onD
       monotone_onI
       monotone_on_empty[simp]
+      monotone_on_o
       monotone_on_subset
 
 * Theory "HOL.Relation":
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -29,14 +29,14 @@
 qed
 
 proposition mono_on_imp_deriv_nonneg:
-  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
+  assumes mono: "mono_on A f" and deriv: "(f has_real_derivative D) (at x)"
   assumes "x \<in> interior A"
   shows "D \<ge> 0"
 proof (rule tendsto_lowerbound)
   let ?A' = "(\<lambda>y. y - x) ` interior A"
   from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
       by (simp add: field_has_derivative_at has_field_derivative_def)
-  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
+  from mono have mono': "mono_on (interior A) f" by (rule mono_on_subset) (rule interior_subset)
 
   show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
   proof (subst eventually_at_topological, intro exI conjI ballI impI)
@@ -58,11 +58,11 @@
 proposition mono_on_ctble_discont:
   fixes f :: "real \<Rightarrow> real"
   fixes A :: "real set"
-  assumes "mono_on f A"
+  assumes "mono_on A f"
   shows "countable {a\<in>A. \<not> continuous (at a within A) f}"
 proof -
   have mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
-    using \<open>mono_on f A\<close> by (simp add: mono_on_def)
+    using \<open>mono_on A f\<close> by (simp add: mono_on_def)
   have "\<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}. \<exists>q :: nat \<times> rat.
       (fst q = 0 \<and> of_rat (snd q) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd q))) \<or>
       (fst q = 1 \<and> of_rat (snd q) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd q)))"
@@ -125,7 +125,7 @@
 lemma mono_on_ctble_discont_open:
   fixes f :: "real \<Rightarrow> real"
   fixes A :: "real set"
-  assumes "open A" "mono_on f A"
+  assumes "open A" "mono_on A f"
   shows "countable {a\<in>A. \<not>isCont f a}"
 proof -
   have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}"
@@ -139,7 +139,7 @@
   fixes f :: "real \<Rightarrow> real"
   assumes "mono f"
   shows "countable {a. \<not> isCont f a}"
-  using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto
+  using assms mono_on_ctble_discont [of UNIV f] unfolding mono_on_def mono_def by auto
 
 lemma has_real_derivative_imp_continuous_on:
   assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
@@ -1819,7 +1819,7 @@
 
 lemma borel_measurable_mono_on_fnc:
   fixes f :: "real \<Rightarrow> real" and A :: "real set"
-  assumes "mono_on f A"
+  assumes "mono_on A f"
   shows "f \<in> borel_measurable (restrict_space borel A)"
   apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
   apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
@@ -1830,14 +1830,14 @@
 
 lemma borel_measurable_piecewise_mono:
   fixes f::"real \<Rightarrow> real" and C::"real set set"
-  assumes "countable C" "\<And>c. c \<in> C \<Longrightarrow> c \<in> sets borel" "\<And>c. c \<in> C \<Longrightarrow> mono_on f c" "(\<Union>C) = UNIV"
+  assumes "countable C" "\<And>c. c \<in> C \<Longrightarrow> c \<in> sets borel" "\<And>c. c \<in> C \<Longrightarrow> mono_on c f" "(\<Union>C) = UNIV"
   shows "f \<in> borel_measurable borel"
   by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms)
 
 lemma borel_measurable_mono:
   fixes f :: "real \<Rightarrow> real"
   shows "mono f \<Longrightarrow> f \<in> borel_measurable borel"
-  using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def)
+  using borel_measurable_mono_on_fnc[of UNIV f] by (simp add: mono_def mono_on_def)
 
 lemma measurable_bdd_below_real[measurable (raw)]:
   fixes F :: "'a \<Rightarrow> 'i \<Rightarrow> real"
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -1587,7 +1587,7 @@
 (*Can these be generalised from type real?*)
 lemma integrable_mono_on_nonneg:
   fixes f :: "real \<Rightarrow> real"
-  assumes mon: "mono_on f {a..b}" and 0: "\<And>x. 0 \<le> f x"
+  assumes mon: "mono_on {a..b} f" and 0: "\<And>x. 0 \<le> f x"
   shows "integrable (lebesgue_on {a..b}) f" 
 proof -
   have "space lborel = space lebesgue" "sets borel \<subseteq> sets lebesgue"
@@ -1641,11 +1641,11 @@
 
 lemma integrable_mono_on:
   fixes f :: "real \<Rightarrow> real"
-  assumes "mono_on f {a..b}" 
+  assumes "mono_on {a..b} f"
   shows "integrable (lebesgue_on {a..b}) f" 
 proof -
   define f' where "f' \<equiv> \<lambda>x. if x \<in> {a..b} then f x - f a else 0"
-  have "mono_on f' {a..b}"
+  have "mono_on {a..b} f'"
     by (smt (verit, best) assms f'_def mono_on_def)
   moreover have 0: "\<And>x. 0 \<le> f' x"
     by (smt (verit, best) assms atLeastAtMost_iff f'_def mono_on_def)
@@ -1663,7 +1663,7 @@
 
 lemma integrable_on_mono_on:
   fixes f :: "real \<Rightarrow> real"
-  assumes "mono_on f {a..b}" 
+  assumes "mono_on {a..b} f"
   shows "f integrable_on {a..b}"
   by (simp add: assms integrable_mono_on integrable_on_lebesgue_on) 
 
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Fun.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -953,7 +953,7 @@
   by (simp add: monotone_on_def)
 
 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
-  by (simp add: monotone_onD)
+  by (rule monotone_onD[of UNIV, simplified])
 
 lemma monotone_on_subset: "monotone_on A orda ordb f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> monotone_on B orda ordb f"
   by (auto intro: monotone_onI dest: monotone_onD)
@@ -961,34 +961,58 @@
 lemma monotone_on_empty[simp]: "monotone_on {} orda ordb f"
   by (auto intro: monotone_onI dest: monotone_onD)
 
-definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
+lemma monotone_on_o:
+  assumes
+    mono_f: "monotone_on A orda ordb f" and
+    mono_g: "monotone_on B ordc orda g" and
+    "g ` B \<subseteq> A"
+  shows "monotone_on B ordc ordb (f \<circ> g)"
+proof (rule monotone_onI)
+  fix x y assume "x \<in> B" and "y \<in> B" and "ordc x y"
+  hence "orda (g x) (g y)"
+    by (rule mono_g[THEN monotone_onD])
+  moreover from \<open>g ` B \<subseteq> A\<close> \<open>x \<in> B\<close> \<open>y \<in> B\<close> have "g x \<in> A" and "g y \<in> A"
+    unfolding image_subset_iff by simp_all
+  ultimately show "ordb ((f \<circ> g) x) ((f \<circ> g) y)"
+    using mono_f[THEN monotone_onD] by simp
+qed
+
+abbreviation mono_on :: "('a :: ord) 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)"
+  by (auto simp add: monotone_on_def)
 
 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 f A"
-  unfolding mono_on_def by simp
+  "(\<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 f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
-  unfolding mono_on_def by simp
+  "\<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 f A"
+lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
   unfolding mono_def mono_on_def by auto
 
-lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
-  unfolding mono_on_def by auto
+lemma mono_on_subset: "mono_on A f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on B f"
+  by (rule monotone_on_subset)
 
-definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
+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 f A"
-  unfolding strict_mono_on_def by simp
+  "(\<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 f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
-  unfolding strict_mono_on_def by simp
+  "\<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_greaterD:
-  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
+  assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
   shows "x > y"
 proof (rule ccontr)
   assume "\<not>x > y"
@@ -1009,7 +1033,7 @@
 qed
 
 lemma strict_mono_on_imp_inj_on:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
+  assumes "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder))"
   shows "inj_on f A"
 proof (rule inj_onI)
   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
@@ -1019,7 +1043,7 @@
 qed
 
 lemma strict_mono_on_leD:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
+  assumes "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder)" "x \<in> A" "y \<in> A" "x \<le> y"
   shows "f x \<le> f y"
 proof (insert le_less_linear[of y x], elim disjE)
   assume "x < y"
@@ -1029,12 +1053,12 @@
 
 lemma strict_mono_on_eqD:
   fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
-  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
+  assumes "strict_mono_on A f" "f x = f y" "x \<in> A" "y \<in> A"
   shows "y = x"
   using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
 
 lemma strict_mono_on_imp_mono_on:
-  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
+  "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
   by (rule mono_onI, rule strict_mono_on_leD)
 
 
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -425,7 +425,7 @@
 lemma strict_mono_inv_on_range:
   fixes f :: "'a::linorder \<Rightarrow> 'b::order"
   assumes "strict_mono f"
-  shows "strict_mono_on (inv f) (range f)"
+  shows "strict_mono_on (range f) (inv f)"
 proof (clarsimp simp: strict_mono_on_def)
   fix x y
   assume "f x < f y"
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -467,7 +467,7 @@
 
 lemma finite_enumerate:
   assumes fS: "finite S"
-  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on r {..<card S} \<and> (\<forall>n<card S. r n \<in> S)"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on {..<card S} r \<and> (\<forall>n<card S. r n \<in> S)"
   unfolding strict_mono_def
   using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
   by (metis lessThan_iff strict_mono_on_def)
@@ -603,11 +603,11 @@
 lemma ex_bij_betw_strict_mono_card:
   fixes M :: "'a::wellorder set"
   assumes "finite M" 
-  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
+  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
 proof
   show "bij_betw (enumerate M) {..<card M} M"
     by (simp add: assms finite_bij_enumerate)
-  show "strict_mono_on (enumerate M) {..<card M}"
+  show "strict_mono_on {..<card M} (enumerate M)"
     by (simp add: assms finite_enumerate_mono strict_mono_on_def)
 qed
 
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -87,14 +87,14 @@
   assumes nonnegf: "\<And>x. f x \<ge> 0"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"
-  assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
+  assumes mono: "strict_mono_on {a..b} g" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
   assumes range: "{a..b} \<subseteq> range h"
   shows "emeasure (distr (density lborel f) lborel h) {a..b} =
              emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
 proof (cases "a < b")
   assume "a < b"
   from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
-  from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
+  from mono have mono': "mono_on {a..b} g" by (rule strict_mono_on_imp_mono_on)
   from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
     by (rule mono_on_imp_deriv_nonneg) auto
   from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
diff -r 0f7cb6cd08fe -r da901dcafc29 src/HOL/Probability/Weak_Convergence.thy
--- a/src/HOL/Probability/Weak_Convergence.thy	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -65,7 +65,7 @@
 lemma pseudoinverse': "\<forall>\<omega>\<in>{a<..<b}. \<forall>x. \<omega> \<le> f x \<longleftrightarrow> I \<omega> \<le> x"
   by (intro ballI allI impI pseudoinverse) auto
 
-lemma mono_I: "mono_on I {a <..< b}"
+lemma mono_I: "mono_on {a <..< b} I"
   unfolding mono_on_def by (metis order.trans order.refl pseudoinverse')
 
 end