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"
```