src/HOL/Lattice/Lattice.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 61986 2461779da2b8 child 69597 ff784d5a5bfb permissions -rw-r--r--
tuned;
1 (*  Title:      HOL/Lattice/Lattice.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 section \<open>Lattices\<close>
7 theory Lattice imports Bounds begin
9 subsection \<open>Lattice operations\<close>
11 text \<open>
12   A \emph{lattice} is a partial order with infimum and supremum of any
13   two elements (thus any \emph{finite} number of elements have bounds
14   as well).
15 \<close>
17 class lattice =
18   assumes ex_inf: "\<exists>inf. is_inf x y inf"
19   assumes ex_sup: "\<exists>sup. is_sup x y sup"
21 text \<open>
22   The \<open>\<sqinter>\<close> (meet) and \<open>\<squnion>\<close> (join) operations select such
23   infimum and supremum elements.
24 \<close>
26 definition
27   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70) where
28   "x \<sqinter> y = (THE inf. is_inf x y inf)"
29 definition
30   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65) where
31   "x \<squnion> y = (THE sup. is_sup x y sup)"
33 text \<open>
34   Due to unique existence of bounds, the lattice operations may be
35   exhibited as follows.
36 \<close>
38 lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
39 proof (unfold meet_def)
40   assume "is_inf x y inf"
41   then show "(THE inf. is_inf x y inf) = inf"
42     by (rule the_equality) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
43 qed
45 lemma meetI [intro?]:
46     "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"
47   by (rule meet_equality, rule is_infI) blast+
49 lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
50 proof (unfold join_def)
51   assume "is_sup x y sup"
52   then show "(THE sup. is_sup x y sup) = sup"
53     by (rule the_equality) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
54 qed
56 lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
57     (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"
58   by (rule join_equality, rule is_supI) blast+
61 text \<open>
62   \medskip The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations indeed determine
63   bounds on a lattice structure.
64 \<close>
66 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
67 proof (unfold meet_def)
68   from ex_inf obtain inf where "is_inf x y inf" ..
69   then show "is_inf x y (THE inf. is_inf x y inf)"
70     by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
71 qed
73 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
74   by (rule is_inf_greatest) (rule is_inf_meet)
76 lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"
77   by (rule is_inf_lower) (rule is_inf_meet)
79 lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"
80   by (rule is_inf_lower) (rule is_inf_meet)
83 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
84 proof (unfold join_def)
85   from ex_sup obtain sup where "is_sup x y sup" ..
86   then show "is_sup x y (THE sup. is_sup x y sup)"
87     by (rule theI) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
88 qed
90 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
91   by (rule is_sup_least) (rule is_sup_join)
93 lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"
94   by (rule is_sup_upper) (rule is_sup_join)
96 lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"
97   by (rule is_sup_upper) (rule is_sup_join)
100 subsection \<open>Duality\<close>
102 text \<open>
103   The class of lattices is closed under formation of dual structures.
104   This means that for any theorem of lattice theory, the dualized
105   statement holds as well; this important fact simplifies many proofs
106   of lattice theory.
107 \<close>
109 instance dual :: (lattice) lattice
110 proof
111   fix x' y' :: "'a::lattice dual"
112   show "\<exists>inf'. is_inf x' y' inf'"
113   proof -
114     have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
115     then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
116       by (simp only: dual_inf)
117     then show ?thesis by (simp add: dual_ex [symmetric])
118   qed
119   show "\<exists>sup'. is_sup x' y' sup'"
120   proof -
121     have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
122     then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
123       by (simp only: dual_sup)
124     then show ?thesis by (simp add: dual_ex [symmetric])
125   qed
126 qed
128 text \<open>
129   Apparently, the \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are dual to each
130   other.
131 \<close>
133 theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
134 proof -
135   from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
136   then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
137   then show ?thesis ..
138 qed
140 theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
141 proof -
142   from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
143   then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
144   then show ?thesis ..
145 qed
148 subsection \<open>Algebraic properties \label{sec:lattice-algebra}\<close>
150 text \<open>
151   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations have the following
152   characteristic algebraic properties: associative (A), commutative
153   (C), and absorptive (AB).
154 \<close>
156 theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
157 proof
158   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
159   proof
160     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
161     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
162     proof -
163       have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
164       also have "\<dots> \<sqsubseteq> y" ..
165       finally show ?thesis .
166     qed
167   qed
168   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
169   proof -
170     have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
171     also have "\<dots> \<sqsubseteq> z" ..
172     finally show ?thesis .
173   qed
174   fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
175   show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
176   proof
177     show "w \<sqsubseteq> x"
178     proof -
179       have "w \<sqsubseteq> x \<sqinter> y" by fact
180       also have "\<dots> \<sqsubseteq> x" ..
181       finally show ?thesis .
182     qed
183     show "w \<sqsubseteq> y \<sqinter> z"
184     proof
185       show "w \<sqsubseteq> y"
186       proof -
187         have "w \<sqsubseteq> x \<sqinter> y" by fact
188         also have "\<dots> \<sqsubseteq> y" ..
189         finally show ?thesis .
190       qed
191       show "w \<sqsubseteq> z" by fact
192     qed
193   qed
194 qed
196 theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
197 proof -
198   have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"
199     by (simp only: dual_join)
200   also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"
201     by (rule meet_assoc)
202   also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"
203     by (simp only: dual_join)
204   finally show ?thesis ..
205 qed
207 theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
208 proof
209   show "y \<sqinter> x \<sqsubseteq> x" ..
210   show "y \<sqinter> x \<sqsubseteq> y" ..
211   fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
212   then show "z \<sqsubseteq> y \<sqinter> x" ..
213 qed
215 theorem join_commute: "x \<squnion> y = y \<squnion> x"
216 proof -
217   have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..
218   also have "\<dots> = dual y \<sqinter> dual x"
219     by (rule meet_commute)
220   also have "\<dots> = dual (y \<squnion> x)"
221     by (simp only: dual_join)
222   finally show ?thesis ..
223 qed
225 theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
226 proof
227   show "x \<sqsubseteq> x" ..
228   show "x \<sqsubseteq> x \<squnion> y" ..
229   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
230   show "z \<sqsubseteq> x" by fact
231 qed
233 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
234 proof -
235   have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
236     by (rule meet_join_absorb)
237   then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
238     by (simp only: dual_meet dual_join)
239   then show ?thesis ..
240 qed
242 text \<open>
243   \medskip Some further algebraic properties hold as well.  The
244   property idempotent (I) is a basic algebraic consequence of (AB).
245 \<close>
247 theorem meet_idem: "x \<sqinter> x = x"
248 proof -
249   have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
250   also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
251   finally show ?thesis .
252 qed
254 theorem join_idem: "x \<squnion> x = x"
255 proof -
256   have "dual x \<sqinter> dual x = dual x"
257     by (rule meet_idem)
258   then have "dual (x \<squnion> x) = dual x"
259     by (simp only: dual_join)
260   then show ?thesis ..
261 qed
263 text \<open>
264   Meet and join are trivial for related elements.
265 \<close>
267 theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
268 proof
269   assume "x \<sqsubseteq> y"
270   show "x \<sqsubseteq> x" ..
271   show "x \<sqsubseteq> y" by fact
272   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
273   show "z \<sqsubseteq> x" by fact
274 qed
276 theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
277 proof -
278   assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
279   then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
280   also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
281   also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
282   finally show ?thesis ..
283 qed
286 subsection \<open>Order versus algebraic structure\<close>
288 text \<open>
289   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are connected with the
290   underlying \<open>\<sqsubseteq>\<close> relation in a canonical manner.
291 \<close>
293 theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
294 proof
295   assume "x \<sqsubseteq> y"
296   then have "is_inf x y x" ..
297   then show "x \<sqinter> y = x" ..
298 next
299   have "x \<sqinter> y \<sqsubseteq> y" ..
300   also assume "x \<sqinter> y = x"
301   finally show "x \<sqsubseteq> y" .
302 qed
304 theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
305 proof
306   assume "x \<sqsubseteq> y"
307   then have "is_sup x y y" ..
308   then show "x \<squnion> y = y" ..
309 next
310   have "x \<sqsubseteq> x \<squnion> y" ..
311   also assume "x \<squnion> y = y"
312   finally show "x \<sqsubseteq> y" .
313 qed
315 text \<open>
316   \medskip The most fundamental result of the meta-theory of lattices
317   is as follows (we do not prove it here).
319   Given a structure with binary operations \<open>\<sqinter>\<close> and \<open>\<squnion>\<close>
320   such that (A), (C), and (AB) hold (cf.\
321   \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
322   if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
323   (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and
324   supremum with respect to this ordering coincide with the original
325   \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations.
326 \<close>
329 subsection \<open>Example instances\<close>
331 subsubsection \<open>Linear orders\<close>
333 text \<open>
334   Linear orders with @{term minimum} and @{term maximum} operations
335   are a (degenerate) example of lattice structures.
336 \<close>
338 definition
339   minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
340   "minimum x y = (if x \<sqsubseteq> y then x else y)"
341 definition
342   maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
343   "maximum x y = (if x \<sqsubseteq> y then y else x)"
345 lemma is_inf_minimum: "is_inf x y (minimum x y)"
346 proof
347   let ?min = "minimum x y"
348   from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)
349   from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)
350   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
351   with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)
352 qed
354 lemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)
355 proof
356   let ?max = "maximum x y"
357   from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)
358   from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)
359   fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
360   with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
361 qed
363 instance linear_order \<subseteq> lattice
364 proof
365   fix x y :: "'a::linear_order"
366   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
367   from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
368 qed
370 text \<open>
371   The lattice operations on linear orders indeed coincide with @{term
372   minimum} and @{term maximum}.
373 \<close>
375 theorem meet_mimimum: "x \<sqinter> y = minimum x y"
376   by (rule meet_equality) (rule is_inf_minimum)
378 theorem meet_maximum: "x \<squnion> y = maximum x y"
379   by (rule join_equality) (rule is_sup_maximum)
383 subsubsection \<open>Binary products\<close>
385 text \<open>
386   The class of lattices is closed under direct binary products (cf.\
387   \S\ref{sec:prod-order}).
388 \<close>
390 lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
391 proof
392   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"
393   proof -
394     have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..
395     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..
396     ultimately show ?thesis by (simp add: leq_prod_def)
397   qed
398   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"
399   proof -
400     have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..
401     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..
402     ultimately show ?thesis by (simp add: leq_prod_def)
403   qed
404   fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"
405   show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
406   proof -
407     have "fst r \<sqsubseteq> fst p \<sqinter> fst q"
408     proof
409       from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)
410       from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)
411     qed
412     moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"
413     proof
414       from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)
415       from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)
416     qed
417     ultimately show ?thesis by (simp add: leq_prod_def)
418   qed
419 qed
421 lemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)
422 proof
423   show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
424   proof -
425     have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..
426     moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..
427     ultimately show ?thesis by (simp add: leq_prod_def)
428   qed
429   show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
430   proof -
431     have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..
432     moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..
433     ultimately show ?thesis by (simp add: leq_prod_def)
434   qed
435   fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"
436   show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"
437   proof -
438     have "fst p \<squnion> fst q \<sqsubseteq> fst r"
439     proof
440       from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)
441       from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)
442     qed
443     moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"
444     proof
445       from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)
446       from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)
447     qed
448     ultimately show ?thesis by (simp add: leq_prod_def)
449   qed
450 qed
452 instance prod :: (lattice, lattice) lattice
453 proof
454   fix p q :: "'a::lattice \<times> 'b::lattice"
455   from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
456   from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
457 qed
459 text \<open>
460   The lattice operations on a binary product structure indeed coincide
461   with the products of the original ones.
462 \<close>
464 theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
465   by (rule meet_equality) (rule is_inf_prod)
467 theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"
468   by (rule join_equality) (rule is_sup_prod)
471 subsubsection \<open>General products\<close>
473 text \<open>
474   The class of lattices is closed under general products (function
475   spaces) as well (cf.\ \S\ref{sec:fun-order}).
476 \<close>
478 lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
479 proof
480   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"
481   proof
482     fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..
483   qed
484   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"
485   proof
486     fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..
487   qed
488   fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"
489   show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"
490   proof
491     fix x
492     show "h x \<sqsubseteq> f x \<sqinter> g x"
493     proof
494       from hf show "h x \<sqsubseteq> f x" ..
495       from hg show "h x \<sqsubseteq> g x" ..
496     qed
497   qed
498 qed
500 lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)"   (* FIXME dualize!? *)
501 proof
502   show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
503   proof
504     fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..
505   qed
506   show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
507   proof
508     fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..
509   qed
510   fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"
511   show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"
512   proof
513     fix x
514     show "f x \<squnion> g x \<sqsubseteq> h x"
515     proof
516       from fh show "f x \<sqsubseteq> h x" ..
517       from gh show "g x \<sqsubseteq> h x" ..
518     qed
519   qed
520 qed
522 instance "fun" :: (type, lattice) lattice
523 proof
524   fix f g :: "'a \<Rightarrow> 'b::lattice"
525   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
526   show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
527 qed
529 text \<open>
530   The lattice operations on a general product structure (function
531   space) indeed emerge by point-wise lifting of the original ones.
532 \<close>
534 theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
535   by (rule meet_equality) (rule is_inf_fun)
537 theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
538   by (rule join_equality) (rule is_sup_fun)
541 subsection \<open>Monotonicity and semi-morphisms\<close>
543 text \<open>
544   The lattice operations are monotone in both argument positions.  In
545   fact, monotonicity of the second position is trivial due to
546   commutativity.
547 \<close>
549 theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
550 proof -
551   {
552     fix a b c :: "'a::lattice"
553     assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
554     proof
555       have "a \<sqinter> b \<sqsubseteq> a" ..
556       also have "\<dots> \<sqsubseteq> c" by fact
557       finally show "a \<sqinter> b \<sqsubseteq> c" .
558       show "a \<sqinter> b \<sqsubseteq> b" ..
559     qed
560   } note this [elim?]
561   assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
562   also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
563   also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
564   also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
565   finally show ?thesis .
566 qed
568 theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
569 proof -
570   assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
571   moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
572   ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
573     by (rule meet_mono)
574   then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
575     by (simp only: dual_join)
576   then show ?thesis ..
577 qed
579 text \<open>
580   \medskip A semi-morphisms is a function \<open>f\<close> that preserves the
581   lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
582   \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of
583   these properties is equivalent with monotonicity.
584 \<close>
586 theorem meet_semimorph:
587   "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
588 proof
589   assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
590   fix x y :: "'a::lattice"
591   assume "x \<sqsubseteq> y"
592   then have "x \<sqinter> y = x" ..
593   then have "x = x \<sqinter> y" ..
594   also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
595   also have "\<dots> \<sqsubseteq> f y" ..
596   finally show "f x \<sqsubseteq> f y" .
597 next
598   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
599   show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
600   proof -
601     fix x y
602     show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
603     proof
604       have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
605       have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
606     qed
607   qed
608 qed
610 lemma join_semimorph:
611   "(\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
612 proof
613   assume morph: "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
614   fix x y :: "'a::lattice"
615   assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..
616   have "f x \<sqsubseteq> f x \<squnion> f y" ..
617   also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)
618   also from \<open>x \<sqsubseteq> y\<close> have "x \<squnion> y = y" ..
619   finally show "f x \<sqsubseteq> f y" .
620 next
621   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
622   show "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
623   proof -
624     fix x y
625     show "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
626     proof
627       have "x \<sqsubseteq> x \<squnion> y" .. then show "f x \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
628       have "y \<sqsubseteq> x \<squnion> y" .. then show "f y \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
629     qed
630   qed
631 qed
633 end