306 notation Groups.one ("1") |
306 notation Groups.one ("1") |
307 |
307 |
308 |
308 |
309 subsection {* Lattice operations on finite sets *} |
309 subsection {* Lattice operations on finite sets *} |
310 |
310 |
311 text {* |
|
312 For historic reasons, there is the sublocale dependency from @{class distrib_lattice} |
|
313 to @{class linorder}. This is badly designed: both should depend on a common abstract |
|
314 distributive lattice rather than having this non-subclass dependecy between two |
|
315 classes. But for the moment we have to live with it. This forces us to setup |
|
316 this sublocale dependency simultaneously with the lattice operations on finite |
|
317 sets, to avoid garbage. |
|
318 *} |
|
319 |
|
320 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
311 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
321 where |
312 where |
322 "Inf_fin = semilattice_set.F inf" |
313 "Inf_fin = semilattice_set.F inf" |
323 |
314 |
324 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
315 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
325 where |
316 where |
326 "Sup_fin = semilattice_set.F sup" |
317 "Sup_fin = semilattice_set.F sup" |
327 |
|
328 context linorder |
|
329 begin |
|
330 |
|
331 definition Min :: "'a set \<Rightarrow> 'a" |
|
332 where |
|
333 "Min = semilattice_set.F min" |
|
334 |
|
335 definition Max :: "'a set \<Rightarrow> 'a" |
|
336 where |
|
337 "Max = semilattice_set.F max" |
|
338 |
|
339 sublocale Min!: semilattice_order_set min less_eq less |
|
340 + Max!: semilattice_order_set max greater_eq greater |
|
341 where |
|
342 "semilattice_set.F min = Min" |
|
343 and "semilattice_set.F max = Max" |
|
344 proof - |
|
345 show "semilattice_order_set min less_eq less" by default (auto simp add: min_def) |
|
346 then interpret Min!: semilattice_order_set min less_eq less . |
|
347 show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def) |
|
348 then interpret Max!: semilattice_order_set max greater_eq greater . |
|
349 from Min_def show "semilattice_set.F min = Min" by rule |
|
350 from Max_def show "semilattice_set.F max = Max" by rule |
|
351 qed |
|
352 |
|
353 |
|
354 text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *} |
|
355 |
|
356 sublocale min_max!: distrib_lattice min less_eq less max |
|
357 where |
|
358 "semilattice_inf.Inf_fin min = Min" |
|
359 and "semilattice_sup.Sup_fin max = Max" |
|
360 proof - |
|
361 show "class.distrib_lattice min less_eq less max" |
|
362 proof |
|
363 fix x y z |
|
364 show "max x (min y z) = min (max x y) (max x z)" |
|
365 by (auto simp add: min_def max_def) |
|
366 qed (auto simp add: min_def max_def not_le less_imp_le) |
|
367 then interpret min_max!: distrib_lattice min less_eq less max . |
|
368 show "semilattice_inf.Inf_fin min = Min" |
|
369 by (simp only: min_max.Inf_fin_def Min_def) |
|
370 show "semilattice_sup.Sup_fin max = Max" |
|
371 by (simp only: min_max.Sup_fin_def Max_def) |
|
372 qed |
|
373 |
|
374 lemmas le_maxI1 = max.cobounded1 |
|
375 lemmas le_maxI2 = max.cobounded2 |
|
376 lemmas min_ac = min.assoc min.commute min.left_commute |
|
377 lemmas max_ac = max.assoc max.commute max.left_commute |
|
378 |
|
379 end |
|
380 |
|
381 |
|
382 text {* Lattice operations proper *} |
|
383 |
318 |
384 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less |
319 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less |
385 where |
320 where |
386 "semilattice_set.F inf = Inf_fin" |
321 "semilattice_set.F inf = Inf_fin" |
387 proof - |
322 proof - |
396 proof - |
331 proof - |
397 show "semilattice_order_set sup greater_eq greater" .. |
332 show "semilattice_order_set sup greater_eq greater" .. |
398 then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . |
333 then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . |
399 from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule |
334 from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule |
400 qed |
335 qed |
401 |
|
402 |
|
403 text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *} |
|
404 |
|
405 lemma Inf_fin_Min: |
|
406 "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" |
|
407 by (simp add: Inf_fin_def Min_def inf_min) |
|
408 |
|
409 lemma Sup_fin_Max: |
|
410 "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)" |
|
411 by (simp add: Sup_fin_def Max_def sup_max) |
|
412 |
|
413 |
336 |
414 |
337 |
415 subsection {* Infimum and Supremum over non-empty sets *} |
338 subsection {* Infimum and Supremum over non-empty sets *} |
416 |
339 |
417 text {* |
340 text {* |
544 |
467 |
545 end |
468 end |
546 |
469 |
547 |
470 |
548 subsection {* Minimum and Maximum over non-empty sets *} |
471 subsection {* Minimum and Maximum over non-empty sets *} |
|
472 |
|
473 context linorder |
|
474 begin |
|
475 |
|
476 definition Min :: "'a set \<Rightarrow> 'a" |
|
477 where |
|
478 "Min = semilattice_set.F min" |
|
479 |
|
480 definition Max :: "'a set \<Rightarrow> 'a" |
|
481 where |
|
482 "Max = semilattice_set.F max" |
|
483 |
|
484 sublocale Min!: semilattice_order_set min less_eq less |
|
485 + Max!: semilattice_order_set max greater_eq greater |
|
486 where |
|
487 "semilattice_set.F min = Min" |
|
488 and "semilattice_set.F max = Max" |
|
489 proof - |
|
490 show "semilattice_order_set min less_eq less" by default (auto simp add: min_def) |
|
491 then interpret Min!: semilattice_order_set min less_eq less . |
|
492 show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def) |
|
493 then interpret Max!: semilattice_order_set max greater_eq greater . |
|
494 from Min_def show "semilattice_set.F min = Min" by rule |
|
495 from Max_def show "semilattice_set.F max = Max" by rule |
|
496 qed |
|
497 |
|
498 end |
|
499 |
|
500 text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *} |
|
501 |
|
502 lemma Inf_fin_Min: |
|
503 "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" |
|
504 by (simp add: Inf_fin_def Min_def inf_min) |
|
505 |
|
506 lemma Sup_fin_Max: |
|
507 "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)" |
|
508 by (simp add: Sup_fin_def Max_def sup_max) |
549 |
509 |
550 context linorder |
510 context linorder |
551 begin |
511 begin |
552 |
512 |
553 lemma dual_min: |
513 lemma dual_min: |