# HG changeset patch
# User desharna
# Date 1740495281 -3600
# Node ID b1af763166f424fe9a3a8b992d60e8d358b57a0b
# Parent  62c039ce397c4d2dad787f205065deee4a264d72
added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)

diff -r 62c039ce397c -r b1af763166f4 NEWS
--- a/NEWS	Tue Feb 25 14:23:25 2025 +0100
+++ b/NEWS	Tue Feb 25 15:54:41 2025 +0100
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+* Theory "HOL.Fun":
+  - Added lemmas.
+      antimonotone_on_inf_fun
+      antimonotone_on_sup_fun
+      monotone_on_inf_fun
+      monotone_on_sup_fun
 
 
 New in Isabelle2025 (March 2025)
diff -r 62c039ce397c -r b1af763166f4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Feb 25 14:23:25 2025 +0100
+++ b/src/HOL/Fun.thy	Tue Feb 25 15:54:41 2025 +0100
@@ -1339,6 +1339,26 @@
   for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
+lemma monotone_on_sup_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+  shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<squnion> g)"
+  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma monotone_on_inf_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+  shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<sqinter> g)"
+  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
+lemma antimonotone_on_sup_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+  shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<squnion> g)"
+  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma antimonotone_on_inf_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+  shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<sqinter> g)"
+  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
 lemma (in linorder) min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)