
diff -r 470b579f35d2 -r 412c9e0381a1 src/HOL/Library/Finite_Lattice.thy
--- 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
+




