Theory Triangular_Numbers

(*
  Title:     HOL/ex/Triangular_Numbers.thy
  Author:    Manuel Eberl, TU München
*)
section ‹Triangular Numbers›
theory Triangular_Numbers
  imports Complex_Main
begin

definition triangle_num :: "nat ⇒ nat" where
  "triangle_num n = (n * (n + 1)) div 2"

lemma real_triangle_num:
  "real (triangle_num n) = real n * (real n + 1) / 2"
  by (simp add: triangle_num_def field_char_0_class.of_nat_div algebra_simps)

lemma triangle_num_altdef: "triangle_num n = (∑k≤n. k)"
  by (induction n) (auto simp: triangle_num_def)


lemma triangle_num_ge: "triangle_num n ≥ n"
  unfolding triangle_num_altdef by (rule member_le_sum) auto

lemma triangle_num_Suc: "triangle_num (Suc n) = triangle_num n + Suc n"
  by (simp add: triangle_num_altdef)

lemma triangle_num_0 [simp]: "triangle_num 0 = 0"
  and triangle_num_1 [simp]: "triangle_num 1 = 1"
  by (simp_all add: triangle_num_def)

lemma triangle_num_numeral [simp]:
  "triangle_num (numeral n) = fst (divmod (n * Num.inc n) (Num.Bit0 Num.One))"
  unfolding fst_divmod numeral_mult numeral_inc triangle_num_def ..

lemma triangle_num_eq_0_iff [simp]: "triangle_num n = 0 ⟷ n = 0"
  using triangle_num_ge[of n] by auto

lemma triangle_num_gt_0_iff [simp]: "triangle_num n > 0 ⟷ n > 0"
  using triangle_num_eq_0_iff[of n] by linarith


lemma strict_mono_triangle_num: "strict_mono triangle_num"
  unfolding strict_mono_Suc_iff by (auto simp: triangle_num_altdef)

lemma triangle_num_le: "m ≤ n ⟹ triangle_num m ≤ triangle_num n"
  using strict_mono_leD[OF strict_mono_triangle_num] .

lemma triangle_num_less: "m < n ⟹ triangle_num m < triangle_num n"
  using strict_monoD[OF strict_mono_triangle_num] .

lemma triangle_num_less_iff: "triangle_num m < triangle_num n ⟷ m < n"
  using strict_mono_less[OF strict_mono_triangle_num] .

lemma triangle_num_le_iff: "triangle_num m ≤ triangle_num n ⟷ m ≤ n"
  using strict_mono_less_eq[OF strict_mono_triangle_num] .

lemma triangle_num_eq_iff: "triangle_num m = triangle_num n ⟷ m = n"
  using strict_mono_eq[OF strict_mono_triangle_num] .


theorem inverse_triangle_num_sums: "(λn. 1 / triangle_num (Suc n)) sums 2"
proof -
  have "(λn. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) sums
          (inverse (real (Suc 0)) - 0)"
    by (intro telescope_sums' LIMSEQ_inverse_real_of_nat)
  also have "(λn. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) =
               (λn. 1 / real (2 * triangle_num (Suc n)))"
    by (auto simp: field_simps triangle_num_def)
  also have "inverse (real (Suc 0)) - 0 = 1"
    by simp
  finally have "(λn. 2 * (1 / real (2 * triangle_num (Suc n)))) sums (2 * 1)"
    by (intro sums_mult)
  thus ?thesis by simp
qed

end