dual orders and dual lattices
authorhaftmann
Wed Jan 30 10:57:46 2008 +0100 (2008-01-30)
changeset 2601400c2c3525bef
parent 26013 8764a1f1253b
child 26015 ad2756de580e
dual orders and dual lattices
src/HOL/Lattices.thy
src/HOL/Orderings.thy
     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"
     2.1 --- a/src/HOL/Orderings.thy	Wed Jan 30 10:57:44 2008 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Wed Jan 30 10:57:46 2008 +0100
     2.3 @@ -106,9 +106,9 @@
     2.4  by (rule less_asym)
     2.5  
     2.6  
     2.7 -text {* Reverse order *}
     2.8 +text {* Dual order *}
     2.9  
    2.10 -lemma order_reverse:
    2.11 +lemma dual_order:
    2.12    "order (op \<ge>) (op >)"
    2.13  by unfold_locales
    2.14     (simp add: less_le, auto intro: antisym order_trans)
    2.15 @@ -179,9 +179,9 @@
    2.16  unfolding not_le .
    2.17  
    2.18  
    2.19 -text {* Reverse order *}
    2.20 +text {* Dual order *}
    2.21  
    2.22 -lemma linorder_reverse:
    2.23 +lemma dual_linorder:
    2.24    "linorder (op \<ge>) (op >)"
    2.25  by unfold_locales
    2.26    (simp add: less_le, auto intro: antisym order_trans simp add: linear)