# HG changeset patch
# User desharna
# Date 1656060580 -7200
# Node ID 19ec8f844e08fc0d8baf71512249399e67268d57
# Parent  6c542e152b8a07c852a4138699ca2bb6a49fef97
added lemma monotone_on_o

diff -r 6c542e152b8a -r 19ec8f844e08 NEWS
--- a/NEWS	Fri Jun 24 15:05:04 2022 +0200
+++ b/NEWS	Fri Jun 24 10:49:40 2022 +0200
@@ -52,6 +52,7 @@
       monotone_onD
       monotone_onI
       monotone_on_empty[simp]
+      monotone_on_o
       monotone_on_subset
 
 * Theory "HOL.Relation":
diff -r 6c542e152b8a -r 19ec8f844e08 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jun 24 15:05:04 2022 +0200
+++ b/src/HOL/Fun.thy	Fri Jun 24 10:49:40 2022 +0200
@@ -961,6 +961,22 @@
 lemma monotone_on_empty[simp]: "monotone_on {} orda ordb f"
   by (auto intro: monotone_onI dest: monotone_onD)
 
+lemma monotone_on_o:
+  assumes
+    mono_f: "monotone_on A orda ordb f" and
+    mono_g: "monotone_on B ordc orda g" and
+    "g ` B \<subseteq> A"
+  shows "monotone_on B ordc ordb (f \<circ> g)"
+proof (rule monotone_onI)
+  fix x y assume "x \<in> B" and "y \<in> B" and "ordc x y"
+  hence "orda (g x) (g y)"
+    by (rule mono_g[THEN monotone_onD])
+  moreover from \<open>g ` B \<subseteq> A\<close> \<open>x \<in> B\<close> \<open>y \<in> B\<close> have "g x \<in> A" and "g y \<in> A"
+    unfolding image_subset_iff by simp_all
+  ultimately show "ordb ((f \<circ> g) x) ((f \<circ> g) y)"
+    using mono_f[THEN monotone_onD] by simp
+qed
+
 abbreviation mono_on :: "('a :: ord) set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
   where "mono_on A \<equiv> monotone_on A (\<le>) (\<le>)"