# HG changeset patch
# User desharna
# Date 1655811546 -7200
# Node ID 6fb4a0829cc41bb03e7cef4075a6e244147bdd17
# Parent  d32201f08e98721aa8fbceafe285d25c56ee4d7d
added predicate monotone_on and redefined monotone to be an abbreviation.

diff -r d32201f08e98 -r 6fb4a0829cc4 NEWS
--- a/NEWS	Mon Jun 20 11:06:33 2022 +0200
+++ b/NEWS	Tue Jun 21 13:39:06 2022 +0200
@@ -40,8 +40,16 @@
 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
 longer. INCOMPATIBILITY.
 
+* Theory "HOL.Fun":
+  - 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.
+  - Added lemmas.
+      monotone_onD
+      monotone_onI
+
 * Theory "HOL.Relation":
-  - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+  - Added predicate reflp_on and redefined reflp to be an abbreviation.
     Lemma reflp_def is explicitly provided for backward compatibility
     but its usage is discouraged. Minor INCOMPATIBILITY.
   - Added predicate totalp_on and abbreviation totalp.
diff -r d32201f08e98 -r 6fb4a0829cc4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jun 20 11:06:33 2022 +0200
+++ b/src/HOL/Fun.thy	Tue Jun 21 13:39:06 2022 +0200
@@ -927,8 +927,34 @@
   then show False by blast
 qed
 
+
 subsection \<open>Monotonic functions over a set\<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))"
+
+abbreviation monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "monotone \<equiv> monotone_on UNIV"
+
+lemma monotone_def[no_atp]: "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
+  by (simp add: monotone_on_def)
+
+text \<open>Lemma @{thm [source] monotone_def} is provided for backward compatibility.\<close>
+
+lemma monotone_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone_on A orda ordb f"
+  by (simp add: monotone_on_def)
+
+lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
+  by (rule monotone_onI)
+
+lemma monotone_onD:
+  "monotone_on A orda ordb f \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
+  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)
+
 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 mono_onI:
diff -r d32201f08e98 -r 6fb4a0829cc4 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Jun 20 11:06:33 2022 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jun 21 13:39:06 2022 +0200
@@ -373,9 +373,9 @@
       | NONE => NONE
   in
     case Thm.term_of ct of
-      t as Const (\<^const_name>\<open>ccpo.admissible\<close>, _) $ _ $ _ $ _ => mk_thm t
-    | t as Const (\<^const_name>\<open>mcont\<close>, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
-    | t as Const (\<^const_name>\<open>monotone\<close>, _) $ _ $ _ $ _ => mk_thm t
+      t as \<^Const_>\<open>ccpo.admissible _ for _ _ _\<close> => mk_thm t
+    | t as \<^Const_>\<open>mcont _ _ for _ _ _ _ _\<close> => mk_thm t
+    | t as \<^Const_>\<open>monotone_on _ _ for \<^Const_>\<open>Orderings.top _\<close> _ _ _\<close> => mk_thm t
     | _ => NONE
   end
   handle THM _ => NONE 
diff -r d32201f08e98 -r 6fb4a0829cc4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jun 20 11:06:33 2022 +0200
+++ b/src/HOL/Orderings.thy	Tue Jun 21 13:39:06 2022 +0200
@@ -1060,15 +1060,6 @@
 
 subsection \<open>Monotonicity\<close>
 
-definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
-
-lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
-  unfolding monotone_def by iprover
-
-lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
-  unfolding monotone_def by iprover
-
 context order
 begin