1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:14:19 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:26:07 2011 +0200
     1.3 @@ -349,14 +349,24 @@
     1.4    by (unfold Inter_eq) blast
     1.5  
     1.6  lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
     1.7 -  by blast
     1.8 +  by (fact Inf_lower)
     1.9 +
    1.10 +lemma (in complete_lattice) Inf_less_eq:
    1.11 +  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
    1.12 +    and "A \<noteq> {}"
    1.13 +  shows "\<Sqinter>A \<le> u"
    1.14 +proof -
    1.15 +  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
    1.16 +  moreover with assms have "v \<sqsubseteq> u" by blast
    1.17 +  ultimately show ?thesis by (rule Inf_lower2)
    1.18 +qed
    1.19  
    1.20  lemma Inter_subset:
    1.21    "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
    1.22 -  by blast
    1.23 +  by (fact Inf_less_eq)
    1.24  
    1.25  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
    1.26 -  by (iprover intro: InterI subsetI dest: subsetD)
    1.27 +  by (fact Inf_greatest)
    1.28  
    1.29  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
    1.30    by (fact Inf_binary [symmetric])