equal
deleted
inserted
replaced
2400 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>A = fold1 (op \<sqinter>) A" |
2400 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>A = fold1 (op \<sqinter>) A" |
2401 by (induct A set: finite) |
2401 by (induct A set: finite) |
2402 (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]) |
2403 |
2403 |
2404 lemma (in complete_lattice) Sup_fold1: |
2404 lemma (in complete_lattice) Sup_fold1: |
2405 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>A = fold1 (op \<squnion>) A" |
2405 "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>A = fold1 (op \<squnion>) A" |
2406 by (induct A set: finite) |
2406 by (induct A set: finite) |
2407 (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]) |
2408 |
2408 |
2409 |
2409 |
2410 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} |
2410 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} |
2413 As an application of @{text fold1} we define minimum |
2413 As an application of @{text fold1} we define minimum |
2414 and maximum in (not necessarily complete!) linear orders |
2414 and maximum in (not necessarily complete!) linear orders |
2415 over (non-empty) sets by means of @{text fold1}. |
2415 over (non-empty) sets by means of @{text fold1}. |
2416 *} |
2416 *} |
2417 |
2417 |
2418 locale Linorder = linorder -- {* we do not pollute the @{text linorder} clas *} |
2418 locale Linorder = linorder -- {* we do not pollute the @{text linorder} class *} |
2419 begin |
2419 begin |
2420 |
2420 |
2421 definition |
2421 definition |
2422 Min :: "'a set \<Rightarrow> 'a" |
2422 Min :: "'a set \<Rightarrow> 'a" |
2423 where |
2423 where |
2612 show "Linorder.Max (op \<le>) A = Max A" |
2612 show "Linorder.Max (op \<le>) A = Max A" |
2613 by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms] |
2613 by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms] |
2614 ord_class.max) |
2614 ord_class.max) |
2615 qed |
2615 qed |
2616 |
2616 |
|
2617 (*FIXME: temporary solution - doesn't work properly*) |
2617 interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]: |
2618 interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]: |
2618 Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"] |
2619 Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"] |
2619 by (rule Linorder_ab_semigroup_add.intro, |
2620 by (rule Linorder_ab_semigroup_add.intro, |
2620 rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms) |
2621 rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms) |
2621 hide const Min Max |
2622 hide const Min Max |