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 |
|
|
19 |
locale lower_semilattice = partial_order +
|
|
20 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
|
21312
|
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 |
|
|
24 |
locale upper_semilattice = partial_order +
|
|
25 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
|
21312
|
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 |
|
|
29 |
locale lattice = lower_semilattice + upper_semilattice
|
|
30 |
|
21733
|
31 |
subsubsection{* Intro and elim rules*}
|
|
32 |
|
|
33 |
context lower_semilattice
|
|
34 |
begin
|
21249
|
35 |
|
21733
|
36 |
lemmas antisym_intro[intro!] = antisym
|
21249
|
37 |
|
21733
|
38 |
lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
|
|
39 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
|
|
40 |
apply(blast intro:trans)
|
|
41 |
apply simp
|
|
42 |
done
|
21249
|
43 |
|
21733
|
44 |
lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
|
|
45 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
|
|
46 |
apply(blast intro:trans)
|
|
47 |
apply simp
|
|
48 |
done
|
|
49 |
|
|
50 |
lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
|
|
51 |
by(blast intro: inf_greatest)
|
21249
|
52 |
|
21733
|
53 |
lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
|
|
54 |
by(blast intro: trans)
|
21249
|
55 |
|
21733
|
56 |
lemma less_eq_inf_conv [simp]:
|
|
57 |
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
|
|
58 |
by blast
|
|
59 |
|
|
60 |
lemmas below_inf_conv = less_eq_inf_conv
|
|
61 |
-- {* a duplicate for backward compatibility *}
|
21249
|
62 |
|
21733
|
63 |
end
|
|
64 |
|
|
65 |
|
|
66 |
context upper_semilattice
|
|
67 |
begin
|
21249
|
68 |
|
21733
|
69 |
lemmas antisym_intro[intro!] = antisym
|
21249
|
70 |
|
21733
|
71 |
lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
|
|
72 |
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
|
|
73 |
apply(blast intro:trans)
|
|
74 |
apply simp
|
|
75 |
done
|
21249
|
76 |
|
21733
|
77 |
lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
|
|
78 |
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
|
|
79 |
apply(blast intro:trans)
|
|
80 |
apply simp
|
|
81 |
done
|
|
82 |
|
|
83 |
lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
|
|
84 |
by(blast intro: sup_least)
|
21249
|
85 |
|
21733
|
86 |
lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
|
|
87 |
by(blast intro: trans)
|
21249
|
88 |
|
21733
|
89 |
lemma above_sup_conv[simp]:
|
|
90 |
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
|
|
91 |
by blast
|
|
92 |
|
|
93 |
end
|
|
94 |
|
|
95 |
|
|
96 |
subsubsection{* Equational laws *}
|
21249
|
97 |
|
|
98 |
|
21733
|
99 |
context lower_semilattice
|
|
100 |
begin
|
|
101 |
|
|
102 |
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
|
|
103 |
by blast
|
|
104 |
|
|
105 |
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
|
|
106 |
by blast
|
|
107 |
|
|
108 |
lemma inf_idem[simp]: "x \<sqinter> x = x"
|
|
109 |
by blast
|
|
110 |
|
|
111 |
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
|
|
112 |
by blast
|
|
113 |
|
|
114 |
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
|
|
115 |
by blast
|
|
116 |
|
|
117 |
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
|
|
118 |
by blast
|
|
119 |
|
|
120 |
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
|
|
121 |
by blast
|
|
122 |
|
|
123 |
lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
|
|
124 |
|
|
125 |
end
|
|
126 |
|
|
127 |
|
|
128 |
context upper_semilattice
|
|
129 |
begin
|
21249
|
130 |
|
21733
|
131 |
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
|
|
132 |
by blast
|
|
133 |
|
|
134 |
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
|
|
135 |
by blast
|
|
136 |
|
|
137 |
lemma sup_idem[simp]: "x \<squnion> x = x"
|
|
138 |
by blast
|
|
139 |
|
|
140 |
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
|
|
141 |
by blast
|
|
142 |
|
|
143 |
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
|
|
144 |
by blast
|
|
145 |
|
|
146 |
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
|
|
147 |
by blast
|
21249
|
148 |
|
21733
|
149 |
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
|
|
150 |
by blast
|
|
151 |
|
|
152 |
lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
|
|
153 |
|
|
154 |
end
|
21249
|
155 |
|
21733
|
156 |
context lattice
|
|
157 |
begin
|
|
158 |
|
|
159 |
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
|
|
160 |
by(blast intro: antisym inf_le1 inf_greatest sup_ge1)
|
|
161 |
|
|
162 |
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
|
|
163 |
by(blast intro: antisym sup_ge1 sup_least inf_le1)
|
|
164 |
|
|
165 |
lemmas (in lattice) ACI = inf_ACI sup_ACI
|
21249
|
166 |
|
|
167 |
text{* Towards distributivity: if you have one of them, you have them all. *}
|
|
168 |
|
21733
|
169 |
lemma distrib_imp1:
|
21249
|
170 |
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
|
|
171 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
|
|
172 |
proof-
|
|
173 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
|
|
174 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
|
|
175 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
|
|
176 |
by(simp add:inf_sup_absorb inf_commute)
|
|
177 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
|
|
178 |
finally show ?thesis .
|
|
179 |
qed
|
|
180 |
|
21733
|
181 |
lemma distrib_imp2:
|
21249
|
182 |
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
|
|
183 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
|
|
184 |
proof-
|
|
185 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
|
|
186 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
|
|
187 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
|
|
188 |
by(simp add:sup_inf_absorb sup_commute)
|
|
189 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
|
|
190 |
finally show ?thesis .
|
|
191 |
qed
|
|
192 |
|
21733
|
193 |
end
|
21249
|
194 |
|
|
195 |
|
|
196 |
subsection{* Distributive lattices *}
|
|
197 |
|
|
198 |
locale distrib_lattice = lattice +
|
|
199 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
|
|
200 |
|
21733
|
201 |
context distrib_lattice
|
|
202 |
begin
|
|
203 |
|
|
204 |
lemma sup_inf_distrib2:
|
21249
|
205 |
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
|
|
206 |
by(simp add:ACI sup_inf_distrib1)
|
|
207 |
|
21733
|
208 |
lemma inf_sup_distrib1:
|
21249
|
209 |
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
|
|
210 |
by(rule distrib_imp2[OF sup_inf_distrib1])
|
|
211 |
|
21733
|
212 |
lemma inf_sup_distrib2:
|
21249
|
213 |
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
|
|
214 |
by(simp add:ACI inf_sup_distrib1)
|
|
215 |
|
21733
|
216 |
lemmas distrib =
|
21249
|
217 |
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
|
|
218 |
|
21733
|
219 |
end
|
|
220 |
|
21249
|
221 |
|
21381
|
222 |
subsection {* min/max on linear orders as special case of inf/sup *}
|
21249
|
223 |
|
|
224 |
interpretation min_max:
|
21381
|
225 |
distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
|
21249
|
226 |
apply unfold_locales
|
21381
|
227 |
apply (simp add: min_def linorder_not_le order_less_imp_le)
|
|
228 |
apply (simp add: min_def linorder_not_le order_less_imp_le)
|
|
229 |
apply (simp add: min_def linorder_not_le order_less_imp_le)
|
|
230 |
apply (simp add: max_def linorder_not_le order_less_imp_le)
|
|
231 |
apply (simp add: max_def linorder_not_le order_less_imp_le)
|
|
232 |
unfolding min_def max_def by auto
|
21249
|
233 |
|
21733
|
234 |
text{* Now we have inherited antisymmetry as an intro-rule on all
|
|
235 |
linear orders. This is a problem because it applies to bool, which is
|
|
236 |
undesirable. *}
|
|
237 |
|
|
238 |
declare
|
|
239 |
min_max.antisym_intro[rule del]
|
|
240 |
min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
|
|
241 |
min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
|
|
242 |
min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
|
|
243 |
min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
|
|
244 |
|
21249
|
245 |
lemmas le_maxI1 = min_max.sup_ge1
|
|
246 |
lemmas le_maxI2 = min_max.sup_ge2
|
21381
|
247 |
|
21249
|
248 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
|
|
249 |
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
|
|
250 |
|
|
251 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
|
|
252 |
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
|
|
253 |
|
21733
|
254 |
text {* ML legacy bindings *}
|
|
255 |
|
|
256 |
ML {*
|
|
257 |
val Least_def = thm "Least_def";
|
|
258 |
val Least_equality = thm "Least_equality";
|
|
259 |
val min_def = thm "min_def";
|
|
260 |
val min_of_mono = thm "min_of_mono";
|
|
261 |
val max_def = thm "max_def";
|
|
262 |
val max_of_mono = thm "max_of_mono";
|
|
263 |
val min_leastL = thm "min_leastL";
|
|
264 |
val max_leastL = thm "max_leastL";
|
|
265 |
val min_leastR = thm "min_leastR";
|
|
266 |
val max_leastR = thm "max_leastR";
|
|
267 |
val le_max_iff_disj = thm "le_max_iff_disj";
|
|
268 |
val le_maxI1 = thm "le_maxI1";
|
|
269 |
val le_maxI2 = thm "le_maxI2";
|
|
270 |
val less_max_iff_disj = thm "less_max_iff_disj";
|
|
271 |
val max_less_iff_conj = thm "max_less_iff_conj";
|
|
272 |
val min_less_iff_conj = thm "min_less_iff_conj";
|
|
273 |
val min_le_iff_disj = thm "min_le_iff_disj";
|
|
274 |
val min_less_iff_disj = thm "min_less_iff_disj";
|
|
275 |
val split_min = thm "split_min";
|
|
276 |
val split_max = thm "split_max";
|
|
277 |
*}
|
|
278 |
|
21249
|
279 |
end
|