# HG changeset patch
# User haftmann
# Date 1253809768 -7200
# Node ID de1f7d4da21ac1eeec19eefa1aed115a4e5e182d
# Parent  b629fbcc53134d2e7193db037ca4ccf5804fae46
added dual for complete lattice

diff -r b629fbcc5313 -r de1f7d4da21a src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Sep 24 08:28:27 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Sep 24 18:29:28 2009 +0200
@@ -10,7 +10,9 @@
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
   inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65)
+  sup  (infixl "\<squnion>" 65) and
+  top ("\<top>") and
+  bot ("\<bottom>")
 
 
 subsection {* Abstract complete lattices *}
@@ -24,6 +26,15 @@
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
+term complete_lattice
+
+lemma dual_complete_lattice:
+  "complete_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom> Sup Inf"
+  by (auto intro!: complete_lattice.intro dual_lattice
+    bot.intro top.intro dual_preorder, unfold_locales)
+      (fact bot_least top_greatest
+        Sup_upper Sup_least Inf_lower Inf_greatest)+
+
 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
@@ -784,7 +795,9 @@
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
   Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  Sup  ("\<Squnion>_" [900] 900) and
+  top ("\<top>") and
+  bot ("\<bottom>")
 
 lemmas mem_simps =
   insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff