|
69716
|
1 |
(*
|
|
|
2 |
Title: HOL/ex/Triangular_Numbers.thy
|
|
|
3 |
Author: Manuel Eberl, TU München
|
|
|
4 |
*)
|
|
|
5 |
section \<open>Triangular Numbers\<close>
|
|
|
6 |
theory Triangular_Numbers
|
|
|
7 |
imports Complex_Main
|
|
|
8 |
begin
|
|
|
9 |
|
|
|
10 |
definition triangle_num :: "nat \<Rightarrow> nat" where
|
|
|
11 |
"triangle_num n = (n * (n + 1)) div 2"
|
|
|
12 |
|
|
|
13 |
lemma real_triangle_num:
|
|
|
14 |
"real (triangle_num n) = real n * (real n + 1) / 2"
|
|
|
15 |
by (simp add: triangle_num_def field_char_0_class.of_nat_div algebra_simps)
|
|
|
16 |
|
|
|
17 |
lemma triangle_num_altdef: "triangle_num n = (\<Sum>k\<le>n. k)"
|
|
|
18 |
by (induction n) (auto simp: triangle_num_def)
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
lemma triangle_num_ge: "triangle_num n \<ge> n"
|
|
|
22 |
unfolding triangle_num_altdef by (rule member_le_sum) auto
|
|
|
23 |
|
|
|
24 |
lemma triangle_num_Suc: "triangle_num (Suc n) = triangle_num n + Suc n"
|
|
|
25 |
by (simp add: triangle_num_altdef)
|
|
|
26 |
|
|
|
27 |
lemma triangle_num_0 [simp]: "triangle_num 0 = 0"
|
|
|
28 |
and triangle_num_1 [simp]: "triangle_num 1 = 1"
|
|
|
29 |
by (simp_all add: triangle_num_def)
|
|
|
30 |
|
|
|
31 |
lemma triangle_num_numeral [simp]:
|
|
|
32 |
"triangle_num (numeral n) = fst (divmod (n * Num.inc n) (Num.Bit0 Num.One))"
|
|
|
33 |
unfolding fst_divmod numeral_mult numeral_inc triangle_num_def ..
|
|
|
34 |
|
|
|
35 |
lemma triangle_num_eq_0_iff [simp]: "triangle_num n = 0 \<longleftrightarrow> n = 0"
|
|
|
36 |
using triangle_num_ge[of n] by auto
|
|
|
37 |
|
|
|
38 |
lemma triangle_num_gt_0_iff [simp]: "triangle_num n > 0 \<longleftrightarrow> n > 0"
|
|
|
39 |
using triangle_num_eq_0_iff[of n] by linarith
|
|
|
40 |
|
|
|
41 |
|
|
|
42 |
lemma strict_mono_triangle_num: "strict_mono triangle_num"
|
|
|
43 |
unfolding strict_mono_Suc_iff by (auto simp: triangle_num_altdef)
|
|
|
44 |
|
|
|
45 |
lemma triangle_num_le: "m \<le> n \<Longrightarrow> triangle_num m \<le> triangle_num n"
|
|
|
46 |
using strict_mono_leD[OF strict_mono_triangle_num] .
|
|
|
47 |
|
|
|
48 |
lemma triangle_num_less: "m < n \<Longrightarrow> triangle_num m < triangle_num n"
|
|
|
49 |
using strict_monoD[OF strict_mono_triangle_num] .
|
|
|
50 |
|
|
|
51 |
lemma triangle_num_less_iff: "triangle_num m < triangle_num n \<longleftrightarrow> m < n"
|
|
|
52 |
using strict_mono_less[OF strict_mono_triangle_num] .
|
|
|
53 |
|
|
|
54 |
lemma triangle_num_le_iff: "triangle_num m \<le> triangle_num n \<longleftrightarrow> m \<le> n"
|
|
|
55 |
using strict_mono_less_eq[OF strict_mono_triangle_num] .
|
|
|
56 |
|
|
|
57 |
lemma triangle_num_eq_iff: "triangle_num m = triangle_num n \<longleftrightarrow> m = n"
|
|
|
58 |
using strict_mono_eq[OF strict_mono_triangle_num] .
|
|
|
59 |
|
|
|
60 |
|
|
|
61 |
theorem inverse_triangle_num_sums: "(\<lambda>n. 1 / triangle_num (Suc n)) sums 2"
|
|
|
62 |
proof -
|
|
|
63 |
have "(\<lambda>n. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) sums
|
|
|
64 |
(inverse (real (Suc 0)) - 0)"
|
|
|
65 |
by (intro telescope_sums' LIMSEQ_inverse_real_of_nat)
|
|
|
66 |
also have "(\<lambda>n. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) =
|
|
|
67 |
(\<lambda>n. 1 / real (2 * triangle_num (Suc n)))"
|
|
|
68 |
by (auto simp: field_simps triangle_num_def)
|
|
|
69 |
also have "inverse (real (Suc 0)) - 0 = 1"
|
|
|
70 |
by simp
|
|
|
71 |
finally have "(\<lambda>n. 2 * (1 / real (2 * triangle_num (Suc n)))) sums (2 * 1)"
|
|
|
72 |
by (intro sums_mult)
|
|
|
73 |
thus ?thesis by simp
|
|
|
74 |
qed
|
|
|
75 |
|
|
|
76 |
end |