3 *) |
3 *) |
4 |
4 |
5 header {* Abstract lattices *} |
5 header {* Abstract lattices *} |
6 |
6 |
7 theory Lattices |
7 theory Lattices |
8 imports Orderings |
8 imports Orderings Groups |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Lattices *} |
11 subsection {* Abstract semilattice *} |
|
12 |
|
13 text {* |
|
14 This locales provide a basic structure for interpretation into |
|
15 bigger structures; extensions require careful thinking, otherwise |
|
16 undesired effects may occur due to interpretation. |
|
17 *} |
|
18 |
|
19 locale semilattice = abel_semigroup + |
|
20 assumes idem [simp]: "f a a = a" |
|
21 begin |
|
22 |
|
23 lemma left_idem [simp]: |
|
24 "f a (f a b) = f a b" |
|
25 by (simp add: assoc [symmetric]) |
|
26 |
|
27 end |
|
28 |
|
29 |
|
30 subsection {* Idempotent semigroup *} |
|
31 |
|
32 class ab_semigroup_idem_mult = ab_semigroup_mult + |
|
33 assumes mult_idem: "x * x = x" |
|
34 |
|
35 sublocale ab_semigroup_idem_mult < times!: semilattice times proof |
|
36 qed (fact mult_idem) |
|
37 |
|
38 context ab_semigroup_idem_mult |
|
39 begin |
|
40 |
|
41 lemmas mult_left_idem = times.left_idem |
|
42 |
|
43 end |
|
44 |
|
45 |
|
46 subsection {* Concrete lattices *} |
12 |
47 |
13 notation |
48 notation |
14 less_eq (infix "\<sqsubseteq>" 50) and |
49 less_eq (infix "\<sqsubseteq>" 50) and |
15 less (infix "\<sqsubset>" 50) and |
50 less (infix "\<sqsubset>" 50) and |
16 top ("\<top>") and |
51 top ("\<top>") and |
17 bot ("\<bottom>") |
52 bot ("\<bottom>") |
18 |
53 |
19 class lower_semilattice = order + |
54 class semilattice_inf = order + |
20 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
55 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
21 assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
56 assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
22 and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
57 and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
23 and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
58 and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
24 |
59 |
25 class upper_semilattice = order + |
60 class semilattice_sup = order + |
26 fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
61 fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
27 assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
62 assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
28 and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
63 and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
29 and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
64 and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
30 begin |
65 begin |
31 |
66 |
32 text {* Dual lattice *} |
67 text {* Dual lattice *} |
33 |
68 |
34 lemma dual_semilattice: |
69 lemma dual_semilattice: |
35 "lower_semilattice (op \<ge>) (op >) sup" |
70 "semilattice_inf (op \<ge>) (op >) sup" |
36 by (rule lower_semilattice.intro, rule dual_order) |
71 by (rule semilattice_inf.intro, rule dual_order) |
37 (unfold_locales, simp_all add: sup_least) |
72 (unfold_locales, simp_all add: sup_least) |
38 |
73 |
39 end |
74 end |
40 |
75 |
41 class lattice = lower_semilattice + upper_semilattice |
76 class lattice = semilattice_inf + semilattice_sup |
42 |
77 |
43 |
78 |
44 subsubsection {* Intro and elim rules*} |
79 subsubsection {* Intro and elim rules*} |
45 |
80 |
46 context lower_semilattice |
81 context semilattice_inf |
47 begin |
82 begin |
48 |
83 |
49 lemma le_infI1: |
84 lemma le_infI1: |
50 "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
85 "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
51 by (rule order_trans) auto |
86 by (rule order_trans) auto |
53 lemma le_infI2: |
88 lemma le_infI2: |
54 "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
89 "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
55 by (rule order_trans) auto |
90 by (rule order_trans) auto |
56 |
91 |
57 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
92 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
58 by (blast intro: inf_greatest) |
93 by (rule inf_greatest) (* FIXME: duplicate lemma *) |
59 |
94 |
60 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
95 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
61 by (blast intro: order_trans le_infI1 le_infI2) |
96 by (blast intro: order_trans inf_le1 inf_le2) |
62 |
97 |
63 lemma le_inf_iff [simp]: |
98 lemma le_inf_iff [simp]: |
64 "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
99 "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
65 by (blast intro: le_infI elim: le_infE) |
100 by (blast intro: le_infI elim: le_infE) |
66 |
101 |
67 lemma le_iff_inf: |
102 lemma le_iff_inf: |
68 "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
103 "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
69 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) |
104 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) |
70 |
105 |
|
106 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" |
|
107 by (fast intro: inf_greatest le_infI1 le_infI2) |
|
108 |
71 lemma mono_inf: |
109 lemma mono_inf: |
72 fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice" |
110 fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf" |
73 shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" |
111 shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" |
74 by (auto simp add: mono_def intro: Lattices.inf_greatest) |
112 by (auto simp add: mono_def intro: Lattices.inf_greatest) |
75 |
113 |
76 end |
114 end |
77 |
115 |
78 context upper_semilattice |
116 context semilattice_sup |
79 begin |
117 begin |
80 |
118 |
81 lemma le_supI1: |
119 lemma le_supI1: |
82 "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
120 "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
83 by (rule order_trans) auto |
121 by (rule order_trans) auto |
86 "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
124 "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
87 by (rule order_trans) auto |
125 by (rule order_trans) auto |
88 |
126 |
89 lemma le_supI: |
127 lemma le_supI: |
90 "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
128 "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
91 by (blast intro: sup_least) |
129 by (rule sup_least) (* FIXME: duplicate lemma *) |
92 |
130 |
93 lemma le_supE: |
131 lemma le_supE: |
94 "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
132 "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
95 by (blast intro: le_supI1 le_supI2 order_trans) |
133 by (blast intro: order_trans sup_ge1 sup_ge2) |
96 |
134 |
97 lemma le_sup_iff [simp]: |
135 lemma le_sup_iff [simp]: |
98 "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
136 "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
99 by (blast intro: le_supI elim: le_supE) |
137 by (blast intro: le_supI elim: le_supE) |
100 |
138 |
101 lemma le_iff_sup: |
139 lemma le_iff_sup: |
102 "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
140 "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
103 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) |
141 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) |
104 |
142 |
|
143 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" |
|
144 by (fast intro: sup_least le_supI1 le_supI2) |
|
145 |
105 lemma mono_sup: |
146 lemma mono_sup: |
106 fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice" |
147 fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup" |
107 shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" |
148 shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" |
108 by (auto simp add: mono_def intro: Lattices.sup_least) |
149 by (auto simp add: mono_def intro: Lattices.sup_least) |
109 |
150 |
110 end |
151 end |
111 |
152 |
112 |
153 |
113 subsubsection {* Equational laws *} |
154 subsubsection {* Equational laws *} |
114 |
155 |
115 context lower_semilattice |
156 sublocale semilattice_inf < inf!: semilattice inf |
116 begin |
157 proof |
|
158 fix a b c |
|
159 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
|
160 by (rule antisym) (auto intro: le_infI1 le_infI2) |
|
161 show "a \<sqinter> b = b \<sqinter> a" |
|
162 by (rule antisym) auto |
|
163 show "a \<sqinter> a = a" |
|
164 by (rule antisym) auto |
|
165 qed |
|
166 |
|
167 context semilattice_inf |
|
168 begin |
|
169 |
|
170 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
171 by (fact inf.assoc) |
117 |
172 |
118 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
173 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
119 by (rule antisym) auto |
174 by (fact inf.commute) |
120 |
175 |
121 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
176 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
122 by (rule antisym) (auto intro: le_infI1 le_infI2) |
177 by (fact inf.left_commute) |
123 |
178 |
124 lemma inf_idem[simp]: "x \<sqinter> x = x" |
179 lemma inf_idem: "x \<sqinter> x = x" |
125 by (rule antisym) auto |
180 by (fact inf.idem) |
126 |
181 |
127 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
182 lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
128 by (rule antisym) (auto intro: le_infI2) |
183 by (fact inf.left_idem) |
129 |
184 |
130 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
185 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
131 by (rule antisym) auto |
186 by (rule antisym) auto |
132 |
187 |
133 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
188 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
134 by (rule antisym) auto |
189 by (rule antisym) auto |
135 |
190 |
136 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
|
137 by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+ |
|
138 |
|
139 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
191 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
140 |
192 |
141 end |
193 end |
142 |
194 |
143 context upper_semilattice |
195 sublocale semilattice_sup < sup!: semilattice sup |
144 begin |
196 proof |
|
197 fix a b c |
|
198 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
|
199 by (rule antisym) (auto intro: le_supI1 le_supI2) |
|
200 show "a \<squnion> b = b \<squnion> a" |
|
201 by (rule antisym) auto |
|
202 show "a \<squnion> a = a" |
|
203 by (rule antisym) auto |
|
204 qed |
|
205 |
|
206 context semilattice_sup |
|
207 begin |
|
208 |
|
209 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
210 by (fact sup.assoc) |
145 |
211 |
146 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
212 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
147 by (rule antisym) auto |
213 by (fact sup.commute) |
148 |
214 |
149 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
215 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
150 by (rule antisym) (auto intro: le_supI1 le_supI2) |
216 by (fact sup.left_commute) |
151 |
217 |
152 lemma sup_idem[simp]: "x \<squnion> x = x" |
218 lemma sup_idem: "x \<squnion> x = x" |
153 by (rule antisym) auto |
219 by (fact sup.idem) |
154 |
220 |
155 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
221 lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
156 by (rule antisym) (auto intro: le_supI2) |
222 by (fact sup.left_idem) |
157 |
223 |
158 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
224 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
159 by (rule antisym) auto |
225 by (rule antisym) auto |
160 |
226 |
161 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
227 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
162 by (rule antisym) auto |
228 by (rule antisym) auto |
163 |
229 |
164 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
|
165 by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+ |
|
166 |
|
167 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
230 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
168 |
231 |
169 end |
232 end |
170 |
233 |
171 context lattice |
234 context lattice |
172 begin |
235 begin |
173 |
236 |
174 lemma dual_lattice: |
237 lemma dual_lattice: |
175 "lattice (op \<ge>) (op >) sup inf" |
238 "lattice (op \<ge>) (op >) sup inf" |
176 by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order) |
239 by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order) |
177 (unfold_locales, auto) |
240 (unfold_locales, auto) |
178 |
241 |
179 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" |
242 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" |
180 by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
243 by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
181 |
244 |
235 "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
298 "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
236 by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
299 by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
237 |
300 |
238 end |
301 end |
239 |
302 |
240 context upper_semilattice |
303 context semilattice_sup |
241 begin |
304 begin |
242 |
305 |
243 lemma less_supI1: |
306 lemma less_supI1: |
244 "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
307 "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
245 proof - |
308 proof - |
246 interpret dual: lower_semilattice "op \<ge>" "op >" sup |
309 interpret dual: semilattice_inf "op \<ge>" "op >" sup |
247 by (fact dual_semilattice) |
310 by (fact dual_semilattice) |
248 assume "x \<sqsubset> a" |
311 assume "x \<sqsubset> a" |
249 then show "x \<sqsubset> a \<squnion> b" |
312 then show "x \<sqsubset> a \<squnion> b" |
250 by (fact dual.less_infI1) |
313 by (fact dual.less_infI1) |
251 qed |
314 qed |
252 |
315 |
253 lemma less_supI2: |
316 lemma less_supI2: |
254 "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
317 "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
255 proof - |
318 proof - |
256 interpret dual: lower_semilattice "op \<ge>" "op >" sup |
319 interpret dual: semilattice_inf "op \<ge>" "op >" sup |
257 by (fact dual_semilattice) |
320 by (fact dual_semilattice) |
258 assume "x \<sqsubset> b" |
321 assume "x \<sqsubset> b" |
259 then show "x \<sqsubset> a \<squnion> b" |
322 then show "x \<sqsubset> a \<squnion> b" |
260 by (fact dual.less_infI2) |
323 by (fact dual.less_infI2) |
261 qed |
324 qed |
333 |
402 |
334 lemma sup_bot_right [simp]: |
403 lemma sup_bot_right [simp]: |
335 "x \<squnion> \<bottom> = x" |
404 "x \<squnion> \<bottom> = x" |
336 by (rule sup_absorb1) simp |
405 by (rule sup_absorb1) simp |
337 |
406 |
338 lemma inf_eq_top_eq1: |
407 lemma inf_eq_top_iff [simp]: |
339 assumes "A \<sqinter> B = \<top>" |
408 "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
340 shows "A = \<top>" |
409 by (simp add: eq_iff) |
341 proof (cases "B = \<top>") |
410 |
342 case True with assms show ?thesis by simp |
411 lemma sup_eq_bot_iff [simp]: |
343 next |
412 "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
344 case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans) |
413 by (simp add: eq_iff) |
345 then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2) |
|
346 with assms show ?thesis by simp |
|
347 qed |
|
348 |
|
349 lemma inf_eq_top_eq2: |
|
350 assumes "A \<sqinter> B = \<top>" |
|
351 shows "B = \<top>" |
|
352 by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms) |
|
353 |
|
354 lemma sup_eq_bot_eq1: |
|
355 assumes "A \<squnion> B = \<bottom>" |
|
356 shows "A = \<bottom>" |
|
357 proof - |
|
358 interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
|
359 by (rule dual_bounded_lattice) |
|
360 from dual.inf_eq_top_eq1 assms show ?thesis . |
|
361 qed |
|
362 |
|
363 lemma sup_eq_bot_eq2: |
|
364 assumes "A \<squnion> B = \<bottom>" |
|
365 shows "B = \<bottom>" |
|
366 proof - |
|
367 interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
|
368 by (rule dual_bounded_lattice) |
|
369 from dual.inf_eq_top_eq2 assms show ?thesis . |
|
370 qed |
|
371 |
414 |
372 end |
415 end |
373 |
416 |
374 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + |
417 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + |
375 assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>" |
418 assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>" |
439 qed |
479 qed |
440 |
480 |
441 lemma compl_inf [simp]: |
481 lemma compl_inf [simp]: |
442 "- (x \<sqinter> y) = - x \<squnion> - y" |
482 "- (x \<sqinter> y) = - x \<squnion> - y" |
443 proof (rule compl_unique) |
483 proof (rule compl_unique) |
444 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)" |
484 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
445 by (rule inf_sup_distrib1) |
485 by (simp only: inf_sup_distrib inf_aci) |
446 also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
486 then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
447 by (simp only: inf_commute inf_assoc inf_left_commute) |
|
448 finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
|
449 by (simp add: inf_compl_bot) |
487 by (simp add: inf_compl_bot) |
450 next |
488 next |
451 have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))" |
489 have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" |
452 by (rule sup_inf_distrib2) |
490 by (simp only: sup_inf_distrib sup_aci) |
453 also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" |
491 then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
454 by (simp only: sup_commute sup_assoc sup_left_commute) |
|
455 finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
|
456 by (simp add: sup_compl_top) |
492 by (simp add: sup_compl_top) |
457 qed |
493 qed |
458 |
494 |
459 lemma compl_sup [simp]: |
495 lemma compl_sup [simp]: |
460 "- (x \<squnion> y) = - x \<sqinter> - y" |
496 "- (x \<squnion> y) = - x \<sqinter> - y" |
462 interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
498 interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
463 by (rule dual_boolean_algebra) |
499 by (rule dual_boolean_algebra) |
464 then show ?thesis by simp |
500 then show ?thesis by simp |
465 qed |
501 qed |
466 |
502 |
|
503 lemma compl_mono: |
|
504 "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x" |
|
505 proof - |
|
506 assume "x \<sqsubseteq> y" |
|
507 then have "x \<squnion> y = y" by (simp only: le_iff_sup) |
|
508 then have "- (x \<squnion> y) = - y" by simp |
|
509 then have "- x \<sqinter> - y = - y" by simp |
|
510 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
|
511 then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf) |
|
512 qed |
|
513 |
|
514 lemma compl_le_compl_iff: (* TODO: declare [simp] ? *) |
|
515 "- x \<le> - y \<longleftrightarrow> y \<le> x" |
|
516 by (auto dest: compl_mono) |
|
517 |
467 end |
518 end |
468 |
519 |
469 |
520 |
470 subsection {* Uniqueness of inf and sup *} |
521 subsection {* Uniqueness of inf and sup *} |
471 |
522 |
472 lemma (in lower_semilattice) inf_unique: |
523 lemma (in semilattice_inf) inf_unique: |
473 fixes f (infixl "\<triangle>" 70) |
524 fixes f (infixl "\<triangle>" 70) |
474 assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" |
525 assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" |
475 and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
526 and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
476 shows "x \<sqinter> y = x \<triangle> y" |
527 shows "x \<sqinter> y = x \<triangle> y" |
477 proof (rule antisym) |
528 proof (rule antisym) |
479 next |
530 next |
480 have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest) |
531 have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest) |
481 show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all |
532 show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all |
482 qed |
533 qed |
483 |
534 |
484 lemma (in upper_semilattice) sup_unique: |
535 lemma (in semilattice_sup) sup_unique: |
485 fixes f (infixl "\<nabla>" 70) |
536 fixes f (infixl "\<nabla>" 70) |
486 assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" |
537 assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" |
487 and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" |
538 and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" |
488 shows "x \<squnion> y = x \<nabla> y" |
539 shows "x \<squnion> y = x \<nabla> y" |
489 proof (rule antisym) |
540 proof (rule antisym) |
490 show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) |
541 show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) |
491 next |
542 next |
492 have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least) |
543 have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least) |
493 show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all |
544 show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all |
494 qed |
545 qed |
495 |
546 |
496 |
547 |
497 subsection {* @{const min}/@{const max} on linear orders as |
548 subsection {* @{const min}/@{const max} on linear orders as |
498 special case of @{const inf}/@{const sup} *} |
549 special case of @{const inf}/@{const sup} *} |
499 |
550 |
500 sublocale linorder < min_max!: distrib_lattice less_eq less min max |
551 sublocale linorder < min_max!: distrib_lattice less_eq less min max |
502 fix x y z |
553 fix x y z |
503 show "max x (min y z) = min (max x y) (max x z)" |
554 show "max x (min y z) = min (max x y) (max x z)" |
504 by (auto simp add: min_def max_def) |
555 by (auto simp add: min_def max_def) |
505 qed (auto simp add: min_def max_def not_le less_imp_le) |
556 qed (auto simp add: min_def max_def not_le less_imp_le) |
506 |
557 |
507 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
558 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
508 by (rule ext)+ (auto intro: antisym) |
559 by (rule ext)+ (auto intro: antisym) |
509 |
560 |
510 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
561 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
511 by (rule ext)+ (auto intro: antisym) |
562 by (rule ext)+ (auto intro: antisym) |
512 |
563 |
513 lemmas le_maxI1 = min_max.sup_ge1 |
564 lemmas le_maxI1 = min_max.sup_ge1 |
514 lemmas le_maxI2 = min_max.sup_ge2 |
565 lemmas le_maxI2 = min_max.sup_ge2 |
515 |
566 |
|
567 lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
|
568 min_max.inf.left_commute |
|
569 |
516 lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
570 lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
517 mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] |
571 min_max.sup.left_commute |
518 |
572 |
519 lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
|
520 mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] |
|
521 |
573 |
522 |
574 |
523 subsection {* Bool as lattice *} |
575 subsection {* Bool as lattice *} |
524 |
576 |
525 instantiation bool :: boolean_algebra |
577 instantiation bool :: boolean_algebra |