19 locale semilattice = abel_semigroup + |
19 locale semilattice = abel_semigroup + |
20 assumes idem [simp]: "a \<^bold>* a = a" |
20 assumes idem [simp]: "a \<^bold>* a = a" |
21 begin |
21 begin |
22 |
22 |
23 lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" |
23 lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" |
24 by (simp add: assoc [symmetric]) |
24 by (simp add: assoc [symmetric]) |
25 |
25 |
26 lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" |
26 lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" |
27 by (simp add: assoc) |
27 by (simp add: assoc) |
28 |
28 |
29 end |
29 end |
30 |
30 |
31 locale semilattice_neutr = semilattice + comm_monoid |
31 locale semilattice_neutr = semilattice + comm_monoid |
32 |
32 |
33 locale semilattice_order = semilattice + |
33 locale semilattice_order = semilattice + |
34 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) |
34 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) |
35 and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50) |
35 and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50) |
36 assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b" |
36 assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b" |
37 and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b" |
37 and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b" |
38 begin |
38 begin |
39 |
39 |
40 lemma orderI: |
40 lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b" |
41 "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b" |
|
42 by (simp add: order_iff) |
41 by (simp add: order_iff) |
43 |
42 |
44 lemma orderE: |
43 lemma orderE: |
45 assumes "a \<^bold>\<le> b" |
44 assumes "a \<^bold>\<le> b" |
46 obtains "a = a \<^bold>* b" |
45 obtains "a = a \<^bold>* b" |
47 using assms by (unfold order_iff) |
46 using assms by (unfold order_iff) |
48 |
47 |
49 sublocale ordering less_eq less |
48 sublocale ordering less_eq less |
50 proof |
49 proof |
51 fix a b |
50 fix a b |
52 show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" |
51 show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b |
53 by (simp add: order_iff strict_order_iff) |
52 by (simp add: order_iff strict_order_iff) |
54 next |
53 next |
55 fix a |
54 fix a |
56 show "a \<^bold>\<le> a" |
55 show "a \<^bold>\<le> a" |
57 by (simp add: order_iff) |
56 by (simp add: order_iff) |
188 subsubsection \<open>Intro and elim rules\<close> |
179 subsubsection \<open>Intro and elim rules\<close> |
189 |
180 |
190 context semilattice_inf |
181 context semilattice_inf |
191 begin |
182 begin |
192 |
183 |
193 lemma le_infI1: |
184 lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
194 "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
|
195 by (rule order_trans) auto |
185 by (rule order_trans) auto |
196 |
186 |
197 lemma le_infI2: |
187 lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
198 "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
|
199 by (rule order_trans) auto |
188 by (rule order_trans) auto |
200 |
189 |
201 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
190 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
202 by (fact inf_greatest) (* FIXME: duplicate lemma *) |
191 by (fact inf_greatest) (* FIXME: duplicate lemma *) |
203 |
192 |
204 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
193 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
205 by (blast intro: order_trans inf_le1 inf_le2) |
194 by (blast intro: order_trans inf_le1 inf_le2) |
206 |
195 |
207 lemma le_inf_iff: |
196 lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
208 "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
|
209 by (blast intro: le_infI elim: le_infE) |
197 by (blast intro: le_infI elim: le_infE) |
210 |
198 |
211 lemma le_iff_inf: |
199 lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
212 "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
|
213 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) |
200 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) |
214 |
201 |
215 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" |
202 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" |
216 by (fast intro: inf_greatest le_infI1 le_infI2) |
203 by (fast intro: inf_greatest le_infI1 le_infI2) |
217 |
204 |
218 lemma mono_inf: |
205 lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf" |
219 fixes f :: "'a \<Rightarrow> 'b::semilattice_inf" |
|
220 shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" |
|
221 by (auto simp add: mono_def intro: Lattices.inf_greatest) |
206 by (auto simp add: mono_def intro: Lattices.inf_greatest) |
222 |
207 |
223 end |
208 end |
224 |
209 |
225 context semilattice_sup |
210 context semilattice_sup |
226 begin |
211 begin |
227 |
212 |
228 lemma le_supI1: |
213 lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
229 "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
|
230 by (rule order_trans) auto |
214 by (rule order_trans) auto |
231 |
215 |
232 lemma le_supI2: |
216 lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
233 "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
217 by (rule order_trans) auto |
234 by (rule order_trans) auto |
218 |
235 |
219 lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
236 lemma le_supI: |
|
237 "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
|
238 by (fact sup_least) (* FIXME: duplicate lemma *) |
220 by (fact sup_least) (* FIXME: duplicate lemma *) |
239 |
221 |
240 lemma le_supE: |
222 lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
241 "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
|
242 by (blast intro: order_trans sup_ge1 sup_ge2) |
223 by (blast intro: order_trans sup_ge1 sup_ge2) |
243 |
224 |
244 lemma le_sup_iff: |
225 lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
245 "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
246 by (blast intro: le_supI elim: le_supE) |
226 by (blast intro: le_supI elim: le_supE) |
247 |
227 |
248 lemma le_iff_sup: |
228 lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
249 "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
|
250 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) |
229 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) |
251 |
230 |
252 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" |
231 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" |
253 by (fast intro: sup_least le_supI1 le_supI2) |
232 by (fast intro: sup_least le_supI1 le_supI2) |
254 |
233 |
255 lemma mono_sup: |
234 lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup" |
256 fixes f :: "'a \<Rightarrow> 'b::semilattice_sup" |
|
257 shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" |
|
258 by (auto simp add: mono_def intro: Lattices.sup_least) |
235 by (auto simp add: mono_def intro: Lattices.sup_least) |
259 |
236 |
260 end |
237 end |
261 |
238 |
262 |
239 |
373 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
349 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
374 |
350 |
375 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" |
351 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" |
376 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
352 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
377 |
353 |
378 text\<open>If you have one of them, you have them all.\<close> |
354 text \<open>If you have one of them, you have them all.\<close> |
379 |
355 |
380 lemma distrib_imp1: |
356 lemma distrib_imp1: |
381 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
357 assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
382 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
358 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
383 proof- |
359 proof- |
384 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp |
360 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" |
|
361 by simp |
385 also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
362 also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
386 by (simp add: D inf_commute sup_assoc del: sup_inf_absorb) |
363 by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) |
387 also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
364 also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
388 by(simp add: inf_commute) |
365 by (simp add: inf_commute) |
389 also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
366 also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib) |
390 finally show ?thesis . |
367 finally show ?thesis . |
391 qed |
368 qed |
392 |
369 |
393 lemma distrib_imp2: |
370 lemma distrib_imp2: |
394 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
371 assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
395 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
372 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
396 proof- |
373 proof- |
397 have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp |
374 have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" |
|
375 by simp |
398 also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
376 also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
399 by (simp add: D sup_commute inf_assoc del: inf_sup_absorb) |
377 by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) |
400 also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
378 also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
401 by(simp add: sup_commute) |
379 by (simp add: sup_commute) |
402 also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
380 also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib) |
403 finally show ?thesis . |
381 finally show ?thesis . |
404 qed |
382 qed |
405 |
383 |
406 end |
384 end |
407 |
385 |
|
386 |
408 subsubsection \<open>Strict order\<close> |
387 subsubsection \<open>Strict order\<close> |
409 |
388 |
410 context semilattice_inf |
389 context semilattice_inf |
411 begin |
390 begin |
412 |
391 |
413 lemma less_infI1: |
392 lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
414 "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
|
415 by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
393 by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
416 |
394 |
417 lemma less_infI2: |
395 lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
418 "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
|
419 by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
396 by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
420 |
397 |
421 end |
398 end |
422 |
399 |
423 context semilattice_sup |
400 context semilattice_sup |
424 begin |
401 begin |
425 |
402 |
426 lemma less_supI1: |
403 lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
427 "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
|
428 using dual_semilattice |
404 using dual_semilattice |
429 by (rule semilattice_inf.less_infI1) |
405 by (rule semilattice_inf.less_infI1) |
430 |
406 |
431 lemma less_supI2: |
407 lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
432 "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
|
433 using dual_semilattice |
408 using dual_semilattice |
434 by (rule semilattice_inf.less_infI2) |
409 by (rule semilattice_inf.less_infI2) |
435 |
410 |
436 end |
411 end |
437 |
412 |
492 begin |
459 begin |
493 |
460 |
494 sublocale sup_bot: semilattice_neutr sup bot |
461 sublocale sup_bot: semilattice_neutr sup bot |
495 + sup_bot: semilattice_neutr_order sup bot greater_eq greater |
462 + sup_bot: semilattice_neutr_order sup bot greater_eq greater |
496 proof |
463 proof |
497 fix x |
464 show "x \<squnion> \<bottom> = x" for x |
498 show "x \<squnion> \<bottom> = x" |
|
499 by (rule sup_absorb1) simp |
465 by (rule sup_absorb1) simp |
500 qed |
466 qed |
501 |
467 |
502 end |
468 end |
503 |
469 |
504 class bounded_lattice_bot = lattice + order_bot |
470 class bounded_lattice_bot = lattice + order_bot |
505 begin |
471 begin |
506 |
472 |
507 subclass bounded_semilattice_sup_bot .. |
473 subclass bounded_semilattice_sup_bot .. |
508 |
474 |
509 lemma inf_bot_left [simp]: |
475 lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>" |
510 "\<bottom> \<sqinter> x = \<bottom>" |
|
511 by (rule inf_absorb1) simp |
476 by (rule inf_absorb1) simp |
512 |
477 |
513 lemma inf_bot_right [simp]: |
478 lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>" |
514 "x \<sqinter> \<bottom> = \<bottom>" |
|
515 by (rule inf_absorb2) simp |
479 by (rule inf_absorb2) simp |
516 |
480 |
517 lemma sup_bot_left: |
481 lemma sup_bot_left: "\<bottom> \<squnion> x = x" |
518 "\<bottom> \<squnion> x = x" |
|
519 by (fact sup_bot.left_neutral) |
482 by (fact sup_bot.left_neutral) |
520 |
483 |
521 lemma sup_bot_right: |
484 lemma sup_bot_right: "x \<squnion> \<bottom> = x" |
522 "x \<squnion> \<bottom> = x" |
|
523 by (fact sup_bot.right_neutral) |
485 by (fact sup_bot.right_neutral) |
524 |
486 |
525 lemma sup_eq_bot_iff [simp]: |
487 lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
526 "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
527 by (simp add: eq_iff) |
488 by (simp add: eq_iff) |
528 |
489 |
529 lemma bot_eq_sup_iff [simp]: |
490 lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
530 "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
531 by (simp add: eq_iff) |
491 by (simp add: eq_iff) |
532 |
492 |
533 end |
493 end |
534 |
494 |
535 class bounded_lattice_top = lattice + order_top |
495 class bounded_lattice_top = lattice + order_top |
536 begin |
496 begin |
537 |
497 |
538 subclass bounded_semilattice_inf_top .. |
498 subclass bounded_semilattice_inf_top .. |
539 |
499 |
540 lemma sup_top_left [simp]: |
500 lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>" |
541 "\<top> \<squnion> x = \<top>" |
|
542 by (rule sup_absorb1) simp |
501 by (rule sup_absorb1) simp |
543 |
502 |
544 lemma sup_top_right [simp]: |
503 lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>" |
545 "x \<squnion> \<top> = \<top>" |
|
546 by (rule sup_absorb2) simp |
504 by (rule sup_absorb2) simp |
547 |
505 |
548 lemma inf_top_left: |
506 lemma inf_top_left: "\<top> \<sqinter> x = x" |
549 "\<top> \<sqinter> x = x" |
|
550 by (fact inf_top.left_neutral) |
507 by (fact inf_top.left_neutral) |
551 |
508 |
552 lemma inf_top_right: |
509 lemma inf_top_right: "x \<sqinter> \<top> = x" |
553 "x \<sqinter> \<top> = x" |
|
554 by (fact inf_top.right_neutral) |
510 by (fact inf_top.right_neutral) |
555 |
511 |
556 lemma inf_eq_top_iff [simp]: |
512 lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
557 "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
558 by (simp add: eq_iff) |
513 by (simp add: eq_iff) |
559 |
514 |
560 end |
515 end |
561 |
516 |
562 class bounded_lattice = lattice + order_bot + order_top |
517 class bounded_lattice = lattice + order_bot + order_top |
563 begin |
518 begin |
564 |
519 |
565 subclass bounded_lattice_bot .. |
520 subclass bounded_lattice_bot .. |
566 subclass bounded_lattice_top .. |
521 subclass bounded_lattice_top .. |
567 |
522 |
568 lemma dual_bounded_lattice: |
523 lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>" |
569 "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>" |
|
570 by unfold_locales (auto simp add: less_le_not_le) |
524 by unfold_locales (auto simp add: less_le_not_le) |
571 |
525 |
572 end |
526 end |
573 |
527 |
574 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + |
528 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + |
604 then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" |
556 then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" |
605 using sup_compl_top assms(2) by simp |
557 using sup_compl_top assms(2) by simp |
606 then show "- x = y" by simp |
558 then show "- x = y" by simp |
607 qed |
559 qed |
608 |
560 |
609 lemma double_compl [simp]: |
561 lemma double_compl [simp]: "- (- x) = x" |
610 "- (- x) = x" |
|
611 using compl_inf_bot compl_sup_top by (rule compl_unique) |
562 using compl_inf_bot compl_sup_top by (rule compl_unique) |
612 |
563 |
613 lemma compl_eq_compl_iff [simp]: |
564 lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y" |
614 "- x = - y \<longleftrightarrow> x = y" |
|
615 proof |
565 proof |
616 assume "- x = - y" |
566 assume "- x = - y" |
617 then have "- (- x) = - (- y)" by (rule arg_cong) |
567 then have "- (- x) = - (- y)" by (rule arg_cong) |
618 then show "x = y" by simp |
568 then show "x = y" by simp |
619 next |
569 next |
620 assume "x = y" |
570 assume "x = y" |
621 then show "- x = - y" by simp |
571 then show "- x = - y" by simp |
622 qed |
572 qed |
623 |
573 |
624 lemma compl_bot_eq [simp]: |
574 lemma compl_bot_eq [simp]: "- \<bottom> = \<top>" |
625 "- \<bottom> = \<top>" |
|
626 proof - |
575 proof - |
627 from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . |
576 from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . |
628 then show ?thesis by simp |
577 then show ?thesis by simp |
629 qed |
578 qed |
630 |
579 |
631 lemma compl_top_eq [simp]: |
580 lemma compl_top_eq [simp]: "- \<top> = \<bottom>" |
632 "- \<top> = \<bottom>" |
|
633 proof - |
581 proof - |
634 from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . |
582 from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . |
635 then show ?thesis by simp |
583 then show ?thesis by simp |
636 qed |
584 qed |
637 |
585 |
638 lemma compl_inf [simp]: |
586 lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y" |
639 "- (x \<sqinter> y) = - x \<squnion> - y" |
|
640 proof (rule compl_unique) |
587 proof (rule compl_unique) |
641 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
588 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
642 by (simp only: inf_sup_distrib inf_aci) |
589 by (simp only: inf_sup_distrib inf_aci) |
643 then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
590 then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
644 by (simp add: inf_compl_bot) |
591 by (simp add: inf_compl_bot) |
647 by (simp only: sup_inf_distrib sup_aci) |
594 by (simp only: sup_inf_distrib sup_aci) |
648 then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
595 then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
649 by (simp add: sup_compl_top) |
596 by (simp add: sup_compl_top) |
650 qed |
597 qed |
651 |
598 |
652 lemma compl_sup [simp]: |
599 lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y" |
653 "- (x \<squnion> y) = - x \<sqinter> - y" |
|
654 using dual_boolean_algebra |
600 using dual_boolean_algebra |
655 by (rule boolean_algebra.compl_inf) |
601 by (rule boolean_algebra.compl_inf) |
656 |
602 |
657 lemma compl_mono: |
603 lemma compl_mono: |
658 "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x" |
604 assumes "x \<sqsubseteq> y" |
|
605 shows "- y \<sqsubseteq> - x" |
659 proof - |
606 proof - |
660 assume "x \<sqsubseteq> y" |
607 from assms have "x \<squnion> y = y" by (simp only: le_iff_sup) |
661 then have "x \<squnion> y = y" by (simp only: le_iff_sup) |
|
662 then have "- (x \<squnion> y) = - y" by simp |
608 then have "- (x \<squnion> y) = - y" by simp |
663 then have "- x \<sqinter> - y = - y" by simp |
609 then have "- x \<sqinter> - y = - y" by simp |
664 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
610 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
665 then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf) |
611 then show ?thesis by (simp only: le_iff_inf) |
666 qed |
612 qed |
667 |
613 |
668 lemma compl_le_compl_iff [simp]: |
614 lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x" |
669 "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x" |
|
670 by (auto dest: compl_mono) |
615 by (auto dest: compl_mono) |
671 |
616 |
672 lemma compl_le_swap1: |
617 lemma compl_le_swap1: |
673 assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y" |
618 assumes "y \<sqsubseteq> - x" |
|
619 shows "x \<sqsubseteq> -y" |
674 proof - |
620 proof - |
675 from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff) |
621 from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff) |
676 then show ?thesis by simp |
622 then show ?thesis by simp |
677 qed |
623 qed |
678 |
624 |
679 lemma compl_le_swap2: |
625 lemma compl_le_swap2: |
680 assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y" |
626 assumes "- y \<sqsubseteq> x" |
|
627 shows "- x \<sqsubseteq> y" |
681 proof - |
628 proof - |
682 from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff) |
629 from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff) |
683 then show ?thesis by simp |
630 then show ?thesis by simp |
684 qed |
631 qed |
685 |
632 |
686 lemma compl_less_compl_iff: (* TODO: declare [simp] ? *) |
633 lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x" (* TODO: declare [simp] ? *) |
687 "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x" |
|
688 by (auto simp add: less_le) |
634 by (auto simp add: less_le) |
689 |
635 |
690 lemma compl_less_swap1: |
636 lemma compl_less_swap1: |
691 assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y" |
637 assumes "y \<sqsubset> - x" |
|
638 shows "x \<sqsubset> - y" |
692 proof - |
639 proof - |
693 from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff) |
640 from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff) |
694 then show ?thesis by simp |
641 then show ?thesis by simp |
695 qed |
642 qed |
696 |
643 |
697 lemma compl_less_swap2: |
644 lemma compl_less_swap2: |
698 assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y" |
645 assumes "- y \<sqsubset> x" |
|
646 shows "- x \<sqsubset> y" |
699 proof - |
647 proof - |
700 from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff) |
648 from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff) |
701 then show ?thesis by simp |
649 then show ?thesis by simp |
702 qed |
650 qed |
703 |
651 |
704 lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" |
652 lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" |
705 by(simp add: inf_sup_aci sup_compl_top) |
653 by (simp add: inf_sup_aci sup_compl_top) |
706 |
654 |
707 lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" |
655 lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" |
708 by(simp add: inf_sup_aci sup_compl_top) |
656 by (simp add: inf_sup_aci sup_compl_top) |
709 |
657 |
710 lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" |
658 lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" |
711 by(simp add: inf_sup_aci inf_compl_bot) |
659 by (simp add: inf_sup_aci inf_compl_bot) |
712 |
660 |
713 lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" |
661 lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" |
714 by(simp add: inf_sup_aci inf_compl_bot) |
662 by (simp add: inf_sup_aci inf_compl_bot) |
715 |
663 |
716 declare inf_compl_bot [simp] sup_compl_top [simp] |
664 declare inf_compl_bot [simp] and sup_compl_top [simp] |
717 |
665 |
718 lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" |
666 lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" |
719 by(simp add: sup_assoc[symmetric]) |
667 by (simp add: sup_assoc[symmetric]) |
720 |
668 |
721 lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" |
669 lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" |
722 using sup_compl_top_left1[of "- x" y] by simp |
670 using sup_compl_top_left1[of "- x" y] by simp |
723 |
671 |
724 lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" |
672 lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" |
725 by(simp add: inf_assoc[symmetric]) |
673 by (simp add: inf_assoc[symmetric]) |
726 |
674 |
727 lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" |
675 lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" |
728 using inf_compl_bot_left1[of "- x" y] by simp |
676 using inf_compl_bot_left1[of "- x" y] by simp |
729 |
677 |
730 lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" |
678 lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" |
731 by(subst inf_left_commute) simp |
679 by (subst inf_left_commute) simp |
732 |
680 |
733 end |
681 end |
734 |
682 |
735 ML_file "Tools/boolean_algebra_cancel.ML" |
683 ML_file "Tools/boolean_algebra_cancel.ML" |
736 |
684 |
737 simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = |
685 simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = |
738 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close> |
686 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close> |
739 |
687 |
740 simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = |
688 simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = |
741 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close> |
689 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close> |
|
690 |
742 |
691 |
743 subsection \<open>\<open>min/max\<close> as special case of lattice\<close> |
692 subsection \<open>\<open>min/max\<close> as special case of lattice\<close> |
744 |
693 |
745 context linorder |
694 context linorder |
746 begin |
695 begin |
747 |
696 |
748 sublocale min: semilattice_order min less_eq less |
697 sublocale min: semilattice_order min less_eq less |
749 + max: semilattice_order max greater_eq greater |
698 + max: semilattice_order max greater_eq greater |
750 by standard (auto simp add: min_def max_def) |
699 by standard (auto simp add: min_def max_def) |
751 |
700 |
752 lemma min_le_iff_disj: |
701 lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
753 "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
|
754 unfolding min_def using linear by (auto intro: order_trans) |
702 unfolding min_def using linear by (auto intro: order_trans) |
755 |
703 |
756 lemma le_max_iff_disj: |
704 lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" |
757 "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" |
|
758 unfolding max_def using linear by (auto intro: order_trans) |
705 unfolding max_def using linear by (auto intro: order_trans) |
759 |
706 |
760 lemma min_less_iff_disj: |
707 lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z" |
761 "min x y < z \<longleftrightarrow> x < z \<or> y < z" |
|
762 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
708 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
763 |
709 |
764 lemma less_max_iff_disj: |
710 lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y" |
765 "z < max x y \<longleftrightarrow> z < x \<or> z < y" |
|
766 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
711 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
767 |
712 |
768 lemma min_less_iff_conj [simp]: |
713 lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y" |
769 "z < min x y \<longleftrightarrow> z < x \<and> z < y" |
|
770 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
714 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
771 |
715 |
772 lemma max_less_iff_conj [simp]: |
716 lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
773 "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
|
774 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
717 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
775 |
718 |
776 lemma min_max_distrib1: |
719 lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" |
777 "min (max b c) a = max (min b a) (min c a)" |
|
778 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
720 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
779 |
721 |
780 lemma min_max_distrib2: |
722 lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" |
781 "min a (max b c) = max (min a b) (min a c)" |
|
782 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
723 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
783 |
724 |
784 lemma max_min_distrib1: |
725 lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" |
785 "max (min b c) a = min (max b a) (max c a)" |
|
786 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
726 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
787 |
727 |
788 lemma max_min_distrib2: |
728 lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" |
789 "max a (min b c) = min (max a b) (max a c)" |
|
790 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
729 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
791 |
730 |
792 lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
731 lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
793 |
732 |
794 lemma split_min [no_atp]: |
733 lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
795 "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
|
796 by (simp add: min_def) |
734 by (simp add: min_def) |
797 |
735 |
798 lemma split_max [no_atp]: |
736 lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" |
799 "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" |
|
800 by (simp add: max_def) |
737 by (simp add: max_def) |
801 |
738 |
802 lemma min_of_mono: |
739 lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder" |
803 fixes f :: "'a \<Rightarrow> 'b::linorder" |
|
804 shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" |
|
805 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) |
740 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) |
806 |
741 |
807 lemma max_of_mono: |
742 lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder" |
808 fixes f :: "'a \<Rightarrow> 'b::linorder" |
|
809 shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" |
|
810 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) |
743 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) |
811 |
744 |
812 end |
745 end |
813 |
746 |
814 lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
747 lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
819 |
752 |
820 |
753 |
821 subsection \<open>Uniqueness of inf and sup\<close> |
754 subsection \<open>Uniqueness of inf and sup\<close> |
822 |
755 |
823 lemma (in semilattice_inf) inf_unique: |
756 lemma (in semilattice_inf) inf_unique: |
824 fixes f (infixl "\<triangle>" 70) |
757 fixes f (infixl "\<triangle>" 70) |
825 assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" |
758 assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" |
826 and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
759 and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" |
|
760 and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
827 shows "x \<sqinter> y = x \<triangle> y" |
761 shows "x \<sqinter> y = x \<triangle> y" |
828 proof (rule antisym) |
762 proof (rule antisym) |
829 show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) |
763 show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" |
830 next |
764 by (rule le_infI) (rule le1, rule le2) |
831 have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest) |
765 have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
832 show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all |
766 by (blast intro: greatest) |
|
767 show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" |
|
768 by (rule leI) simp_all |
833 qed |
769 qed |
834 |
770 |
835 lemma (in semilattice_sup) sup_unique: |
771 lemma (in semilattice_sup) sup_unique: |
836 fixes f (infixl "\<nabla>" 70) |
772 fixes f (infixl "\<nabla>" 70) |
837 assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" |
773 assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" |
838 and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" |
774 and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" |
|
775 and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" |
839 shows "x \<squnion> y = x \<nabla> y" |
776 shows "x \<squnion> y = x \<nabla> y" |
840 proof (rule antisym) |
777 proof (rule antisym) |
841 show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) |
778 show "x \<squnion> y \<sqsubseteq> x \<nabla> y" |
842 next |
779 by (rule le_supI) (rule ge1, rule ge2) |
843 have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least) |
780 have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" |
844 show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all |
781 by (blast intro: least) |
|
782 show "x \<nabla> y \<sqsubseteq> x \<squnion> y" |
|
783 by (rule leI) simp_all |
845 qed |
784 qed |
846 |
785 |
847 |
786 |
848 subsection \<open>Lattice on @{typ bool}\<close> |
787 subsection \<open>Lattice on @{typ bool}\<close> |
849 |
788 |
850 instantiation bool :: boolean_algebra |
789 instantiation bool :: boolean_algebra |
851 begin |
790 begin |
852 |
791 |
853 definition |
792 definition bool_Compl_def [simp]: "uminus = Not" |
854 bool_Compl_def [simp]: "uminus = Not" |
793 |
855 |
794 definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B" |
856 definition |
795 |
857 bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B" |
796 definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
858 |
797 |
859 definition |
798 definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
860 [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
799 |
861 |
800 instance by standard auto |
862 definition |
801 |
863 [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
802 end |
864 |
803 |
865 instance proof |
804 lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q" |
866 qed auto |
|
867 |
|
868 end |
|
869 |
|
870 lemma sup_boolI1: |
|
871 "P \<Longrightarrow> P \<squnion> Q" |
|
872 by simp |
805 by simp |
873 |
806 |
874 lemma sup_boolI2: |
807 lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q" |
875 "Q \<Longrightarrow> P \<squnion> Q" |
|
876 by simp |
808 by simp |
877 |
809 |
878 lemma sup_boolE: |
810 lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
879 "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
|
880 by auto |
811 by auto |
881 |
812 |
882 |
813 |
883 subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close> |
814 subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close> |
884 |
815 |
885 instantiation "fun" :: (type, semilattice_sup) semilattice_sup |
816 instantiation "fun" :: (type, semilattice_sup) semilattice_sup |
886 begin |
817 begin |
887 |
818 |
888 definition |
819 definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
889 "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
820 |
890 |
821 lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" |
891 lemma sup_apply [simp, code]: |
|
892 "(f \<squnion> g) x = f x \<squnion> g x" |
|
893 by (simp add: sup_fun_def) |
822 by (simp add: sup_fun_def) |
894 |
823 |
895 instance proof |
824 instance by standard (simp_all add: le_fun_def) |
896 qed (simp_all add: le_fun_def) |
|
897 |
825 |
898 end |
826 end |
899 |
827 |
900 instantiation "fun" :: (type, semilattice_inf) semilattice_inf |
828 instantiation "fun" :: (type, semilattice_inf) semilattice_inf |
901 begin |
829 begin |
902 |
830 |
903 definition |
831 definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
904 "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
832 |
905 |
833 lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" |
906 lemma inf_apply [simp, code]: |
|
907 "(f \<sqinter> g) x = f x \<sqinter> g x" |
|
908 by (simp add: inf_fun_def) |
834 by (simp add: inf_fun_def) |
909 |
835 |
910 instance proof |
836 instance by standard (simp_all add: le_fun_def) |
911 qed (simp_all add: le_fun_def) |
|
912 |
837 |
913 end |
838 end |
914 |
839 |
915 instance "fun" :: (type, lattice) lattice .. |
840 instance "fun" :: (type, lattice) lattice .. |
916 |
841 |
917 instance "fun" :: (type, distrib_lattice) distrib_lattice proof |
842 instance "fun" :: (type, distrib_lattice) distrib_lattice |
918 qed (rule ext, simp add: sup_inf_distrib1) |
843 by standard (rule ext, simp add: sup_inf_distrib1) |
919 |
844 |
920 instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
845 instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
921 |
846 |
922 instantiation "fun" :: (type, uminus) uminus |
847 instantiation "fun" :: (type, uminus) uminus |
923 begin |
848 begin |
924 |
849 |
925 definition |
850 definition fun_Compl_def: "- A = (\<lambda>x. - A x)" |
926 fun_Compl_def: "- A = (\<lambda>x. - A x)" |
851 |
927 |
852 lemma uminus_apply [simp, code]: "(- A) x = - (A x)" |
928 lemma uminus_apply [simp, code]: |
|
929 "(- A) x = - (A x)" |
|
930 by (simp add: fun_Compl_def) |
853 by (simp add: fun_Compl_def) |
931 |
854 |
932 instance .. |
855 instance .. |
933 |
856 |
934 end |
857 end |
935 |
858 |
936 instantiation "fun" :: (type, minus) minus |
859 instantiation "fun" :: (type, minus) minus |
937 begin |
860 begin |
938 |
861 |
939 definition |
862 definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)" |
940 fun_diff_def: "A - B = (\<lambda>x. A x - B x)" |
863 |
941 |
864 lemma minus_apply [simp, code]: "(A - B) x = A x - B x" |
942 lemma minus_apply [simp, code]: |
|
943 "(A - B) x = A x - B x" |
|
944 by (simp add: fun_diff_def) |
865 by (simp add: fun_diff_def) |
945 |
866 |
946 instance .. |
867 instance .. |
947 |
868 |
948 end |
869 end |
949 |
870 |
950 instance "fun" :: (type, boolean_algebra) boolean_algebra proof |
871 instance "fun" :: (type, boolean_algebra) boolean_algebra |
951 qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ |
872 by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ |
952 |
873 |
953 |
874 |
954 subsection \<open>Lattice on unary and binary predicates\<close> |
875 subsection \<open>Lattice on unary and binary predicates\<close> |
955 |
876 |
956 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" |
877 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" |