--- a/NEWS Sun Mar 30 20:20:27 2025 +0200
+++ b/NEWS Mon Mar 31 22:46:18 2025 +0100
@@ -35,10 +35,17 @@
* Theory "HOL.Fun":
- Added lemmas.
+ mono_on_strict_invE
+ mono_on_invE
+ strict_mono_on_eq
+ strict_mono_on_less_eq
+ strict_mono_on_less
antimonotone_on_inf_fun
antimonotone_on_sup_fun
monotone_on_inf_fun
monotone_on_sup_fun
+ - Removed lemmas. Minor INCOMPATIBILITY.
+ mono_on_greaterD (use mono_invE instead)
* Theory "HOL.Relation":
- Changed definition of predicate refl_on to not constrain the domain
--- a/src/HOL/Fun.thy Sun Mar 30 20:20:27 2025 +0200
+++ b/src/HOL/Fun.thy Mon Mar 31 22:46:18 2025 +0100
@@ -1041,10 +1041,10 @@
where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
abbreviation antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
- where "antimono_on A \<equiv> monotone_on A (\<le>) (\<ge>)"
+ where "antimono_on A \<equiv> monotone_on A (\<le>) (\<lambda>x y. y \<le> x)"
abbreviation strict_antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
- where "strict_antimono_on A \<equiv> monotone_on A (<) (>)"
+ where "strict_antimono_on A \<equiv> monotone_on A (<) (\<lambda>x y. y < x)"
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)
@@ -1075,17 +1075,6 @@
end
-lemma mono_on_greaterD:
- fixes g :: "'a::linorder \<Rightarrow> 'b::linorder"
- assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > g y"
- shows "x > y"
-proof (rule ccontr)
- assume "\<not>x > y"
- hence "x \<le> y" by (simp add: not_less)
- from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
- with assms(4) show False by simp
-qed
-
context order begin
abbreviation mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
@@ -1144,62 +1133,54 @@
from assms show "f x \<ge> f y" by (simp add: antimono_def)
qed
+end
+
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
+lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \<Longrightarrow> mono_on A f"
+ for f :: "'a::order \<Rightarrow> 'b::preorder"
+proof (intro mono_onI)
+ fix r s :: 'a assume asm: "r \<le> s" "strict_mono_on A f" "r \<in> A" "s \<in> A"
+ from this(1) consider "r < s" | "r = s" by fastforce
+ then show "f r \<le> f s"
+ proof(cases)
+ case 1
+ from strict_mono_onD[OF asm(2-4) this] show ?thesis by (fact order.strict_implies_order)
+ qed simp
qed
+lemma strict_mono_mono [dest?]:
+ "strict_mono f \<Longrightarrow> mono f"
+ by (fact strict_mono_on_imp_mono_on)
+
lemma mono_on_ident: "mono_on S (\<lambda>x. x)"
- by (simp add: monotone_on_def)
+ by (intro monotone_onI)
+
+lemma mono_on_id: "mono_on S id"
+ unfolding id_def by (fact mono_on_ident)
lemma strict_mono_on_ident: "strict_mono_on S (\<lambda>x. x)"
- by (simp add: monotone_on_def)
+ by (intro monotone_onI)
+
+lemma strict_mono_on_id: "strict_mono_on S id"
+ unfolding id_def by (fact strict_mono_on_ident)
lemma mono_on_const:
- fixes a :: "'b::order" shows "mono_on S (\<lambda>x. a)"
- by (simp add: mono_on_def)
+ fixes a :: "'b::preorder" shows "mono_on S (\<lambda>x. a)"
+ by (intro monotone_onI order.refl)
lemma antimono_on_const:
- fixes a :: "'b::order" shows "antimono_on S (\<lambda>x. a)"
- by (simp add: monotone_on_def)
+ fixes a :: "'b::preorder" shows "antimono_on S (\<lambda>x. a)"
+ by (intro monotone_onI order.refl)
-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"
+lemma mono_on_strict_invE:
+ fixes f :: "'a \<Rightarrow> 'b::preorder"
+ assumes "mono_on S f"
+ assumes "x \<in> S" "y \<in> S"
assumes "f x < f y"
obtains "x < y"
proof
@@ -1207,47 +1188,68 @@
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
+ with \<open>mono_on S f\<close> \<open>x \<in> S\<close> \<open>y \<in> S\<close> have "f y \<le> f x" by (simp only: monotone_onD)
+ with \<open>f x < f y\<close> show False by (simp add: preorder_class.less_le_not_le)
qed
qed
-lemma strict_mono_eq:
- assumes "strict_mono f"
+corollary mono_on_invE:
+ fixes f :: "'a \<Rightarrow> 'b::preorder"
+ assumes "mono_on S f"
+ assumes "x \<in> S" "y \<in> S"
+ assumes "f x < f y"
+ obtains "x \<le> y"
+ using assms mono_on_strict_invE[of S f x y thesis] by simp
+
+lemma strict_mono_on_eq:
+ assumes "strict_mono_on S (f::'a \<Rightarrow> 'b::preorder)"
+ assumes "x \<in> S" "y \<in> S"
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
+ case less with assms have "f x < f y" by (simp add: monotone_onD)
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
+ case greater with assms have "f y < f x" by (simp add: monotone_onD)
with \<open>f x = f y\<close> show ?thesis by simp
qed
qed simp
-lemma strict_mono_less_eq:
- assumes "strict_mono f"
+lemma strict_mono_on_less_eq:
+ assumes "strict_mono_on S (f::'a \<Rightarrow> 'b::preorder)"
+ assumes "x \<in> S" "y \<in> S"
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
+ then show "f x \<le> f y"
+ using nless_le[of x y] monotone_onD[OF assms] order_less_imp_le[of "f x" "f y"]
+ by blast
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
+ show "x \<le> y"
+ proof (rule ccontr)
+ assume "\<not> x \<le> y"
+ then have "y < x" by simp
+ with assms have "f y < f x" by (simp add: monotone_onD)
+ with \<open>f x \<le> f y\<close> show False by (simp add: preorder_class.less_le_not_le)
qed
qed
-lemma strict_mono_less:
- assumes "strict_mono f"
+lemma strict_mono_on_less:
+ assumes "strict_mono_on S (f::'a \<Rightarrow> _::preorder)"
+ assumes "x \<in> S" "y \<in> S"
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)
+ using assms strict_mono_on_eq[of S f x y]
+ by (auto simp add: strict_mono_on_less_eq preorder_class.less_le_not_le)
+
+lemmas mono_invE = mono_on_invE[OF _ UNIV_I UNIV_I]
+lemmas mono_strict_invE = mono_on_strict_invE[OF _ UNIV_I UNIV_I]
+lemmas strict_mono_eq = strict_mono_on_eq[OF _ UNIV_I UNIV_I]
+lemmas strict_mono_less_eq = strict_mono_on_less_eq[OF _ UNIV_I UNIV_I]
+lemmas strict_mono_less = strict_mono_on_less[OF _ UNIV_I UNIV_I]
end
@@ -1274,7 +1276,7 @@
qed
lemma strict_mono_on_leD:
- fixes f :: "'a::linorder \<Rightarrow> 'b::preorder"
+ fixes f :: "'a::order \<Rightarrow> 'b::preorder"
assumes "strict_mono_on A f" "x \<in> A" "y \<in> A" "x \<le> y"
shows "f x \<le> f y"
proof (cases "x = y")
@@ -1293,10 +1295,6 @@
shows "y = x"
using assms by (cases rule: linorder_cases) (auto dest: strict_mono_onD)
-lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \<Longrightarrow> mono_on A f"
- for f :: "'a::linorder \<Rightarrow> 'b::preorder"
- by (rule mono_onI, rule strict_mono_on_leD)
-
lemma mono_imp_strict_mono:
fixes f :: "'a::order \<Rightarrow> 'b::order"
shows "\<lbrakk>mono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_mono_on S f"
--- a/src/HOL/Nat.thy Sun Mar 30 20:20:27 2025 +0200
+++ b/src/HOL/Nat.thy Mon Mar 31 22:46:18 2025 +0100
@@ -1986,7 +1986,7 @@
("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
\<open>K (try o Nat_Arith.cancel_diff_conv)\<close>
-context order
+context preorder
begin
lemma lift_Suc_mono_le:
@@ -1996,7 +1996,7 @@
proof (cases "n < n'")
case True
then show ?thesis
- by (induct n n' rule: less_Suc_induct) (auto intro: mono)
+ by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans)
next
case False
with \<open>n \<le> n'\<close> show ?thesis by auto
@@ -2009,7 +2009,7 @@
proof (cases "n < n'")
case True
then show ?thesis
- by (induct n n' rule: less_Suc_induct) (auto intro: mono)
+ by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans)
next
case False
with \<open>n \<le> n'\<close> show ?thesis by auto
@@ -2019,7 +2019,7 @@
assumes mono: "\<And>n. f n < f (Suc n)"
and "n < n'"
shows "f n < f n'"
- using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
+ using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono order.strict_trans)
lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
by (blast intro: less_asym' lift_Suc_mono_less [of f]