author | haftmann |
Fri, 16 Mar 2007 21:32:07 +0100 | |
changeset 22451 | 989182f660e0 |
parent 22422 | ee19cdb07528 |
child 22454 | c3654ba76a09 |
permissions | -rw-r--r-- |
21249 | 1 |
(* Title: HOL/Lattices.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
*) |
|
5 |
||
21733 | 6 |
header {* Lattices via Locales *} |
21249 | 7 |
|
8 |
theory Lattices |
|
9 |
imports Orderings |
|
10 |
begin |
|
11 |
||
12 |
subsection{* Lattices *} |
|
13 |
||
14 |
text{* This theory of lattice locales only defines binary sup and inf |
|
15 |
operations. The extension to finite sets is done in theory @{text |
|
16 |
Finite_Set}. In the longer term it may be better to define arbitrary |
|
17 |
sups and infs via @{text THE}. *} |
|
18 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
19 |
class lower_semilattice = order + |
21249 | 20 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
21 |
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
21733 | 22 |
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
21249 | 23 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
24 |
class upper_semilattice = order + |
21249 | 25 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
26 |
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
21733 | 27 |
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
21249 | 28 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
29 |
class lattice = lower_semilattice + upper_semilattice |
21249 | 30 |
|
21733 | 31 |
subsubsection{* Intro and elim rules*} |
32 |
||
33 |
context lower_semilattice |
|
34 |
begin |
|
21249 | 35 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
36 |
lemmas antisym_intro [intro!] = antisym |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
37 |
lemmas (in -) [rule del] = antisym_intro |
21249 | 38 |
|
21734 | 39 |
lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
21733 | 40 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
41 |
apply(blast intro: order_trans) |
21733 | 42 |
apply simp |
43 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
44 |
lemmas (in -) [rule del] = le_infI1 |
21249 | 45 |
|
21734 | 46 |
lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
21733 | 47 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
48 |
apply(blast intro: order_trans) |
21733 | 49 |
apply simp |
50 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
51 |
lemmas (in -) [rule del] = le_infI2 |
21733 | 52 |
|
21734 | 53 |
lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
21733 | 54 |
by(blast intro: inf_greatest) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
55 |
lemmas (in -) [rule del] = le_infI |
21249 | 56 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
57 |
lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
58 |
by (blast intro: order_trans) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
59 |
lemmas (in -) [rule del] = le_infE |
21249 | 60 |
|
21734 | 61 |
lemma le_inf_iff [simp]: |
21733 | 62 |
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)" |
63 |
by blast |
|
64 |
||
21734 | 65 |
lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
22168 | 66 |
by(blast dest:eq_iff[THEN iffD1]) |
21249 | 67 |
|
21733 | 68 |
end |
69 |
||
70 |
||
71 |
context upper_semilattice |
|
72 |
begin |
|
21249 | 73 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
74 |
lemmas antisym_intro [intro!] = antisym |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
75 |
lemmas (in -) [rule del] = antisym_intro |
21249 | 76 |
|
21734 | 77 |
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
21733 | 78 |
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
79 |
apply(blast intro: order_trans) |
21733 | 80 |
apply simp |
81 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
82 |
lemmas (in -) [rule del] = le_supI1 |
21249 | 83 |
|
21734 | 84 |
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
21733 | 85 |
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
86 |
apply(blast intro: order_trans) |
21733 | 87 |
apply simp |
88 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
89 |
lemmas (in -) [rule del] = le_supI2 |
21733 | 90 |
|
21734 | 91 |
lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
21733 | 92 |
by(blast intro: sup_least) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
93 |
lemmas (in -) [rule del] = le_supI |
21249 | 94 |
|
21734 | 95 |
lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
96 |
by (blast intro: order_trans) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
97 |
lemmas (in -) [rule del] = le_supE |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
98 |
|
21249 | 99 |
|
21734 | 100 |
lemma ge_sup_conv[simp]: |
21733 | 101 |
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)" |
102 |
by blast |
|
103 |
||
21734 | 104 |
lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
22168 | 105 |
by(blast dest:eq_iff[THEN iffD1]) |
21734 | 106 |
|
21733 | 107 |
end |
108 |
||
109 |
||
110 |
subsubsection{* Equational laws *} |
|
21249 | 111 |
|
112 |
||
21733 | 113 |
context lower_semilattice |
114 |
begin |
|
115 |
||
116 |
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
|
117 |
by blast |
|
118 |
||
119 |
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
120 |
by blast |
|
121 |
||
122 |
lemma inf_idem[simp]: "x \<sqinter> x = x" |
|
123 |
by blast |
|
124 |
||
125 |
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
|
126 |
by blast |
|
127 |
||
128 |
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
129 |
by blast |
|
130 |
||
131 |
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
|
132 |
by blast |
|
133 |
||
134 |
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
|
135 |
by blast |
|
136 |
||
137 |
lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem |
|
138 |
||
139 |
end |
|
140 |
||
141 |
||
142 |
context upper_semilattice |
|
143 |
begin |
|
21249 | 144 |
|
21733 | 145 |
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
146 |
by blast |
|
147 |
||
148 |
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
149 |
by blast |
|
150 |
||
151 |
lemma sup_idem[simp]: "x \<squnion> x = x" |
|
152 |
by blast |
|
153 |
||
154 |
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
|
155 |
by blast |
|
156 |
||
157 |
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
|
158 |
by blast |
|
159 |
||
160 |
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
161 |
by blast |
|
21249 | 162 |
|
21733 | 163 |
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
164 |
by blast |
|
165 |
||
166 |
lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem |
|
167 |
||
168 |
end |
|
21249 | 169 |
|
21733 | 170 |
context lattice |
171 |
begin |
|
172 |
||
173 |
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" |
|
174 |
by(blast intro: antisym inf_le1 inf_greatest sup_ge1) |
|
175 |
||
176 |
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
177 |
by(blast intro: antisym sup_ge1 sup_least inf_le1) |
|
178 |
||
21734 | 179 |
lemmas ACI = inf_ACI sup_ACI |
180 |
||
181 |
text{* Towards distributivity *} |
|
21249 | 182 |
|
21734 | 183 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
184 |
by blast |
|
185 |
||
186 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" |
|
187 |
by blast |
|
188 |
||
189 |
||
190 |
text{* If you have one of them, you have them all. *} |
|
21249 | 191 |
|
21733 | 192 |
lemma distrib_imp1: |
21249 | 193 |
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
194 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
195 |
proof- |
|
196 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) |
|
197 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) |
|
198 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
|
199 |
by(simp add:inf_sup_absorb inf_commute) |
|
200 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
|
201 |
finally show ?thesis . |
|
202 |
qed |
|
203 |
||
21733 | 204 |
lemma distrib_imp2: |
21249 | 205 |
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
206 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
207 |
proof- |
|
208 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) |
|
209 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) |
|
210 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
|
211 |
by(simp add:sup_inf_absorb sup_commute) |
|
212 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
|
213 |
finally show ?thesis . |
|
214 |
qed |
|
215 |
||
21734 | 216 |
(* seems unused *) |
217 |
lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z" |
|
218 |
by blast |
|
219 |
||
21733 | 220 |
end |
21249 | 221 |
|
222 |
||
223 |
subsection{* Distributive lattices *} |
|
224 |
||
225 |
locale distrib_lattice = lattice + |
|
226 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
227 |
||
21733 | 228 |
context distrib_lattice |
229 |
begin |
|
230 |
||
231 |
lemma sup_inf_distrib2: |
|
21249 | 232 |
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
233 |
by(simp add:ACI sup_inf_distrib1) |
|
234 |
||
21733 | 235 |
lemma inf_sup_distrib1: |
21249 | 236 |
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
237 |
by(rule distrib_imp2[OF sup_inf_distrib1]) |
|
238 |
||
21733 | 239 |
lemma inf_sup_distrib2: |
21249 | 240 |
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
241 |
by(simp add:ACI inf_sup_distrib1) |
|
242 |
||
21733 | 243 |
lemmas distrib = |
21249 | 244 |
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
245 |
||
21733 | 246 |
end |
247 |
||
21249 | 248 |
|
21381 | 249 |
subsection {* min/max on linear orders as special case of inf/sup *} |
21249 | 250 |
|
251 |
interpretation min_max: |
|
21381 | 252 |
distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] |
21249 | 253 |
apply unfold_locales |
21381 | 254 |
apply (simp add: min_def linorder_not_le order_less_imp_le) |
255 |
apply (simp add: min_def linorder_not_le order_less_imp_le) |
|
256 |
apply (simp add: min_def linorder_not_le order_less_imp_le) |
|
257 |
apply (simp add: max_def linorder_not_le order_less_imp_le) |
|
258 |
apply (simp add: max_def linorder_not_le order_less_imp_le) |
|
259 |
unfolding min_def max_def by auto |
|
21249 | 260 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
261 |
text {* |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
262 |
Now we have inherited antisymmetry as an intro-rule on all |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
263 |
linear orders. This is a problem because it applies to bool, which is |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
264 |
undesirable. |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
265 |
*} |
21733 | 266 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
267 |
lemmas [rule del] = min_max.antisym_intro min_max.le_infI min_max.le_supI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
268 |
min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
269 |
min_max.le_infI1 min_max.le_infI2 |
21733 | 270 |
|
21249 | 271 |
lemmas le_maxI1 = min_max.sup_ge1 |
272 |
lemmas le_maxI2 = min_max.sup_ge2 |
|
21381 | 273 |
|
21249 | 274 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
275 |
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] |
21249 | 276 |
|
277 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
278 |
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] |
21249 | 279 |
|
21733 | 280 |
text {* ML legacy bindings *} |
281 |
||
282 |
ML {* |
|
22139 | 283 |
val Least_def = @{thm Least_def} |
284 |
val Least_equality = @{thm Least_equality} |
|
285 |
val min_def = @{thm min_def} |
|
286 |
val min_of_mono = @{thm min_of_mono} |
|
287 |
val max_def = @{thm max_def} |
|
288 |
val max_of_mono = @{thm max_of_mono} |
|
289 |
val min_leastL = @{thm min_leastL} |
|
290 |
val max_leastL = @{thm max_leastL} |
|
291 |
val min_leastR = @{thm min_leastR} |
|
292 |
val max_leastR = @{thm max_leastR} |
|
293 |
val le_max_iff_disj = @{thm le_max_iff_disj} |
|
294 |
val le_maxI1 = @{thm le_maxI1} |
|
295 |
val le_maxI2 = @{thm le_maxI2} |
|
296 |
val less_max_iff_disj = @{thm less_max_iff_disj} |
|
297 |
val max_less_iff_conj = @{thm max_less_iff_conj} |
|
298 |
val min_less_iff_conj = @{thm min_less_iff_conj} |
|
299 |
val min_le_iff_disj = @{thm min_le_iff_disj} |
|
300 |
val min_less_iff_disj = @{thm min_less_iff_disj} |
|
301 |
val split_min = @{thm split_min} |
|
302 |
val split_max = @{thm split_max} |
|
21733 | 303 |
*} |
304 |
||
21249 | 305 |
end |