src/HOL/Library/Finite_Lattice.thy
 author haftmann Tue Feb 19 19:44:10 2013 +0100 (2013-02-19) changeset 51188 9b5bf1a9a710 parent 51115 7dbd6832a689 child 51489 f738e6dbd844 permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
```     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 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
```