author hoelzl Tue, 12 Nov 2013 19:28:54 +0100 changeset 54414 72949fae4f81 parent 54413 88a036a95967 child 54415 eaf25431d4c4
add equalities for SUP and INF over constant functions
```--- 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 +```