Fixed lattice defns
authornipkow
Tue Feb 08 09:46:00 2005 +0100 (2005-02-08)
changeset 15505c929e1cbef88
parent 15504 5bc81e50f2c5
child 15506 864238c95b56
Fixed lattice defns
src/HOL/Finite_Set.thy
     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.6  
     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.12  
    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.18  
    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.26  
    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.31  
    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.43 +by(simp add:ACI sup_inf_distrib1)
    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.49 +by(simp add:ACI inf_sup_distrib1)
    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.56  
    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.62  
    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.72  
    1.73  
    1.74  subsection{*Min and Max*}