src/HOL/Library/Finite_Lattice.thy
author nipkow
Sat Dec 29 17:18:01 2012 +0100 (2012-12-29)
changeset 50634 009a9fdabbad
child 51115 7dbd6832a689
permissions -rw-r--r--
new theory Library/Finite_Lattice
     1 (* Author: Alessandro Coglio *)
     2 
     3 theory Finite_Lattice
     4 imports Product_Lattice
     5 begin
     6 
     7 text {* A non-empty finite lattice is a complete lattice.
     8 Since types are never empty in Isabelle/HOL,
     9 a type of classes @{class finite} and @{class lattice}
    10 should also have class @{class complete_lattice}.
    11 A type class is defined
    12 that extends classes @{class finite} and @{class lattice}
    13 with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
    14 along with assumptions that define these operators
    15 in terms of the ones of classes @{class finite} and @{class lattice}.
    16 The resulting class is a subclass of @{class complete_lattice}.
    17 Classes @{class bot} and @{class top} already include assumptions that suffice
    18 to define the operators @{const bot} and @{const top} (as proved below),
    19 and so no explicit assumptions on these two operators are needed
    20 in the following type class.%
    21 \footnote{The Isabelle/HOL library does not provide
    22 syntactic classes for the operators @{const bot} and @{const top}.} *}
    23 
    24 class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
    25 assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    26 assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    27 -- "No explicit assumptions on @{const bot} or @{const top}."
    28 
    29 instance finite_lattice_complete \<subseteq> bounded_lattice ..
    30 -- "This subclass relation eases the proof of the next two lemmas."
    31 
    32 lemma finite_lattice_complete_bot_def:
    33   "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
    34 by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
    35 -- "Derived definition of @{const bot}."
    36 
    37 lemma finite_lattice_complete_top_def:
    38   "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
    39 by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
    40 -- "Derived definition of @{const top}."
    41 
    42 text {* The definitional assumptions
    43 on the operators @{const Inf} and @{const Sup}
    44 of class @{class finite_lattice_complete}
    45 ensure that they yield infimum and supremum,
    46 as required for a complete lattice. *}
    47 
    48 lemma finite_lattice_complete_Inf_lower:
    49   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    50 unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf)
    51 
    52 lemma finite_lattice_complete_Inf_greatest:
    53   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    54 unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right)
    55 
    56 lemma finite_lattice_complete_Sup_upper:
    57   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    58 unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup)
    59 
    60 lemma finite_lattice_complete_Sup_least:
    61   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
    62 unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right)
    63 
    64 instance finite_lattice_complete \<subseteq> complete_lattice
    65 proof
    66 qed (auto simp:
    67  finite_lattice_complete_Inf_lower
    68  finite_lattice_complete_Inf_greatest
    69  finite_lattice_complete_Sup_upper
    70  finite_lattice_complete_Sup_least)
    71 
    72 
    73 text {* The product of two finite lattices is already a finite lattice. *}
    74 
    75 lemma finite_Inf_prod:
    76   "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    77   Finite_Set.fold inf top A"
    78 by (metis Inf_fold_inf finite_code)
    79 
    80 lemma finite_Sup_prod:
    81   "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    82   Finite_Set.fold sup bot A"
    83 by (metis Sup_fold_sup finite_code)
    84 
    85 instance prod ::
    86   (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
    87 proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
    88 
    89 text {* Functions with a finite domain and with a finite lattice as codomain
    90 already form a finite lattice. *}
    91 
    92 lemma finite_Inf_fun:
    93   "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
    94   Finite_Set.fold inf top A"
    95 by (metis Inf_fold_inf finite_code)
    96 
    97 lemma finite_Sup_fun:
    98   "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
    99   Finite_Set.fold sup bot A"
   100 by (metis Sup_fold_sup finite_code)
   101 
   102 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   103 proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
   104 
   105 
   106 subsection {* Finite Distributive Lattices *}
   107 
   108 text {* A finite distributive lattice is a complete lattice
   109 whose @{const inf} and @{const sup} operators
   110 distribute over @{const Sup} and @{const Inf}. *}
   111 
   112 class finite_distrib_lattice_complete =
   113   distrib_lattice + finite_lattice_complete
   114 
   115 lemma finite_distrib_lattice_complete_sup_Inf:
   116   "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   117 apply (rule finite_induct)
   118 apply (metis finite_code)
   119 apply (metis INF_empty Inf_empty sup_top_right)
   120 apply (metis INF_insert Inf_insert sup_inf_distrib1)
   121 done
   122 
   123 lemma finite_distrib_lattice_complete_inf_Sup:
   124   "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   125 apply (rule finite_induct)
   126 apply (metis finite_code)
   127 apply (metis SUP_empty Sup_empty inf_bot_right)
   128 apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   129 done
   130 
   131 instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   132 proof
   133 qed (auto simp:
   134  finite_distrib_lattice_complete_sup_Inf
   135  finite_distrib_lattice_complete_inf_Sup)
   136 
   137 text {* The product of two finite distributive lattices
   138 is already a finite distributive lattice. *}
   139 
   140 instance prod ::
   141   (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   142   finite_distrib_lattice_complete
   143 ..
   144 
   145 text {* Functions with a finite domain
   146 and with a finite distributive lattice as codomain
   147 already form a finite distributive lattice. *}
   148 
   149 instance "fun" ::
   150   (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   151 ..
   152 
   153 
   154 subsection {* Linear Orders *}
   155 
   156 text {* A linear order is a distributive lattice.
   157 Since in Isabelle/HOL
   158 a subclass must have all the parameters of its superclasses,
   159 class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
   160 So class @{class linorder} is extended with
   161 the operators @{const inf} and @{const sup},
   162 along with assumptions that define these operators
   163 in terms of the ones of class @{class linorder}.
   164 The resulting class is a subclass of @{class distrib_lattice}. *}
   165 
   166 class linorder_lattice = linorder + inf + sup +
   167 assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   168 assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   169 
   170 text {* The definitional assumptions
   171 on the operators @{const inf} and @{const sup}
   172 of class @{class linorder_lattice}
   173 ensure that they yield infimum and supremum,
   174 and that they distribute over each other,
   175 as required for a distributive lattice. *}
   176 
   177 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   178 unfolding inf_def by (metis (full_types) linorder_linear)
   179 
   180 lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   181 unfolding inf_def by (metis (full_types) linorder_linear)
   182 
   183 lemma linorder_lattice_inf_greatest:
   184   "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   185 unfolding inf_def by (metis (full_types))
   186 
   187 lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   188 unfolding sup_def by (metis (full_types) linorder_linear)
   189 
   190 lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   191 unfolding sup_def by (metis (full_types) linorder_linear)
   192 
   193 lemma linorder_lattice_sup_least:
   194   "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   195 by (auto simp: sup_def)
   196 
   197 lemma linorder_lattice_sup_inf_distrib1:
   198   "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   199 by (auto simp: inf_def sup_def)
   200  
   201 instance linorder_lattice \<subseteq> distrib_lattice
   202 proof                                                     
   203 qed (auto simp:
   204  linorder_lattice_inf_le1
   205  linorder_lattice_inf_le2
   206  linorder_lattice_inf_greatest
   207  linorder_lattice_sup_ge1
   208  linorder_lattice_sup_ge2
   209  linorder_lattice_sup_least
   210  linorder_lattice_sup_inf_distrib1)
   211 
   212 
   213 subsection {* Finite Linear Orders *}
   214 
   215 text {* A (non-empty) finite linear order is a complete linear order. *}
   216 
   217 class finite_linorder_complete = linorder_lattice + finite_lattice_complete
   218 
   219 instance finite_linorder_complete \<subseteq> complete_linorder ..
   220 
   221 text {* A (non-empty) finite linear order is a complete lattice
   222 whose @{const inf} and @{const sup} operators
   223 distribute over @{const Sup} and @{const Inf}. *}
   224 
   225 instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   226 
   227 
   228 end