# HG changeset patch
# User hoelzl
# Date 1384280934 -3600
# Node ID 72949fae4f817e4ace0556c5717481ba8b70ee28
# Parent  88a036a95967f890ad286ce5f62d5730b45e2f35
add equalities for SUP and INF over constant functions

diff -r 88a036a95967 -r 72949fae4f81 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Nov 12 19:28:54 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Nov 12 19:28:54 2013 +0100
@@ -418,6 +418,22 @@
 lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
   unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
 
+lemma SUP_eq_const:
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
+  by (auto intro: SUP_eqI)
+
+lemma INF_eq_const:
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFI I f = x"
+  by (auto intro: INF_eqI)
+
+lemma SUP_eq_iff:
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPR I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+  using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
+
+lemma INF_eq_iff:
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFI I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+  using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
+
 end
 
 class complete_distrib_lattice = complete_lattice +