factored syntactic type classes for bot and top (by Alessandro Coglio)
authorhaftmann
Thu, 25 Jul 2013 08:57:16 +0200
changeset 52729 412c9e0381a1
parent 52728 470b579f35d2
child 52730 6bf02eb4ddf7
factored syntactic type classes for bot and top (by Alessandro Coglio)
src/HOL/Complete_Lattices.thy
src/HOL/GCD.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/IMP/Abs_State.thy
src/HOL/Lattices.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Product_Lexorder.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Saturated.thy
src/HOL/Library/Sublist.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/FinFunPred.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -22,17 +22,31 @@
 
 subsection {* Abstract complete lattices *}
 
-class complete_lattice = bounded_lattice + Inf + Sup +
+text {* A complete lattice always has a bottom and a top,
+so we include them into the following type class,
+along with assumptions that define bottom and top
+in terms of infimum and supremum. *}
+
+class complete_lattice = lattice + Inf + Sup + bot + top +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
      and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+  assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
+  assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
 begin
 
+subclass bounded_lattice
+proof
+  fix a
+  show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
+  show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
+qed
+
 lemma dual_complete_lattice:
   "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
-  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
-    (unfold_locales, (fact bot_least top_greatest
+  by (auto intro!: class.complete_lattice.intro dual_lattice)
+    (unfold_locales, (fact Inf_empty Sup_empty
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -141,17 +155,21 @@
 lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   by (auto simp add: SUP_def Sup_le_iff)
 
-lemma Inf_empty [simp]:
-  "\<Sqinter>{} = \<top>"
-  by (auto intro: antisym Inf_greatest)
+lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
+
+lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+  by (simp add: INF_def)
+
+lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
+
+lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+  by (simp add: SUP_def)
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   by (simp add: INF_def)
 
-lemma Sup_empty [simp]:
-  "\<Squnion>{} = \<bottom>"
-  by (auto intro: antisym Sup_least)
-
 lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   by (simp add: SUP_def)
 
@@ -163,18 +181,6 @@
   "\<Squnion>UNIV = \<top>"
   by (auto intro!: antisym Sup_upper)
 
-lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
-  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
-
-lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
-  by (simp add: INF_def)
-
-lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
-  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
-
-lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
-  by (simp add: SUP_def)
-
 lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
   by (simp add: INF_def image_image)
 
--- a/src/HOL/GCD.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/GCD.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -1560,17 +1560,17 @@
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
   proof
-    case goal1 show ?case by simp
+    case goal1 thus ?case by (simp add: Gcd_nat_def)
   next
-    case goal2 show ?case by simp
+    case goal2 thus ?case by (simp add: Gcd_nat_def)
   next
-    case goal5 thus ?case by (rule dvd_Lcm_nat)
+    case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
   next
-    case goal6 thus ?case by simp
+    case goal6 show ?case by (simp add: Lcm_nat_empty)
   next
-    case goal3 thus ?case by (simp add: Gcd_nat_def)
+    case goal3 thus ?case by simp
   next
-    case goal4 thus ?case by (simp add: Gcd_nat_def)
+    case goal4 thus ?case by simp
   qed
   then interpret gcd_lcm_complete_lattice_nat:
     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -6,11 +6,11 @@
 
 subsection "Orderings"
 
-text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are
+text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
 defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
 If you view this theory with jedit, just click on the names to get there. *}
 
-class semilattice_sup_top = semilattice_sup + top
+class semilattice_sup_top = semilattice_sup + order_top
 
 
 instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..
@@ -78,7 +78,7 @@
 lemma [simp]: "(Some x < Some y) = (x < y)"
 by(auto simp: less_le)
 
-instantiation option :: (order)bot
+instantiation option :: (order)order_bot
 begin
 
 definition bot_option :: "'a option" where
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -100,7 +100,7 @@
 subsubsection "Termination"
 
 locale Measure1 =
-fixes m :: "'av::{order,top} \<Rightarrow> nat"
+fixes m :: "'av::{order,order_top} \<Rightarrow> nat"
 fixes h :: "nat"
 assumes h: "m x \<le> h"
 begin
@@ -134,14 +134,14 @@
 
 end
 
-fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
+fun top_on_st :: "'a::order_top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
 "top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
 
-fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
+fun top_on_opt :: "'a::order_top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
 "top_on_opt (Some S)  X = top_on_st S X" |
 "top_on_opt None X = True"
 
-definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
+definition top_on_acom :: "'a::order_top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
 "top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
 
 lemma top_on_top: "top_on_opt (\<top>::_ st option) X"
--- a/src/HOL/IMP/Abs_Int3.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -25,7 +25,7 @@
 
 end
 
-lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,top})"
+lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})"
 by (metis eq_iff top_greatest widen2)
 
 instantiation ivl :: wn
@@ -53,7 +53,7 @@
 
 end
 
-instantiation st :: ("{top,wn}")wn
+instantiation st :: ("{order_top,wn}")wn
 begin
 
 lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
@@ -335,7 +335,7 @@
 widening. *}
 
 locale Measure_wn = Measure1 where m=m
-  for m :: "'av::{top,wn} \<Rightarrow> nat" +
+  for m :: "'av::{order_top,wn} \<Rightarrow> nat" +
 fixes n :: "'av \<Rightarrow> nat"
 assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
 assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
--- a/src/HOL/IMP/Abs_State.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -6,7 +6,7 @@
 
 type_synonym 'a st_rep = "(vname * 'a) list"
 
-fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
+fun fun_rep :: "('a::order_top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
 "fun_rep [] = (\<lambda>x. \<top>)" |
 "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
 
@@ -14,23 +14,23 @@
   "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
 by(induction ps rule: fun_rep.induct) auto
 
-definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
+definition eq_st :: "('a::order_top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
 hide_type st  --"hide previous def to avoid long names"
 
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type 'a st = "('a::order_top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)
 
-lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
+lift_definition update :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
   is "\<lambda>ps x a. (x,a)#ps"
 by(auto simp: eq_st_def)
 
-lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
+lift_definition "fun" :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
 by(simp add: eq_st_def)
 
-definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
+definition show_st :: "vname set \<Rightarrow> ('a::order_top) st \<Rightarrow> (vname * 'a)set" where
 "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
 
 definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
@@ -39,10 +39,10 @@
 lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
 by transfer auto
 
-definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
+definition \<gamma>_st :: "(('a::order_top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
 "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
 
-instantiation st :: ("{order,top}") order
+instantiation st :: ("{order,order_top}") order
 begin
 
 definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
@@ -83,7 +83,7 @@
 lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
 by transfer (rule less_eq_st_rep_iff)
 
-fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
+fun map2_st_rep :: "('a::order_top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
 "map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
 "map2_st_rep f ((x,y)#ps1) ps2 =
   (let y2 = fun_rep ps2 x
--- a/src/HOL/Lattices.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Lattices.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -466,7 +466,7 @@
 
 subsection {* Bounded lattices and boolean algebras *}
 
-class bounded_semilattice_inf_top = semilattice_inf + top
+class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
 
 sublocale inf_top!: semilattice_neutr inf top
@@ -479,7 +479,7 @@
 
 end
 
-class bounded_semilattice_sup_bot = semilattice_sup + bot
+class bounded_semilattice_sup_bot = semilattice_sup + order_bot
 begin
 
 sublocale sup_bot!: semilattice_neutr sup bot
@@ -492,7 +492,7 @@
 
 end
 
-class bounded_lattice_bot = lattice + bot
+class bounded_lattice_bot = lattice + order_bot
 begin
 
 subclass bounded_semilattice_sup_bot ..
@@ -523,7 +523,7 @@
 
 end
 
-class bounded_lattice_top = lattice + top
+class bounded_lattice_top = lattice + order_top
 begin
 
 subclass bounded_semilattice_inf_top ..
@@ -550,7 +550,7 @@
 
 end
 
-class bounded_lattice = lattice + bot + top
+class bounded_lattice = lattice + order_bot + order_top
 begin
 
 subclass bounded_lattice_bot ..
--- a/src/HOL/Library/Extended_Nat.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -452,7 +452,7 @@
 apply (erule (1) le_less_trans)
 done
 
-instantiation enat :: "{bot, top}"
+instantiation enat :: "{order_bot, order_top}"
 begin
 
 definition bot_enat :: enat where
@@ -623,7 +623,8 @@
       unfolding Sup_enat_def by (cases "finite A") auto }
   { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
       unfolding Sup_enat_def using finite_enat_bounded by auto }
-qed (simp_all add: inf_enat_def sup_enat_def)
+qed (simp_all add:
+ inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def)
 end
 
 instance enat :: complete_linorder ..
--- a/src/HOL/Library/Extended_Real.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -1144,8 +1144,22 @@
   using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
 
 instance
-  by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
-                   simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
+proof
+  show "Sup {} = (bot::ereal)"
+  apply (auto simp: bot_ereal_def Sup_ereal_def)
+  apply (rule some1_equality)
+  apply (metis ereal_bot ereal_less_eq(2))
+  apply (metis ereal_less_eq(2))
+  done
+next
+  show "Inf {} = (top::ereal)"
+  apply (auto simp: top_ereal_def Inf_ereal_def)
+  apply (rule some1_equality)
+  apply (metis ereal_top ereal_less_eq(1))
+  apply (metis ereal_less_eq(1))
+  done
+qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
+  simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
 
 end
 
--- a/src/HOL/Library/Finite_Lattice.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -13,31 +13,39 @@
 with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
 along with assumptions that define these operators
 in terms of the ones of classes @{class finite} and @{class lattice}.
-The resulting class is a subclass of @{class complete_lattice}.
-Classes @{class bot} and @{class top} already include assumptions that suffice
-to define the operators @{const bot} and @{const top} (as proved below),
-and so no explicit assumptions on these two operators are needed
-in the following type class.%
-\footnote{The Isabelle/HOL library does not provide
-syntactic classes for the operators @{const bot} and @{const top}.} *}
+The resulting class is a subclass of @{class complete_lattice}. *}
 
 class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
+assumes bot_def: "bot = Inf_fin UNIV"
+assumes top_def: "top = Sup_fin UNIV"
 assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
 assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
--- "No explicit assumptions on @{const bot} or @{const top}."
+
+text {* The definitional assumptions
+on the operators @{const bot} and @{const top}
+of class @{class finite_lattice_complete}
+ensure that they yield bottom and top. *}
+
+lemma finite_lattice_complete_bot_least:
+"(bot::'a::finite_lattice_complete) \<le> x"
+by (auto simp: bot_def intro: Inf_fin.coboundedI)
+
+instance finite_lattice_complete \<subseteq> order_bot
+proof qed (auto simp: finite_lattice_complete_bot_least)
+
+lemma finite_lattice_complete_top_greatest:
+"(top::'a::finite_lattice_complete) \<ge> x"
+by (auto simp: top_def Sup_fin.coboundedI)
+
+instance finite_lattice_complete \<subseteq> order_top
+proof qed (auto simp: finite_lattice_complete_top_greatest)
 
 instance finite_lattice_complete \<subseteq> bounded_lattice ..
--- "This subclass relation eases the proof of the next two lemmas."
 
-lemma finite_lattice_complete_bot_def:
-  "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
-by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
--- "Derived definition of @{const bot}."
-
-lemma finite_lattice_complete_top_def:
-  "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
-by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
--- "Derived definition of @{const top}."
+text {* The definitional assumptions
+on the operators @{const Inf} and @{const Sup}
+of class @{class finite_lattice_complete}
+ensure that they yield infimum and supremum. *}
 
 lemma finite_lattice_complete_Inf_empty:
   "Inf {} = (top :: 'a::finite_lattice_complete)"
@@ -63,12 +71,6 @@
   show ?thesis by (simp add: Sup_def)
 qed
 
-text {* The definitional assumptions
-on the operators @{const Inf} and @{const Sup}
-of class @{class finite_lattice_complete}
-ensure that they yield infimum and supremum,
-as required for a complete lattice. *}
-
 lemma finite_lattice_complete_Inf_lower:
   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
@@ -91,28 +93,48 @@
  finite_lattice_complete_Inf_lower
  finite_lattice_complete_Inf_greatest
  finite_lattice_complete_Sup_upper
- finite_lattice_complete_Sup_least)
-
+ finite_lattice_complete_Sup_least
+ finite_lattice_complete_Inf_empty
+ finite_lattice_complete_Sup_empty)
 
 text {* The product of two finite lattices is already a finite lattice. *}
 
+lemma finite_bot_prod:
+  "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
+   Inf_fin UNIV"
+by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
+
+lemma finite_top_prod:
+  "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
+   Sup_fin UNIV"
+by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
+
 lemma finite_Inf_prod:
-  "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
+  "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   Finite_Set.fold inf top A"
 by (metis Inf_fold_inf finite_code)
 
 lemma finite_Sup_prod:
-  "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
+  "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   Finite_Set.fold sup bot A"
 by (metis Sup_fold_sup finite_code)
 
 instance prod ::
   (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
-proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
+proof
+qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
 
 text {* Functions with a finite domain and with a finite lattice as codomain
 already form a finite lattice. *}
 
+lemma finite_bot_fun:
+  "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
+by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
+
+lemma finite_top_fun:
+  "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
+by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
+
 lemma finite_Inf_fun:
   "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   Finite_Set.fold inf top A"
@@ -124,7 +146,8 @@
 by (metis Sup_fold_sup finite_code)
 
 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
-proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
+proof
+qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
 
 
 subsection {* Finite Distributive Lattices *}
@@ -178,11 +201,9 @@
 subsection {* Linear Orders *}
 
 text {* A linear order is a distributive lattice.
-Since in Isabelle/HOL
-a subclass must have all the parameters of its superclasses,
-class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
-So class @{class linorder} is extended with
-the operators @{const inf} and @{const sup},
+A type class is defined
+that extends class @{class linorder}
+with the operators @{const inf} and @{const sup},
 along with assumptions that define these operators
 in terms of the ones of class @{class linorder}.
 The resulting class is a subclass of @{class distrib_lattice}. *}
@@ -194,9 +215,8 @@
 text {* The definitional assumptions
 on the operators @{const inf} and @{const sup}
 of class @{class linorder_lattice}
-ensure that they yield infimum and supremum,
-and that they distribute over each other,
-as required for a distributive lattice. *}
+ensure that they yield infimum and supremum
+and that they distribute over each other. *}
 
 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
 unfolding inf_def by (metis (full_types) linorder_linear)
@@ -250,3 +270,4 @@
 
 
 end
+
--- a/src/HOL/Library/List_lexord.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/List_lexord.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -91,7 +91,7 @@
 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   by (unfold list_le_def) auto
 
-instantiation list :: (order) bot
+instantiation list :: (order) order_bot
 begin
 
 definition
--- a/src/HOL/Library/Option_ord.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Option_ord.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -73,7 +73,7 @@
 instance option :: (linorder) linorder proof
 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
 
-instantiation option :: (order) bot
+instantiation option :: (order) order_bot
 begin
 
 definition bot_option where
@@ -84,7 +84,7 @@
 
 end
 
-instantiation option :: (top) top
+instantiation option :: (order_top) order_top
 begin
 
 definition top_option where
@@ -272,6 +272,12 @@
     then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
     with Some show ?thesis by (simp add: Sup_option_def)
   qed
+next
+  show "\<Squnion>{} = (\<bottom>::'a option)"
+  by (auto simp: bot_option_def)
+next
+  show "\<Sqinter>{} = (\<top>::'a option)"
+  by (auto simp: top_option_def Inf_option_def)
 qed
 
 end
--- a/src/HOL/Library/Product_Lexorder.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Product_Lexorder.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -65,22 +65,26 @@
 definition
   "bot = (bot, bot)"
 
-instance
-  by default (auto simp add: bot_prod_def)
+instance ..
 
 end
 
+instance prod :: (order_bot, order_bot) order_bot
+  by default (auto simp add: bot_prod_def)
+
 instantiation prod :: (top, top) top
 begin
 
 definition
   "top = (top, top)"
 
-instance
-  by default (auto simp add: top_prod_def)
+instance ..
 
 end
 
+instance prod :: (order_top, order_top) order_top
+  by default (auto simp add: top_prod_def)
+
 instance prod :: (wellorder, wellorder) wellorder
 proof
   fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
--- 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
 
--- a/src/HOL/Library/Saturated.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Saturated.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -263,6 +263,12 @@
   note finite
   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   ultimately show "Sup A \<le> z" by (induct A) auto
+next
+  show "Inf {} = (top::'a sat)"
+    by (auto simp: top_sat_def)
+next
+  show "Sup {} = (bot::'a sat)"
+    by (auto simp: bot_sat_def)
 qed
 
 hide_const (open) sat_of_nat
--- a/src/HOL/Library/Sublist.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Sublist.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -20,7 +20,7 @@
 interpretation prefix_order: order prefixeq prefix
   by default (auto simp: prefixeq_def prefix_def)
 
-interpretation prefix_bot: bot prefixeq prefix Nil
+interpretation prefix_bot: order_bot Nil prefixeq prefix
   by default (simp add: prefixeq_def)
 
 lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
--- a/src/HOL/Nat.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Nat.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -444,7 +444,7 @@
 
 end
 
-instantiation nat :: bot
+instantiation nat :: order_bot
 begin
 
 definition bot_nat :: nat where
@@ -1318,7 +1318,8 @@
 
 subsection {* Kleene iteration *}
 
-lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
+lemma Kleene_iter_lpfp:
+assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
 proof(induction k)
   case 0 show ?case by simp
 next
--- a/src/HOL/Orderings.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Orderings.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -1167,14 +1167,16 @@
 
 subsection {* (Unique) top and bottom elements *}
 
-class bot = order +
+class bot =
   fixes bot :: 'a ("\<bottom>")
+
+class order_bot = order + bot +
   assumes bot_least: "\<bottom> \<le> a"
 
-sublocale bot < bot!: ordering_top greater_eq greater bot
+sublocale order_bot < bot!: ordering_top greater_eq greater bot
   by default (fact bot_least)
 
-context bot
+context order_bot
 begin
 
 lemma le_bot:
@@ -1195,14 +1197,16 @@
 
 end
 
-class top = order +
+class top =
   fixes top :: 'a ("\<top>")
+
+class order_top = order + top +
   assumes top_greatest: "a \<le> \<top>"
 
-sublocale top < top!: ordering_top less_eq less top
+sublocale order_top < top!: ordering_top less_eq less top
   by default (fact top_greatest)
 
-context top
+context order_top
 begin
 
 lemma top_le:
@@ -1380,7 +1384,7 @@
 
 subsection {* Order on @{typ bool} *}
 
-instantiation bool :: "{bot, top, linorder}"
+instantiation bool :: "{order_bot, order_top, linorder}"
 begin
 
 definition
@@ -1454,6 +1458,13 @@
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
+instance ..
+
+end
+
+instantiation "fun" :: (type, order_bot) order_bot
+begin
+
 lemma bot_apply [simp, code]:
   "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
@@ -1469,6 +1480,13 @@
 definition
   [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 
+instance ..
+
+end
+
+instantiation "fun" :: (type, order_top) order_top
+begin
+
 lemma top_apply [simp, code]:
   "\<top> x = \<top>"
   by (simp add: top_fun_def)
--- a/src/HOL/Set_Interval.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Set_Interval.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -197,8 +197,8 @@
 by (simp add: atLeastAtMost_def)
 
 text {* The above four lemmas could be declared as iffs. Unfortunately this
-breaks many proofs. Since it only helps blast, it is better to leave well
-alone *}
+breaks many proofs. Since it only helps blast, it is better to leave them
+alone. *}
 
 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
   by auto
@@ -452,10 +452,10 @@
   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   using atLeastLessThan_inj assms by auto
 
-lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
 by (auto simp: set_eq_iff intro: le_bot)
 
-lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
 by (auto simp: set_eq_iff intro: top_le)
 
 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
--- a/src/HOL/Topological_Spaces.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -471,27 +471,28 @@
     unfolding le_filter_def by simp }
   { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
     unfolding le_filter_def filter_eq_iff by fast }
-  { show "F \<le> top"
-    unfolding le_filter_def eventually_top by (simp add: always_eventually) }
-  { show "bot \<le> F"
-    unfolding le_filter_def by simp }
-  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
-    unfolding le_filter_def eventually_sup by simp_all }
-  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
-    unfolding le_filter_def eventually_sup by simp }
   { show "inf F F' \<le> F" and "inf F F' \<le> F'"
     unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
     unfolding le_filter_def eventually_inf
     by (auto elim!: eventually_mono intro: eventually_conj) }
+  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
+    unfolding le_filter_def eventually_sup by simp_all }
+  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
+    unfolding le_filter_def eventually_sup by simp }
+  { assume "F'' \<in> S" thus "Inf S \<le> F''"
+    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
+    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   { assume "F \<in> S" thus "F \<le> Sup S"
     unfolding le_filter_def eventually_Sup by simp }
   { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
     unfolding le_filter_def eventually_Sup by simp }
-  { assume "F'' \<in> S" thus "Inf S \<le> F''"
-    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
-  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
-    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+  { show "Inf {} = (top::'a filter)"
+    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
+      (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) }
+  { show "Sup {} = (bot::'a filter)"
+    by (auto simp: bot_filter_def Sup_filter_def) }
 qed
 
 end
--- a/src/HOL/ex/FinFunPred.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -31,7 +31,7 @@
 instance "finfun" :: (type, order) order
 by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
 
-instantiation "finfun" :: (type, bot) bot begin
+instantiation "finfun" :: (type, order_bot) order_bot begin
 definition "bot = finfun_const bot"
 instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
 end
@@ -39,7 +39,7 @@
 lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
 by(auto simp add: bot_finfun_def)
 
-instantiation "finfun" :: (type, top) top begin
+instantiation "finfun" :: (type, order_top) order_top begin
 definition "top = finfun_const top"
 instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
 end