1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:17:33 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:42:53 2011 +0200
     1.3 @@ -386,18 +386,25 @@
     1.4  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
     1.5    by (fact Inf_inter_less)
     1.6  
     1.7 -(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
     1.8 +lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
     1.9 +  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
    1.10  
    1.11  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    1.12 -  by blast
    1.13 +  by (fact Inf_union_distrib)
    1.14 +
    1.15 +(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
    1.16 +  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
    1.17  
    1.18  lemma Inter_UNIV_conv [simp,no_atp]:
    1.19    "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
    1.20    "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
    1.21    by blast+
    1.22  
    1.23 +lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    1.24 +  by (auto intro: Inf_greatest Inf_lower)
    1.25 +
    1.26  lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
    1.27 -  by blast
    1.28 +  by (fact Inf_anti_mono)
    1.29  
    1.30  
    1.31  subsection {* Intersections of families *}