src/HOL/Lattices.thy

   min_max.le_infI1 min_max.le_infI2
 
 
 subsection {* Complete lattices *}
 
-class complete_lattice = lattice + top + bot +
+class complete_lattice = lattice + bot + top +
   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   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"

 
 lemma Sup_binary:
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert_simp)
 
+lemma bot_def:
+  "bot = \<Squnion>{}"
+  by (auto intro: antisym Sup_least)
+
 lemma top_def:
   "top = \<Sqinter>{}"
   by (auto intro: antisym Inf_greatest)
 
-lemma bot_def:
-  "bot = \<Squnion>{}"
-  by (auto intro: antisym Sup_least)
-
-definition
-  SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
+lemma sup_bot [simp]:
+  "x \<squnion> bot = x"
+  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+
+lemma inf_top [simp]:
+  "x \<sqinter> top = x"
+  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+
+definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f == \<Squnion> (f ` A)"
 
-definition
-  INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "INFI A f == \<Sqinter> (f ` A)"
 
 end
 
 syntax