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 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
311 context semilattice_inf |
|
312 begin |
|
313 |
|
314 definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
312 where |
315 where |
313 "Inf_fin = semilattice_set.F inf" |
316 "Inf_fin = semilattice_set.F inf" |
314 |
317 |
315 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
318 sublocale Inf_fin!: semilattice_order_set inf less_eq less |
316 where |
|
317 "Sup_fin = semilattice_set.F sup" |
|
318 |
|
319 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less |
|
320 where |
319 where |
321 "semilattice_set.F inf = Inf_fin" |
320 "semilattice_set.F inf = Inf_fin" |
322 proof - |
321 proof - |
323 show "semilattice_order_set inf less_eq less" .. |
322 show "semilattice_order_set inf less_eq less" .. |
324 then interpret Inf_fin!: semilattice_order_set inf less_eq less . |
323 then interpret Inf_fin!: semilattice_order_set inf less_eq less . |
325 from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule |
324 from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule |
326 qed |
325 qed |
327 |
326 |
328 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater |
327 end |
|
328 |
|
329 context semilattice_sup |
|
330 begin |
|
331 |
|
332 definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
|
333 where |
|
334 "Sup_fin = semilattice_set.F sup" |
|
335 |
|
336 sublocale Sup_fin!: semilattice_order_set sup greater_eq greater |
329 where |
337 where |
330 "semilattice_set.F sup = Sup_fin" |
338 "semilattice_set.F sup = Sup_fin" |
331 proof - |
339 proof - |
332 show "semilattice_order_set sup greater_eq greater" .. |
340 show "semilattice_order_set sup greater_eq greater" .. |
333 then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . |
341 then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . |
334 from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule |
342 from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule |
335 qed |
343 qed |
336 |
344 |
|
345 end |
|
346 |
337 |
347 |
338 subsection {* Infimum and Supremum over non-empty sets *} |
348 subsection {* Infimum and Supremum over non-empty sets *} |
339 |
|
340 text {* |
|
341 After this non-regular bootstrap, things continue canonically. |
|
342 *} |
|
343 |
349 |
344 context lattice |
350 context lattice |
345 begin |
351 begin |
346 |
352 |
347 lemma Inf_fin_le_Sup_fin [simp]: |
353 lemma Inf_fin_le_Sup_fin [simp]: |
447 context complete_lattice |
453 context complete_lattice |
448 begin |
454 begin |
449 |
455 |
450 lemma Inf_fin_Inf: |
456 lemma Inf_fin_Inf: |
451 assumes "finite A" and "A \<noteq> {}" |
457 assumes "finite A" and "A \<noteq> {}" |
452 shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A" |
458 shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A" |
453 proof - |
459 proof - |
454 from assms obtain b B where "A = insert b B" and "finite B" by auto |
460 from assms obtain b B where "A = insert b B" and "finite B" by auto |
455 then show ?thesis |
461 then show ?thesis |
456 by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) |
462 by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) |
457 qed |
463 qed |
458 |
464 |
459 lemma Sup_fin_Sup: |
465 lemma Sup_fin_Sup: |
460 assumes "finite A" and "A \<noteq> {}" |
466 assumes "finite A" and "A \<noteq> {}" |
461 shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A" |
467 shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A" |
462 proof - |
468 proof - |
463 from assms obtain b B where "A = insert b B" and "finite B" by auto |
469 from assms obtain b B where "A = insert b B" and "finite B" by auto |
464 then show ?thesis |
470 then show ?thesis |
465 by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) |
471 by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) |
466 qed |
472 qed |