# HG changeset patch
# User haftmann
# Date 1310330573 -7200
# Node ID 15ea1a07a8cf1b36be0e1c4a56be0d73d708d712
# Parent  5e4a595e63fc6f4febe2584ffa0b67e5b9bfb8ea
tuned proofs

diff -r 5e4a595e63fc -r 15ea1a07a8cf src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:17:33 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:42:53 2011 +0200
@@ -386,18 +386,25 @@
 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   by (fact Inf_inter_less)
 
-(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
+lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
+  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
 
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
-  by blast
+  by (fact Inf_union_distrib)
+
+(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
+  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
 
 lemma Inter_UNIV_conv [simp,no_atp]:
   "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   by blast+
 
+lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+  by (auto intro: Inf_greatest Inf_lower)
+
 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
-  by blast
+  by (fact Inf_anti_mono)
 
 
 subsection {* Intersections of families *}