# HG changeset patch
# User desharna
# Date 1653482386 -7200
# Node ID 84e6f9b542e2a2d8b3466fae8768438ffb7fcfad
# Parent  8e2285baadba7faea98ca1be44f518f18d97f33a
move monotone from Complete_Partial_Order to Orderings

diff -r 8e2285baadba -r 84e6f9b542e2 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Wed May 25 10:57:07 2022 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Wed May 25 14:39:46 2022 +0200
@@ -9,19 +9,6 @@
   imports Product_Type
 begin
 
-subsection \<open>Monotone functions\<close>
-
-text \<open>Dictionary-passing version of \<^const>\<open>Orderings.mono\<close>.\<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
-
 
 subsection \<open>Chains\<close>
 
diff -r 8e2285baadba -r 84e6f9b542e2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed May 25 10:57:07 2022 +0100
+++ b/src/HOL/Orderings.thy	Wed May 25 14:39:46 2022 +0200
@@ -1060,6 +1060,15 @@
 
 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