new theory Library/Finite_Lattice
authornipkow
Sat Dec 29 17:18:01 2012 +0100 (2012-12-29)
changeset 50634009a9fdabbad
parent 50633 87961472b404
child 50635 5543eff56b16
new theory Library/Finite_Lattice
NEWS
src/HOL/Library/Finite_Lattice.thy
src/HOL/ROOT
     1.1 --- a/NEWS	Fri Dec 28 23:31:51 2012 +0100
     1.2 +++ b/NEWS	Sat Dec 29 17:18:01 2012 +0100
     1.3 @@ -308,6 +308,8 @@
     1.4  
     1.5  * Library/IArray.thy: immutable arrays with code generation.
     1.6  
     1.7 +* Library/Finite_Lattice.thy: theory of finite lattices
     1.8 +
     1.9  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.10  expressions.
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Sat Dec 29 17:18:01 2012 +0100
     2.3 @@ -0,0 +1,228 @@
     2.4 +(* Author: Alessandro Coglio *)
     2.5 +
     2.6 +theory Finite_Lattice
     2.7 +imports Product_Lattice
     2.8 +begin
     2.9 +
    2.10 +text {* A non-empty finite lattice is a complete lattice.
    2.11 +Since types are never empty in Isabelle/HOL,
    2.12 +a type of classes @{class finite} and @{class lattice}
    2.13 +should also have class @{class complete_lattice}.
    2.14 +A type class is defined
    2.15 +that extends classes @{class finite} and @{class lattice}
    2.16 +with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
    2.17 +along with assumptions that define these operators
    2.18 +in terms of the ones of classes @{class finite} and @{class lattice}.
    2.19 +The resulting class is a subclass of @{class complete_lattice}.
    2.20 +Classes @{class bot} and @{class top} already include assumptions that suffice
    2.21 +to define the operators @{const bot} and @{const top} (as proved below),
    2.22 +and so no explicit assumptions on these two operators are needed
    2.23 +in the following type class.%
    2.24 +\footnote{The Isabelle/HOL library does not provide
    2.25 +syntactic classes for the operators @{const bot} and @{const top}.} *}
    2.26 +
    2.27 +class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
    2.28 +assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    2.29 +assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    2.30 +-- "No explicit assumptions on @{const bot} or @{const top}."
    2.31 +
    2.32 +instance finite_lattice_complete \<subseteq> bounded_lattice ..
    2.33 +-- "This subclass relation eases the proof of the next two lemmas."
    2.34 +
    2.35 +lemma finite_lattice_complete_bot_def:
    2.36 +  "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
    2.37 +by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
    2.38 +-- "Derived definition of @{const bot}."
    2.39 +
    2.40 +lemma finite_lattice_complete_top_def:
    2.41 +  "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
    2.42 +by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
    2.43 +-- "Derived definition of @{const top}."
    2.44 +
    2.45 +text {* The definitional assumptions
    2.46 +on the operators @{const Inf} and @{const Sup}
    2.47 +of class @{class finite_lattice_complete}
    2.48 +ensure that they yield infimum and supremum,
    2.49 +as required for a complete lattice. *}
    2.50 +
    2.51 +lemma finite_lattice_complete_Inf_lower:
    2.52 +  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    2.53 +unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf)
    2.54 +
    2.55 +lemma finite_lattice_complete_Inf_greatest:
    2.56 +  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    2.57 +unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right)
    2.58 +
    2.59 +lemma finite_lattice_complete_Sup_upper:
    2.60 +  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    2.61 +unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup)
    2.62 +
    2.63 +lemma finite_lattice_complete_Sup_least:
    2.64 +  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
    2.65 +unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right)
    2.66 +
    2.67 +instance finite_lattice_complete \<subseteq> complete_lattice
    2.68 +proof
    2.69 +qed (auto simp:
    2.70 + finite_lattice_complete_Inf_lower
    2.71 + finite_lattice_complete_Inf_greatest
    2.72 + finite_lattice_complete_Sup_upper
    2.73 + finite_lattice_complete_Sup_least)
    2.74 +
    2.75 +
    2.76 +text {* The product of two finite lattices is already a finite lattice. *}
    2.77 +
    2.78 +lemma finite_Inf_prod:
    2.79 +  "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    2.80 +  Finite_Set.fold inf top A"
    2.81 +by (metis Inf_fold_inf finite_code)
    2.82 +
    2.83 +lemma finite_Sup_prod:
    2.84 +  "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    2.85 +  Finite_Set.fold sup bot A"
    2.86 +by (metis Sup_fold_sup finite_code)
    2.87 +
    2.88 +instance prod ::
    2.89 +  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
    2.90 +proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
    2.91 +
    2.92 +text {* Functions with a finite domain and with a finite lattice as codomain
    2.93 +already form a finite lattice. *}
    2.94 +
    2.95 +lemma finite_Inf_fun:
    2.96 +  "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
    2.97 +  Finite_Set.fold inf top A"
    2.98 +by (metis Inf_fold_inf finite_code)
    2.99 +
   2.100 +lemma finite_Sup_fun:
   2.101 +  "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   2.102 +  Finite_Set.fold sup bot A"
   2.103 +by (metis Sup_fold_sup finite_code)
   2.104 +
   2.105 +instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   2.106 +proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
   2.107 +
   2.108 +
   2.109 +subsection {* Finite Distributive Lattices *}
   2.110 +
   2.111 +text {* A finite distributive lattice is a complete lattice
   2.112 +whose @{const inf} and @{const sup} operators
   2.113 +distribute over @{const Sup} and @{const Inf}. *}
   2.114 +
   2.115 +class finite_distrib_lattice_complete =
   2.116 +  distrib_lattice + finite_lattice_complete
   2.117 +
   2.118 +lemma finite_distrib_lattice_complete_sup_Inf:
   2.119 +  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   2.120 +apply (rule finite_induct)
   2.121 +apply (metis finite_code)
   2.122 +apply (metis INF_empty Inf_empty sup_top_right)
   2.123 +apply (metis INF_insert Inf_insert sup_inf_distrib1)
   2.124 +done
   2.125 +
   2.126 +lemma finite_distrib_lattice_complete_inf_Sup:
   2.127 +  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   2.128 +apply (rule finite_induct)
   2.129 +apply (metis finite_code)
   2.130 +apply (metis SUP_empty Sup_empty inf_bot_right)
   2.131 +apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   2.132 +done
   2.133 +
   2.134 +instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   2.135 +proof
   2.136 +qed (auto simp:
   2.137 + finite_distrib_lattice_complete_sup_Inf
   2.138 + finite_distrib_lattice_complete_inf_Sup)
   2.139 +
   2.140 +text {* The product of two finite distributive lattices
   2.141 +is already a finite distributive lattice. *}
   2.142 +
   2.143 +instance prod ::
   2.144 +  (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   2.145 +  finite_distrib_lattice_complete
   2.146 +..
   2.147 +
   2.148 +text {* Functions with a finite domain
   2.149 +and with a finite distributive lattice as codomain
   2.150 +already form a finite distributive lattice. *}
   2.151 +
   2.152 +instance "fun" ::
   2.153 +  (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   2.154 +..
   2.155 +
   2.156 +
   2.157 +subsection {* Linear Orders *}
   2.158 +
   2.159 +text {* A linear order is a distributive lattice.
   2.160 +Since in Isabelle/HOL
   2.161 +a subclass must have all the parameters of its superclasses,
   2.162 +class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
   2.163 +So class @{class linorder} is extended with
   2.164 +the operators @{const inf} and @{const sup},
   2.165 +along with assumptions that define these operators
   2.166 +in terms of the ones of class @{class linorder}.
   2.167 +The resulting class is a subclass of @{class distrib_lattice}. *}
   2.168 +
   2.169 +class linorder_lattice = linorder + inf + sup +
   2.170 +assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   2.171 +assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   2.172 +
   2.173 +text {* The definitional assumptions
   2.174 +on the operators @{const inf} and @{const sup}
   2.175 +of class @{class linorder_lattice}
   2.176 +ensure that they yield infimum and supremum,
   2.177 +and that they distribute over each other,
   2.178 +as required for a distributive lattice. *}
   2.179 +
   2.180 +lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   2.181 +unfolding inf_def by (metis (full_types) linorder_linear)
   2.182 +
   2.183 +lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   2.184 +unfolding inf_def by (metis (full_types) linorder_linear)
   2.185 +
   2.186 +lemma linorder_lattice_inf_greatest:
   2.187 +  "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   2.188 +unfolding inf_def by (metis (full_types))
   2.189 +
   2.190 +lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   2.191 +unfolding sup_def by (metis (full_types) linorder_linear)
   2.192 +
   2.193 +lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   2.194 +unfolding sup_def by (metis (full_types) linorder_linear)
   2.195 +
   2.196 +lemma linorder_lattice_sup_least:
   2.197 +  "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   2.198 +by (auto simp: sup_def)
   2.199 +
   2.200 +lemma linorder_lattice_sup_inf_distrib1:
   2.201 +  "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   2.202 +by (auto simp: inf_def sup_def)
   2.203 + 
   2.204 +instance linorder_lattice \<subseteq> distrib_lattice
   2.205 +proof                                                     
   2.206 +qed (auto simp:
   2.207 + linorder_lattice_inf_le1
   2.208 + linorder_lattice_inf_le2
   2.209 + linorder_lattice_inf_greatest
   2.210 + linorder_lattice_sup_ge1
   2.211 + linorder_lattice_sup_ge2
   2.212 + linorder_lattice_sup_least
   2.213 + linorder_lattice_sup_inf_distrib1)
   2.214 +
   2.215 +
   2.216 +subsection {* Finite Linear Orders *}
   2.217 +
   2.218 +text {* A (non-empty) finite linear order is a complete linear order. *}
   2.219 +
   2.220 +class finite_linorder_complete = linorder_lattice + finite_lattice_complete
   2.221 +
   2.222 +instance finite_linorder_complete \<subseteq> complete_linorder ..
   2.223 +
   2.224 +text {* A (non-empty) finite linear order is a complete lattice
   2.225 +whose @{const inf} and @{const sup} operators
   2.226 +distribute over @{const Sup} and @{const Inf}. *}
   2.227 +
   2.228 +instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   2.229 +
   2.230 +
   2.231 +end
     3.1 --- a/src/HOL/ROOT	Fri Dec 28 23:31:51 2012 +0100
     3.2 +++ b/src/HOL/ROOT	Sat Dec 29 17:18:01 2012 +0100
     3.3 @@ -41,7 +41,7 @@
     3.4      Sublist
     3.5      List_lexord
     3.6      Sublist_Order
     3.7 -    Product_Lattice
     3.8 +    Finite_Lattice
     3.9      Code_Char_chr
    3.10      Code_Char_ord
    3.11      Code_Integer