theory list_sum
imports Main
begin

lemma add_start_foldl_sum:
  "!!(y::'a::semigroup_add).
   x + foldl op + y xs = foldl op + (x+y) xs"
by (induct xs) (simp_all add: add_assoc)


lemma "foldl op + (0::'a::{ab_semigroup_add, zero}) xs = foldr op + xs 0"
proof (induct xs)
  case (Cons x xs) note calculation = this
  moreover
  have "0 + x = x + 0" by (rule add_commute)
  ultimately
  show ?case by (simp add: add_start_foldl_sum[symmetric])
qed simp


constdefs list_sum::"'a list \<Rightarrow> ('a::{zero,plus})"
  "list_sum xs == foldr op + xs 0"


lemma
  list_sum_Nil[simp]:  "list_sum [] = 0"
and
  list_sum_Cons[simp]: "list_sum (x#xs) = x + list_sum xs"
by (simp_all add: list_sum_def)


lemma distinct_list_sum_set_eq:
  "distinct xs \<Longrightarrow> list_sum xs = \<Sum>(set xs)"
by (induct xs) simp_all


lemma list_sum_append:
 "list_sum (xs@ys) = list_sum (xs::'a::{comm_monoid_add} list) + list_sum ys"
by (induct xs) (simp_all add: add_assoc)


lemma add_list_sum_take_drop:
 "n \<le> length (xs::'a::{comm_monoid_add} list) \<Longrightarrow>
  list_sum (take n xs) + list_sum(drop n xs) = list_sum xs"
by (simp add: list_sum_append[symmetric])

lemma list_sum_nat_mono:
 "n \<le> length (xs::nat list)
  \<Longrightarrow> list_sum (take n xs) \<le> list_sum xs"
by (simp add: add_list_sum_take_drop[symmetric])


end