author | haftmann |
Thu, 25 Jul 2013 08:57:16 +0200 | |
changeset 52729 | 412c9e0381a1 |
parent 51489 | f738e6dbd844 |
child 56740 | 5ebaa364d8ab |
permissions | -rw-r--r-- |
50634 | 1 |
(* Author: Alessandro Coglio *) |
2 |
||
3 |
theory Finite_Lattice |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50634
diff
changeset
|
4 |
imports Product_Order |
50634 | 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}. |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
16 |
The resulting class is a subclass of @{class complete_lattice}. *} |
50634 | 17 |
|
18 |
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup + |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
19 |
assumes bot_def: "bot = Inf_fin UNIV" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
20 |
assumes top_def: "top = Sup_fin UNIV" |
50634 | 21 |
assumes Inf_def: "Inf A = Finite_Set.fold inf top A" |
22 |
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
|
23 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
24 |
text {* The definitional assumptions |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
25 |
on the operators @{const bot} and @{const top} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
26 |
of class @{class finite_lattice_complete} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
27 |
ensure that they yield bottom and top. *} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
28 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
29 |
lemma finite_lattice_complete_bot_least: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
30 |
"(bot::'a::finite_lattice_complete) \<le> x" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
31 |
by (auto simp: bot_def intro: Inf_fin.coboundedI) |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
32 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
33 |
instance finite_lattice_complete \<subseteq> order_bot |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
34 |
proof qed (auto simp: finite_lattice_complete_bot_least) |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
35 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
36 |
lemma finite_lattice_complete_top_greatest: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
37 |
"(top::'a::finite_lattice_complete) \<ge> x" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
38 |
by (auto simp: top_def Sup_fin.coboundedI) |
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 |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
41 |
proof qed (auto simp: finite_lattice_complete_top_greatest) |
50634 | 42 |
|
43 |
instance finite_lattice_complete \<subseteq> bounded_lattice .. |
|
44 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
45 |
text {* The definitional assumptions |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
46 |
on the operators @{const Inf} and @{const Sup} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
47 |
of class @{class finite_lattice_complete} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
48 |
ensure that they yield infimum and supremum. *} |
50634 | 49 |
|
51489 | 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 |
||
50634 | 74 |
lemma finite_lattice_complete_Inf_lower: |
75 |
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x" |
|
51489 | 76 |
using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2) |
50634 | 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" |
|
51489 | 80 |
using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert) |
50634 | 81 |
|
82 |
lemma finite_lattice_complete_Sup_upper: |
|
83 |
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x" |
|
51489 | 84 |
using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2) |
50634 | 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" |
|
51489 | 88 |
using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert) |
50634 | 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 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
96 |
finite_lattice_complete_Sup_least |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
97 |
finite_lattice_complete_Inf_empty |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
98 |
finite_lattice_complete_Sup_empty) |
50634 | 99 |
|
100 |
text {* The product of two finite lattices is already a finite lattice. *} |
|
101 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
102 |
lemma finite_bot_prod: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
103 |
"(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
104 |
Inf_fin UNIV" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
105 |
by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV) |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
106 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
107 |
lemma finite_top_prod: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
108 |
"(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
109 |
Sup_fin UNIV" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
110 |
by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV) |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
111 |
|
50634 | 112 |
lemma finite_Inf_prod: |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
113 |
"Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = |
50634 | 114 |
Finite_Set.fold inf top A" |
115 |
by (metis Inf_fold_inf finite_code) |
|
116 |
||
117 |
lemma finite_Sup_prod: |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
118 |
"Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = |
50634 | 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 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
124 |
proof |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
125 |
qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod) |
50634 | 126 |
|
127 |
text {* Functions with a finite domain and with a finite lattice as codomain |
|
128 |
already form a finite lattice. *} |
|
129 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
130 |
lemma finite_bot_fun: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
131 |
"(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
132 |
by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code) |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
133 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
134 |
lemma finite_top_fun: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
135 |
"(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV" |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
136 |
by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code) |
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) = |
|
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 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
149 |
proof |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
150 |
qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun) |
50634 | 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. |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
204 |
A type class is defined |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
205 |
that extends class @{class linorder} |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
206 |
with the operators @{const inf} and @{const sup}, |
50634 | 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} |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
218 |
ensure that they yield infimum and supremum |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
219 |
and that they distribute over each other. *} |
50634 | 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 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset
|
273 |