add some lemmas about complete lattices
authorhuffman
Sat Mar 06 08:08:30 2010 -0800 (2010-03-06)
changeset 3562957f1a5e93b6b
parent 35609 0f2c634c8ab7
child 35630 8e562d56d404
add some lemmas about complete lattices
src/HOL/Complete_Lattice.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Mar 06 11:21:09 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Mar 06 08:08:30 2010 -0800
     1.3 @@ -82,6 +82,12 @@
     1.4    "\<Squnion>UNIV = top"
     1.5    by (simp add: Inf_Sup Inf_empty [symmetric])
     1.6  
     1.7 +lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
     1.8 +  by (auto intro: Sup_least dest: Sup_upper)
     1.9 +
    1.10 +lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
    1.11 +  by (auto intro: Inf_greatest dest: Inf_lower)
    1.12 +
    1.13  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.14    "SUPR A f = \<Squnion> (f ` A)"
    1.15  
    1.16 @@ -126,6 +132,12 @@
    1.17  lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
    1.18    by (auto simp add: INFI_def intro: Inf_greatest)
    1.19  
    1.20 +lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
    1.21 +  unfolding SUPR_def by (auto simp add: Sup_le_iff)
    1.22 +
    1.23 +lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    1.24 +  unfolding INFI_def by (auto simp add: le_Inf_iff)
    1.25 +
    1.26  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
    1.27    by (auto intro: antisym SUP_leI le_SUPI)
    1.28  
    1.29 @@ -384,7 +396,7 @@
    1.30    by blast
    1.31  
    1.32  lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
    1.33 -  by blast
    1.34 +  by (fact SUP_le_iff)
    1.35  
    1.36  lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
    1.37    by blast
    1.38 @@ -591,7 +603,7 @@
    1.39    by blast
    1.40  
    1.41  lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
    1.42 -  by blast
    1.43 +  by (fact le_INF_iff)
    1.44  
    1.45  lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
    1.46    by blast