# HG changeset patch
# User haftmann
# Date 1201687066 -3600
# Node ID 00c2c3525bef8efb3ac3a0d28507262a50b3c65b
# Parent  8764a1f1253bf0527c3741c465d2aaad1371ac5c
dual orders and dual lattices

diff -r 8764a1f1253b -r 00c2c3525bef src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Jan 30 10:57:44 2008 +0100
+++ b/src/HOL/Lattices.thy	Wed Jan 30 10:57:46 2008 +0100
@@ -26,6 +26,16 @@
   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
+begin
+
+text {* Dual lattice *}
+
+lemma dual_lattice:
+  "lower_semilattice (op \<ge>) (op >) sup"
+by unfold_locales
+  (auto simp add: sup_least)
+
+end
 
 class lattice = lower_semilattice + upper_semilattice
 
@@ -87,7 +97,7 @@
 lemmas (in -) [rule del] = le_supI2
 
 lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
-by(blast intro: sup_least)
+  by (blast intro: sup_least)
 lemmas (in -) [rule del] = le_supI
 
 lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
diff -r 8764a1f1253b -r 00c2c3525bef src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jan 30 10:57:44 2008 +0100
+++ b/src/HOL/Orderings.thy	Wed Jan 30 10:57:46 2008 +0100
@@ -106,9 +106,9 @@
 by (rule less_asym)
 
 
-text {* Reverse order *}
+text {* Dual order *}
 
-lemma order_reverse:
+lemma dual_order:
   "order (op \<ge>) (op >)"
 by unfold_locales
    (simp add: less_le, auto intro: antisym order_trans)
@@ -179,9 +179,9 @@
 unfolding not_le .
 
 
-text {* Reverse order *}
+text {* Dual order *}
 
-lemma linorder_reverse:
+lemma dual_linorder:
   "linorder (op \<ge>) (op >)"
 by unfold_locales
   (simp add: less_le, auto intro: antisym order_trans simp add: linear)