author haftmann Sun, 17 Jul 2011 20:46:51 +0200 changeset 43871 79c3231e0593 parent 43870 92129f505125 child 43872 6b917e5877d2
```--- 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>"
-
-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)"

-lemma (in complete_lattice) INF_eq:
+lemma SUP_constant:
+  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
+
+lemma INF_eq:
"(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"

-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"
+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)"```