author | ballarin |
Fri, 12 Jan 2007 15:37:21 +0100 | |
changeset 22063 | 717425609192 |
parent 21896 | 9a7949815a84 |
child 22265 | 3c5c6bdf61de |
permissions | -rw-r--r-- |
14551 | 1 |
(* |
14706 | 2 |
Title: HOL/Algebra/Lattice.thy |
14551 | 3 |
Id: $Id$ |
4 |
Author: Clemens Ballarin, started 7 November 2003 |
|
5 |
Copyright: Clemens Ballarin |
|
6 |
*) |
|
7 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
8 |
theory Lattice imports Main begin |
14551 | 9 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
10 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
11 |
section {* Orders and Lattices *} |
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
12 |
|
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
13 |
text {* Object with a carrier set. *} |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
14 |
|
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
15 |
record 'a partial_object = |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
16 |
carrier :: "'a set" |
14551 | 17 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
18 |
|
14551 | 19 |
subsection {* Partial Orders *} |
20 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
21 |
record 'a order = "'a partial_object" + |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
22 |
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset
|
23 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
24 |
locale partial_order = |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
25 |
fixes L (structure) |
14551 | 26 |
assumes refl [intro, simp]: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
27 |
"x \<in> carrier L ==> x \<sqsubseteq> x" |
14551 | 28 |
and anti_sym [intro]: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
29 |
"[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" |
14551 | 30 |
and trans [trans]: |
31 |
"[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
32 |
x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
33 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
34 |
constdefs (structure L) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
35 |
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
36 |
"x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
37 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
38 |
-- {* Upper and lower bounds of a set. *} |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
39 |
Upper :: "[_, 'a set] => 'a set" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
40 |
"Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
41 |
carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
42 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
43 |
Lower :: "[_, 'a set] => 'a set" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
44 |
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
45 |
carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
46 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
47 |
-- {* Least and greatest, as predicate. *} |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
48 |
least :: "[_, 'a, 'a set] => bool" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
49 |
"least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
50 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
51 |
greatest :: "[_, 'a, 'a set] => bool" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
52 |
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
53 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
54 |
-- {* Supremum and infimum *} |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
55 |
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
56 |
"\<Squnion>A == THE x. least L x (Upper L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
57 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
58 |
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
59 |
"\<Sqinter>A == THE x. greatest L x (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
60 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
61 |
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
62 |
"x \<squnion> y == sup L {x, y}" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
63 |
|
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
64 |
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
65 |
"x \<sqinter> y == inf L {x, y}" |
14551 | 66 |
|
14651 | 67 |
|
68 |
subsubsection {* Upper *} |
|
14551 | 69 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
70 |
lemma Upper_closed [intro, simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
71 |
"Upper L A \<subseteq> carrier L" |
14551 | 72 |
by (unfold Upper_def) clarify |
73 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
74 |
lemma UpperD [dest]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
75 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
76 |
shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" |
14693 | 77 |
by (unfold Upper_def) blast |
14551 | 78 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
79 |
lemma Upper_memI: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
80 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
81 |
shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" |
14693 | 82 |
by (unfold Upper_def) blast |
14551 | 83 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
84 |
lemma Upper_antimono: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
85 |
"A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" |
14551 | 86 |
by (unfold Upper_def) blast |
87 |
||
14651 | 88 |
|
89 |
subsubsection {* Lower *} |
|
14551 | 90 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
91 |
lemma Lower_closed [intro, simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
92 |
"Lower L A \<subseteq> carrier L" |
14551 | 93 |
by (unfold Lower_def) clarify |
94 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
95 |
lemma LowerD [dest]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
96 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
97 |
shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x" |
14693 | 98 |
by (unfold Lower_def) blast |
14551 | 99 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
100 |
lemma Lower_memI: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
101 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
102 |
shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A" |
14693 | 103 |
by (unfold Lower_def) blast |
14551 | 104 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
105 |
lemma Lower_antimono: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
106 |
"A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" |
14551 | 107 |
by (unfold Lower_def) blast |
108 |
||
14651 | 109 |
|
110 |
subsubsection {* least *} |
|
14551 | 111 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
112 |
lemma least_carrier [intro, simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
113 |
shows "least L l A ==> l \<in> carrier L" |
14551 | 114 |
by (unfold least_def) fast |
115 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
116 |
lemma least_mem: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
117 |
"least L l A ==> l \<in> A" |
14551 | 118 |
by (unfold least_def) fast |
119 |
||
120 |
lemma (in partial_order) least_unique: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
121 |
"[| least L x A; least L y A |] ==> x = y" |
14551 | 122 |
by (unfold least_def) blast |
123 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
124 |
lemma least_le: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
125 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
126 |
shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a" |
14551 | 127 |
by (unfold least_def) fast |
128 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
129 |
lemma least_UpperI: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
130 |
fixes L (structure) |
14551 | 131 |
assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
132 |
and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
133 |
and L: "A \<subseteq> carrier L" "s \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
134 |
shows "least L s (Upper L A)" |
14693 | 135 |
proof - |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
136 |
have "Upper L A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
137 |
moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
138 |
moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast |
14693 | 139 |
ultimately show ?thesis by (simp add: least_def) |
14551 | 140 |
qed |
141 |
||
14651 | 142 |
|
143 |
subsubsection {* greatest *} |
|
14551 | 144 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
145 |
lemma greatest_carrier [intro, simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
146 |
shows "greatest L l A ==> l \<in> carrier L" |
14551 | 147 |
by (unfold greatest_def) fast |
148 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
149 |
lemma greatest_mem: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
150 |
"greatest L l A ==> l \<in> A" |
14551 | 151 |
by (unfold greatest_def) fast |
152 |
||
153 |
lemma (in partial_order) greatest_unique: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
154 |
"[| greatest L x A; greatest L y A |] ==> x = y" |
14551 | 155 |
by (unfold greatest_def) blast |
156 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
157 |
lemma greatest_le: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
158 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
159 |
shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" |
14551 | 160 |
by (unfold greatest_def) fast |
161 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
162 |
lemma greatest_LowerI: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
163 |
fixes L (structure) |
14551 | 164 |
assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
165 |
and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
166 |
and L: "A \<subseteq> carrier L" "i \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
167 |
shows "greatest L i (Lower L A)" |
14693 | 168 |
proof - |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
169 |
have "Lower L A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
170 |
moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
171 |
moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast |
14693 | 172 |
ultimately show ?thesis by (simp add: greatest_def) |
14551 | 173 |
qed |
174 |
||
14693 | 175 |
|
14551 | 176 |
subsection {* Lattices *} |
177 |
||
178 |
locale lattice = partial_order + |
|
179 |
assumes sup_of_two_exists: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
180 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
14551 | 181 |
and inf_of_two_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
182 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
14551 | 183 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
184 |
lemma least_Upper_above: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
185 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
186 |
shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" |
14551 | 187 |
by (unfold least_def) blast |
188 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
189 |
lemma greatest_Lower_above: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
190 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
191 |
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" |
14551 | 192 |
by (unfold greatest_def) blast |
193 |
||
14666 | 194 |
|
14551 | 195 |
subsubsection {* Supremum *} |
196 |
||
197 |
lemma (in lattice) joinI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
198 |
"[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
14551 | 199 |
==> P (x \<squnion> y)" |
200 |
proof (unfold join_def sup_def) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
201 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
202 |
and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
203 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
204 |
with L show "P (THE l. least L l (Upper L {x, y}))" |
14693 | 205 |
by (fast intro: theI2 least_unique P) |
14551 | 206 |
qed |
207 |
||
208 |
lemma (in lattice) join_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
209 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
210 |
by (rule joinI) (rule least_carrier) |
14551 | 211 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
212 |
lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
213 |
"x \<in> carrier L ==> least L x (Upper L {x})" |
14551 | 214 |
by (rule least_UpperI) fast+ |
215 |
||
216 |
lemma (in partial_order) sup_of_singleton [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
217 |
"x \<in> carrier L ==> \<Squnion>{x} = x" |
14551 | 218 |
by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
219 |
||
14666 | 220 |
|
221 |
text {* Condition on @{text A}: supremum exists. *} |
|
14551 | 222 |
|
223 |
lemma (in lattice) sup_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
224 |
"[| !!s. least L s (Upper L (insert x A)) ==> P s; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
225 |
least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
14693 | 226 |
==> P (\<Squnion>(insert x A))" |
14551 | 227 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
228 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
229 |
and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
230 |
and least_a: "least L a (Upper L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
231 |
from L least_a have La: "a \<in> carrier L" by simp |
14551 | 232 |
from L sup_of_two_exists least_a |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
233 |
obtain s where least_s: "least L s (Upper L {a, x})" by blast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
234 |
show "P (THE l. least L l (Upper L (insert x A)))" |
14693 | 235 |
proof (rule theI2) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
236 |
show "least L s (Upper L (insert x A))" |
14551 | 237 |
proof (rule least_UpperI) |
238 |
fix z |
|
14693 | 239 |
assume "z \<in> insert x A" |
240 |
then show "z \<sqsubseteq> s" |
|
241 |
proof |
|
242 |
assume "z = x" then show ?thesis |
|
243 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
244 |
next |
|
245 |
assume "z \<in> A" |
|
246 |
with L least_s least_a show ?thesis |
|
247 |
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
248 |
qed |
|
249 |
next |
|
250 |
fix y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
251 |
assume y: "y \<in> Upper L (insert x A)" |
14693 | 252 |
show "s \<sqsubseteq> y" |
253 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
254 |
fix z |
|
255 |
assume z: "z \<in> {a, x}" |
|
256 |
then show "z \<sqsubseteq> y" |
|
257 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
258 |
have y': "y \<in> Upper L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
259 |
apply (rule subsetD [where A = "Upper L (insert x A)"]) |
14693 | 260 |
apply (rule Upper_antimono) apply clarify apply assumption |
261 |
done |
|
262 |
assume "z = a" |
|
263 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
264 |
next |
|
265 |
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) |
|
266 |
with y L show ?thesis by blast |
|
267 |
qed |
|
268 |
qed (rule Upper_closed [THEN subsetD]) |
|
269 |
next |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
270 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
271 |
from least_s show "s \<in> carrier L" by simp |
14551 | 272 |
qed |
273 |
next |
|
274 |
fix l |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
275 |
assume least_l: "least L l (Upper L (insert x A))" |
14551 | 276 |
show "l = s" |
277 |
proof (rule least_unique) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
278 |
show "least L s (Upper L (insert x A))" |
14551 | 279 |
proof (rule least_UpperI) |
14693 | 280 |
fix z |
281 |
assume "z \<in> insert x A" |
|
282 |
then show "z \<sqsubseteq> s" |
|
283 |
proof |
|
284 |
assume "z = x" then show ?thesis |
|
285 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
286 |
next |
|
287 |
assume "z \<in> A" |
|
288 |
with L least_s least_a show ?thesis |
|
289 |
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
14551 | 290 |
qed |
291 |
next |
|
14693 | 292 |
fix y |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
293 |
assume y: "y \<in> Upper L (insert x A)" |
14693 | 294 |
show "s \<sqsubseteq> y" |
295 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
296 |
fix z |
|
297 |
assume z: "z \<in> {a, x}" |
|
298 |
then show "z \<sqsubseteq> y" |
|
299 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
300 |
have y': "y \<in> Upper L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
301 |
apply (rule subsetD [where A = "Upper L (insert x A)"]) |
14693 | 302 |
apply (rule Upper_antimono) apply clarify apply assumption |
303 |
done |
|
304 |
assume "z = a" |
|
305 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
306 |
next |
|
307 |
assume "z \<in> {x}" |
|
308 |
with y L show ?thesis by blast |
|
309 |
qed |
|
310 |
qed (rule Upper_closed [THEN subsetD]) |
|
14551 | 311 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
312 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
313 |
from least_s show "s \<in> carrier L" by simp |
14551 | 314 |
qed |
315 |
qed |
|
316 |
qed |
|
317 |
qed |
|
318 |
||
319 |
lemma (in lattice) finite_sup_least: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
320 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)" |
14551 | 321 |
proof (induct set: Finites) |
14693 | 322 |
case empty |
323 |
then show ?case by simp |
|
14551 | 324 |
next |
15328 | 325 |
case (insert x A) |
14551 | 326 |
show ?case |
327 |
proof (cases "A = {}") |
|
328 |
case True |
|
329 |
with insert show ?thesis by (simp add: sup_of_singletonI) |
|
330 |
next |
|
331 |
case False |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
332 |
with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
14693 | 333 |
with _ show ?thesis |
334 |
by (rule sup_insertI) (simp_all add: insert [simplified]) |
|
14551 | 335 |
qed |
336 |
qed |
|
337 |
||
338 |
lemma (in lattice) finite_sup_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
339 |
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
340 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 341 |
shows "P (\<Squnion> (insert x A))" |
342 |
proof (cases "A = {}") |
|
343 |
case True with P and xA show ?thesis |
|
344 |
by (simp add: sup_of_singletonI) |
|
345 |
next |
|
346 |
case False with P and xA show ?thesis |
|
347 |
by (simp add: sup_insertI finite_sup_least) |
|
348 |
qed |
|
349 |
||
350 |
lemma (in lattice) finite_sup_closed: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
351 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
14551 | 352 |
proof (induct set: Finites) |
353 |
case empty then show ?case by simp |
|
354 |
next |
|
15328 | 355 |
case insert then show ?case |
14693 | 356 |
by - (rule finite_sup_insertI, simp_all) |
14551 | 357 |
qed |
358 |
||
359 |
lemma (in lattice) join_left: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
360 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
14693 | 361 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 362 |
|
363 |
lemma (in lattice) join_right: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
364 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
14693 | 365 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 366 |
|
367 |
lemma (in lattice) sup_of_two_least: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
368 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
14551 | 369 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
370 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
371 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
372 |
with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
14551 | 373 |
by (fast intro: theI2 least_unique) (* blast fails *) |
374 |
qed |
|
375 |
||
376 |
lemma (in lattice) join_le: |
|
14693 | 377 |
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
378 |
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 379 |
shows "x \<squnion> y \<sqsubseteq> z" |
380 |
proof (rule joinI) |
|
381 |
fix s |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
382 |
assume "least L s (Upper L {x, y})" |
14551 | 383 |
with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
384 |
qed |
|
14693 | 385 |
|
14551 | 386 |
lemma (in lattice) join_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
387 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14693 | 388 |
shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
14551 | 389 |
proof (rule finite_sup_insertI) |
14651 | 390 |
-- {* The textbook argument in Jacobson I, p 457 *} |
14551 | 391 |
fix s |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
392 |
assume sup: "least L s (Upper L {x, y, z})" |
14551 | 393 |
show "x \<squnion> (y \<squnion> z) = s" |
394 |
proof (rule anti_sym) |
|
395 |
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
|
396 |
by (fastsimp intro!: join_le elim: least_Upper_above) |
|
397 |
next |
|
398 |
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
399 |
by (erule_tac least_le) |
|
400 |
(blast intro!: Upper_memI intro: trans join_left join_right join_closed) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
401 |
qed (simp_all add: L least_carrier [OF sup]) |
14551 | 402 |
qed (simp_all add: L) |
403 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
404 |
lemma join_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
405 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
406 |
shows "x \<squnion> y = y \<squnion> x" |
14551 | 407 |
by (unfold join_def) (simp add: insert_commute) |
408 |
||
409 |
lemma (in lattice) join_assoc: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
410 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 411 |
shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
412 |
proof - |
|
413 |
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
|
14693 | 414 |
also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) |
415 |
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) |
|
14551 | 416 |
also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) |
417 |
finally show ?thesis . |
|
418 |
qed |
|
419 |
||
14693 | 420 |
|
14551 | 421 |
subsubsection {* Infimum *} |
422 |
||
423 |
lemma (in lattice) meetI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
424 |
"[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
425 |
x \<in> carrier L; y \<in> carrier L |] |
14551 | 426 |
==> P (x \<sqinter> y)" |
427 |
proof (unfold meet_def inf_def) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
428 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
429 |
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
430 |
with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
431 |
with L show "P (THE g. greatest L g (Lower L {x, y}))" |
14551 | 432 |
by (fast intro: theI2 greatest_unique P) |
433 |
qed |
|
434 |
||
435 |
lemma (in lattice) meet_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
436 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
437 |
by (rule meetI) (rule greatest_carrier) |
14551 | 438 |
|
14651 | 439 |
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
440 |
"x \<in> carrier L ==> greatest L x (Lower L {x})" |
14551 | 441 |
by (rule greatest_LowerI) fast+ |
442 |
||
443 |
lemma (in partial_order) inf_of_singleton [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
444 |
"x \<in> carrier L ==> \<Sqinter> {x} = x" |
14551 | 445 |
by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
446 |
||
447 |
text {* Condition on A: infimum exists. *} |
|
448 |
||
449 |
lemma (in lattice) inf_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
450 |
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
451 |
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
14693 | 452 |
==> P (\<Sqinter>(insert x A))" |
14551 | 453 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
454 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
455 |
and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
456 |
and greatest_a: "greatest L a (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
457 |
from L greatest_a have La: "a \<in> carrier L" by simp |
14551 | 458 |
from L inf_of_two_exists greatest_a |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
459 |
obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
460 |
show "P (THE g. greatest L g (Lower L (insert x A)))" |
14693 | 461 |
proof (rule theI2) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
462 |
show "greatest L i (Lower L (insert x A))" |
14551 | 463 |
proof (rule greatest_LowerI) |
464 |
fix z |
|
14693 | 465 |
assume "z \<in> insert x A" |
466 |
then show "i \<sqsubseteq> z" |
|
467 |
proof |
|
468 |
assume "z = x" then show ?thesis |
|
469 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
470 |
next |
|
471 |
assume "z \<in> A" |
|
472 |
with L greatest_i greatest_a show ?thesis |
|
473 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
474 |
qed |
|
475 |
next |
|
476 |
fix y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
477 |
assume y: "y \<in> Lower L (insert x A)" |
14693 | 478 |
show "y \<sqsubseteq> i" |
479 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
480 |
fix z |
|
481 |
assume z: "z \<in> {a, x}" |
|
482 |
then show "y \<sqsubseteq> z" |
|
483 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
484 |
have y': "y \<in> Lower L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
485 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
14693 | 486 |
apply (rule Lower_antimono) apply clarify apply assumption |
487 |
done |
|
488 |
assume "z = a" |
|
489 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
490 |
next |
|
491 |
assume "z \<in> {x}" |
|
492 |
with y L show ?thesis by blast |
|
493 |
qed |
|
494 |
qed (rule Lower_closed [THEN subsetD]) |
|
495 |
next |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
496 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
497 |
from greatest_i show "i \<in> carrier L" by simp |
14551 | 498 |
qed |
499 |
next |
|
500 |
fix g |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
501 |
assume greatest_g: "greatest L g (Lower L (insert x A))" |
14551 | 502 |
show "g = i" |
503 |
proof (rule greatest_unique) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
504 |
show "greatest L i (Lower L (insert x A))" |
14551 | 505 |
proof (rule greatest_LowerI) |
14693 | 506 |
fix z |
507 |
assume "z \<in> insert x A" |
|
508 |
then show "i \<sqsubseteq> z" |
|
509 |
proof |
|
510 |
assume "z = x" then show ?thesis |
|
511 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
512 |
next |
|
513 |
assume "z \<in> A" |
|
514 |
with L greatest_i greatest_a show ?thesis |
|
515 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
516 |
qed |
|
14551 | 517 |
next |
14693 | 518 |
fix y |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
519 |
assume y: "y \<in> Lower L (insert x A)" |
14693 | 520 |
show "y \<sqsubseteq> i" |
521 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
522 |
fix z |
|
523 |
assume z: "z \<in> {a, x}" |
|
524 |
then show "y \<sqsubseteq> z" |
|
525 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
526 |
have y': "y \<in> Lower L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
527 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
14693 | 528 |
apply (rule Lower_antimono) apply clarify apply assumption |
529 |
done |
|
530 |
assume "z = a" |
|
531 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
532 |
next |
|
533 |
assume "z \<in> {x}" |
|
534 |
with y L show ?thesis by blast |
|
14551 | 535 |
qed |
14693 | 536 |
qed (rule Lower_closed [THEN subsetD]) |
14551 | 537 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
538 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
539 |
from greatest_i show "i \<in> carrier L" by simp |
14551 | 540 |
qed |
541 |
qed |
|
542 |
qed |
|
543 |
qed |
|
544 |
||
545 |
lemma (in lattice) finite_inf_greatest: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
546 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" |
14551 | 547 |
proof (induct set: Finites) |
548 |
case empty then show ?case by simp |
|
549 |
next |
|
15328 | 550 |
case (insert x A) |
14551 | 551 |
show ?case |
552 |
proof (cases "A = {}") |
|
553 |
case True |
|
554 |
with insert show ?thesis by (simp add: inf_of_singletonI) |
|
555 |
next |
|
556 |
case False |
|
557 |
from insert show ?thesis |
|
558 |
proof (rule_tac inf_insertI) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
559 |
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
14551 | 560 |
qed simp_all |
561 |
qed |
|
562 |
qed |
|
563 |
||
564 |
lemma (in lattice) finite_inf_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
565 |
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
566 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 567 |
shows "P (\<Sqinter> (insert x A))" |
568 |
proof (cases "A = {}") |
|
569 |
case True with P and xA show ?thesis |
|
570 |
by (simp add: inf_of_singletonI) |
|
571 |
next |
|
572 |
case False with P and xA show ?thesis |
|
573 |
by (simp add: inf_insertI finite_inf_greatest) |
|
574 |
qed |
|
575 |
||
576 |
lemma (in lattice) finite_inf_closed: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
577 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
14551 | 578 |
proof (induct set: Finites) |
579 |
case empty then show ?case by simp |
|
580 |
next |
|
15328 | 581 |
case insert then show ?case |
14551 | 582 |
by (rule_tac finite_inf_insertI) (simp_all) |
583 |
qed |
|
584 |
||
585 |
lemma (in lattice) meet_left: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
586 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
14693 | 587 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 588 |
|
589 |
lemma (in lattice) meet_right: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
590 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
14693 | 591 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 592 |
|
593 |
lemma (in lattice) inf_of_two_greatest: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
594 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
595 |
greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
14551 | 596 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
597 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
598 |
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
14551 | 599 |
with L |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
600 |
show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
14551 | 601 |
by (fast intro: theI2 greatest_unique) (* blast fails *) |
602 |
qed |
|
603 |
||
604 |
lemma (in lattice) meet_le: |
|
14693 | 605 |
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
606 |
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 607 |
shows "z \<sqsubseteq> x \<sqinter> y" |
608 |
proof (rule meetI) |
|
609 |
fix i |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
610 |
assume "greatest L i (Lower L {x, y})" |
14551 | 611 |
with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
612 |
qed |
|
14693 | 613 |
|
14551 | 614 |
lemma (in lattice) meet_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
615 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14693 | 616 |
shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
14551 | 617 |
proof (rule finite_inf_insertI) |
618 |
txt {* The textbook argument in Jacobson I, p 457 *} |
|
619 |
fix i |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
620 |
assume inf: "greatest L i (Lower L {x, y, z})" |
14551 | 621 |
show "x \<sqinter> (y \<sqinter> z) = i" |
622 |
proof (rule anti_sym) |
|
623 |
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
624 |
by (fastsimp intro!: meet_le elim: greatest_Lower_above) |
|
625 |
next |
|
626 |
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" |
|
627 |
by (erule_tac greatest_le) |
|
628 |
(blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
629 |
qed (simp_all add: L greatest_carrier [OF inf]) |
14551 | 630 |
qed (simp_all add: L) |
631 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
632 |
lemma meet_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
633 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
634 |
shows "x \<sqinter> y = y \<sqinter> x" |
14551 | 635 |
by (unfold meet_def) (simp add: insert_commute) |
636 |
||
637 |
lemma (in lattice) meet_assoc: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
638 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 639 |
shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
640 |
proof - |
|
641 |
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) |
|
642 |
also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) |
|
643 |
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) |
|
644 |
also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) |
|
645 |
finally show ?thesis . |
|
646 |
qed |
|
647 |
||
14693 | 648 |
|
14551 | 649 |
subsection {* Total Orders *} |
650 |
||
651 |
locale total_order = lattice + |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
652 |
assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
14551 | 653 |
|
654 |
text {* Introduction rule: the usual definition of total order *} |
|
655 |
||
656 |
lemma (in partial_order) total_orderI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
657 |
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
658 |
shows "total_order L" |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
659 |
proof intro_locales |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
660 |
show "lattice_axioms L" |
14551 | 661 |
proof (rule lattice_axioms.intro) |
662 |
fix x y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
663 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
664 |
show "EX s. least L s (Upper L {x, y})" |
14551 | 665 |
proof - |
666 |
note total L |
|
667 |
moreover |
|
668 |
{ |
|
14693 | 669 |
assume "x \<sqsubseteq> y" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
670 |
with L have "least L y (Upper L {x, y})" |
14693 | 671 |
by (rule_tac least_UpperI) auto |
14551 | 672 |
} |
673 |
moreover |
|
674 |
{ |
|
14693 | 675 |
assume "y \<sqsubseteq> x" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
676 |
with L have "least L x (Upper L {x, y})" |
14693 | 677 |
by (rule_tac least_UpperI) auto |
14551 | 678 |
} |
679 |
ultimately show ?thesis by blast |
|
680 |
qed |
|
681 |
next |
|
682 |
fix x y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
683 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
684 |
show "EX i. greatest L i (Lower L {x, y})" |
14551 | 685 |
proof - |
686 |
note total L |
|
687 |
moreover |
|
688 |
{ |
|
14693 | 689 |
assume "y \<sqsubseteq> x" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
690 |
with L have "greatest L y (Lower L {x, y})" |
14693 | 691 |
by (rule_tac greatest_LowerI) auto |
14551 | 692 |
} |
693 |
moreover |
|
694 |
{ |
|
14693 | 695 |
assume "x \<sqsubseteq> y" |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
696 |
with L have "greatest L x (Lower L {x, y})" |
14693 | 697 |
by (rule_tac greatest_LowerI) auto |
14551 | 698 |
} |
699 |
ultimately show ?thesis by blast |
|
700 |
qed |
|
701 |
qed |
|
702 |
qed (assumption | rule total_order_axioms.intro)+ |
|
703 |
||
14693 | 704 |
|
14551 | 705 |
subsection {* Complete lattices *} |
706 |
||
707 |
locale complete_lattice = lattice + |
|
708 |
assumes sup_exists: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
709 |
"[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
14551 | 710 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
711 |
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset
|
712 |
|
14551 | 713 |
text {* Introduction rule: the usual definition of complete lattice *} |
714 |
||
715 |
lemma (in partial_order) complete_latticeI: |
|
716 |
assumes sup_exists: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
717 |
"!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
14551 | 718 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
719 |
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
720 |
shows "complete_lattice L" |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
721 |
proof intro_locales |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
722 |
show "lattice_axioms L" |
14693 | 723 |
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
14551 | 724 |
qed (assumption | rule complete_lattice_axioms.intro)+ |
725 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
726 |
constdefs (structure L) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
727 |
top :: "_ => 'a" ("\<top>\<index>") |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
728 |
"\<top> == sup L (carrier L)" |
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset
|
729 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
730 |
bottom :: "_ => 'a" ("\<bottom>\<index>") |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
731 |
"\<bottom> == inf L (carrier L)" |
14551 | 732 |
|
733 |
||
734 |
lemma (in complete_lattice) supI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
735 |
"[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] |
14651 | 736 |
==> P (\<Squnion>A)" |
14551 | 737 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
738 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
739 |
and P: "!!l. least L l (Upper L A) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
740 |
with sup_exists obtain s where "least L s (Upper L A)" by blast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
741 |
with L show "P (THE l. least L l (Upper L A))" |
14551 | 742 |
by (fast intro: theI2 least_unique P) |
743 |
qed |
|
744 |
||
745 |
lemma (in complete_lattice) sup_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
746 |
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" |
14551 | 747 |
by (rule supI) simp_all |
748 |
||
749 |
lemma (in complete_lattice) top_closed [simp, intro]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
750 |
"\<top> \<in> carrier L" |
14551 | 751 |
by (unfold top_def) simp |
752 |
||
753 |
lemma (in complete_lattice) infI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
754 |
"[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] |
14693 | 755 |
==> P (\<Sqinter>A)" |
14551 | 756 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
757 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
758 |
and P: "!!l. greatest L l (Lower L A) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
759 |
with inf_exists obtain s where "greatest L s (Lower L A)" by blast |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
760 |
with L show "P (THE l. greatest L l (Lower L A))" |
14551 | 761 |
by (fast intro: theI2 greatest_unique P) |
762 |
qed |
|
763 |
||
764 |
lemma (in complete_lattice) inf_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
765 |
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" |
14551 | 766 |
by (rule infI) simp_all |
767 |
||
768 |
lemma (in complete_lattice) bottom_closed [simp, intro]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
769 |
"\<bottom> \<in> carrier L" |
14551 | 770 |
by (unfold bottom_def) simp |
771 |
||
772 |
text {* Jacobson: Theorem 8.1 *} |
|
773 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
774 |
lemma Lower_empty [simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
775 |
"Lower L {} = carrier L" |
14551 | 776 |
by (unfold Lower_def) simp |
777 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
778 |
lemma Upper_empty [simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
779 |
"Upper L {} = carrier L" |
14551 | 780 |
by (unfold Upper_def) simp |
781 |
||
782 |
theorem (in partial_order) complete_lattice_criterion1: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
783 |
assumes top_exists: "EX g. greatest L g (carrier L)" |
14551 | 784 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
785 |
"!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
786 |
shows "complete_lattice L" |
14551 | 787 |
proof (rule complete_latticeI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
788 |
from top_exists obtain top where top: "greatest L top (carrier L)" .. |
14551 | 789 |
fix A |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
790 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
791 |
let ?B = "Upper L A" |
14551 | 792 |
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) |
793 |
then have B_non_empty: "?B ~= {}" by fast |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
794 |
have B_L: "?B \<subseteq> carrier L" by simp |
14551 | 795 |
from inf_exists [OF B_L B_non_empty] |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
796 |
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
797 |
have "least L b (Upper L A)" |
14551 | 798 |
apply (rule least_UpperI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
799 |
apply (rule greatest_le [where A = "Lower L ?B"]) |
14551 | 800 |
apply (rule b_inf_B) |
801 |
apply (rule Lower_memI) |
|
802 |
apply (erule UpperD) |
|
803 |
apply assumption |
|
804 |
apply (rule L) |
|
805 |
apply (fast intro: L [THEN subsetD]) |
|
806 |
apply (erule greatest_Lower_above [OF b_inf_B]) |
|
807 |
apply simp |
|
808 |
apply (rule L) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
809 |
apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) |
14551 | 810 |
done |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
811 |
then show "EX s. least L s (Upper L A)" .. |
14551 | 812 |
next |
813 |
fix A |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
814 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
815 |
show "EX i. greatest L i (Lower L A)" |
14551 | 816 |
proof (cases "A = {}") |
817 |
case True then show ?thesis |
|
818 |
by (simp add: top_exists) |
|
819 |
next |
|
820 |
case False with L show ?thesis |
|
821 |
by (rule inf_exists) |
|
822 |
qed |
|
823 |
qed |
|
824 |
||
825 |
(* TODO: prove dual version *) |
|
826 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
827 |
|
14551 | 828 |
subsection {* Examples *} |
829 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
830 |
subsubsection {* Powerset of a Set is a Complete Lattice *} |
14551 | 831 |
|
832 |
theorem powerset_is_complete_lattice: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
833 |
"complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
834 |
(is "complete_lattice ?L") |
14551 | 835 |
proof (rule partial_order.complete_latticeI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
836 |
show "partial_order ?L" |
14551 | 837 |
by (rule partial_order.intro) auto |
838 |
next |
|
839 |
fix B |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
840 |
assume "B \<subseteq> carrier ?L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
841 |
then have "least ?L (\<Union> B) (Upper ?L B)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
842 |
by (fastsimp intro!: least_UpperI simp: Upper_def) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
843 |
then show "EX s. least ?L s (Upper ?L B)" .. |
14551 | 844 |
next |
845 |
fix B |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
846 |
assume "B \<subseteq> carrier ?L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
847 |
then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" |
14551 | 848 |
txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: |
849 |
@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
850 |
by (fastsimp intro!: greatest_LowerI simp: Lower_def) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
851 |
then show "EX i. greatest ?L i (Lower ?L B)" .. |
14551 | 852 |
qed |
853 |
||
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
854 |
text {* An other example, that of the lattice of subgroups of a group, |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
855 |
can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
14551 | 856 |
|
14693 | 857 |
end |