# HG changeset patch
# User haftmann
# Date 1310300767 -7200
# Node ID 3316e6831801a7e2c7eb9e62e34adb9c03c3817a
# Parent  4529a3c5660967bfbb1ee8031bc0a3b7be06c68e
more succinct proofs

diff -r 4529a3c56609 -r 3316e6831801 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:14:19 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:26:07 2011 +0200
@@ -349,14 +349,24 @@
   by (unfold Inter_eq) blast
 
 lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
-  by blast
+  by (fact Inf_lower)
+
+lemma (in complete_lattice) Inf_less_eq:
+  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+    and "A \<noteq> {}"
+  shows "\<Sqinter>A \<le> u"
+proof -
+  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+  moreover with assms have "v \<sqsubseteq> u" by blast
+  ultimately show ?thesis by (rule Inf_lower2)
+qed
 
 lemma Inter_subset:
   "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
-  by blast
+  by (fact Inf_less_eq)
 
 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
-  by (iprover intro: InterI subsetI dest: subsetD)
+  by (fact Inf_greatest)
 
 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   by (fact Inf_binary [symmetric])