src/HOL/Library/Finite_Lattice.thy
changeset 50634 009a9fdabbad
child 51115 7dbd6832a689
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Sat Dec 29 17:18:01 2012 +0100
     1.3 @@ -0,0 +1,228 @@
     1.4 +(* Author: Alessandro Coglio *)
     1.5 +
     1.6 +theory Finite_Lattice
     1.7 +imports Product_Lattice
     1.8 +begin
     1.9 +
    1.10 +text {* A non-empty finite lattice is a complete lattice.
    1.11 +Since types are never empty in Isabelle/HOL,
    1.12 +a type of classes @{class finite} and @{class lattice}
    1.13 +should also have class @{class complete_lattice}.
    1.14 +A type class is defined
    1.15 +that extends classes @{class finite} and @{class lattice}
    1.16 +with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
    1.17 +along with assumptions that define these operators
    1.18 +in terms of the ones of classes @{class finite} and @{class lattice}.
    1.19 +The resulting class is a subclass of @{class complete_lattice}.
    1.20 +Classes @{class bot} and @{class top} already include assumptions that suffice
    1.21 +to define the operators @{const bot} and @{const top} (as proved below),
    1.22 +and so no explicit assumptions on these two operators are needed
    1.23 +in the following type class.%
    1.24 +\footnote{The Isabelle/HOL library does not provide
    1.25 +syntactic classes for the operators @{const bot} and @{const top}.} *}
    1.26 +
    1.27 +class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
    1.28 +assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    1.29 +assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    1.30 +-- "No explicit assumptions on @{const bot} or @{const top}."
    1.31 +
    1.32 +instance finite_lattice_complete \<subseteq> bounded_lattice ..
    1.33 +-- "This subclass relation eases the proof of the next two lemmas."
    1.34 +
    1.35 +lemma finite_lattice_complete_bot_def:
    1.36 +  "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
    1.37 +by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
    1.38 +-- "Derived definition of @{const bot}."
    1.39 +
    1.40 +lemma finite_lattice_complete_top_def:
    1.41 +  "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
    1.42 +by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
    1.43 +-- "Derived definition of @{const top}."
    1.44 +
    1.45 +text {* The definitional assumptions
    1.46 +on the operators @{const Inf} and @{const Sup}
    1.47 +of class @{class finite_lattice_complete}
    1.48 +ensure that they yield infimum and supremum,
    1.49 +as required for a complete lattice. *}
    1.50 +
    1.51 +lemma finite_lattice_complete_Inf_lower:
    1.52 +  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    1.53 +unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf)
    1.54 +
    1.55 +lemma finite_lattice_complete_Inf_greatest:
    1.56 +  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    1.57 +unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right)
    1.58 +
    1.59 +lemma finite_lattice_complete_Sup_upper:
    1.60 +  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    1.61 +unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup)
    1.62 +
    1.63 +lemma finite_lattice_complete_Sup_least:
    1.64 +  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
    1.65 +unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right)
    1.66 +
    1.67 +instance finite_lattice_complete \<subseteq> complete_lattice
    1.68 +proof
    1.69 +qed (auto simp:
    1.70 + finite_lattice_complete_Inf_lower
    1.71 + finite_lattice_complete_Inf_greatest
    1.72 + finite_lattice_complete_Sup_upper
    1.73 + finite_lattice_complete_Sup_least)
    1.74 +
    1.75 +
    1.76 +text {* The product of two finite lattices is already a finite lattice. *}
    1.77 +
    1.78 +lemma finite_Inf_prod:
    1.79 +  "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    1.80 +  Finite_Set.fold inf top A"
    1.81 +by (metis Inf_fold_inf finite_code)
    1.82 +
    1.83 +lemma finite_Sup_prod:
    1.84 +  "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    1.85 +  Finite_Set.fold sup bot A"
    1.86 +by (metis Sup_fold_sup finite_code)
    1.87 +
    1.88 +instance prod ::
    1.89 +  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
    1.90 +proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
    1.91 +
    1.92 +text {* Functions with a finite domain and with a finite lattice as codomain
    1.93 +already form a finite lattice. *}
    1.94 +
    1.95 +lemma finite_Inf_fun:
    1.96 +  "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
    1.97 +  Finite_Set.fold inf top A"
    1.98 +by (metis Inf_fold_inf finite_code)
    1.99 +
   1.100 +lemma finite_Sup_fun:
   1.101 +  "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   1.102 +  Finite_Set.fold sup bot A"
   1.103 +by (metis Sup_fold_sup finite_code)
   1.104 +
   1.105 +instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   1.106 +proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
   1.107 +
   1.108 +
   1.109 +subsection {* Finite Distributive Lattices *}
   1.110 +
   1.111 +text {* A finite distributive lattice is a complete lattice
   1.112 +whose @{const inf} and @{const sup} operators
   1.113 +distribute over @{const Sup} and @{const Inf}. *}
   1.114 +
   1.115 +class finite_distrib_lattice_complete =
   1.116 +  distrib_lattice + finite_lattice_complete
   1.117 +
   1.118 +lemma finite_distrib_lattice_complete_sup_Inf:
   1.119 +  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   1.120 +apply (rule finite_induct)
   1.121 +apply (metis finite_code)
   1.122 +apply (metis INF_empty Inf_empty sup_top_right)
   1.123 +apply (metis INF_insert Inf_insert sup_inf_distrib1)
   1.124 +done
   1.125 +
   1.126 +lemma finite_distrib_lattice_complete_inf_Sup:
   1.127 +  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   1.128 +apply (rule finite_induct)
   1.129 +apply (metis finite_code)
   1.130 +apply (metis SUP_empty Sup_empty inf_bot_right)
   1.131 +apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   1.132 +done
   1.133 +
   1.134 +instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   1.135 +proof
   1.136 +qed (auto simp:
   1.137 + finite_distrib_lattice_complete_sup_Inf
   1.138 + finite_distrib_lattice_complete_inf_Sup)
   1.139 +
   1.140 +text {* The product of two finite distributive lattices
   1.141 +is already a finite distributive lattice. *}
   1.142 +
   1.143 +instance prod ::
   1.144 +  (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   1.145 +  finite_distrib_lattice_complete
   1.146 +..
   1.147 +
   1.148 +text {* Functions with a finite domain
   1.149 +and with a finite distributive lattice as codomain
   1.150 +already form a finite distributive lattice. *}
   1.151 +
   1.152 +instance "fun" ::
   1.153 +  (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   1.154 +..
   1.155 +
   1.156 +
   1.157 +subsection {* Linear Orders *}
   1.158 +
   1.159 +text {* A linear order is a distributive lattice.
   1.160 +Since in Isabelle/HOL
   1.161 +a subclass must have all the parameters of its superclasses,
   1.162 +class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
   1.163 +So class @{class linorder} is extended with
   1.164 +the operators @{const inf} and @{const sup},
   1.165 +along with assumptions that define these operators
   1.166 +in terms of the ones of class @{class linorder}.
   1.167 +The resulting class is a subclass of @{class distrib_lattice}. *}
   1.168 +
   1.169 +class linorder_lattice = linorder + inf + sup +
   1.170 +assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   1.171 +assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   1.172 +
   1.173 +text {* The definitional assumptions
   1.174 +on the operators @{const inf} and @{const sup}
   1.175 +of class @{class linorder_lattice}
   1.176 +ensure that they yield infimum and supremum,
   1.177 +and that they distribute over each other,
   1.178 +as required for a distributive lattice. *}
   1.179 +
   1.180 +lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   1.181 +unfolding inf_def by (metis (full_types) linorder_linear)
   1.182 +
   1.183 +lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   1.184 +unfolding inf_def by (metis (full_types) linorder_linear)
   1.185 +
   1.186 +lemma linorder_lattice_inf_greatest:
   1.187 +  "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   1.188 +unfolding inf_def by (metis (full_types))
   1.189 +
   1.190 +lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   1.191 +unfolding sup_def by (metis (full_types) linorder_linear)
   1.192 +
   1.193 +lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   1.194 +unfolding sup_def by (metis (full_types) linorder_linear)
   1.195 +
   1.196 +lemma linorder_lattice_sup_least:
   1.197 +  "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   1.198 +by (auto simp: sup_def)
   1.199 +
   1.200 +lemma linorder_lattice_sup_inf_distrib1:
   1.201 +  "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   1.202 +by (auto simp: inf_def sup_def)
   1.203 + 
   1.204 +instance linorder_lattice \<subseteq> distrib_lattice
   1.205 +proof                                                     
   1.206 +qed (auto simp:
   1.207 + linorder_lattice_inf_le1
   1.208 + linorder_lattice_inf_le2
   1.209 + linorder_lattice_inf_greatest
   1.210 + linorder_lattice_sup_ge1
   1.211 + linorder_lattice_sup_ge2
   1.212 + linorder_lattice_sup_least
   1.213 + linorder_lattice_sup_inf_distrib1)
   1.214 +
   1.215 +
   1.216 +subsection {* Finite Linear Orders *}
   1.217 +
   1.218 +text {* A (non-empty) finite linear order is a complete linear order. *}
   1.219 +
   1.220 +class finite_linorder_complete = linorder_lattice + finite_lattice_complete
   1.221 +
   1.222 +instance finite_linorder_complete \<subseteq> complete_linorder ..
   1.223 +
   1.224 +text {* A (non-empty) finite linear order is a complete lattice
   1.225 +whose @{const inf} and @{const sup} operators
   1.226 +distribute over @{const Sup} and @{const Inf}. *}
   1.227 +
   1.228 +instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   1.229 +
   1.230 +
   1.231 +end