# HG changeset patch
# User haftmann
# Date 1225120547 -3600
# Node ID a2bc5ce0c9fccb2d66c1e48e7951e36ef60d2045
# Parent  0dafa8aa59833750e6216a33012bb4b00e687e2b
sup_bot and inf_top

diff -r 0dafa8aa5983 -r a2bc5ce0c9fc src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Oct 27 16:14:51 2008 +0100
+++ b/src/HOL/Lattices.thy	Mon Oct 27 16:15:47 2008 +0100
@@ -332,7 +332,7 @@
 
 subsection {* Complete lattices *}
 
-class complete_lattice = lattice + top + bot +
+class complete_lattice = lattice + bot + top +
   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
@@ -383,22 +383,26 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert_simp)
 
-lemma top_def:
-  "top = \<Sqinter>{}"
-  by (auto intro: antisym Inf_greatest)
-
 lemma bot_def:
   "bot = \<Squnion>{}"
   by (auto intro: antisym Sup_least)
 
-definition
-  SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
+lemma top_def:
+  "top = \<Sqinter>{}"
+  by (auto intro: antisym Inf_greatest)
+
+lemma sup_bot [simp]:
+  "x \<squnion> bot = x"
+  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+
+lemma inf_top [simp]:
+  "x \<sqinter> top = x"
+  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+
+definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f == \<Squnion> (f ` A)"
 
-definition
-  INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "INFI A f == \<Sqinter> (f ` A)"
 
 end