Theory Discrete_Summation

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Some basic facts about discrete summation›

theory Discrete_Summation
imports Main
begin

subsection ‹Auxiliary›

lemma add_sum_orient:
  "sum f {k..<j} + sum f {l..<k} = sum f {l..<k} + sum f {k..<j}"
  by (fact add.commute)

lemma add_sum_int:
  fixes j k l :: int
  shows "j < k ⟹ k < l ⟹
    sum f {j..<k} + sum f {k..<l} = sum f {j..<l}"
  by (simp_all add: sum.union_inter [symmetric] ivl_disj_un)


subsection ‹The shift operator›

definition Δ :: "('b::ring_1 ⇒ 'a::ab_group_add) ⇒ int ⇒ 'a"
where
  "Δ f k = f (of_int (k + 1)) - f (of_int 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 ∘ f ∘ of_int = g ∘ of_int"
proof -
  let ?F = "λk. f (of_int k)"
  let ?G = "λk. g (of_int k)"
  from assms have "⋀k. Δ f (of_int k) = Δ g (of_int 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 del: of_int_add of_int_diff of_int_0)
  qed
  then have "⋀k. (plus (?G 0 - ?F 0) ∘ ?F) k = ?G k"
    by (simp add: algebra_simps)
  then have "plus (?G 0 - ?F 0) ∘ ?F = ?G" ..
  then have "plus (?G 0 - ?F 0) ∘ f ∘ of_int = g ∘ of_int"
    by (simp only: comp_def)
  then show ?thesis ..
qed

lemma Δ_add:
  "Δ (λk. f k + g k) k = Δ f k + Δ g k"
  by (simp add: Δ_def)

lemma Δ_factor:
  "Δ (λk. c * k) k = c"
  by (simp add: Δ_def algebra_simps)


subsection ‹The formal sum operator›

definition Σ :: "('b::ring_1 ⇒ 'a::ab_group_add) ⇒ int ⇒ int ⇒ 'a"
where
  "Σ f j l = (if j < l then sum (f ∘ of_int) {j..<l}
    else if j > l then - sum (f ∘ of_int) {l..<j}
    else 0)"

lemma Σ_same [simp]:
  "Σ f j j = 0"
  by (simp add: Σ_def)

lemma Σ_positive:
  "j < l ⟹ Σ f j l = sum (f ∘ of_int) {j..<l}"
  by (simp add: Σ_def)

lemma Σ_negative:
  "j > l ⟹ Σ f j l = - Σ f l j"
  by (simp add: Σ_def)

lemma Σ_comp_of_int:
  "Σ (f ∘ of_int) = Σ f"
  by (simp add: Σ_def fun_eq_iff)

lemma Σ_const:
  "Σ (λk. c) j l = of_int (l - j) * c"
  by (simp add: Σ_def algebra_simps)

lemma Σ_add:
  "Σ (λk. f k + g k) j l = Σ f j l + Σ g j l"
  by (simp add: Σ_def sum.distrib)

lemma Σ_factor:
  "Σ (λk. c * f k) j l = (c::'a::ring) * Σ (λk. f k) j l"
  by (simp add: Σ_def sum_distrib_left)

lemma Σ_concat:
  "Σ f j k + Σ f k l = Σ f j l"
  by (simp add: Σ_def algebra_simps add_sum_int)
    (simp_all add: add_sum_orient [of "λk. f (of_int k)" k j l]
      add_sum_orient [of "λk. f (of_int k)" j l k]
      add_sum_orient [of "λk. f (of_int k)" j k l] add_sum_int)

lemma Σ_incr_upper:
  "Σ f j (l + 1) = Σ f j l + f (of_int l)"
proof -
  have "{l..<l+1} = {l}" by auto
  then have "Σ f l (l + 1) = f (of_int l)" by (simp add: Σ_def)
  moreover have "Σ f j (l + 1) = Σ f j l + Σ f l (l + 1)" by (simp add: Σ_concat)
  ultimately show ?thesis by simp
qed


subsection ‹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 (of_int l) - f (of_int j)"
proof -
  from Δ_Σ have "Δ (Σ (Δ f) j) = Δ f" .
  then obtain k where "plus k ∘ Σ (Δ f) j ∘ of_int = f ∘ of_int"
    by (blast dest: Δ_same_shift)
  then have "⋀q. f (of_int q) = k + Σ (Δ f) j q"
    by (simp add: fun_eq_iff)
  then show ?thesis by simp
qed

end