author | nipkow |
Mon, 30 May 2022 20:58:45 +0200 | |
changeset 75496 | 99b37c391433 |
parent 73832 | 9db620f007fa |
child 77811 | ae9e6218443d |
permissions | -rw-r--r-- |
56796 | 1 |
(* Title: HOL/Library/Finite_Lattice.thy |
2 |
Author: Alessandro Coglio |
|
3 |
*) |
|
50634 | 4 |
|
5 |
theory Finite_Lattice |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50634
diff
changeset
|
6 |
imports Product_Order |
50634 | 7 |
begin |
8 |
||
60500 | 9 |
text \<open>A non-empty finite lattice is a complete lattice. |
50634 | 10 |
Since types are never empty in Isabelle/HOL, |
69593 | 11 |
a type of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close> |
12 |
should also have class \<^class>\<open>complete_lattice\<close>. |
|
50634 | 13 |
A type class is defined |
69593 | 14 |
that extends classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close> |
15 |
with the operators \<^const>\<open>bot\<close>, \<^const>\<open>top\<close>, \<^const>\<open>Inf\<close>, and \<^const>\<open>Sup\<close>, |
|
50634 | 16 |
along with assumptions that define these operators |
69593 | 17 |
in terms of the ones of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>. |
18 |
The resulting class is a subclass of \<^class>\<open>complete_lattice\<close>.\<close> |
|
50634 | 19 |
|
20 |
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup + |
|
56796 | 21 |
assumes bot_def: "bot = Inf_fin UNIV" |
22 |
assumes top_def: "top = Sup_fin UNIV" |
|
23 |
assumes Inf_def: "Inf A = Finite_Set.fold inf top A" |
|
24 |
assumes Sup_def: "Sup A = Finite_Set.fold sup bot A" |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
25 |
|
60500 | 26 |
text \<open>The definitional assumptions |
69593 | 27 |
on the operators \<^const>\<open>bot\<close> and \<^const>\<open>top\<close> |
28 |
of class \<^class>\<open>finite_lattice_complete\<close> |
|
60500 | 29 |
ensure that they yield bottom and top.\<close> |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
30 |
|
56796 | 31 |
lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x" |
32 |
by (auto simp: bot_def intro: Inf_fin.coboundedI) |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
33 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
34 |
instance finite_lattice_complete \<subseteq> order_bot |
60679 | 35 |
by standard (auto simp: finite_lattice_complete_bot_least) |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
36 |
|
56796 | 37 |
lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x" |
38 |
by (auto simp: top_def Sup_fin.coboundedI) |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
39 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
40 |
instance finite_lattice_complete \<subseteq> order_top |
60679 | 41 |
by standard (auto simp: finite_lattice_complete_top_greatest) |
50634 | 42 |
|
43 |
instance finite_lattice_complete \<subseteq> bounded_lattice .. |
|
44 |
||
60500 | 45 |
text \<open>The definitional assumptions |
69593 | 46 |
on the operators \<^const>\<open>Inf\<close> and \<^const>\<open>Sup\<close> |
47 |
of class \<^class>\<open>finite_lattice_complete\<close> |
|
60500 | 48 |
ensure that they yield infimum and supremum.\<close> |
50634 | 49 |
|
56796 | 50 |
lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)" |
51489 | 51 |
by (simp add: Inf_def) |
52 |
||
56796 | 53 |
lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)" |
51489 | 54 |
by (simp add: Sup_def) |
55 |
||
56 |
lemma finite_lattice_complete_Inf_insert: |
|
57 |
fixes A :: "'a::finite_lattice_complete set" |
|
58 |
shows "Inf (insert x A) = inf x (Inf A)" |
|
59 |
proof - |
|
56796 | 60 |
interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" |
61 |
by (fact comp_fun_idem_inf) |
|
51489 | 62 |
show ?thesis by (simp add: Inf_def) |
63 |
qed |
|
64 |
||
65 |
lemma finite_lattice_complete_Sup_insert: |
|
66 |
fixes A :: "'a::finite_lattice_complete set" |
|
67 |
shows "Sup (insert x A) = sup x (Sup A)" |
|
68 |
proof - |
|
56796 | 69 |
interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" |
70 |
by (fact comp_fun_idem_sup) |
|
51489 | 71 |
show ?thesis by (simp add: Sup_def) |
72 |
qed |
|
73 |
||
50634 | 74 |
lemma finite_lattice_complete_Inf_lower: |
75 |
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x" |
|
56796 | 76 |
using finite [of A] |
77 |
by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2) |
|
50634 | 78 |
|
79 |
lemma finite_lattice_complete_Inf_greatest: |
|
80 |
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A" |
|
56796 | 81 |
using finite [of A] |
82 |
by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert) |
|
50634 | 83 |
|
84 |
lemma finite_lattice_complete_Sup_upper: |
|
85 |
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x" |
|
56796 | 86 |
using finite [of A] |
87 |
by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2) |
|
50634 | 88 |
|
89 |
lemma finite_lattice_complete_Sup_least: |
|
90 |
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A" |
|
56796 | 91 |
using finite [of A] |
92 |
by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert) |
|
50634 | 93 |
|
94 |
instance finite_lattice_complete \<subseteq> complete_lattice |
|
95 |
proof |
|
96 |
qed (auto simp: |
|
56796 | 97 |
finite_lattice_complete_Inf_lower |
98 |
finite_lattice_complete_Inf_greatest |
|
99 |
finite_lattice_complete_Sup_upper |
|
100 |
finite_lattice_complete_Sup_least |
|
101 |
finite_lattice_complete_Inf_empty |
|
102 |
finite_lattice_complete_Sup_empty) |
|
50634 | 103 |
|
60500 | 104 |
text \<open>The product of two finite lattices is already a finite lattice.\<close> |
50634 | 105 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
106 |
lemma finite_bot_prod: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
107 |
"(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = |
56796 | 108 |
Inf_fin UNIV" |
109 |
by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV) |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
110 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
111 |
lemma finite_top_prod: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
112 |
"(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = |
56796 | 113 |
Sup_fin UNIV" |
114 |
by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV) |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
115 |
|
50634 | 116 |
lemma finite_Inf_prod: |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
117 |
"Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = |
56796 | 118 |
Finite_Set.fold inf top A" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
119 |
by (metis Inf_fold_inf finite) |
50634 | 120 |
|
121 |
lemma finite_Sup_prod: |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
122 |
"Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = |
56796 | 123 |
Finite_Set.fold sup bot A" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
124 |
by (metis Sup_fold_sup finite) |
50634 | 125 |
|
56796 | 126 |
instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete |
60679 | 127 |
by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod) |
50634 | 128 |
|
60500 | 129 |
text \<open>Functions with a finite domain and with a finite lattice as codomain |
130 |
already form a finite lattice.\<close> |
|
50634 | 131 |
|
56796 | 132 |
lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
133 |
by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite) |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
134 |
|
56796 | 135 |
lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
136 |
by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite) |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
137 |
|
50634 | 138 |
lemma finite_Inf_fun: |
139 |
"Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) = |
|
56796 | 140 |
Finite_Set.fold inf top A" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
141 |
by (metis Inf_fold_inf finite) |
50634 | 142 |
|
143 |
lemma finite_Sup_fun: |
|
144 |
"Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) = |
|
56796 | 145 |
Finite_Set.fold sup bot A" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
146 |
by (metis Sup_fold_sup finite) |
50634 | 147 |
|
148 |
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete |
|
60679 | 149 |
by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun) |
50634 | 150 |
|
151 |
||
60500 | 152 |
subsection \<open>Finite Distributive Lattices\<close> |
50634 | 153 |
|
60500 | 154 |
text \<open>A finite distributive lattice is a complete lattice |
69593 | 155 |
whose \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close> operators |
156 |
distribute over \<^const>\<open>Sup\<close> and \<^const>\<open>Inf\<close>.\<close> |
|
50634 | 157 |
|
158 |
class finite_distrib_lattice_complete = |
|
159 |
distrib_lattice + finite_lattice_complete |
|
160 |
||
161 |
lemma finite_distrib_lattice_complete_sup_Inf: |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
162 |
"sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y\<in>A. sup x y)" |
56796 | 163 |
using finite |
164 |
by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1) |
|
50634 | 165 |
|
166 |
lemma finite_distrib_lattice_complete_inf_Sup: |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
167 |
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y\<in>A. inf x y)" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
60679
diff
changeset
|
168 |
using finite [of A] by induct (simp_all add: inf_sup_distrib1) |
50634 | 169 |
|
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
170 |
context finite_distrib_lattice_complete |
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
171 |
begin |
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
172 |
subclass finite_distrib_lattice |
73832 | 173 |
proof - |
174 |
show "class.finite_distrib_lattice Inf Sup inf (\<le>) (<) sup bot top" |
|
175 |
proof |
|
176 |
show "bot = Inf UNIV" |
|
177 |
unfolding bot_def top_def Inf_def |
|
178 |
using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force |
|
179 |
next |
|
180 |
show "top = Sup UNIV" |
|
181 |
unfolding bot_def top_def Sup_def |
|
182 |
using Sup_fin.eq_fold Sup_fin.insert by force |
|
183 |
next |
|
184 |
show "Inf {} = Sup UNIV" |
|
185 |
unfolding Inf_def Sup_def bot_def top_def |
|
186 |
using Sup_fin.eq_fold Sup_fin.insert by force |
|
187 |
next |
|
188 |
show "Sup {} = Inf UNIV" |
|
189 |
unfolding Inf_def Sup_def bot_def top_def |
|
190 |
using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force |
|
191 |
next |
|
192 |
interpret comp_fun_idem_inf: comp_fun_idem inf |
|
193 |
by (fact comp_fun_idem_inf) |
|
194 |
show "Inf (insert a A) = inf a (Inf A)" for a A |
|
195 |
using comp_fun_idem_inf.fold_insert_idem Inf_def finite by simp |
|
196 |
next |
|
197 |
interpret comp_fun_idem_sup: comp_fun_idem sup |
|
198 |
by (fact comp_fun_idem_sup) |
|
199 |
show "Sup (insert a A) = sup a (Sup A)" for a A |
|
200 |
using comp_fun_idem_sup.fold_insert_idem Sup_def finite by simp |
|
201 |
qed |
|
202 |
qed |
|
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
203 |
end |
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
204 |
|
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
62343
diff
changeset
|
205 |
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice .. |
50634 | 206 |
|
60500 | 207 |
text \<open>The product of two finite distributive lattices |
208 |
is already a finite distributive lattice.\<close> |
|
50634 | 209 |
|
210 |
instance prod :: |
|
211 |
(finite_distrib_lattice_complete, finite_distrib_lattice_complete) |
|
212 |
finite_distrib_lattice_complete |
|
56796 | 213 |
.. |
50634 | 214 |
|
60500 | 215 |
text \<open>Functions with a finite domain |
50634 | 216 |
and with a finite distributive lattice as codomain |
60500 | 217 |
already form a finite distributive lattice.\<close> |
50634 | 218 |
|
219 |
instance "fun" :: |
|
220 |
(finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete |
|
56796 | 221 |
.. |
50634 | 222 |
|
60500 | 223 |
subsection \<open>Linear Orders\<close> |
50634 | 224 |
|
60500 | 225 |
text \<open>A linear order is a distributive lattice. |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
226 |
A type class is defined |
69593 | 227 |
that extends class \<^class>\<open>linorder\<close> |
228 |
with the operators \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close>, |
|
50634 | 229 |
along with assumptions that define these operators |
69593 | 230 |
in terms of the ones of class \<^class>\<open>linorder\<close>. |
231 |
The resulting class is a subclass of \<^class>\<open>distrib_lattice\<close>.\<close> |
|
50634 | 232 |
|
233 |
class linorder_lattice = linorder + inf + sup + |
|
56796 | 234 |
assumes inf_def: "inf x y = (if x \<le> y then x else y)" |
235 |
assumes sup_def: "sup x y = (if x \<ge> y then x else y)" |
|
50634 | 236 |
|
60500 | 237 |
text \<open>The definitional assumptions |
69593 | 238 |
on the operators \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close> |
239 |
of class \<^class>\<open>linorder_lattice\<close> |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
240 |
ensure that they yield infimum and supremum |
60500 | 241 |
and that they distribute over each other.\<close> |
50634 | 242 |
|
243 |
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x" |
|
56796 | 244 |
unfolding inf_def by (metis (full_types) linorder_linear) |
50634 | 245 |
|
246 |
lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y" |
|
56796 | 247 |
unfolding inf_def by (metis (full_types) linorder_linear) |
50634 | 248 |
|
249 |
lemma linorder_lattice_inf_greatest: |
|
250 |
"(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" |
|
56796 | 251 |
unfolding inf_def by (metis (full_types)) |
50634 | 252 |
|
253 |
lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x" |
|
56796 | 254 |
unfolding sup_def by (metis (full_types) linorder_linear) |
50634 | 255 |
|
256 |
lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y" |
|
56796 | 257 |
unfolding sup_def by (metis (full_types) linorder_linear) |
50634 | 258 |
|
259 |
lemma linorder_lattice_sup_least: |
|
260 |
"(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z" |
|
56796 | 261 |
by (auto simp: sup_def) |
50634 | 262 |
|
263 |
lemma linorder_lattice_sup_inf_distrib1: |
|
264 |
"sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)" |
|
56796 | 265 |
by (auto simp: inf_def sup_def) |
266 |
||
50634 | 267 |
instance linorder_lattice \<subseteq> distrib_lattice |
56796 | 268 |
proof |
50634 | 269 |
qed (auto simp: |
56796 | 270 |
linorder_lattice_inf_le1 |
271 |
linorder_lattice_inf_le2 |
|
272 |
linorder_lattice_inf_greatest |
|
273 |
linorder_lattice_sup_ge1 |
|
274 |
linorder_lattice_sup_ge2 |
|
275 |
linorder_lattice_sup_least |
|
276 |
linorder_lattice_sup_inf_distrib1) |
|
50634 | 277 |
|
278 |
||
60500 | 279 |
subsection \<open>Finite Linear Orders\<close> |
50634 | 280 |
|
60500 | 281 |
text \<open>A (non-empty) finite linear order is a complete linear order.\<close> |
50634 | 282 |
|
283 |
class finite_linorder_complete = linorder_lattice + finite_lattice_complete |
|
284 |
||
285 |
instance finite_linorder_complete \<subseteq> complete_linorder .. |
|
286 |
||
60500 | 287 |
text \<open>A (non-empty) finite linear order is a complete lattice |
69593 | 288 |
whose \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close> operators |
289 |
distribute over \<^const>\<open>Sup\<close> and \<^const>\<open>Inf\<close>.\<close> |
|
50634 | 290 |
|
291 |
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete .. |
|
292 |
||
293 |
end |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
294 |