# HG changeset patch
# User paulson
# Date 1743457578 -3600
# Node ID e9089202f3dfec521471a83c0ab707be142afe94
# Parent  ec39ec5447e68f8a53a918f15f85eeae49712b68# Parent  558bff66be22b8970b0a7bc71bdbcbe193764634
merged

diff -r ec39ec5447e6 -r e9089202f3df NEWS
--- 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
diff -r ec39ec5447e6 -r e9089202f3df src/HOL/Fun.thy
--- 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"
diff -r ec39ec5447e6 -r e9089202f3df src/HOL/Nat.thy
--- 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]