# HG changeset patch
# User haftmann
# Date 1310928411 -7200
# Node ID 79c3231e0593635639e56e8e5ac684b05f1d6dcf
# Parent  92129f50512526cbb4aa3836556e31dc79b7f531
more lemmas about SUP

diff -r 92129f505125 -r 79c3231e0593 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:29:54 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:46:51 2011 +0200
@@ -293,11 +293,7 @@
 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
   by (iprover intro: SUP_leI le_SUPI order_trans antisym)
 
-lemma (in complete_lattice) INFI_empty:
-  "(\<Sqinter>x\<in>{}. B x) = \<top>"
-  by (simp add: INFI_def)
-
-lemma (in complete_lattice) INFI_absorb:
+lemma INF_absorb:
   assumes "k \<in> I"
   shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
 proof -
@@ -305,36 +301,74 @@
   then show ?thesis by (simp add: INF_insert)
 qed
 
-lemma (in complete_lattice) INF_union:
+lemma SUP_absorb:
+  assumes "k \<in> I"
+  shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
+proof -
+  from assms obtain J where "I = insert k J" by blast
+  then show ?thesis by (simp add: SUP_insert)
+qed
+
+lemma INF_union:
   "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
 
-lemma (in complete_lattice) INF_constant:
+lemma SUP_union:
+  "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
+  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUPI)
+
+lemma INF_constant:
   "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   by (simp add: INF_empty)
 
-lemma (in complete_lattice) INF_eq:
+lemma SUP_constant:
+  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
+  by (simp add: SUP_empty)
+
+lemma INF_eq:
   "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
   by (simp add: INFI_def image_def)
 
-lemma (in complete_lattice) INF_top_conv:
+lemma SUP_eq:
+  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
+  by (simp add: SUPR_def image_def)
+
+lemma INF_top_conv:
  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
  "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   by (auto simp add: INFI_def Inf_top_conv)
 
-lemma (in complete_lattice) INFI_UNIV_range:
-  "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
-  by (simp add: INFI_def)
+lemma SUP_bot_conv:
+ "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+ "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+  by (auto simp add: SUPR_def Sup_bot_conv)
 
-lemma (in complete_lattice) INF_bool_eq:
+lemma (in complete_lattice) INF_UNIV_range:
+  "(\<Sqinter>x. f x) = \<Sqinter>range f"
+  by (fact INFI_def)
+
+lemma (in complete_lattice) SUP_UNIV_range:
+  "(\<Squnion>x. f x) = \<Squnion>range f"
+  by (fact SUPR_def)
+
+lemma INF_bool_eq:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
 
-lemma (in complete_lattice) INF_anti_mono:
+lemma SUP_bool_eq:
+  "(\<Squnion>b. A b) = A True \<squnion> A False"
+  by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
+
+lemma INF_anti_mono:
   "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   -- {* The last inclusion is POSITIVE! *}
   by (blast intro: INF_mono dest: subsetD)
 
+lemma SUP_anti_mono:
+  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<sqsubseteq> f x) \<Longrightarrow> (\<Squnion>x\<in>B. g x) \<sqsubseteq> (\<Squnion>x\<in>B. f x)"
+  -- {* The last inclusion is POSITIVE! *}
+  by (blast intro: SUP_mono dest: subsetD)
+
 end
 
 lemma Inf_less_iff:
@@ -342,16 +376,16 @@
   shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   unfolding not_le [symmetric] le_Inf_iff by auto
 
+lemma less_Sup_iff:
+  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+  shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+  unfolding not_le [symmetric] Sup_le_iff by auto
+
 lemma INF_less_iff:
   fixes a :: "'a::{complete_lattice,linorder}"
   shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   unfolding INFI_def Inf_less_iff by auto
 
-lemma less_Sup_iff:
-  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
-  shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
-  unfolding not_le [symmetric] Sup_le_iff by auto
-
 lemma less_SUP_iff:
   fixes a :: "'a::{complete_lattice,linorder}"
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"