--- a/src/HOL/Library/Product_Order.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Product_Order.thy Thu Jul 25 08:57:16 2013 +0200
@@ -108,6 +108,10 @@
definition
"top = (top, top)"
+instance ..
+
+end
+
lemma fst_top [simp]: "fst top = top"
unfolding top_prod_def by simp
@@ -117,17 +121,19 @@
lemma Pair_top_top: "(top, top) = top"
unfolding top_prod_def by simp
-instance
+instance prod :: (order_top, order_top) order_top
by default (auto simp add: top_prod_def)
-end
-
instantiation prod :: (bot, bot) bot
begin
definition
"bot = (bot, bot)"
+instance ..
+
+end
+
lemma fst_bot [simp]: "fst bot = bot"
unfolding bot_prod_def by simp
@@ -137,11 +143,9 @@
lemma Pair_bot_bot: "(bot, bot) = bot"
unfolding bot_prod_def by simp
-instance
+instance prod :: (order_bot, order_bot) order_bot
by default (auto simp add: bot_prod_def)
-end
-
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
@@ -161,7 +165,7 @@
instance
by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
- INF_lower SUP_upper le_INF_iff SUP_le_iff)
+ INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
end