Session Discrete_Summation

Theory Factorials

(* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen with contributions by Lukas Bulwahn *)

section ‹Falling factorials›

theory Factorials
  imports Complex_Main "HOL-Combinatorics.Stirling"
begin

lemma pochhammer_0 [simp]: ― ‹TODO move›
  "pochhammer 0 n = (0::nat)" if "n > 0"
  using that by (simp add: pochhammer_prod)

definition ffact :: "nat  'a::comm_semiring_1_cancel  'a"
  where "ffact n a = pochhammer (a + 1 - of_nat n) n"

lemma ffact_0 [simp]:
  "ffact 0 = (λx. 1)"
  by (simp add: fun_eq_iff ffact_def)

lemma ffact_Suc:
  "ffact (Suc n) a = a * ffact n (a - 1)"
    for a :: "'a :: comm_ring_1"
  by (simp add: ffact_def pochhammer_prod prod.atLeast0_lessThan_Suc algebra_simps)

(* TODO: what's the right class here? *)
lemma ffact_Suc_rev:
  "ffact (Suc n) m = (m - of_nat n) * ffact n m"
    for m :: "'a :: {comm_semiring_1_cancel, ab_group_add}"
unfolding ffact_def pochhammer_rec by (simp add: diff_add_eq)

lemma ffact_nat_triv:
  "ffact n m = 0" if "m < n"
  using that by (simp add: ffact_def)

lemma ffact_Suc_nat:
  "ffact (Suc n) m = m * ffact n (m - 1)"
    for m :: nat
proof (cases "n  m")
  case True
  then show ?thesis
    by (simp add: ffact_def pochhammer_prod algebra_simps prod.atLeast0_lessThan_Suc)
next
  case False
  then have "m < n"
    by simp
  then show ?thesis
    by (simp add: ffact_nat_triv)
qed

lemma ffact_Suc_rev_nat:
  "ffact (Suc n) m = (m - n) * ffact n m"
proof (cases "n  m")
  case True
  then show ?thesis
    by (simp add: ffact_def pochhammer_rec Suc_diff_le)
next
  case False
  then have "m < n" by simp
  then show ?thesis by (simp add: ffact_nat_triv)
qed

lemma fact_div_fact_ffact:
  "fact n div fact m = ffact (n - m) n" if "m  n"
proof -
  from that have "fact n = ffact (n - m) n * fact m"
    by (simp add: ffact_def pochhammer_product pochhammer_fact)
  moreover have "fact m dvd (fact n :: nat)"
    using that by (rule fact_dvd)
  ultimately show ?thesis
    by simp
qed

lemma fact_div_fact_ffact_nat:
  "fact n div fact (n - k) = ffact k n" if "k  n"
using that by (simp add: fact_div_fact_ffact)

lemma ffact_fact:
  "ffact n (of_nat n) = (of_nat (fact n) :: 'a :: comm_ring_1)"
  by (induct n) (simp_all add: algebra_simps ffact_Suc)

lemma ffact_add_diff_assoc:
  "(a - of_nat n) * ffact n a + of_nat n * ffact n a = a * ffact n a"
    for a :: "'a :: comm_ring_1"
  by (simp add: algebra_simps)

lemma mult_ffact:
  "a * ffact n a = ffact (Suc n) a + of_nat n * ffact n a"
    for a :: "'a :: comm_ring_1"
proof -
  have "ffact (Suc n) a + of_nat n * (ffact n a) = (a - of_nat n) * (ffact n a) + of_nat n * (ffact n a)"
    using ffact_Suc_rev [of n] by auto
  also have " = a * ffact n a" using ffact_add_diff_assoc by (simp add: algebra_simps)
  finally show ?thesis by simp
qed

(* TODO: what's the right class here? *)
lemma prod_ffact:
  fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
  shows "(i = 0..<n. m - of_nat i) = ffact n m"
proof -
  have "inj_on (λj. j - 1) {1..n}"
    by (force intro: inj_on_diff_nat)
  moreover have "{0..<n} = (λj. j - 1) ` {1..n}"
  proof -
    have "i  (λj. j - 1) ` {1..n}" if "i  {0..<n}" for i
      using that by (auto intro: image_eqI[where x="i + 1"])
    from this show ?thesis by auto
  qed
  moreover have "m - of_nat (i - 1) = m + 1 - of_nat n + of_nat (n - i)" if "i  {1..n}" for i
    using that by (simp add: of_nat_diff)
  ultimately have "(i = 0..<n. m - of_nat i) = (i = 1..n. m + 1 - of_nat n + of_nat (n - i))"
    by (rule prod.reindex_cong)
  from this show ?thesis
    unfolding ffact_def by (simp only: pochhammer_prod_rev)
qed

lemma prod_ffact_nat:
  fixes m :: nat
  shows "(i = 0..<n. m - i) = ffact n m"
proof cases
  assume "n  m"
  have "inj_on (λj. j - 1) {1..n}" by (force intro: inj_on_diff_nat)
  moreover have "{0..<n} = (λj. j - 1) ` {1..n}"
  proof -
    have "i  (λj. j - 1) ` {1..n}" if "i  {0..<n}" for i
      using that by (auto intro: image_eqI[where x="i + 1"])
    from this show ?thesis by auto
  qed
  ultimately have "(i = 0..<n. m - i) = (i = 1..n. (m + 1) - i)"
    by (auto intro: prod.reindex_cong[where l="λi. i - 1"])
  from this n  m show ?thesis
    unfolding ffact_def by (simp add: pochhammer_prod_rev)
next
  assume "¬ n  m"
  from this show ?thesis by (auto simp add: ffact_nat_triv)
qed

(* TODO: what's the right class here? *)
lemma prod_rev_ffact:
  fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
  shows "(i = 1..n. m - of_nat n + of_nat i) = ffact n m"
proof -
  have "inj_on (λi. i + 1) {0..<n}" by simp
  moreover have "{1..n} = (λi. i + 1) ` {0..<n}" by auto
  moreover have "m - of_nat n + of_nat (i + 1) = m + 1 - of_nat n + of_nat i" for i by simp
  ultimately have "(i = 1..n. m - of_nat n + of_nat i) = (i = 0..<n. m + 1 - of_nat n + of_nat i)"
    by (rule prod.reindex_cong[where l="λi. i + 1"])
  from this show ?thesis
    unfolding ffact_def by (simp only: pochhammer_prod)
qed

lemma prod_rev_ffact_nat:
  fixes m :: nat
  assumes "n  m"
  shows "(i = 1..n. m - n + i) = ffact n m"
proof -
  have "inj_on (λi. i + 1) {0..<n}" by simp
  moreover have "{1..n} = (λi. i + 1) ` {0..<n}" by auto
  moreover have "m - n + (i + 1) = m + 1 - n + i" for i
    using  n  m by auto
  ultimately have "(i = 1..n. m - n + i) = (i = 0..<n. m + 1 - n + i)"
    by (rule prod.reindex_cong)
 from this show ?thesis
   unfolding ffact_def by (simp only: pochhammer_prod of_nat_id)
qed

lemma prod_rev_ffact_nat':
  fixes m :: nat
  assumes "n  m"
  shows "{m - n + 1..m} = ffact n m"
proof -
  have "inj_on (λi. m - n + i) {1::nat..n}" by (auto intro: inj_onI)
  moreover have "{m - n + 1..m} = (λi. m - n + i) ` {1::nat..n}"
  proof -
    have "i  (λi. m + i - n) ` {Suc 0..n}" if "i  {m - n + 1..m}" for i
      using that n  m by (auto intro!: image_eqI[where x="i - (m - n)"])
    with n  m show ?thesis by auto
  qed
  moreover have "m - n + i = m - n + i" for i ..
  ultimately have "{m - n + (1::nat)..m} = (i = 1..n. m - n + i)"
    by (rule prod.reindex_cong)
  from this show ?thesis
    using n  m by (simp only: prod_rev_ffact_nat)
qed

lemma ffact_eq_fact_mult_binomial:
  "ffact k n = fact k * (n choose k)"
proof cases
  assume "k  n"
  have "ffact k n = fact n div fact (n - k)"
    using k  n by (simp add: fact_div_fact_ffact_nat)
  also have " = fact k * (n choose k)"
    using k  n by (simp add: binomial_fact_lemma[symmetric])
  finally show ?thesis .
next
  assume "¬ k  n"
  from this ffact_nat_triv show ?thesis by force
qed

lemma of_nat_ffact:
  "of_nat (ffact n m) = ffact n (of_nat m :: 'a :: comm_ring_1)"
proof (induct n arbitrary: m)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof (cases m)
    case 0
    then show ?thesis
      by (simp add: ffact_Suc_nat ffact_Suc)
  next
    case (Suc m)
    with Suc.hyps show ?thesis
      by (simp add: algebra_simps ffact_Suc_nat ffact_Suc)
  qed
qed

lemma of_int_ffact:
  "of_int (ffact n k) = ffact n (of_int k :: 'a :: comm_ring_1)"
proof (induct n arbitrary: k)
  case 0 then show ?case by simp
next
  case (Suc n k)
  then have "of_int (ffact n (k - 1)) = ffact n (of_int (k - 1) :: 'a)" .
  then show ?case
    by (simp add: ffact_Suc_nat ffact_Suc)
qed

lemma ffact_minus:
  fixes x :: "'a :: comm_ring_1"
  shows "ffact n (- x) = (- 1) ^ n * pochhammer x n"
proof -
  have "ffact n (- x) = pochhammer (- x + 1 - of_nat n) n"
    unfolding ffact_def ..
  also have " = pochhammer (- x - of_nat n + 1) n"
    by (simp add: diff_add_eq)
  also have " = (- 1) ^ n * pochhammer (- (- x)) n"
    by (rule pochhammer_minus')
  also have " = (- 1) ^ n * pochhammer x n" by simp
  finally show ?thesis .
qed

text ‹Conversion of natural potences into falling factorials and back›

lemma monomial_ffact:
  "a ^ n = (k = 0..n. of_nat (Stirling n k) * ffact k a)"
    for a :: "'a :: comm_ring_1"
proof (induct n)
  case 0 then show ?case by simp
next
  case (Suc n)
  then have "a ^ Suc n = a * (k = 0..n. of_nat (Stirling n k) * ffact k a)"
    by simp
  also have " = (k = 0..n. of_nat (Stirling n k) * (a * ffact k a))"
    by (simp add: sum_distrib_left algebra_simps)
  also have " = (k = 0..n. of_nat (Stirling n k) * ffact (Suc k) a) +
    (k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a))"
    by (simp add: sum.distrib algebra_simps mult_ffact)
  also have " = (k = 0.. Suc n. of_nat (Stirling n k) * ffact (Suc k) a) +
    (k = 0..Suc n. of_nat ((Suc k) * (Stirling n (Suc k))) * (ffact (Suc k) a))"
  proof -
    have "(k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
      (k = 0..n+2. of_nat (Stirling n k) * (of_nat k * ffact k a))" by simp
    also have " = (k = Suc 0 .. Suc (Suc n). of_nat (Stirling n k) * (of_nat k * ffact k a)) "
      by (simp only: sum.atLeast_Suc_atMost [of 0 "n + 2"]) simp
    also have " = (k = 0 .. Suc n. of_nat (Stirling n (Suc k)) * (of_nat (Suc k) * ffact (Suc k) a))"
      by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
    also have " = (k = 0 .. Suc n. of_nat ((Suc k) * Stirling n (Suc k)) * ffact (Suc k) a)"
      by (simp only: of_nat_mult algebra_simps)
    finally have "(k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
      (k = 0..Suc n. of_nat (Suc k * Stirling n (Suc k)) * ffact (Suc k) a)"
      by simp
    then show ?thesis by simp
  qed
  also have " = (k = 0..n. of_nat (Stirling (Suc n) (Suc k)) * ffact (Suc k) a)"
    by (simp add: algebra_simps sum.distrib)
  also have " = (k = Suc 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
    by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
  also have " = (k = 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
    by (simp only: sum.atLeast_Suc_atMost [of "0" "Suc n"]) simp
  finally show ?case by simp
qed

lemma ffact_monomial:
  "ffact n a = (k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
    for a :: "'a :: comm_ring_1"
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  then have "ffact (Suc n) a = (a - of_nat n) * (k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
    by (simp add: ffact_Suc_rev)
  also have " = (k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ (Suc k)) +
    (k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * (stirling n k)) * a ^ k)"
    by (simp only: diff_conv_add_uminus distrib_right) (simp add: sum_distrib_left field_simps)
  also have " = (k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (stirling n k) * a ^ Suc k) +
  (k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
  proof -
    have "(k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * stirling n k) * a ^ k) =
      (k = 0..n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
      by (simp add: Suc_diff_le)
    also have " = (k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
      by (simp add: sum.atLeast_Suc_atMost) (cases n; simp)
    also have " = (k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
      by (simp only: sum.shift_bounds_cl_Suc_ivl)
    finally show ?thesis by simp
  qed
  also have " = (k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k) + stirling n k) * a ^ Suc k)"
    by (simp add: sum.distrib algebra_simps)
  also have " = (k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (stirling (Suc n) (Suc k)) * a ^ Suc k)"
    by (simp only: stirling.simps)
  also have " = (k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
    by (simp only: sum.shift_bounds_cl_Suc_ivl)
  also have " = (k = 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
    by (simp add: sum.atLeast_Suc_atMost)
  finally show ?case .
qed

end

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

Theory Summation_Conversion

(* Author: Florian Haftmann, TU Muenchen *)

section ‹A barebone conversion for discrete summation›

theory Summation_Conversion
imports Factorials Discrete_Summation
begin

text ‹Extensible theorem collection for solving summation problems›

named_theorems summation "rules for solving summation problems"

declare
  Σ_const [summation] Σ_add [summation]
  Σ_factor [summation] monomial_ffact [summation]

lemma intervall_simps [summation]:
  "(k::nat = 0..0. f k) = f 0"
  "(k::nat = 0..Suc n. f k) = f (Suc n) + (k::nat = 0..n. f k)"
  by (simp_all add: add.commute)

lemma Δ_ffact:
  (ffact (Suc n)) k = of_nat (Suc n) * ffact n (of_int k :: 'a :: comm_ring_1)"
proof (induct n)
  case 0 then show ?case
    by (simp add: Δ_def ffact_Suc)
next
  case (Suc n)
  obtain m where "m = Suc n" by blast
  have (ffact (Suc m)) k =
    ffact (Suc m) (of_int (k + 1)) - ffact (Suc m) (of_int k :: 'a)" 
    by (simp add: Δ_def)
  also have " = of_int (k + 1) * ffact m (of_int k)
    - (ffact m (of_int k) * (of_int k - of_nat m))"
    using ffact_Suc_rev [of m "(of_int k :: 'a :: comm_ring_1)"]
    by (simp add: ac_simps ffact_Suc)
  also have " = (of_int k + 1 - of_int k + of_nat m) * ffact m (of_int k)"
    by (simp add: algebra_simps)
  also have " = of_nat (Suc m) * ffact m (of_int k)" by simp
  also have " = of_nat (Suc m) * ffact (Suc m - 1) (of_int k)" by simp
  finally show ?case by (simp only: m = Suc n diff_Suc_1)
qed

lemma Σ_ffact_divide [summation]:
  (ffact n) j l =
    (ffact (Suc n) (of_int l :: 'a :: {idom_divide, semiring_char_0}) - ffact (Suc n) (of_int j)) div of_nat (Suc n)"
proof -
  have *: "(of_nat (Suc n) * Σ (ffact n) j l) div of_nat (Suc n) = (Σ (ffact n) j l :: 'a)"
    using of_nat_neq_0 [where ?'a = 'a] by simp
  have "ffact (Suc n) (of_int l :: 'a) - ffact (Suc n) (of_int j) =
    Σ (λk. Δ (ffact (Suc n)) k) j l"
    by (simp add: Σ_Δ)
  also have " = Σ (λk. of_nat (Suc n) * ffact n (of_int k)) j l"
    by (simp add: Δ_ffact)
  also have " = of_nat (Suc n) * Σ (ffact n  of_int) j l"
    by (simp add: Σ_factor comp_def)
  finally show ?thesis by (simp only: Σ_comp_of_int * of_nat_eq_0_iff)
qed


text ‹Various other rules›

lemma of_int_coeff:
  "(of_int l :: 'a::comm_ring_1) * numeral k = of_int (l * numeral k)"
  by simp

lemmas nat_simps =
  add_0_left add_0_right add_Suc add_Suc_right
  mult_Suc mult_Suc_right mult_zero_left mult_zero_right
  One_nat_def of_nat_simps

lemmas of_int_pull_out =
  of_int_add [symmetric] of_int_diff [symmetric] of_int_mult [symmetric]
  of_int_coeff

lemma of_nat_coeff:
  "(of_nat n :: 'a::comm_semiring_1) * numeral m = of_nat (n * numeral m)"
  by (induct n) simp_all
  
lemmas of_nat_pull_out =
  of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_coeff

lemmas nat_pull_in =
  nat_int_add

lemmas of_int_pull_in =
  of_int_pull_out [symmetric] add_divide_distrib diff_divide_distrib of_int_power
  of_int_numeral of_int_neg_numeral times_divide_eq_left [symmetric]

  
text ‹Special for @{typ nat}

definition lift_nat :: "(nat  nat)  int  int"
where
  "lift_nat f = int  f  nat"

definition Σ_nat :: "(nat  nat)  nat  nat  nat" ("Σ")
where
  [summation]: "Σ f m n = nat (Σ (lift_nat f) (int m) (int n))"  

definition pos_id :: "int  int"
where
  "pos_id k = (if k < 0 then 0 else k)"

lemma Σ_pos_id [summation]:
  "0  k  0  l  Σ (λr. f (pos_id r)) k l = Σ f k l"
  by (simp add: Σ_def pos_id_def)

lemma [summation]:
  "(0::int)  0"
  "(0::int)  1"
  "(0::int)  numeral m"
  "(0::int)  int n"
  by simp_all
  
lemma [summation]:
  "lift_nat (λn. m) = (λk. int m)"
  by (simp add: lift_nat_def fun_eq_iff)

lemma [summation]:
  "lift_nat (λn. n) = pos_id"
  by (simp add: lift_nat_def fun_eq_iff pos_id_def)

lemma [summation]:
  "lift_nat (λn. f n + g n) = (λk. lift_nat f k + lift_nat g k)"
  by (simp add: lift_nat_def fun_eq_iff)

lemma [summation]:
  "lift_nat (λn. m * f n) = (λk. int m * lift_nat f k)"
  by (simp add: lift_nat_def fun_eq_iff)

lemma [summation]:
  "lift_nat (λn. f n * m) = (λk. lift_nat f k * int m)"
  by (simp add: lift_nat_def fun_eq_iff)

lemma [summation]:
  "lift_nat (λn. f n ^ m) = (λk. lift_nat f k ^ m)"
  by (simp add: lift_nat_def fun_eq_iff)

  
text ‹Generic conversion›  

ML signature SUMMATION =
sig
  val conv: Proof.context -> conv
end

structure Summation : SUMMATION =
struct

val simps2 = @{thms Stirling.simps ffact_0 ffact_Suc nat_simps};
val simpset3 =
  @{context}
  |> fold Simplifier.add_simp @{thms field_simps}
  |> Simplifier.simpset_of;
val simps4 = @{thms of_int_pull_out of_nat_pull_out nat_pull_in};
val simps6 = @{thms of_int_pull_in};

fun conv ctxt =
  let
    val ctxt1 =
      ctxt
      |> put_simpset HOL_basic_ss
      |> fold Simplifier.add_simp (Named_Theorems.get ctxt @{named_theorems summation})
    val ctxt2 =
      ctxt
      |> put_simpset HOL_basic_ss
      |> fold Simplifier.add_simp simps2
    val ctxt3 =
      ctxt
      |> put_simpset simpset3
    val ctxt4 =
      ctxt
      |> put_simpset HOL_basic_ss
      |> fold Simplifier.add_simp simps4
    val semiring_conv_base = Semiring_Normalizer.semiring_normalize_conv ctxt
    val semiring_conv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv semiring_conv_base))
      else_conv Conv.arg1_conv (Conv.arg_conv semiring_conv_base)
      else_conv semiring_conv_base
    val ctxt6 =
      ctxt
      |> put_simpset HOL_basic_ss
      |> fold Simplifier.add_simp simps6
  in
     Simplifier.rewrite ctxt1
     then_conv Simplifier.rewrite ctxt2
     then_conv Simplifier.rewrite ctxt3
     then_conv Simplifier.rewrite ctxt4
     then_conv semiring_conv
     then_conv Simplifier.rewrite ctxt6
  end

end

hide_fact (open) nat_simps of_int_pull_out of_int_pull_in

end

Theory Examples

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Simple examples›

theory Examples
imports Summation_Conversion
begin

ML Summation.conv @{context}
  @{cterm (λq::rat. q ^ Suc (Suc (Suc 0)) + 3) 0 j"}

ML Summation.conv @{context}
  @{cterm (λx::real. x ^ Suc (Suc (Suc 0)) + 3) 0 j"}

ML Summation.conv @{context}
  @{cterm (λk::int. k ^ Suc (Suc (Suc 0)) + 3) 0 j"}

ML Summation.conv @{context}
  @{cterm "Σ (λn::nat. n ^ Suc (Suc (Suc 0)) + 3) 0 m"}

end