author | boehmes |
Thu, 27 May 2010 17:09:06 +0200 | |
changeset 37155 | e3f18cfc9829 |
parent 35317 | d57da4abb47d |
child 56154 | f0a927235162 |
permissions | -rw-r--r-- |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Lattice/CompleteLattice.thy |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
3 |
*) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
4 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
5 |
header {* Complete lattices *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
6 |
|
16417 | 7 |
theory CompleteLattice imports Lattice begin |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
8 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
9 |
subsection {* Complete lattice operations *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
10 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
11 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
12 |
A \emph{complete lattice} is a partial order with general |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
13 |
(infinitary) infimum of any set of elements. General supremum |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
14 |
exists as well, as a consequence of the connection of infinitary |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
15 |
bounds (see \S\ref{sec:connect-bounds}). |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
16 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
17 |
|
35317 | 18 |
class complete_lattice = |
19 |
assumes ex_Inf: "\<exists>inf. is_Inf A inf" |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
20 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
21 |
theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
22 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
23 |
from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast |
23373 | 24 |
then have "is_Sup A sup" by (rule Inf_Sup) |
25 |
then show ?thesis .. |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
26 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
27 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
28 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
29 |
The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
30 |
such infimum and supremum elements. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
31 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
32 |
|
19736 | 33 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
34 |
Meet :: "'a::complete_lattice set \<Rightarrow> 'a" where |
19736 | 35 |
"Meet A = (THE inf. is_Inf A inf)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
36 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
37 |
Join :: "'a::complete_lattice set \<Rightarrow> 'a" where |
19736 | 38 |
"Join A = (THE sup. is_Sup A sup)" |
39 |
||
21210 | 40 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
41 |
Meet ("\<Sqinter>_" [90] 90) and |
19736 | 42 |
Join ("\<Squnion>_" [90] 90) |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
43 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
44 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
45 |
Due to unique existence of bounds, the complete lattice operations |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
46 |
may be exhibited as follows. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
47 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
48 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
49 |
lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
50 |
proof (unfold Meet_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
51 |
assume "is_Inf A inf" |
23373 | 52 |
then show "(THE inf. is_Inf A inf) = inf" |
53 |
by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`]) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
54 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
55 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
56 |
lemma MeetI [intro?]: |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
57 |
"(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow> |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
58 |
(\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow> |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
59 |
\<Sqinter>A = inf" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
60 |
by (rule Meet_equality, rule is_InfI) blast+ |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
61 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
62 |
lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
63 |
proof (unfold Join_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
64 |
assume "is_Sup A sup" |
23373 | 65 |
then show "(THE sup. is_Sup A sup) = sup" |
66 |
by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`]) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
67 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
68 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
69 |
lemma JoinI [intro?]: |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
70 |
"(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow> |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
71 |
(\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow> |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
72 |
\<Squnion>A = sup" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
73 |
by (rule Join_equality, rule is_SupI) blast+ |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
74 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
75 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
76 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
77 |
\medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
78 |
bounds on a complete lattice structure. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
79 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
80 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
81 |
lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
82 |
proof (unfold Meet_def) |
11441 | 83 |
from ex_Inf obtain inf where "is_Inf A inf" .. |
23373 | 84 |
then show "is_Inf A (THE inf. is_Inf A inf)" |
85 |
by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`]) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
86 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
87 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
88 |
lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
89 |
by (rule is_Inf_greatest, rule is_Inf_Meet) blast |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
90 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
91 |
lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
92 |
by (rule is_Inf_lower) (rule is_Inf_Meet) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
93 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
94 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
95 |
lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
96 |
proof (unfold Join_def) |
11441 | 97 |
from ex_Sup obtain sup where "is_Sup A sup" .. |
23373 | 98 |
then show "is_Sup A (THE sup. is_Sup A sup)" |
99 |
by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`]) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
100 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
101 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
102 |
lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
103 |
by (rule is_Sup_least, rule is_Sup_Join) blast |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
104 |
lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
105 |
by (rule is_Sup_upper) (rule is_Sup_Join) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
106 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
107 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
108 |
subsection {* The Knaster-Tarski Theorem *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
109 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
110 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
111 |
The Knaster-Tarski Theorem (in its simplest formulation) states that |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
112 |
any monotone function on a complete lattice has a least fixed-point |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
113 |
(see \cite[pages 93--94]{Davey-Priestley:1990} for example). This |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
114 |
is a consequence of the basic boundary properties of the complete |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
115 |
lattice operations. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
116 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
117 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
118 |
theorem Knaster_Tarski: |
25469 | 119 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
120 |
obtains a :: "'a::complete_lattice" where |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
121 |
"f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a \<sqsubseteq> a'" |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
122 |
proof |
25469 | 123 |
let ?H = "{u. f u \<sqsubseteq> u}" |
124 |
let ?a = "\<Sqinter>?H" |
|
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
125 |
show "f ?a = ?a" |
25469 | 126 |
proof - |
127 |
have ge: "f ?a \<sqsubseteq> ?a" |
|
128 |
proof |
|
129 |
fix x assume x: "x \<in> ?H" |
|
130 |
then have "?a \<sqsubseteq> x" .. |
|
131 |
then have "f ?a \<sqsubseteq> f x" by (rule mono) |
|
132 |
also from x have "... \<sqsubseteq> x" .. |
|
133 |
finally show "f ?a \<sqsubseteq> x" . |
|
134 |
qed |
|
135 |
also have "?a \<sqsubseteq> f ?a" |
|
136 |
proof |
|
137 |
from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono) |
|
138 |
then show "f ?a \<in> ?H" .. |
|
139 |
qed |
|
140 |
finally show ?thesis . |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
141 |
qed |
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
142 |
|
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
143 |
fix a' |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
144 |
assume "f a' = a'" |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
145 |
then have "f a' \<sqsubseteq> a'" by (simp only: leq_refl) |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
146 |
then have "a' \<in> ?H" .. |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
147 |
then show "?a \<sqsubseteq> a'" .. |
25469 | 148 |
qed |
149 |
||
150 |
theorem Knaster_Tarski_dual: |
|
151 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
|
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
152 |
obtains a :: "'a::complete_lattice" where |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
153 |
"f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a' \<sqsubseteq> a" |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
154 |
proof |
25469 | 155 |
let ?H = "{u. u \<sqsubseteq> f u}" |
156 |
let ?a = "\<Squnion>?H" |
|
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
157 |
show "f ?a = ?a" |
25469 | 158 |
proof - |
159 |
have le: "?a \<sqsubseteq> f ?a" |
|
160 |
proof |
|
161 |
fix x assume x: "x \<in> ?H" |
|
162 |
then have "x \<sqsubseteq> f x" .. |
|
163 |
also from x have "x \<sqsubseteq> ?a" .. |
|
164 |
then have "f x \<sqsubseteq> f ?a" by (rule mono) |
|
165 |
finally show "x \<sqsubseteq> f ?a" . |
|
166 |
qed |
|
167 |
have "f ?a \<sqsubseteq> ?a" |
|
168 |
proof |
|
169 |
from le have "f ?a \<sqsubseteq> f (f ?a)" by (rule mono) |
|
170 |
then show "f ?a \<in> ?H" .. |
|
171 |
qed |
|
172 |
from this and le show ?thesis by (rule leq_antisym) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
173 |
qed |
25474
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
174 |
|
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
175 |
fix a' |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
176 |
assume "f a' = a'" |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
177 |
then have "a' \<sqsubseteq> f a'" by (simp only: leq_refl) |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
178 |
then have "a' \<in> ?H" .. |
c41b433b0f65
Knaster_Tarski: turned into Isar statement, tuned proofs;
wenzelm
parents:
25469
diff
changeset
|
179 |
then show "a' \<sqsubseteq> ?a" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
180 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
181 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
182 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
183 |
subsection {* Bottom and top elements *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
184 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
185 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
186 |
With general bounds available, complete lattices also have least and |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
187 |
greatest elements. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
188 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
189 |
|
19736 | 190 |
definition |
25469 | 191 |
bottom :: "'a::complete_lattice" ("\<bottom>") where |
19736 | 192 |
"\<bottom> = \<Sqinter>UNIV" |
25469 | 193 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
194 |
definition |
25469 | 195 |
top :: "'a::complete_lattice" ("\<top>") where |
19736 | 196 |
"\<top> = \<Squnion>UNIV" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
197 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
198 |
lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
199 |
proof (unfold bottom_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
200 |
have "x \<in> UNIV" .. |
23373 | 201 |
then show "\<Sqinter>UNIV \<sqsubseteq> x" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
202 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
203 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
204 |
lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
205 |
proof (unfold bottom_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
206 |
assume "\<And>a. x \<sqsubseteq> a" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
207 |
show "\<Sqinter>UNIV = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
208 |
proof |
23373 | 209 |
fix a show "x \<sqsubseteq> a" by fact |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
210 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
211 |
fix b :: "'a::complete_lattice" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
212 |
assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
213 |
have "x \<in> UNIV" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
214 |
with b show "b \<sqsubseteq> x" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
215 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
216 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
217 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
218 |
lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
219 |
proof (unfold top_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
220 |
have "x \<in> UNIV" .. |
23373 | 221 |
then show "x \<sqsubseteq> \<Squnion>UNIV" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
222 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
223 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
224 |
lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
225 |
proof (unfold top_def) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
226 |
assume "\<And>a. a \<sqsubseteq> x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
227 |
show "\<Squnion>UNIV = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
228 |
proof |
23373 | 229 |
fix a show "a \<sqsubseteq> x" by fact |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
230 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
231 |
fix b :: "'a::complete_lattice" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
232 |
assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
233 |
have "x \<in> UNIV" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
234 |
with b show "x \<sqsubseteq> b" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
235 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
236 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
237 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
238 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
239 |
subsection {* Duality *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
240 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
241 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
242 |
The class of complete lattices is closed under formation of dual |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
243 |
structures. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
244 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
245 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
246 |
instance dual :: (complete_lattice) complete_lattice |
10309 | 247 |
proof |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
248 |
fix A' :: "'a::complete_lattice dual set" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
249 |
show "\<exists>inf'. is_Inf A' inf'" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
250 |
proof - |
10834 | 251 |
have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup) |
23373 | 252 |
then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf) |
253 |
then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric]) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
254 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
255 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
256 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
257 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
258 |
Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
259 |
other. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
260 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
261 |
|
10834 | 262 |
theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
263 |
proof - |
10834 | 264 |
from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" .. |
23373 | 265 |
then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" .. |
266 |
then show ?thesis .. |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
267 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
268 |
|
10834 | 269 |
theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
270 |
proof - |
10834 | 271 |
from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" .. |
23373 | 272 |
then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" .. |
273 |
then show ?thesis .. |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
274 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
275 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
276 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
277 |
Likewise are @{text \<bottom>} and @{text \<top>} duals of each other. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
278 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
279 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
280 |
theorem dual_bottom [intro?]: "dual \<bottom> = \<top>" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
281 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
282 |
have "\<top> = dual \<bottom>" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
283 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
284 |
fix a' have "\<bottom> \<sqsubseteq> undual a'" .. |
23373 | 285 |
then have "dual (undual a') \<sqsubseteq> dual \<bottom>" .. |
286 |
then show "a' \<sqsubseteq> dual \<bottom>" by simp |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
287 |
qed |
23373 | 288 |
then show ?thesis .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
289 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
290 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
291 |
theorem dual_top [intro?]: "dual \<top> = \<bottom>" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
292 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
293 |
have "\<bottom> = dual \<top>" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
294 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
295 |
fix a' have "undual a' \<sqsubseteq> \<top>" .. |
23373 | 296 |
then have "dual \<top> \<sqsubseteq> dual (undual a')" .. |
297 |
then show "dual \<top> \<sqsubseteq> a'" by simp |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
298 |
qed |
23373 | 299 |
then show ?thesis .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
300 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
301 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
302 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
303 |
subsection {* Complete lattices are lattices *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
304 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
305 |
text {* |
10176 | 306 |
Complete lattices (with general bounds available) are indeed plain |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
307 |
lattices as well. This holds due to the connection of general |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
308 |
versus binary bounds that has been formally established in |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
309 |
\S\ref{sec:gen-bin-bounds}. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
310 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
311 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
312 |
lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
313 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
314 |
have "is_Inf {x, y} (\<Sqinter>{x, y})" .. |
23373 | 315 |
then show ?thesis by (simp only: is_Inf_binary) |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
316 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
317 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
318 |
lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
319 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
320 |
have "is_Sup {x, y} (\<Squnion>{x, y})" .. |
23373 | 321 |
then show ?thesis by (simp only: is_Sup_binary) |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
322 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
323 |
|
11099 | 324 |
instance complete_lattice \<subseteq> lattice |
10309 | 325 |
proof |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
326 |
fix x y :: "'a::complete_lattice" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
327 |
from is_inf_binary show "\<exists>inf. is_inf x y inf" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
328 |
from is_sup_binary show "\<exists>sup. is_sup x y sup" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
329 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
330 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
331 |
theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
332 |
by (rule meet_equality) (rule is_inf_binary) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
333 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
334 |
theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
335 |
by (rule join_equality) (rule is_sup_binary) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
336 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
337 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
338 |
subsection {* Complete lattices and set-theory operations *} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
339 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
340 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
341 |
The complete lattice operations are (anti) monotone wrt.\ set |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
342 |
inclusion. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
343 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
344 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
345 |
theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
346 |
proof (rule Meet_greatest) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
347 |
fix a assume "a \<in> A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
348 |
also assume "A \<subseteq> B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
349 |
finally have "a \<in> B" . |
23373 | 350 |
then show "\<Sqinter>B \<sqsubseteq> a" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
351 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
352 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
353 |
theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
354 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
355 |
assume "A \<subseteq> B" |
23373 | 356 |
then have "dual ` A \<subseteq> dual ` B" by blast |
357 |
then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono) |
|
358 |
then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join) |
|
359 |
then show ?thesis by (simp only: dual_leq) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
360 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
361 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
362 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
363 |
Bounds over unions of sets may be obtained separately. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
364 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
365 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
366 |
theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
367 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
368 |
fix a assume "a \<in> A \<union> B" |
23373 | 369 |
then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
370 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
371 |
assume a: "a \<in> A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
372 |
have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
373 |
also from a have "\<dots> \<sqsubseteq> a" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
374 |
finally show ?thesis . |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
375 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
376 |
assume a: "a \<in> B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
377 |
have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
378 |
also from a have "\<dots> \<sqsubseteq> a" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
379 |
finally show ?thesis . |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
380 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
381 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
382 |
fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
383 |
show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
384 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
385 |
show "b \<sqsubseteq> \<Sqinter>A" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
386 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
387 |
fix a assume "a \<in> A" |
23373 | 388 |
then have "a \<in> A \<union> B" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
389 |
with b show "b \<sqsubseteq> a" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
390 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
391 |
show "b \<sqsubseteq> \<Sqinter>B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
392 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
393 |
fix a assume "a \<in> B" |
23373 | 394 |
then have "a \<in> A \<union> B" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
395 |
with b show "b \<sqsubseteq> a" .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
396 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
397 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
398 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
399 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
400 |
theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
401 |
proof - |
10834 | 402 |
have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
403 |
by (simp only: dual_Join image_Un) |
10834 | 404 |
also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)" |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
405 |
by (rule Meet_Un) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
406 |
also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
407 |
by (simp only: dual_join dual_Join) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
408 |
finally show ?thesis .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
409 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
410 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
411 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
412 |
Bounds over singleton sets are trivial. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
413 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
414 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
415 |
theorem Meet_singleton: "\<Sqinter>{x} = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
416 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
417 |
fix a assume "a \<in> {x}" |
23373 | 418 |
then have "a = x" by simp |
419 |
then show "x \<sqsubseteq> a" by (simp only: leq_refl) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
420 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
421 |
fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a" |
23373 | 422 |
then show "b \<sqsubseteq> x" by simp |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
423 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
424 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
425 |
theorem Join_singleton: "\<Squnion>{x} = x" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
426 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
427 |
have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
428 |
also have "\<dots> = dual x" by (rule Meet_singleton) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
429 |
finally show ?thesis .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
430 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
431 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
432 |
text {* |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
433 |
Bounds over the empty and universal set correspond to each other. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
434 |
*} |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
435 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
436 |
theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
437 |
proof |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
438 |
fix a :: "'a::complete_lattice" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
439 |
assume "a \<in> {}" |
23373 | 440 |
then have False by simp |
441 |
then show "\<Squnion>UNIV \<sqsubseteq> a" .. |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
442 |
next |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
443 |
fix b :: "'a::complete_lattice" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
444 |
have "b \<in> UNIV" .. |
23373 | 445 |
then show "b \<sqsubseteq> \<Squnion>UNIV" .. |
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
446 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
447 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
448 |
theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV" |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
449 |
proof - |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
450 |
have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
451 |
also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
452 |
also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet) |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
453 |
finally show ?thesis .. |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
454 |
qed |
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
455 |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
diff
changeset
|
456 |
end |