# HG changeset patch
# User desharna
# Date 1655811635 -7200
# Node ID 451e17e0ba9d0bfcd0d90035613f1cdbb3eb7bef
# Parent  6fb4a0829cc41bb03e7cef4075a6e244147bdd17
added lemmas monotone_on_empty[simp] and monotone_on_subset

diff -r 6fb4a0829cc4 -r 451e17e0ba9d NEWS
--- a/NEWS	Tue Jun 21 13:39:06 2022 +0200
+++ b/NEWS	Tue Jun 21 13:40:35 2022 +0200
@@ -47,6 +47,8 @@
   - Added lemmas.
       monotone_onD
       monotone_onI
+      monotone_on_empty[simp]
+      monotone_on_subset
 
 * Theory "HOL.Relation":
   - Added predicate reflp_on and redefined reflp to be an abbreviation.
diff -r 6fb4a0829cc4 -r 451e17e0ba9d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jun 21 13:39:06 2022 +0200
+++ b/src/HOL/Fun.thy	Tue Jun 21 13:40:35 2022 +0200
@@ -955,6 +955,12 @@
 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
   by (simp add: monotone_onD)
 
+lemma monotone_on_subset: "monotone_on A orda ordb f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> monotone_on B orda ordb f"
+  by (auto intro: monotone_onI dest: monotone_onD)
+
+lemma monotone_on_empty[simp]: "monotone_on {} orda ordb f"
+  by (auto intro: monotone_onI dest: 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: