src/HOL/Lattice/CompleteLattice.thy
 author webertj Mon Mar 07 19:30:53 2005 +0100 (2005-03-07) changeset 15584 3478bb4f93ff parent 12399 2ba27248af7f child 16417 9bc16273c2d4 permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
1 (*  Title:      HOL/Lattice/CompleteLattice.thy
2     ID:         $Id$
3     Author:     Markus Wenzel, TU Muenchen
4 *)
6 header {* Complete lattices *}
8 theory CompleteLattice = Lattice:
10 subsection {* Complete lattice operations *}
12 text {*
13   A \emph{complete lattice} is a partial order with general
14   (infinitary) infimum of any set of elements.  General supremum
15   exists as well, as a consequence of the connection of infinitary
16   bounds (see \S\ref{sec:connect-bounds}).
17 *}
19 axclass complete_lattice \<subseteq> partial_order
20   ex_Inf: "\<exists>inf. is_Inf A inf"
22 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
23 proof -
24   from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
25   hence "is_Sup A sup" by (rule Inf_Sup)
26   thus ?thesis ..
27 qed
29 text {*
30   The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
31   such infimum and supremum elements.
32 *}
34 consts
35   Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
36   Join :: "'a::complete_lattice set \<Rightarrow> 'a"
37 syntax (xsymbols)
38   Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_"  90)
39   Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_"  90)
40 defs
41   Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf"
42   Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup"
44 text {*
45   Due to unique existence of bounds, the complete lattice operations
46   may be exhibited as follows.
47 *}
49 lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
50 proof (unfold Meet_def)
51   assume "is_Inf A inf"
52   thus "(THE inf. is_Inf A inf) = inf"
53     by (rule the_equality) (rule is_Inf_uniq)
54 qed
56 lemma MeetI [intro?]:
57   "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>
58     (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
59     \<Sqinter>A = inf"
60   by (rule Meet_equality, rule is_InfI) blast+
62 lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
63 proof (unfold Join_def)
64   assume "is_Sup A sup"
65   thus "(THE sup. is_Sup A sup) = sup"
66     by (rule the_equality) (rule is_Sup_uniq)
67 qed
69 lemma JoinI [intro?]:
70   "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>
71     (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
72     \<Squnion>A = sup"
73   by (rule Join_equality, rule is_SupI) blast+
76 text {*
77   \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
78   bounds on a complete lattice structure.
79 *}
81 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
82 proof (unfold Meet_def)
83   from ex_Inf obtain inf where "is_Inf A inf" ..
84   thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
85 qed
87 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
88   by (rule is_Inf_greatest, rule is_Inf_Meet) blast
90 lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"
91   by (rule is_Inf_lower) (rule is_Inf_Meet)
94 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
95 proof (unfold Join_def)
96   from ex_Sup obtain sup where "is_Sup A sup" ..
97   thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
98 qed
100 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
101   by (rule is_Sup_least, rule is_Sup_Join) blast
102 lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"
103   by (rule is_Sup_upper) (rule is_Sup_Join)
106 subsection {* The Knaster-Tarski Theorem *}
108 text {*
109   The Knaster-Tarski Theorem (in its simplest formulation) states that
110   any monotone function on a complete lattice has a least fixed-point
111   (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
112   is a consequence of the basic boundary properties of the complete
113   lattice operations.
114 *}
116 theorem Knaster_Tarski:
117   "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
118 proof
119   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
120   let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
121   have ge: "f ?a \<sqsubseteq> ?a"
122   proof
123     fix x assume x: "x \<in> ?H"
124     hence "?a \<sqsubseteq> x" ..
125     hence "f ?a \<sqsubseteq> f x" by (rule mono)
126     also from x have "... \<sqsubseteq> x" ..
127     finally show "f ?a \<sqsubseteq> x" .
128   qed
129   also have "?a \<sqsubseteq> f ?a"
130   proof
131     from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
132     thus "f ?a \<in> ?H" ..
133   qed
134   finally show "f ?a = ?a" .
135 qed
138 subsection {* Bottom and top elements *}
140 text {*
141   With general bounds available, complete lattices also have least and
142   greatest elements.
143 *}
145 constdefs
146   bottom :: "'a::complete_lattice"    ("\<bottom>")
147   "\<bottom> \<equiv> \<Sqinter>UNIV"
148   top :: "'a::complete_lattice"    ("\<top>")
149   "\<top> \<equiv> \<Squnion>UNIV"
151 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
152 proof (unfold bottom_def)
153   have "x \<in> UNIV" ..
154   thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
155 qed
157 lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
158 proof (unfold bottom_def)
159   assume "\<And>a. x \<sqsubseteq> a"
160   show "\<Sqinter>UNIV = x"
161   proof
162     fix a show "x \<sqsubseteq> a" .
163   next
164     fix b :: "'a::complete_lattice"
165     assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
166     have "x \<in> UNIV" ..
167     with b show "b \<sqsubseteq> x" ..
168   qed
169 qed
171 lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
172 proof (unfold top_def)
173   have "x \<in> UNIV" ..
174   thus "x \<sqsubseteq> \<Squnion>UNIV" ..
175 qed
177 lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
178 proof (unfold top_def)
179   assume "\<And>a. a \<sqsubseteq> x"
180   show "\<Squnion>UNIV = x"
181   proof
182     fix a show "a \<sqsubseteq> x" .
183   next
184     fix b :: "'a::complete_lattice"
185     assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
186     have "x \<in> UNIV" ..
187     with b show "x \<sqsubseteq> b" ..
188   qed
189 qed
192 subsection {* Duality *}
194 text {*
195   The class of complete lattices is closed under formation of dual
196   structures.
197 *}
199 instance dual :: (complete_lattice) complete_lattice
200 proof
201   fix A' :: "'a::complete_lattice dual set"
202   show "\<exists>inf'. is_Inf A' inf'"
203   proof -
204     have "\<exists>sup. is_Sup (undual  A') sup" by (rule ex_Sup)
205     hence "\<exists>sup. is_Inf (dual  undual  A') (dual sup)" by (simp only: dual_Inf)
206     thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
207   qed
208 qed
210 text {*
211   Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
212   other.
213 *}
215 theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual  A)"
216 proof -
217   from is_Inf_Meet have "is_Sup (dual  A) (dual (\<Sqinter>A))" ..
218   hence "\<Squnion>(dual  A) = dual (\<Sqinter>A)" ..
219   thus ?thesis ..
220 qed
222 theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual  A)"
223 proof -
224   from is_Sup_Join have "is_Inf (dual  A) (dual (\<Squnion>A))" ..
225   hence "\<Sqinter>(dual  A) = dual (\<Squnion>A)" ..
226   thus ?thesis ..
227 qed
229 text {*
230   Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
231 *}
233 theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
234 proof -
235   have "\<top> = dual \<bottom>"
236   proof
237     fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
238     hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
239     thus "a' \<sqsubseteq> dual \<bottom>" by simp
240   qed
241   thus ?thesis ..
242 qed
244 theorem dual_top [intro?]: "dual \<top> = \<bottom>"
245 proof -
246   have "\<bottom> = dual \<top>"
247   proof
248     fix a' have "undual a' \<sqsubseteq> \<top>" ..
249     hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
250     thus "dual \<top> \<sqsubseteq> a'" by simp
251   qed
252   thus ?thesis ..
253 qed
256 subsection {* Complete lattices are lattices *}
258 text {*
259   Complete lattices (with general bounds available) are indeed plain
260   lattices as well.  This holds due to the connection of general
261   versus binary bounds that has been formally established in
262   \S\ref{sec:gen-bin-bounds}.
263 *}
265 lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
266 proof -
267   have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
268   thus ?thesis by (simp only: is_Inf_binary)
269 qed
271 lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
272 proof -
273   have "is_Sup {x, y} (\<Squnion>{x, y})" ..
274   thus ?thesis by (simp only: is_Sup_binary)
275 qed
277 instance complete_lattice \<subseteq> lattice
278 proof
279   fix x y :: "'a::complete_lattice"
280   from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
281   from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
282 qed
284 theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
285   by (rule meet_equality) (rule is_inf_binary)
287 theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"
288   by (rule join_equality) (rule is_sup_binary)
291 subsection {* Complete lattices and set-theory operations *}
293 text {*
294   The complete lattice operations are (anti) monotone wrt.\ set
295   inclusion.
296 *}
298 theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
299 proof (rule Meet_greatest)
300   fix a assume "a \<in> A"
301   also assume "A \<subseteq> B"
302   finally have "a \<in> B" .
303   thus "\<Sqinter>B \<sqsubseteq> a" ..
304 qed
306 theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
307 proof -
308   assume "A \<subseteq> B"
309   hence "dual  A \<subseteq> dual  B" by blast
310   hence "\<Sqinter>(dual  B) \<sqsubseteq> \<Sqinter>(dual  A)" by (rule Meet_subset_antimono)
311   hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
312   thus ?thesis by (simp only: dual_leq)
313 qed
315 text {*
316   Bounds over unions of sets may be obtained separately.
317 *}
319 theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
320 proof
321   fix a assume "a \<in> A \<union> B"
322   thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
323   proof
324     assume a: "a \<in> A"
325     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
326     also from a have "\<dots> \<sqsubseteq> a" ..
327     finally show ?thesis .
328   next
329     assume a: "a \<in> B"
330     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
331     also from a have "\<dots> \<sqsubseteq> a" ..
332     finally show ?thesis .
333   qed
334 next
335   fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
336   show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
337   proof
338     show "b \<sqsubseteq> \<Sqinter>A"
339     proof
340       fix a assume "a \<in> A"
341       hence "a \<in>  A \<union> B" ..
342       with b show "b \<sqsubseteq> a" ..
343     qed
344     show "b \<sqsubseteq> \<Sqinter>B"
345     proof
346       fix a assume "a \<in> B"
347       hence "a \<in>  A \<union> B" ..
348       with b show "b \<sqsubseteq> a" ..
349     qed
350   qed
351 qed
353 theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
354 proof -
355   have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual  A \<union> dual  B)"
356     by (simp only: dual_Join image_Un)
357   also have "\<dots> = \<Sqinter>(dual  A) \<sqinter> \<Sqinter>(dual ` B)"
358     by (rule Meet_Un)
359   also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
360     by (simp only: dual_join dual_Join)
361   finally show ?thesis ..
362 qed
364 text {*
365   Bounds over singleton sets are trivial.
366 *}
368 theorem Meet_singleton: "\<Sqinter>{x} = x"
369 proof
370   fix a assume "a \<in> {x}"
371   hence "a = x" by simp
372   thus "x \<sqsubseteq> a" by (simp only: leq_refl)
373 next
374   fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
375   thus "b \<sqsubseteq> x" by simp
376 qed
378 theorem Join_singleton: "\<Squnion>{x} = x"
379 proof -
380   have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
381   also have "\<dots> = dual x" by (rule Meet_singleton)
382   finally show ?thesis ..
383 qed
385 text {*
386   Bounds over the empty and universal set correspond to each other.
387 *}
389 theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
390 proof
391   fix a :: "'a::complete_lattice"
392   assume "a \<in> {}"
393   hence False by simp
394   thus "\<Squnion>UNIV \<sqsubseteq> a" ..
395 next
396   fix b :: "'a::complete_lattice"
397   have "b \<in> UNIV" ..
398   thus "b \<sqsubseteq> \<Squnion>UNIV" ..
399 qed
401 theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
402 proof -
403   have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
404   also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
405   also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
406   finally show ?thesis ..
407 qed
409 end