--- a/src/HOL/Orderings.thy Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Orderings.thy Wed Dec 08 15:05:46 2010 +0100
@@ -1082,14 +1082,14 @@
subsection {* Top and bottom elements *}
+class bot = preorder +
+ fixes bot :: 'a
+ assumes bot_least [simp]: "bot \<le> x"
+
class top = preorder +
fixes top :: 'a
assumes top_greatest [simp]: "x \<le> top"
-class bot = preorder +
- fixes bot :: 'a
- assumes bot_least [simp]: "bot \<le> x"
-
subsection {* Dense orders *}
@@ -1204,7 +1204,7 @@
subsection {* Order on bool *}
-instantiation bool :: "{order, top, bot}"
+instantiation bool :: "{order, bot, top}"
begin
definition
@@ -1214,10 +1214,10 @@
[simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
definition
- [simp]: "top \<longleftrightarrow> True"
+ [simp]: "bot \<longleftrightarrow> False"
definition
- [simp]: "bot \<longleftrightarrow> False"
+ [simp]: "top \<longleftrightarrow> True"
instance proof
qed auto
@@ -1272,6 +1272,21 @@
instance "fun" :: (type, order) order proof
qed (auto simp add: le_fun_def intro: antisym ext)
+instantiation "fun" :: (type, bot) bot
+begin
+
+definition
+ "bot = (\<lambda>x. bot)"
+
+lemma bot_apply:
+ "bot x = bot"
+ by (simp add: bot_fun_def)
+
+instance proof
+qed (simp add: le_fun_def bot_apply)
+
+end
+
instantiation "fun" :: (type, top) top
begin
@@ -1288,21 +1303,6 @@
end
-instantiation "fun" :: (type, bot) bot
-begin
-
-definition
- "bot = (\<lambda>x. bot)"
-
-lemma bot_apply:
- "bot x = bot"
- by (simp add: bot_fun_def)
-
-instance proof
-qed (simp add: le_fun_def bot_apply)
-
-end
-
lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
unfolding le_fun_def by simp