# HG changeset patch
# User haftmann
# Date 1310846642 -7200
# Node ID 020ddc6a95082e826c3655e7a47101d0644a3e8c
# Parent  7411fbf0a325ae595919f9a6e7e5b8ee0a991cee
consolidated bot and top classes, tuned notation

diff -r 7411fbf0a325 -r 020ddc6a9508 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sat Jul 16 21:53:50 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sat Jul 16 22:04:02 2011 +0200
@@ -108,20 +108,6 @@
   with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
 qed
 
-lemma top_le:
-  "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
-  by (rule antisym) auto
-
-lemma le_bot:
-  "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
-  by (rule antisym) auto
-
-lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
-  using bot_least [of x] by (auto simp: le_less)
-
-lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
-  using top_greatest [of x] by (auto simp: le_less)
-
 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
   using Sup_upper[of u A] by auto
 
diff -r 7411fbf0a325 -r 020ddc6a9508 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Jul 16 21:53:50 2011 +0200
+++ b/src/HOL/Orderings.thy	Sat Jul 16 22:04:02 2011 +0200
@@ -1084,35 +1084,54 @@
 subsection {* (Unique) top and bottom elements *}
 
 class bot = order +
-  fixes bot :: 'a
-  assumes bot_least [simp]: "bot \<le> x"
+  fixes bot :: 'a ("\<bottom>")
+  assumes bot_least [simp]: "\<bottom> \<le> a"
 begin
 
+lemma le_bot:
+  "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
+  by (auto intro: antisym)
+
 lemma bot_unique:
-  "a \<le> bot \<longleftrightarrow> a = bot"
-  by (auto simp add: intro: antisym)
+  "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
+  by (auto intro: antisym)
+
+lemma not_less_bot [simp]:
+  "\<not> (a < \<bottom>)"
+  using bot_least [of a] by (auto simp: le_less)
 
 lemma bot_less:
-  "a \<noteq> bot \<longleftrightarrow> bot < a"
+  "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
   by (auto simp add: less_le_not_le intro!: antisym)
 
 end
 
 class top = order +
-  fixes top :: 'a
-  assumes top_greatest [simp]: "x \<le> top"
+  fixes top :: 'a ("\<top>")
+  assumes top_greatest [simp]: "a \<le> \<top>"
 begin
 
+lemma top_le:
+  "\<top> \<le> a \<Longrightarrow> a = \<top>"
+  by (rule antisym) auto
+
 lemma top_unique:
-  "top \<le> a \<longleftrightarrow> a = top"
-  by (auto simp add: intro: antisym)
+  "\<top> \<le> a \<longleftrightarrow> a = \<top>"
+  by (auto intro: antisym)
+
+lemma not_top_less [simp]: "\<not> (\<top> < a)"
+  using top_greatest [of a] by (auto simp: le_less)
 
 lemma less_top:
-  "a \<noteq> top \<longleftrightarrow> a < top"
+  "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
   by (auto simp add: less_le_not_le intro!: antisym)
 
 end
 
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>")
+
 
 subsection {* Dense orders *}