changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
--- a/NEWS Wed Jun 22 14:52:27 2022 +0200
+++ b/NEWS Thu Jun 23 19:29:22 2022 +0200
@@ -44,6 +44,9 @@
- 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. Minor INCOMPATIBILITY
- Added lemmas.
monotone_onD
monotone_onI
--- a/src/HOL/Analysis/Borel_Space.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Jun 23 19:29:22 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"
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jun 23 19:29:22 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)
--- a/src/HOL/Fun.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Fun.thy Thu Jun 23 19:29:22 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,34 @@
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"
+definition "mono_on A f \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
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"
+ "(\<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"
unfolding mono_on_def by simp
lemma mono_onD:
- "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
+ "\<lbrakk>mono_on A f; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
unfolding mono_on_def by simp
-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"
+lemma mono_on_subset: "mono_on A f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on B f"
unfolding mono_on_def by auto
-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"
+definition "strict_mono_on A f \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < 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 f A"
+ "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on A f"
unfolding strict_mono_on_def by simp
lemma strict_mono_onD:
- "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
+ "\<lbrakk>strict_mono_on A f; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
unfolding strict_mono_on_def by simp
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 +1009,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 +1019,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 +1029,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)
--- a/src/HOL/Hilbert_Choice.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Jun 23 19:29:22 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"
--- a/src/HOL/Library/Infinite_Set.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Thu Jun 23 19:29:22 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
--- a/src/HOL/Probability/Giry_Monad.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Thu Jun 23 19:29:22 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"
--- a/src/HOL/Probability/Weak_Convergence.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy Thu Jun 23 19:29:22 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