2742 using operative_division[OF assms(1-2) division_of_tagged_division[OF assms(3)]] . |
2742 using operative_division[OF assms(1-2) division_of_tagged_division[OF assms(3)]] . |
2743 finally show ?thesis . qed |
2743 finally show ?thesis . qed |
2744 |
2744 |
2745 subsection {* Additivity of content. *} |
2745 subsection {* Additivity of content. *} |
2746 |
2746 |
2747 lemma setsum_iterate:assumes "finite s" shows "setsum f s = iterate op + s f" |
2747 lemma setsum_iterate: |
2748 proof- have *:"setsum f s = setsum f (support op + f s)" |
2748 assumes "finite s" shows "setsum f s = iterate op + s f" |
2749 apply(rule setsum_mono_zero_right) |
2749 proof - |
|
2750 have *: "setsum f s = setsum f (support op + f s)" |
|
2751 apply (rule setsum_mono_zero_right) |
2750 unfolding support_def neutral_monoid using assms by auto |
2752 unfolding support_def neutral_monoid using assms by auto |
2751 thus ?thesis unfolding * setsum_def iterate_def fold_image_def fold'_def |
2753 then show ?thesis unfolding * iterate_def fold'_def setsum.eq_fold |
2752 unfolding neutral_monoid . qed |
2754 unfolding neutral_monoid by (simp add: comp_def) |
|
2755 qed |
2753 |
2756 |
2754 lemma additive_content_division: assumes "d division_of {a..b}" |
2757 lemma additive_content_division: assumes "d division_of {a..b}" |
2755 shows "setsum content d = content({a..b})" |
2758 shows "setsum content d = content({a..b})" |
2756 unfolding operative_division[OF monoidal_monoid operative_content assms,THEN sym] |
2759 unfolding operative_division[OF monoidal_monoid operative_content assms,THEN sym] |
2757 apply(subst setsum_iterate) using assms by auto |
2760 apply(subst setsum_iterate) using assms by auto |