(* Author: Florian Haftmann, TU Muenchen *)

header {* Some basic facts about discrete summation *}

theory Summation

imports Main

begin

text {* Auxiliary. *}

lemma add_setsum_orient:

"setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"

by (fact add.commute)

lemma add_setsum_int:

fixes j k l :: int

shows "j < k ==> k < l ==> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"

by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)

text {* The shift operator. *}

definition Δ :: "(int => 'a::ab_group_add) => int => 'a" where

"Δ f k = f (k + 1) - f k"

lemma Δ_shift:

"Δ (λk. l + f k) = Δ f"

by (simp add: Δ_def fun_eq_iff)

lemma Δ_same_shift:

assumes "Δ f = Δ g"

shows "∃l. plus l o f = g"

proof -

fix k

from assms have "!!k. Δ f k = Δ g k" by simp

then have k_incr: "!!k. f (k + 1) - g (k + 1) = f k - g k"

by (simp add: Δ_def algebra_simps)

then have "!!k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"

by blast

then have k_decr: "!!k. f (k - 1) - g (k - 1) = f k - g k"

by simp

have "!!k. f k - g k = f 0 - g 0"

proof -

fix k

show "f k - g k = f 0 - g 0"

by (induct k rule: int_induct) (simp_all add: k_incr k_decr)

qed

then have "!!k. (plus (g 0 - f 0) o f) k = g k"

by (simp add: algebra_simps)

then have "plus (g 0 - f 0) o f = g" ..

then show ?thesis ..

qed

text {* The formal sum operator. *}

definition Σ :: "(int => 'a::ab_group_add) => int => int => 'a" where

"Σ f j l = (if j < l then setsum f {j..<l}

else if j > l then - setsum f {l..<j}

else 0)"

lemma Σ_same [simp]:

"Σ f j j = 0"

by (simp add: Σ_def)

lemma Σ_positive:

"j < l ==> Σ f j l = setsum f {j..<l}"

by (simp add: Σ_def)

lemma Σ_negative:

"j > l ==> Σ f j l = - Σ f l j"

by (simp add: Σ_def)

lemma add_Σ:

"Σ f j k + Σ f k l = Σ f j l"

by (simp add: Σ_def algebra_simps add_setsum_int)

(simp_all add: add_setsum_orient [of f k j l]

add_setsum_orient [of f j l k]

add_setsum_orient [of f j k l] add_setsum_int)

lemma Σ_incr_upper:

"Σ f j (l + 1) = Σ f j l + f l"

proof -

have "{l..<l+1} = {l}" by auto

then have "Σ f l (l + 1) = f l" by (simp add: Σ_def)

moreover have "Σ f j (l + 1) = Σ f j l + Σ f l (l + 1)" by (simp add: add_Σ)

ultimately show ?thesis by simp

qed

text {* Fundamental lemmas: The relation between @{term Δ} and @{term Σ}. *}

lemma Δ_Σ:

"Δ (Σ f j) = f"

proof

fix k

show "Δ (Σ f j) k = f k"

by (simp add: Δ_def Σ_incr_upper)

qed

lemma Σ_Δ:

"Σ (Δ f) j l = f l - f j"

proof -

from Δ_Σ have "Δ (Σ (Δ f) j) = Δ f" .

then obtain k where "plus k o Σ (Δ f) j = f" by (blast dest: Δ_same_shift)

then have "!!q. f q = k + Σ (Δ f) j q" by (simp add: fun_eq_iff)

then show ?thesis by simp

qed

end