author nipkow Tue Feb 08 09:46:00 2005 +0100 (2005-02-08) changeset 15505 c929e1cbef88 parent 15504 5bc81e50f2c5 child 15506 864238c95b56
Fixed lattice defns
 src/HOL/Finite_Set.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 07 18:20:46 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Feb 08 09:46:00 2005 +0100
1.3 @@ -2112,10 +2112,7 @@
1.4  lemma (in Lattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
1.5  by(blast intro: antisym inf_le1 inf_least refl)
1.7 -text{* Distributive lattices: *}
1.8 -
1.9 -locale DistribLattice = Lattice +
1.10 -  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
1.11 +text{* Towards distributivity: if you have one of them, you have them all. *}
1.13  lemma (in Lattice) distrib_imp1:
1.14  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
1.15 @@ -2141,12 +2138,6 @@
1.16    finally show ?thesis .
1.17  qed
1.19 -
1.20 -lemma (in DistribLattice) inf_sup_distrib1:
1.21 - "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
1.22 -by(rule distrib_imp2[OF sup_inf_distrib1])
1.23 -
1.24 -
1.25  text{* Lattices are semilattices *}
1.27  lemma (in Lattice) ACf_inf: "ACf inf"
1.28 @@ -2191,7 +2182,29 @@
1.29  apply(rule sup_ge2)
1.30  done
1.32 -text{* Fold laws in lattices *}
1.33 +text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
1.34 +
1.35 +lemmas (in Lattice) ACI = ACIf.ACI[OF ACIf_inf] ACIf.ACI[OF ACIf_sup]
1.36 +
1.37 +subsubsection{* Distributive lattices *}
1.38 +
1.39 +locale DistribLattice = Lattice +
1.40 +  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
1.41 +
1.42 +lemma (in DistribLattice) sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
1.44 +
1.45 +lemma (in DistribLattice) inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
1.46 +by(rule distrib_imp2[OF sup_inf_distrib1])
1.47 +
1.48 +lemma (in DistribLattice) inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
1.50 +
1.51 +lemmas (in DistribLattice) distrib =
1.52 +  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
1.53 +
1.54 +
1.55 +subsubsection{* Fold laws in lattices *}
1.57  lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
1.58  apply(unfold Sup_def Inf_def)
1.59 @@ -2235,7 +2248,6 @@
1.60    finally show ?case .
1.61  qed
1.63 -(* FIXME
1.64  lemma (in DistribLattice) sup_Inf2_distrib:
1.65  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1.66  shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
1.67 @@ -2267,7 +2279,6 @@
1.68      by blast
1.69    finally show ?case .
1.70  qed
1.71 -*)
1.74  subsection{*Min and Max*}