2395 Infimum and supremum in complete lattices may also |
2395 Infimum and supremum in complete lattices may also |
2396 be characterized by @{const fold1}: |
2396 be characterized by @{const fold1}: |
2397 *} |
2397 *} |
2398 |
2398 |
2399 lemma (in complete_lattice) Inf_fold1: |
2399 lemma (in complete_lattice) Inf_fold1: |
2400 assumes fin: "finite A" |
2400 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>A = fold1 (op \<sqinter>) A" |
2401 and nonempty: "A \<noteq> {}" |
|
2402 shows "\<Sqinter>A = fold1 (op \<sqinter>) A" |
|
2403 using fin nonempty |
|
2404 by (induct A set: finite) |
2401 by (induct A set: finite) |
2405 (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf]) |
2402 (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf]) |
2406 |
2403 |
2407 lemma (in complete_lattice) Sup_fold1: |
2404 lemma (in complete_lattice) Sup_fold1: |
2408 assumes fin: "finite A" |
2405 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>A = fold1 (op \<squnion>) A" |
2409 and nonempty: "A \<noteq> {}" |
|
2410 shows "\<Squnion>A = fold1 (op \<squnion>) A" |
|
2411 using fin nonempty |
|
2412 by (induct A set: finite) |
2406 by (induct A set: finite) |
2413 (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup]) |
2407 (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup]) |
2414 |
2408 |
2415 |
2409 |
2416 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} |
2410 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} |
2417 |
2411 |
2418 text{* |
2412 text{* |