# HG changeset patch
# User haftmann
# Date 1394697367 -3600
# Node ID 30a60277aa6eebfde8f592e0a3d330e22c1f8c5e
# Parent  29e308b56d23a4e56517b97936cd4bce6d50be10
monotonicity in complete lattices

diff -r 29e308b56d23 -r 30a60277aa6e src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Mar 13 07:07:07 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Mar 13 08:56:07 2014 +0100
@@ -503,6 +503,21 @@
   "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
 
+context
+  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes "mono f"
+begin
+
+lemma mono_Inf:
+  shows "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
+  using `mono f` by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)
+
+lemma mono_Sup:
+  shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
+  using `mono f` by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
+
+end
+
 end
 
 class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice