--- 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
+