Fixed lattice defns

--- a/src/HOL/Finite_Set.thy	Mon Feb 07 18:20:46 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 08 09:46:00 2005 +0100
@@ -2112,10 +2112,7 @@
 lemma (in Lattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
 by(blast intro: antisym inf_le1 inf_least refl)
 
-text{* Distributive lattices: *}
-
-locale DistribLattice = Lattice +
-  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+text{* Towards distributivity: if you have one of them, you have them all. *}
 
 lemma (in Lattice) distrib_imp1:
 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -2141,12 +2138,6 @@
   finally show ?thesis .
 qed
 
-
-lemma (in DistribLattice) inf_sup_distrib1:
- "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
-by(rule distrib_imp2[OF sup_inf_distrib1])
-
-
 text{* Lattices are semilattices *}
 
 lemma (in Lattice) ACf_inf: "ACf inf"
@@ -2191,7 +2182,29 @@
 apply(rule sup_ge2)
 done
 
-text{* Fold laws in lattices *}
+text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
+
+lemmas (in Lattice) ACI = ACIf.ACI[OF ACIf_inf] ACIf.ACI[OF ACIf_sup]
+
+subsubsection{* Distributive lattices *}
+
+locale DistribLattice = Lattice +
+  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+
+lemma (in DistribLattice) sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+by(simp add:ACI sup_inf_distrib1)
+
+lemma (in DistribLattice) inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
+by(rule distrib_imp2[OF sup_inf_distrib1])
+
+lemma (in DistribLattice) inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
+by(simp add:ACI inf_sup_distrib1)
+
+lemmas (in DistribLattice) distrib =
+  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
+
+
+subsubsection{* Fold laws in lattices *}
 
 lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
 apply(unfold Sup_def Inf_def)
@@ -2235,7 +2248,6 @@
   finally show ?case .
 qed
 
-(* FIXME
 lemma (in DistribLattice) sup_Inf2_distrib:
 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
@@ -2267,7 +2279,6 @@
     by blast
   finally show ?case .
 qed
-*)
 
 
 subsection{*Min and Max*}