src/HOL/Lattices.thy
changeset 26014 00c2c3525bef
parent 25510 38c15efe603b
child 26233 3751b3dbb67c
     1.1 --- a/src/HOL/Lattices.thy	Wed Jan 30 10:57:44 2008 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Jan 30 10:57:46 2008 +0100
     1.3 @@ -26,6 +26,16 @@
     1.4    assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
     1.5    and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
     1.6    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
     1.7 +begin
     1.8 +
     1.9 +text {* Dual lattice *}
    1.10 +
    1.11 +lemma dual_lattice:
    1.12 +  "lower_semilattice (op \<ge>) (op >) sup"
    1.13 +by unfold_locales
    1.14 +  (auto simp add: sup_least)
    1.15 +
    1.16 +end
    1.17  
    1.18  class lattice = lower_semilattice + upper_semilattice
    1.19  
    1.20 @@ -87,7 +97,7 @@
    1.21  lemmas (in -) [rule del] = le_supI2
    1.22  
    1.23  lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.24 -by(blast intro: sup_least)
    1.25 +  by (blast intro: sup_least)
    1.26  lemmas (in -) [rule del] = le_supI
    1.27  
    1.28  lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"