author | berghofe |
Wed, 07 May 2008 10:56:58 +0200 | |
changeset 26805 | 27941d7d9a11 |
parent 24087 | eb025d149a34 |
child 27700 | ef4b26efa8b6 |
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)"]) |
23463 | 260 |
apply (rule Upper_antimono) |
261 |
apply blast |
|
262 |
apply (rule y) |
|
14693 | 263 |
done |
264 |
assume "z = a" |
|
265 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
266 |
next |
|
267 |
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) |
|
268 |
with y L show ?thesis by blast |
|
269 |
qed |
|
23350 | 270 |
qed (rule Upper_closed [THEN subsetD, OF y]) |
14693 | 271 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
272 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
273 |
from least_s show "s \<in> carrier L" by simp |
14551 | 274 |
qed |
275 |
next |
|
276 |
fix l |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
277 |
assume least_l: "least L l (Upper L (insert x A))" |
14551 | 278 |
show "l = s" |
279 |
proof (rule least_unique) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
280 |
show "least L s (Upper L (insert x A))" |
14551 | 281 |
proof (rule least_UpperI) |
14693 | 282 |
fix z |
283 |
assume "z \<in> insert x A" |
|
284 |
then show "z \<sqsubseteq> s" |
|
285 |
proof |
|
286 |
assume "z = x" then show ?thesis |
|
287 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
288 |
next |
|
289 |
assume "z \<in> A" |
|
290 |
with L least_s least_a show ?thesis |
|
291 |
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
14551 | 292 |
qed |
293 |
next |
|
14693 | 294 |
fix y |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
295 |
assume y: "y \<in> Upper L (insert x A)" |
14693 | 296 |
show "s \<sqsubseteq> y" |
297 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
298 |
fix z |
|
299 |
assume z: "z \<in> {a, x}" |
|
300 |
then show "z \<sqsubseteq> y" |
|
301 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
302 |
have y': "y \<in> Upper L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
303 |
apply (rule subsetD [where A = "Upper L (insert x A)"]) |
23463 | 304 |
apply (rule Upper_antimono) |
305 |
apply blast |
|
306 |
apply (rule y) |
|
14693 | 307 |
done |
308 |
assume "z = a" |
|
309 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
310 |
next |
|
311 |
assume "z \<in> {x}" |
|
312 |
with y L show ?thesis by blast |
|
313 |
qed |
|
23350 | 314 |
qed (rule Upper_closed [THEN subsetD, OF y]) |
14551 | 315 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
316 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
317 |
from least_s show "s \<in> carrier L" by simp |
14551 | 318 |
qed |
23350 | 319 |
qed (rule least_l) |
320 |
qed (rule P) |
|
14551 | 321 |
qed |
322 |
||
323 |
lemma (in lattice) finite_sup_least: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
324 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)" |
22265 | 325 |
proof (induct set: finite) |
14693 | 326 |
case empty |
327 |
then show ?case by simp |
|
14551 | 328 |
next |
15328 | 329 |
case (insert x A) |
14551 | 330 |
show ?case |
331 |
proof (cases "A = {}") |
|
332 |
case True |
|
333 |
with insert show ?thesis by (simp add: sup_of_singletonI) |
|
334 |
next |
|
335 |
case False |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
336 |
with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
14693 | 337 |
with _ show ?thesis |
338 |
by (rule sup_insertI) (simp_all add: insert [simplified]) |
|
14551 | 339 |
qed |
340 |
qed |
|
341 |
||
342 |
lemma (in lattice) finite_sup_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
343 |
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
|
344 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 345 |
shows "P (\<Squnion> (insert x A))" |
346 |
proof (cases "A = {}") |
|
347 |
case True with P and xA show ?thesis |
|
348 |
by (simp add: sup_of_singletonI) |
|
349 |
next |
|
350 |
case False with P and xA show ?thesis |
|
351 |
by (simp add: sup_insertI finite_sup_least) |
|
352 |
qed |
|
353 |
||
354 |
lemma (in lattice) finite_sup_closed: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
355 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
22265 | 356 |
proof (induct set: finite) |
14551 | 357 |
case empty then show ?case by simp |
358 |
next |
|
15328 | 359 |
case insert then show ?case |
14693 | 360 |
by - (rule finite_sup_insertI, simp_all) |
14551 | 361 |
qed |
362 |
||
363 |
lemma (in lattice) join_left: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
364 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
14693 | 365 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 366 |
|
367 |
lemma (in lattice) join_right: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
368 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
14693 | 369 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 370 |
|
371 |
lemma (in lattice) sup_of_two_least: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
372 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
14551 | 373 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
374 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
375 |
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
|
376 |
with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
14551 | 377 |
by (fast intro: theI2 least_unique) (* blast fails *) |
378 |
qed |
|
379 |
||
380 |
lemma (in lattice) join_le: |
|
14693 | 381 |
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
23350 | 382 |
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" |
14551 | 383 |
shows "x \<squnion> y \<sqsubseteq> z" |
23350 | 384 |
proof (rule joinI [OF _ x y]) |
14551 | 385 |
fix s |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
386 |
assume "least L s (Upper L {x, y})" |
23350 | 387 |
with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
14551 | 388 |
qed |
14693 | 389 |
|
14551 | 390 |
lemma (in lattice) join_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
391 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14693 | 392 |
shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
14551 | 393 |
proof (rule finite_sup_insertI) |
14651 | 394 |
-- {* The textbook argument in Jacobson I, p 457 *} |
14551 | 395 |
fix s |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
396 |
assume sup: "least L s (Upper L {x, y, z})" |
14551 | 397 |
show "x \<squnion> (y \<squnion> z) = s" |
398 |
proof (rule anti_sym) |
|
399 |
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
|
400 |
by (fastsimp intro!: join_le elim: least_Upper_above) |
|
401 |
next |
|
402 |
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
403 |
by (erule_tac least_le) |
|
404 |
(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
|
405 |
qed (simp_all add: L least_carrier [OF sup]) |
14551 | 406 |
qed (simp_all add: L) |
407 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
408 |
lemma join_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
409 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
410 |
shows "x \<squnion> y = y \<squnion> x" |
14551 | 411 |
by (unfold join_def) (simp add: insert_commute) |
412 |
||
413 |
lemma (in lattice) join_assoc: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
414 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 415 |
shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
416 |
proof - |
|
417 |
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
|
14693 | 418 |
also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) |
419 |
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) |
|
14551 | 420 |
also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) |
421 |
finally show ?thesis . |
|
422 |
qed |
|
423 |
||
14693 | 424 |
|
14551 | 425 |
subsubsection {* Infimum *} |
426 |
||
427 |
lemma (in lattice) meetI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
428 |
"[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
429 |
x \<in> carrier L; y \<in> carrier L |] |
14551 | 430 |
==> P (x \<sqinter> y)" |
431 |
proof (unfold meet_def inf_def) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
432 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
433 |
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
434 |
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
|
435 |
with L show "P (THE g. greatest L g (Lower L {x, y}))" |
14551 | 436 |
by (fast intro: theI2 greatest_unique P) |
437 |
qed |
|
438 |
||
439 |
lemma (in lattice) meet_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
440 |
"[| 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
|
441 |
by (rule meetI) (rule greatest_carrier) |
14551 | 442 |
|
14651 | 443 |
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
444 |
"x \<in> carrier L ==> greatest L x (Lower L {x})" |
14551 | 445 |
by (rule greatest_LowerI) fast+ |
446 |
||
447 |
lemma (in partial_order) inf_of_singleton [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
448 |
"x \<in> carrier L ==> \<Sqinter> {x} = x" |
14551 | 449 |
by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
450 |
||
451 |
text {* Condition on A: infimum exists. *} |
|
452 |
||
453 |
lemma (in lattice) inf_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
454 |
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
455 |
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
14693 | 456 |
==> P (\<Sqinter>(insert x A))" |
14551 | 457 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
458 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
459 |
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
|
460 |
and greatest_a: "greatest L a (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
461 |
from L greatest_a have La: "a \<in> carrier L" by simp |
14551 | 462 |
from L inf_of_two_exists greatest_a |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
463 |
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
|
464 |
show "P (THE g. greatest L g (Lower L (insert x A)))" |
14693 | 465 |
proof (rule theI2) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
466 |
show "greatest L i (Lower L (insert x A))" |
14551 | 467 |
proof (rule greatest_LowerI) |
468 |
fix z |
|
14693 | 469 |
assume "z \<in> insert x A" |
470 |
then show "i \<sqsubseteq> z" |
|
471 |
proof |
|
472 |
assume "z = x" then show ?thesis |
|
473 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
474 |
next |
|
475 |
assume "z \<in> A" |
|
476 |
with L greatest_i greatest_a show ?thesis |
|
477 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
478 |
qed |
|
479 |
next |
|
480 |
fix y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
481 |
assume y: "y \<in> Lower L (insert x A)" |
14693 | 482 |
show "y \<sqsubseteq> i" |
483 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
484 |
fix z |
|
485 |
assume z: "z \<in> {a, x}" |
|
486 |
then show "y \<sqsubseteq> z" |
|
487 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
488 |
have y': "y \<in> Lower L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
489 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
23463 | 490 |
apply (rule Lower_antimono) |
491 |
apply blast |
|
492 |
apply (rule y) |
|
14693 | 493 |
done |
494 |
assume "z = a" |
|
495 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
496 |
next |
|
497 |
assume "z \<in> {x}" |
|
498 |
with y L show ?thesis by blast |
|
499 |
qed |
|
23350 | 500 |
qed (rule Lower_closed [THEN subsetD, OF y]) |
14693 | 501 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
502 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
503 |
from greatest_i show "i \<in> carrier L" by simp |
14551 | 504 |
qed |
505 |
next |
|
506 |
fix g |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
507 |
assume greatest_g: "greatest L g (Lower L (insert x A))" |
14551 | 508 |
show "g = i" |
509 |
proof (rule greatest_unique) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
510 |
show "greatest L i (Lower L (insert x A))" |
14551 | 511 |
proof (rule greatest_LowerI) |
14693 | 512 |
fix z |
513 |
assume "z \<in> insert x A" |
|
514 |
then show "i \<sqsubseteq> z" |
|
515 |
proof |
|
516 |
assume "z = x" then show ?thesis |
|
517 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
518 |
next |
|
519 |
assume "z \<in> A" |
|
520 |
with L greatest_i greatest_a show ?thesis |
|
521 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
522 |
qed |
|
14551 | 523 |
next |
14693 | 524 |
fix y |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
525 |
assume y: "y \<in> Lower L (insert x A)" |
14693 | 526 |
show "y \<sqsubseteq> i" |
527 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
528 |
fix z |
|
529 |
assume z: "z \<in> {a, x}" |
|
530 |
then show "y \<sqsubseteq> z" |
|
531 |
proof |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
532 |
have y': "y \<in> Lower L A" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
533 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
23463 | 534 |
apply (rule Lower_antimono) |
535 |
apply blast |
|
536 |
apply (rule y) |
|
14693 | 537 |
done |
538 |
assume "z = a" |
|
539 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
540 |
next |
|
541 |
assume "z \<in> {x}" |
|
542 |
with y L show ?thesis by blast |
|
14551 | 543 |
qed |
23350 | 544 |
qed (rule Lower_closed [THEN subsetD, OF y]) |
14551 | 545 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
546 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
547 |
from greatest_i show "i \<in> carrier L" by simp |
14551 | 548 |
qed |
23350 | 549 |
qed (rule greatest_g) |
550 |
qed (rule P) |
|
14551 | 551 |
qed |
552 |
||
553 |
lemma (in lattice) finite_inf_greatest: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
554 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" |
22265 | 555 |
proof (induct set: finite) |
14551 | 556 |
case empty then show ?case by simp |
557 |
next |
|
15328 | 558 |
case (insert x A) |
14551 | 559 |
show ?case |
560 |
proof (cases "A = {}") |
|
561 |
case True |
|
562 |
with insert show ?thesis by (simp add: inf_of_singletonI) |
|
563 |
next |
|
564 |
case False |
|
565 |
from insert show ?thesis |
|
566 |
proof (rule_tac inf_insertI) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
567 |
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
14551 | 568 |
qed simp_all |
569 |
qed |
|
570 |
qed |
|
571 |
||
572 |
lemma (in lattice) finite_inf_insertI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
573 |
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
|
574 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 575 |
shows "P (\<Sqinter> (insert x A))" |
576 |
proof (cases "A = {}") |
|
577 |
case True with P and xA show ?thesis |
|
578 |
by (simp add: inf_of_singletonI) |
|
579 |
next |
|
580 |
case False with P and xA show ?thesis |
|
581 |
by (simp add: inf_insertI finite_inf_greatest) |
|
582 |
qed |
|
583 |
||
584 |
lemma (in lattice) finite_inf_closed: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
585 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
22265 | 586 |
proof (induct set: finite) |
14551 | 587 |
case empty then show ?case by simp |
588 |
next |
|
15328 | 589 |
case insert then show ?case |
14551 | 590 |
by (rule_tac finite_inf_insertI) (simp_all) |
591 |
qed |
|
592 |
||
593 |
lemma (in lattice) meet_left: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
594 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
14693 | 595 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 596 |
|
597 |
lemma (in lattice) meet_right: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
598 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
14693 | 599 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 600 |
|
601 |
lemma (in lattice) inf_of_two_greatest: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
602 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
603 |
greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
14551 | 604 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
605 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
606 |
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
14551 | 607 |
with L |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
608 |
show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
14551 | 609 |
by (fast intro: theI2 greatest_unique) (* blast fails *) |
610 |
qed |
|
611 |
||
612 |
lemma (in lattice) meet_le: |
|
14693 | 613 |
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
23350 | 614 |
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" |
14551 | 615 |
shows "z \<sqsubseteq> x \<sqinter> y" |
23350 | 616 |
proof (rule meetI [OF _ x y]) |
14551 | 617 |
fix i |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
618 |
assume "greatest L i (Lower L {x, y})" |
23350 | 619 |
with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
14551 | 620 |
qed |
14693 | 621 |
|
14551 | 622 |
lemma (in lattice) meet_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
623 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14693 | 624 |
shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
14551 | 625 |
proof (rule finite_inf_insertI) |
626 |
txt {* The textbook argument in Jacobson I, p 457 *} |
|
627 |
fix i |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
628 |
assume inf: "greatest L i (Lower L {x, y, z})" |
14551 | 629 |
show "x \<sqinter> (y \<sqinter> z) = i" |
630 |
proof (rule anti_sym) |
|
631 |
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
632 |
by (fastsimp intro!: meet_le elim: greatest_Lower_above) |
|
633 |
next |
|
634 |
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" |
|
635 |
by (erule_tac greatest_le) |
|
636 |
(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
|
637 |
qed (simp_all add: L greatest_carrier [OF inf]) |
14551 | 638 |
qed (simp_all add: L) |
639 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
640 |
lemma meet_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
641 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
642 |
shows "x \<sqinter> y = y \<sqinter> x" |
14551 | 643 |
by (unfold meet_def) (simp add: insert_commute) |
644 |
||
645 |
lemma (in lattice) meet_assoc: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
646 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 647 |
shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
648 |
proof - |
|
649 |
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) |
|
650 |
also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) |
|
651 |
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) |
|
652 |
also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) |
|
653 |
finally show ?thesis . |
|
654 |
qed |
|
655 |
||
14693 | 656 |
|
14551 | 657 |
subsection {* Total Orders *} |
658 |
||
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
659 |
locale total_order = partial_order + |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
660 |
assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
14551 | 661 |
|
662 |
text {* Introduction rule: the usual definition of total order *} |
|
663 |
||
664 |
lemma (in partial_order) total_orderI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
665 |
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
|
666 |
shows "total_order L" |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
667 |
by unfold_locales (rule total) |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
668 |
|
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
669 |
text {* Total orders are lattices. *} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
670 |
|
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
671 |
interpretation total_order < lattice |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
672 |
proof unfold_locales |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
673 |
fix x y |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
674 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
675 |
show "EX s. least L s (Upper L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
676 |
proof - |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
677 |
note total L |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
678 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
679 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
680 |
assume "x \<sqsubseteq> y" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
681 |
with L have "least L y (Upper L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
682 |
by (rule_tac least_UpperI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
683 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
684 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
685 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
686 |
assume "y \<sqsubseteq> x" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
687 |
with L have "least L x (Upper L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
688 |
by (rule_tac least_UpperI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
689 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
690 |
ultimately show ?thesis by blast |
14551 | 691 |
qed |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
692 |
next |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
693 |
fix x y |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
694 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
695 |
show "EX i. greatest L i (Lower L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
696 |
proof - |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
697 |
note total L |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
698 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
699 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
700 |
assume "y \<sqsubseteq> x" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
701 |
with L have "greatest L y (Lower L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
702 |
by (rule_tac greatest_LowerI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
703 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
704 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
705 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
706 |
assume "x \<sqsubseteq> y" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
707 |
with L have "greatest L x (Lower L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
708 |
by (rule_tac greatest_LowerI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
709 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
710 |
ultimately show ?thesis by blast |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
711 |
qed |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
712 |
qed |
14551 | 713 |
|
14693 | 714 |
|
14551 | 715 |
subsection {* Complete lattices *} |
716 |
||
717 |
locale complete_lattice = lattice + |
|
718 |
assumes sup_exists: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
719 |
"[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
14551 | 720 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
721 |
"[| 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
|
722 |
|
14551 | 723 |
text {* Introduction rule: the usual definition of complete lattice *} |
724 |
||
725 |
lemma (in partial_order) complete_latticeI: |
|
726 |
assumes sup_exists: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
727 |
"!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
14551 | 728 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
729 |
"!!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
|
730 |
shows "complete_lattice L" |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
731 |
proof intro_locales |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
732 |
show "lattice_axioms L" |
14693 | 733 |
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
23463 | 734 |
qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+ |
14551 | 735 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
736 |
constdefs (structure L) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
737 |
top :: "_ => 'a" ("\<top>\<index>") |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
738 |
"\<top> == sup L (carrier L)" |
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset
|
739 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
740 |
bottom :: "_ => 'a" ("\<bottom>\<index>") |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
741 |
"\<bottom> == inf L (carrier L)" |
14551 | 742 |
|
743 |
||
744 |
lemma (in complete_lattice) supI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
745 |
"[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] |
14651 | 746 |
==> P (\<Squnion>A)" |
14551 | 747 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
748 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
749 |
and P: "!!l. least L l (Upper L A) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
750 |
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
|
751 |
with L show "P (THE l. least L l (Upper L A))" |
14551 | 752 |
by (fast intro: theI2 least_unique P) |
753 |
qed |
|
754 |
||
755 |
lemma (in complete_lattice) sup_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
756 |
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" |
14551 | 757 |
by (rule supI) simp_all |
758 |
||
759 |
lemma (in complete_lattice) top_closed [simp, intro]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
760 |
"\<top> \<in> carrier L" |
14551 | 761 |
by (unfold top_def) simp |
762 |
||
763 |
lemma (in complete_lattice) infI: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
764 |
"[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] |
14693 | 765 |
==> P (\<Sqinter>A)" |
14551 | 766 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
767 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
768 |
and P: "!!l. greatest L l (Lower L A) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
769 |
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
|
770 |
with L show "P (THE l. greatest L l (Lower L A))" |
14551 | 771 |
by (fast intro: theI2 greatest_unique P) |
772 |
qed |
|
773 |
||
774 |
lemma (in complete_lattice) inf_closed [simp]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
775 |
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" |
14551 | 776 |
by (rule infI) simp_all |
777 |
||
778 |
lemma (in complete_lattice) bottom_closed [simp, intro]: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
779 |
"\<bottom> \<in> carrier L" |
14551 | 780 |
by (unfold bottom_def) simp |
781 |
||
782 |
text {* Jacobson: Theorem 8.1 *} |
|
783 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
784 |
lemma Lower_empty [simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
785 |
"Lower L {} = carrier L" |
14551 | 786 |
by (unfold Lower_def) simp |
787 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
788 |
lemma Upper_empty [simp]: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
789 |
"Upper L {} = carrier L" |
14551 | 790 |
by (unfold Upper_def) simp |
791 |
||
792 |
theorem (in partial_order) complete_lattice_criterion1: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
793 |
assumes top_exists: "EX g. greatest L g (carrier L)" |
14551 | 794 |
and inf_exists: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
795 |
"!!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
|
796 |
shows "complete_lattice L" |
14551 | 797 |
proof (rule complete_latticeI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
798 |
from top_exists obtain top where top: "greatest L top (carrier L)" .. |
14551 | 799 |
fix A |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
800 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
801 |
let ?B = "Upper L A" |
14551 | 802 |
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) |
803 |
then have B_non_empty: "?B ~= {}" by fast |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
804 |
have B_L: "?B \<subseteq> carrier L" by simp |
14551 | 805 |
from inf_exists [OF B_L B_non_empty] |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
806 |
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
807 |
have "least L b (Upper L A)" |
14551 | 808 |
apply (rule least_UpperI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
809 |
apply (rule greatest_le [where A = "Lower L ?B"]) |
14551 | 810 |
apply (rule b_inf_B) |
811 |
apply (rule Lower_memI) |
|
812 |
apply (erule UpperD) |
|
813 |
apply assumption |
|
814 |
apply (rule L) |
|
815 |
apply (fast intro: L [THEN subsetD]) |
|
816 |
apply (erule greatest_Lower_above [OF b_inf_B]) |
|
817 |
apply simp |
|
818 |
apply (rule L) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
819 |
apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) |
14551 | 820 |
done |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
821 |
then show "EX s. least L s (Upper L A)" .. |
14551 | 822 |
next |
823 |
fix A |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
824 |
assume L: "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
825 |
show "EX i. greatest L i (Lower L A)" |
14551 | 826 |
proof (cases "A = {}") |
827 |
case True then show ?thesis |
|
828 |
by (simp add: top_exists) |
|
829 |
next |
|
830 |
case False with L show ?thesis |
|
831 |
by (rule inf_exists) |
|
832 |
qed |
|
833 |
qed |
|
834 |
||
835 |
(* TODO: prove dual version *) |
|
836 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
837 |
|
14551 | 838 |
subsection {* Examples *} |
839 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset
|
840 |
subsubsection {* Powerset of a Set is a Complete Lattice *} |
14551 | 841 |
|
842 |
theorem powerset_is_complete_lattice: |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
843 |
"complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
844 |
(is "complete_lattice ?L") |
14551 | 845 |
proof (rule partial_order.complete_latticeI) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
846 |
show "partial_order ?L" |
14551 | 847 |
by (rule partial_order.intro) auto |
848 |
next |
|
849 |
fix B |
|
26805
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
850 |
assume B: "B \<subseteq> carrier ?L" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
851 |
show "EX s. least ?L s (Upper ?L B)" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
852 |
proof |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
853 |
from B show "least ?L (\<Union> B) (Upper ?L B)" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
854 |
by (fastsimp intro!: least_UpperI simp: Upper_def) |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
855 |
qed |
14551 | 856 |
next |
857 |
fix B |
|
26805
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
858 |
assume B: "B \<subseteq> carrier ?L" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
859 |
show "EX i. greatest ?L i (Lower ?L B)" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
860 |
proof |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
861 |
from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
862 |
txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
863 |
@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
864 |
by (fastsimp intro!: greatest_LowerI simp: Lower_def) |
27941d7d9a11
Replaced forward proofs of existential statements by backward proofs
berghofe
parents:
24087
diff
changeset
|
865 |
qed |
14551 | 866 |
qed |
867 |
||
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
868 |
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
|
869 |
can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
14551 | 870 |
|
14693 | 871 |
end |