# HG changeset patch # User nipkow # Date 1356797881 -3600 # Node ID 009a9fdabbad708d21c8057471d8330fce84f07e # Parent 87961472b4040f11f9f070ffdfd3f9a1ede69f86 new theory Library/Finite_Lattice diff -r 87961472b404 -r 009a9fdabbad NEWS --- a/NEWS Fri Dec 28 23:31:51 2012 +0100 +++ b/NEWS Sat Dec 29 17:18:01 2012 +0100 @@ -308,6 +308,8 @@ * Library/IArray.thy: immutable arrays with code generation. +* Library/Finite_Lattice.thy: theory of finite lattices + * Simproc "finite_Collect" rewrites set comprehensions into pointfree expressions. diff -r 87961472b404 -r 009a9fdabbad src/HOL/Library/Finite_Lattice.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Finite_Lattice.thy Sat Dec 29 17:18:01 2012 +0100 @@ -0,0 +1,228 @@ +(* Author: Alessandro Coglio *) + +theory Finite_Lattice +imports Product_Lattice +begin + +text {* A non-empty finite lattice is a complete lattice. +Since types are never empty in Isabelle/HOL, +a type of classes @{class finite} and @{class lattice} +should also have class @{class complete_lattice}. +A type class is defined +that extends classes @{class finite} and @{class lattice} +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}.} *} + +class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup + +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}." + +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, +as required for a complete lattice. *} + +lemma finite_lattice_complete_Inf_lower: + "(x::'a::finite_lattice_complete) \ A \ Inf A \ x" +unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf) + +lemma finite_lattice_complete_Inf_greatest: + "\x::'a::finite_lattice_complete \ A. z \ x \ z \ Inf A" +unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right) + +lemma finite_lattice_complete_Sup_upper: + "(x::'a::finite_lattice_complete) \ A \ Sup A \ x" +unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup) + +lemma finite_lattice_complete_Sup_least: + "\x::'a::finite_lattice_complete \ A. z \ x \ z \ Sup A" +unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right) + +instance finite_lattice_complete \ complete_lattice +proof +qed (auto simp: + finite_lattice_complete_Inf_lower + finite_lattice_complete_Inf_greatest + finite_lattice_complete_Sup_upper + finite_lattice_complete_Sup_least) + + +text {* The product of two finite lattices is already a finite lattice. *} + +lemma finite_Inf_prod: + "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) = + 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) + +text {* Functions with a finite domain and with a finite lattice as codomain +already form a finite lattice. *} + +lemma finite_Inf_fun: + "Inf (A::('a::finite \ 'b::finite_lattice_complete) set) = + Finite_Set.fold inf top A" +by (metis Inf_fold_inf finite_code) + +lemma finite_Sup_fun: + "Sup (A::('a::finite \ 'b::finite_lattice_complete) set) = + Finite_Set.fold sup bot A" +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) + + +subsection {* Finite Distributive Lattices *} + +text {* A finite distributive lattice is a complete lattice +whose @{const inf} and @{const sup} operators +distribute over @{const Sup} and @{const Inf}. *} + +class finite_distrib_lattice_complete = + distrib_lattice + finite_lattice_complete + +lemma finite_distrib_lattice_complete_sup_Inf: + "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)" +apply (rule finite_induct) +apply (metis finite_code) +apply (metis INF_empty Inf_empty sup_top_right) +apply (metis INF_insert Inf_insert sup_inf_distrib1) +done + +lemma finite_distrib_lattice_complete_inf_Sup: + "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)" +apply (rule finite_induct) +apply (metis finite_code) +apply (metis SUP_empty Sup_empty inf_bot_right) +apply (metis SUP_insert Sup_insert inf_sup_distrib1) +done + +instance finite_distrib_lattice_complete \ complete_distrib_lattice +proof +qed (auto simp: + finite_distrib_lattice_complete_sup_Inf + finite_distrib_lattice_complete_inf_Sup) + +text {* The product of two finite distributive lattices +is already a finite distributive lattice. *} + +instance prod :: + (finite_distrib_lattice_complete, finite_distrib_lattice_complete) + finite_distrib_lattice_complete +.. + +text {* Functions with a finite domain +and with a finite distributive lattice as codomain +already form a finite distributive lattice. *} + +instance "fun" :: + (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete +.. + + +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}, +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}. *} + +class linorder_lattice = linorder + inf + sup + +assumes inf_def: "inf x y = (if x \ y then x else y)" +assumes sup_def: "sup x y = (if x \ y then x else y)" + +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. *} + +lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \ x" +unfolding inf_def by (metis (full_types) linorder_linear) + +lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \ y" +unfolding inf_def by (metis (full_types) linorder_linear) + +lemma linorder_lattice_inf_greatest: + "(x::'a::linorder_lattice) \ y \ x \ z \ x \ inf y z" +unfolding inf_def by (metis (full_types)) + +lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \ x" +unfolding sup_def by (metis (full_types) linorder_linear) + +lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \ y" +unfolding sup_def by (metis (full_types) linorder_linear) + +lemma linorder_lattice_sup_least: + "(x::'a::linorder_lattice) \ y \ x \ z \ x \ sup y z" +by (auto simp: sup_def) + +lemma linorder_lattice_sup_inf_distrib1: + "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)" +by (auto simp: inf_def sup_def) + +instance linorder_lattice \ distrib_lattice +proof +qed (auto simp: + linorder_lattice_inf_le1 + linorder_lattice_inf_le2 + linorder_lattice_inf_greatest + linorder_lattice_sup_ge1 + linorder_lattice_sup_ge2 + linorder_lattice_sup_least + linorder_lattice_sup_inf_distrib1) + + +subsection {* Finite Linear Orders *} + +text {* A (non-empty) finite linear order is a complete linear order. *} + +class finite_linorder_complete = linorder_lattice + finite_lattice_complete + +instance finite_linorder_complete \ complete_linorder .. + +text {* A (non-empty) finite linear order is a complete lattice +whose @{const inf} and @{const sup} operators +distribute over @{const Sup} and @{const Inf}. *} + +instance finite_linorder_complete \ finite_distrib_lattice_complete .. + + +end diff -r 87961472b404 -r 009a9fdabbad src/HOL/ROOT --- a/src/HOL/ROOT Fri Dec 28 23:31:51 2012 +0100 +++ b/src/HOL/ROOT Sat Dec 29 17:18:01 2012 +0100 @@ -41,7 +41,7 @@ Sublist List_lexord Sublist_Order - Product_Lattice + Finite_Lattice Code_Char_chr Code_Char_ord Code_Integer