# HG changeset patch
# User haftmann
# Date 1310593796 -7200
# Node ID 05ab37be94ed073238551a372233c73b39df9e1e
# Parent  4f6e2965d82172ec71c352a76dde1307f6e14dc3
uniqueness lemmas for bot and top

diff -r 4f6e2965d821 -r 05ab37be94ed NEWS
--- a/NEWS	Wed Jul 13 23:41:13 2011 +0200
+++ b/NEWS	Wed Jul 13 23:49:56 2011 +0200
@@ -60,7 +60,7 @@
 
 *** HOL ***
 
-* classes bot and top require underlying partial order rather than preorder:
+* Classes bot and top require underlying partial order rather than preorder:
 uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
 * Archimedian_Field.thy:
diff -r 4f6e2965d821 -r 05ab37be94ed src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jul 13 23:41:13 2011 +0200
+++ b/src/HOL/Orderings.thy	Wed Jul 13 23:49:56 2011 +0200
@@ -1088,6 +1088,10 @@
   assumes bot_least [simp]: "bot \<le> x"
 begin
 
+lemma bot_unique:
+  "a \<le> bot \<longleftrightarrow> a = bot"
+  by (auto simp add: intro: antisym)
+
 lemma bot_less:
   "a \<noteq> bot \<longleftrightarrow> bot < a"
   by (auto simp add: less_le_not_le intro!: antisym)
@@ -1099,6 +1103,10 @@
   assumes top_greatest [simp]: "x \<le> top"
 begin
 
+lemma top_unique:
+  "top \<le> a \<longleftrightarrow> a = top"
+  by (auto simp add: intro: antisym)
+
 lemma less_top:
   "a \<noteq> top \<longleftrightarrow> a < top"
   by (auto simp add: less_le_not_le intro!: antisym)