src/HOL/Library/Finite_Lattice.thy
author haftmann
Sat Mar 23 20:50:39 2013 +0100 (2013-03-23)
changeset 51489 f738e6dbd844
parent 51115 7dbd6832a689
child 52729 412c9e0381a1
permissions -rw-r--r--
fundamental revision of big operators on sets
     1 (* Author: Alessandro Coglio *)
     2 
     3 theory Finite_Lattice
     4 imports Product_Order
     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 lemma finite_lattice_complete_Inf_empty:
    43   "Inf {} = (top :: 'a::finite_lattice_complete)"
    44   by (simp add: Inf_def)
    45 
    46 lemma finite_lattice_complete_Sup_empty:
    47   "Sup {} = (bot :: 'a::finite_lattice_complete)"
    48   by (simp add: Sup_def)
    49 
    50 lemma finite_lattice_complete_Inf_insert:
    51   fixes A :: "'a::finite_lattice_complete set"
    52   shows "Inf (insert x A) = inf x (Inf A)"
    53 proof -
    54   interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
    55   show ?thesis by (simp add: Inf_def)
    56 qed
    57 
    58 lemma finite_lattice_complete_Sup_insert:
    59   fixes A :: "'a::finite_lattice_complete set"
    60   shows "Sup (insert x A) = sup x (Sup A)"
    61 proof -
    62   interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
    63   show ?thesis by (simp add: Sup_def)
    64 qed
    65 
    66 text {* The definitional assumptions
    67 on the operators @{const Inf} and @{const Sup}
    68 of class @{class finite_lattice_complete}
    69 ensure that they yield infimum and supremum,
    70 as required for a complete lattice. *}
    71 
    72 lemma finite_lattice_complete_Inf_lower:
    73   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    74   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    75 
    76 lemma finite_lattice_complete_Inf_greatest:
    77   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    78   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    79 
    80 lemma finite_lattice_complete_Sup_upper:
    81   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    82   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
    83 
    84 lemma finite_lattice_complete_Sup_least:
    85   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
    86   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
    87 
    88 instance finite_lattice_complete \<subseteq> complete_lattice
    89 proof
    90 qed (auto simp:
    91  finite_lattice_complete_Inf_lower
    92  finite_lattice_complete_Inf_greatest
    93  finite_lattice_complete_Sup_upper
    94  finite_lattice_complete_Sup_least)
    95 
    96 
    97 text {* The product of two finite lattices is already a finite lattice. *}
    98 
    99 lemma finite_Inf_prod:
   100   "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   101   Finite_Set.fold inf top A"
   102 by (metis Inf_fold_inf finite_code)
   103 
   104 lemma finite_Sup_prod:
   105   "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   106   Finite_Set.fold sup bot A"
   107 by (metis Sup_fold_sup finite_code)
   108 
   109 instance prod ::
   110   (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   111 proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
   112 
   113 text {* Functions with a finite domain and with a finite lattice as codomain
   114 already form a finite lattice. *}
   115 
   116 lemma finite_Inf_fun:
   117   "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   118   Finite_Set.fold inf top A"
   119 by (metis Inf_fold_inf finite_code)
   120 
   121 lemma finite_Sup_fun:
   122   "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   123   Finite_Set.fold sup bot A"
   124 by (metis Sup_fold_sup finite_code)
   125 
   126 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   127 proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
   128 
   129 
   130 subsection {* Finite Distributive Lattices *}
   131 
   132 text {* A finite distributive lattice is a complete lattice
   133 whose @{const inf} and @{const sup} operators
   134 distribute over @{const Sup} and @{const Inf}. *}
   135 
   136 class finite_distrib_lattice_complete =
   137   distrib_lattice + finite_lattice_complete
   138 
   139 lemma finite_distrib_lattice_complete_sup_Inf:
   140   "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   141 apply (rule finite_induct)
   142 apply (metis finite_code)
   143 apply (metis INF_empty Inf_empty sup_top_right)
   144 apply (metis INF_insert Inf_insert sup_inf_distrib1)
   145 done
   146 
   147 lemma finite_distrib_lattice_complete_inf_Sup:
   148   "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   149 apply (rule finite_induct)
   150 apply (metis finite_code)
   151 apply (metis SUP_empty Sup_empty inf_bot_right)
   152 apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   153 done
   154 
   155 instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   156 proof
   157 qed (auto simp:
   158  finite_distrib_lattice_complete_sup_Inf
   159  finite_distrib_lattice_complete_inf_Sup)
   160 
   161 text {* The product of two finite distributive lattices
   162 is already a finite distributive lattice. *}
   163 
   164 instance prod ::
   165   (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   166   finite_distrib_lattice_complete
   167 ..
   168 
   169 text {* Functions with a finite domain
   170 and with a finite distributive lattice as codomain
   171 already form a finite distributive lattice. *}
   172 
   173 instance "fun" ::
   174   (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   175 ..
   176 
   177 
   178 subsection {* Linear Orders *}
   179 
   180 text {* A linear order is a distributive lattice.
   181 Since in Isabelle/HOL
   182 a subclass must have all the parameters of its superclasses,
   183 class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
   184 So class @{class linorder} is extended with
   185 the operators @{const inf} and @{const sup},
   186 along with assumptions that define these operators
   187 in terms of the ones of class @{class linorder}.
   188 The resulting class is a subclass of @{class distrib_lattice}. *}
   189 
   190 class linorder_lattice = linorder + inf + sup +
   191 assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   192 assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   193 
   194 text {* The definitional assumptions
   195 on the operators @{const inf} and @{const sup}
   196 of class @{class linorder_lattice}
   197 ensure that they yield infimum and supremum,
   198 and that they distribute over each other,
   199 as required for a distributive lattice. *}
   200 
   201 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   202 unfolding inf_def by (metis (full_types) linorder_linear)
   203 
   204 lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   205 unfolding inf_def by (metis (full_types) linorder_linear)
   206 
   207 lemma linorder_lattice_inf_greatest:
   208   "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   209 unfolding inf_def by (metis (full_types))
   210 
   211 lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   212 unfolding sup_def by (metis (full_types) linorder_linear)
   213 
   214 lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   215 unfolding sup_def by (metis (full_types) linorder_linear)
   216 
   217 lemma linorder_lattice_sup_least:
   218   "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   219 by (auto simp: sup_def)
   220 
   221 lemma linorder_lattice_sup_inf_distrib1:
   222   "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   223 by (auto simp: inf_def sup_def)
   224  
   225 instance linorder_lattice \<subseteq> distrib_lattice
   226 proof                                                     
   227 qed (auto simp:
   228  linorder_lattice_inf_le1
   229  linorder_lattice_inf_le2
   230  linorder_lattice_inf_greatest
   231  linorder_lattice_sup_ge1
   232  linorder_lattice_sup_ge2
   233  linorder_lattice_sup_least
   234  linorder_lattice_sup_inf_distrib1)
   235 
   236 
   237 subsection {* Finite Linear Orders *}
   238 
   239 text {* A (non-empty) finite linear order is a complete linear order. *}
   240 
   241 class finite_linorder_complete = linorder_lattice + finite_lattice_complete
   242 
   243 instance finite_linorder_complete \<subseteq> complete_linorder ..
   244 
   245 text {* A (non-empty) finite linear order is a complete lattice
   246 whose @{const inf} and @{const sup} operators
   247 distribute over @{const Sup} and @{const Inf}. *}
   248 
   249 instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   250 
   251 
   252 end