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) \ x" +by (auto simp: bot_def intro: Inf_fin.coboundedI) + +instance finite_lattice_complete \ order_bot +proof qed (auto simp: finite_lattice_complete_bot_least) + +lemma finite_lattice_complete_top_greatest: +"(top::'a::finite_lattice_complete) \ x" +by (auto simp: top_def Sup_fin.coboundedI) + +instance finite_lattice_complete \ order_top +proof qed (auto simp: finite_lattice_complete_top_greatest) instance finite_lattice_complete \ bounded_lattice .. --- "This subclass relation eases the proof of the next two lemmas." -lemma finite_lattice_complete_bot_def: - "(bot::'a::finite_lattice_complete) = \\<^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) = \\<^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) \ A \ Inf A \ 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 \ '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 \ '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 \ 'b::finite_lattice_complete) set) = + "Inf(A :: ('a::finite_lattice_complete \ '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 \ 'b::finite_lattice_complete) set) = + "Sup (A :: ('a::finite_lattice_complete \ '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 \ '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 \ '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 \ '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 \ x" unfolding inf_def by (metis (full_types) linorder_linear) @@ -250,3 +270,4 @@ end +