src/HOL/Library/Finite_Lattice.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 52729 412c9e0381a1 child 56740 5ebaa364d8ab permissions -rw-r--r--
prefer Code.abort over code_abort
```     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
```
```    18 class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
```
```    19 assumes bot_def: "bot = Inf_fin UNIV"
```
```    20 assumes top_def: "top = Sup_fin UNIV"
```
```    21 assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
```
```    22 assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
```
```    23
```
```    24 text {* The definitional assumptions
```
```    25 on the operators @{const bot} and @{const top}
```
```    26 of class @{class finite_lattice_complete}
```
```    27 ensure that they yield bottom and top. *}
```
```    28
```
```    29 lemma finite_lattice_complete_bot_least:
```
```    30 "(bot::'a::finite_lattice_complete) \<le> x"
```
```    31 by (auto simp: bot_def intro: Inf_fin.coboundedI)
```
```    32
```
```    33 instance finite_lattice_complete \<subseteq> order_bot
```
```    34 proof qed (auto simp: finite_lattice_complete_bot_least)
```
```    35
```
```    36 lemma finite_lattice_complete_top_greatest:
```
```    37 "(top::'a::finite_lattice_complete) \<ge> x"
```
```    38 by (auto simp: top_def Sup_fin.coboundedI)
```
```    39
```
```    40 instance finite_lattice_complete \<subseteq> order_top
```
```    41 proof qed (auto simp: finite_lattice_complete_top_greatest)
```
```    42
```
```    43 instance finite_lattice_complete \<subseteq> bounded_lattice ..
```
```    44
```
```    45 text {* The definitional assumptions
```
```    46 on the operators @{const Inf} and @{const Sup}
```
```    47 of class @{class finite_lattice_complete}
```
```    48 ensure that they yield infimum and supremum. *}
```
```    49
```
```    50 lemma finite_lattice_complete_Inf_empty:
```
```    51   "Inf {} = (top :: 'a::finite_lattice_complete)"
```
```    52   by (simp add: Inf_def)
```
```    53
```
```    54 lemma finite_lattice_complete_Sup_empty:
```
```    55   "Sup {} = (bot :: 'a::finite_lattice_complete)"
```
```    56   by (simp add: Sup_def)
```
```    57
```
```    58 lemma finite_lattice_complete_Inf_insert:
```
```    59   fixes A :: "'a::finite_lattice_complete set"
```
```    60   shows "Inf (insert x A) = inf x (Inf A)"
```
```    61 proof -
```
```    62   interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
```
```    63   show ?thesis by (simp add: Inf_def)
```
```    64 qed
```
```    65
```
```    66 lemma finite_lattice_complete_Sup_insert:
```
```    67   fixes A :: "'a::finite_lattice_complete set"
```
```    68   shows "Sup (insert x A) = sup x (Sup A)"
```
```    69 proof -
```
```    70   interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
```
```    71   show ?thesis by (simp add: Sup_def)
```
```    72 qed
```
```    73
```
```    74 lemma finite_lattice_complete_Inf_lower:
```
```    75   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
```
```    76   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
```
```    77
```
```    78 lemma finite_lattice_complete_Inf_greatest:
```
```    79   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
```
```    80   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
```
```    81
```
```    82 lemma finite_lattice_complete_Sup_upper:
```
```    83   "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
```
```    84   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
```
```    85
```
```    86 lemma finite_lattice_complete_Sup_least:
```
```    87   "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
```
```    88   using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
```
```    89
```
```    90 instance finite_lattice_complete \<subseteq> complete_lattice
```
```    91 proof
```
```    92 qed (auto simp:
```
```    93  finite_lattice_complete_Inf_lower
```
```    94  finite_lattice_complete_Inf_greatest
```
```    95  finite_lattice_complete_Sup_upper
```
```    96  finite_lattice_complete_Sup_least
```
```    97  finite_lattice_complete_Inf_empty
```
```    98  finite_lattice_complete_Sup_empty)
```
```    99
```
```   100 text {* The product of two finite lattices is already a finite lattice. *}
```
```   101
```
```   102 lemma finite_bot_prod:
```
```   103   "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
```
```   104    Inf_fin UNIV"
```
```   105 by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
```
```   106
```
```   107 lemma finite_top_prod:
```
```   108   "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
```
```   109    Sup_fin UNIV"
```
```   110 by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
```
```   111
```
```   112 lemma finite_Inf_prod:
```
```   113   "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
```
```   114   Finite_Set.fold inf top A"
```
```   115 by (metis Inf_fold_inf finite_code)
```
```   116
```
```   117 lemma finite_Sup_prod:
```
```   118   "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
```
```   119   Finite_Set.fold sup bot A"
```
```   120 by (metis Sup_fold_sup finite_code)
```
```   121
```
```   122 instance prod ::
```
```   123   (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
```
```   124 proof
```
```   125 qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
```
```   126
```
```   127 text {* Functions with a finite domain and with a finite lattice as codomain
```
```   128 already form a finite lattice. *}
```
```   129
```
```   130 lemma finite_bot_fun:
```
```   131   "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
```
```   132 by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
```
```   133
```
```   134 lemma finite_top_fun:
```
```   135   "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
```
```   136 by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
```
```   137
```
```   138 lemma finite_Inf_fun:
```
```   139   "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
```
```   140   Finite_Set.fold inf top A"
```
```   141 by (metis Inf_fold_inf finite_code)
```
```   142
```
```   143 lemma finite_Sup_fun:
```
```   144   "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
```
```   145   Finite_Set.fold sup bot A"
```
```   146 by (metis Sup_fold_sup finite_code)
```
```   147
```
```   148 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
```
```   149 proof
```
```   150 qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
```
```   151
```
```   152
```
```   153 subsection {* Finite Distributive Lattices *}
```
```   154
```
```   155 text {* A finite distributive lattice is a complete lattice
```
```   156 whose @{const inf} and @{const sup} operators
```
```   157 distribute over @{const Sup} and @{const Inf}. *}
```
```   158
```
```   159 class finite_distrib_lattice_complete =
```
```   160   distrib_lattice + finite_lattice_complete
```
```   161
```
```   162 lemma finite_distrib_lattice_complete_sup_Inf:
```
```   163   "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
```
```   164 apply (rule finite_induct)
```
```   165 apply (metis finite_code)
```
```   166 apply (metis INF_empty Inf_empty sup_top_right)
```
```   167 apply (metis INF_insert Inf_insert sup_inf_distrib1)
```
```   168 done
```
```   169
```
```   170 lemma finite_distrib_lattice_complete_inf_Sup:
```
```   171   "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
```
```   172 apply (rule finite_induct)
```
```   173 apply (metis finite_code)
```
```   174 apply (metis SUP_empty Sup_empty inf_bot_right)
```
```   175 apply (metis SUP_insert Sup_insert inf_sup_distrib1)
```
```   176 done
```
```   177
```
```   178 instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
```
```   179 proof
```
```   180 qed (auto simp:
```
```   181  finite_distrib_lattice_complete_sup_Inf
```
```   182  finite_distrib_lattice_complete_inf_Sup)
```
```   183
```
```   184 text {* The product of two finite distributive lattices
```
```   185 is already a finite distributive lattice. *}
```
```   186
```
```   187 instance prod ::
```
```   188   (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
```
```   189   finite_distrib_lattice_complete
```
```   190 ..
```
```   191
```
```   192 text {* Functions with a finite domain
```
```   193 and with a finite distributive lattice as codomain
```
```   194 already form a finite distributive lattice. *}
```
```   195
```
```   196 instance "fun" ::
```
```   197   (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
```
```   198 ..
```
```   199
```
```   200
```
```   201 subsection {* Linear Orders *}
```
```   202
```
```   203 text {* A linear order is a distributive lattice.
```
```   204 A type class is defined
```
```   205 that extends class @{class linorder}
```
```   206 with the operators @{const inf} and @{const sup},
```
```   207 along with assumptions that define these operators
```
```   208 in terms of the ones of class @{class linorder}.
```
```   209 The resulting class is a subclass of @{class distrib_lattice}. *}
```
```   210
```
```   211 class linorder_lattice = linorder + inf + sup +
```
```   212 assumes inf_def: "inf x y = (if x \<le> y then x else y)"
```
```   213 assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
```
```   214
```
```   215 text {* The definitional assumptions
```
```   216 on the operators @{const inf} and @{const sup}
```
```   217 of class @{class linorder_lattice}
```
```   218 ensure that they yield infimum and supremum
```
```   219 and that they distribute over each other. *}
```
```   220
```
```   221 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
```
```   222 unfolding inf_def by (metis (full_types) linorder_linear)
```
```   223
```
```   224 lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
```
```   225 unfolding inf_def by (metis (full_types) linorder_linear)
```
```   226
```
```   227 lemma linorder_lattice_inf_greatest:
```
```   228   "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
```
```   229 unfolding inf_def by (metis (full_types))
```
```   230
```
```   231 lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
```
```   232 unfolding sup_def by (metis (full_types) linorder_linear)
```
```   233
```
```   234 lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
```
```   235 unfolding sup_def by (metis (full_types) linorder_linear)
```
```   236
```
```   237 lemma linorder_lattice_sup_least:
```
```   238   "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
```
```   239 by (auto simp: sup_def)
```
```   240
```
```   241 lemma linorder_lattice_sup_inf_distrib1:
```
```   242   "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
```
```   243 by (auto simp: inf_def sup_def)
```
```   244
```
```   245 instance linorder_lattice \<subseteq> distrib_lattice
```
```   246 proof
```
```   247 qed (auto simp:
```
```   248  linorder_lattice_inf_le1
```
```   249  linorder_lattice_inf_le2
```
```   250  linorder_lattice_inf_greatest
```
```   251  linorder_lattice_sup_ge1
```
```   252  linorder_lattice_sup_ge2
```
```   253  linorder_lattice_sup_least
```
```   254  linorder_lattice_sup_inf_distrib1)
```
```   255
```
```   256
```
```   257 subsection {* Finite Linear Orders *}
```
```   258
```
```   259 text {* A (non-empty) finite linear order is a complete linear order. *}
```
```   260
```
```   261 class finite_linorder_complete = linorder_lattice + finite_lattice_complete
```
```   262
```
```   263 instance finite_linorder_complete \<subseteq> complete_linorder ..
```
```   264
```
```   265 text {* A (non-empty) finite linear order is a complete lattice
```
```   266 whose @{const inf} and @{const sup} operators
```
```   267 distribute over @{const Sup} and @{const Inf}. *}
```
```   268
```
```   269 instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
```
```   270
```
```   271
```
```   272 end
```
```   273
```