author  eberlm 
Mon, 02 Nov 2015 11:56:28 +0100  
changeset 61525  ab2e862263e7 
parent 61076  bdc1e2f0a86a 
child 61533  980dd46a03fb 
permissions  rwrr 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

1 
(* Title : Binomial.thy 
12196  2 
Author : Jacques D. Fleuriot 
3 
Copyright : 1998 University of Cambridge 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

4 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

5 
The integer version of factorial and other additions by Jeremy Avigad. 
12196  6 
*) 
7 

60758  8 
section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close> 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

9 

59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

10 
theory Binomial 
33319  11 
imports Main 
15131  12 
begin 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

13 

60758  14 
subsection \<open>Factorial\<close> 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

15 

59733
cd945dc13bec
more general type class for factorial. Now allows code generation (?)
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset

16 
fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

17 
where "fact 0 = 1"  "fact (Suc n) = of_nat (Suc n) * fact n" 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

18 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

19 
lemmas fact_Suc = fact.simps(2) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

20 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

21 
lemma fact_1 [simp]: "fact 1 = 1" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

22 
by simp 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

23 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

24 
lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

25 
by simp 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

26 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

27 
lemma of_nat_fact [simp]: "of_nat (fact n) = fact n" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

28 
by (induct n) (auto simp add: algebra_simps of_nat_mult) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

29 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

30 
lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n  1)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

31 
by (cases n) auto 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

32 

59733
cd945dc13bec
more general type class for factorial. Now allows code generation (?)
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset

33 
lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

34 
apply (induct n) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

35 
apply auto 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

36 
using of_nat_eq_0_iff by fastforce 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

37 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

38 
lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

39 
by (induct n) (auto simp: le_Suc_eq) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

40 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

41 
lemma fact_in_Nats: "fact n \<in> \<nat>" by (induction n) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

42 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

43 
lemma fact_in_Ints: "fact n \<in> \<int>" by (induction n) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

44 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

45 
context 
60241  46 
assumes "SORT_CONSTRAINT('a::linordered_semidom)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

47 
begin 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

48 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

49 
lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

50 
by (metis of_nat_fact of_nat_le_iff fact_mono_nat) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

51 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

52 
lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

53 
by (metis le0 fact.simps(1) fact_mono) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

54 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

55 
lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

56 
using fact_ge_1 less_le_trans zero_less_one by blast 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

57 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

58 
lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

59 
by (simp add: less_imp_le) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

60 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

61 
lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

62 
by (simp add: not_less_iff_gr_or_eq) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

63 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

64 
lemma fact_le_power: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

65 
"fact n \<le> (of_nat (n^n) ::'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

66 
proof (induct n) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

67 
case (Suc n) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

68 
then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

69 
by (rule order_trans) (simp add: power_mono) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

70 
have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

71 
by (simp add: algebra_simps) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

72 
also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

73 
by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

74 
also have "... \<le> (of_nat (Suc n ^ Suc n) ::'a)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

75 
by (metis of_nat_mult order_refl power_Suc) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

76 
finally show ?case . 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

77 
qed simp 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

78 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

79 
end 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

80 

60758  81 
text\<open>Note that @{term "fact 0 = fact 1"}\<close> 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

82 
lemma fact_less_mono_nat: "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: nat)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

83 
by (induct n) (auto simp: less_Suc_eq) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

84 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

85 
lemma fact_less_mono: 
60241  86 
"\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

87 
by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

88 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

89 
lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

90 
by (metis One_nat_def fact_ge_1) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

91 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

92 
lemma dvd_fact: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

93 
shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

94 
by (induct n) (auto simp: dvdI le_Suc_eq) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

95 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

96 
lemma fact_altdef_nat: "fact n = \<Prod>{1..n}" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

97 
by (induct n) (auto simp: atLeastAtMostSuc_conv) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

98 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

99 
lemma fact_altdef: "fact n = setprod of_nat {1..n}" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

100 
by (induct n) (auto simp: atLeastAtMostSuc_conv) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

101 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

102 
lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

103 
by (induct m) (auto simp: le_Suc_eq) 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

104 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

105 
lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a :: {semiring_div,linordered_semidom}) = 0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

106 
by (auto simp add: fact_dvd) 
40033
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

107 

84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

108 
lemma fact_div_fact: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

109 
assumes "m \<ge> n" 
40033
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

110 
shows "(fact m) div (fact n) = \<Prod>{n + 1..m}" 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

111 
proof  
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

112 
obtain d where "d = m  n" by auto 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

113 
from assms this have "m = n + d" by auto 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

114 
have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}" 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

115 
proof (induct d) 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

116 
case 0 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

117 
show ?case by simp 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

118 
next 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

119 
case (Suc d') 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

120 
have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n" 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

121 
by simp 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

122 
also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}" 
40033
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

123 
unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod) 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

124 
also have "... = \<Prod>{n + 1..n + Suc d'}" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

125 
by (simp add: atLeastAtMostSuc_conv) 
40033
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

126 
finally show ?case . 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

127 
qed 
60758  128 
from this \<open>m = n + d\<close> show ?thesis by simp 
40033
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

129 
qed 
84200d970bf0
added some facts about factorial and dvd, div and mod
bulwahn
parents:
35644
diff
changeset

130 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

131 
lemma fact_num_eq_if: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

132 
"fact m = (if m=0 then 1 else of_nat m * fact (m  1))" 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

133 
by (cases m) auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset

134 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

135 
lemma fact_eq_rev_setprod_nat: "fact k = (\<Prod>i<k. k  i)" 
50224  136 
unfolding fact_altdef_nat 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
57113
diff
changeset

137 
by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k  i" and j="\<lambda>i. k  i"]) auto 
50224  138 

50240
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

139 
lemma fact_div_fact_le_pow: 
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

140 
assumes "r \<le> n" shows "fact n div fact (n  r) \<le> n ^ r" 
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

141 
proof  
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

142 
have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n  r..n} = (n  r) * \<Prod>{Suc (n  r)..n}" 
57418  143 
by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL) 
50240
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

144 
with assms show ?thesis 
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

145 
by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono) 
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

146 
qed 
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using natdivision (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset

147 

60758  148 
lemma fact_numeral: \<open>Evaluation for specific numerals\<close> 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
50240
diff
changeset

149 
"fact (numeral k) = (numeral k) * (fact (pred_numeral k))" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

150 
by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral) 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
50240
diff
changeset

151 

59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

152 

60758  153 
text \<open>This development is based on the work of Andy Gordon and 
154 
Florian Kammueller.\<close> 

59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

155 

60758  156 
subsection \<open>Basic definitions and lemmas\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

157 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

158 
primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

159 
where 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

160 
"0 choose k = (if k = 0 then 1 else 0)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

161 
 "Suc n choose k = (if k = 0 then 1 else (n choose (k  1)) + (n choose k))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

162 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

163 
lemma binomial_n_0 [simp]: "(n choose 0) = 1" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

164 
by (cases n) simp_all 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

165 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

166 
lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

167 
by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

168 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

169 
lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

170 
by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

171 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

172 
lemma choose_reduce_nat: 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

173 
"0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow> 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

174 
(n choose k) = ((n  1) choose (k  1)) + ((n  1) choose k)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

175 
by (metis Suc_diff_1 binomial.simps(2) neq0_conv) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

176 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

177 
lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

178 
by (induct n arbitrary: k) auto 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

179 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

180 
declare binomial.simps [simp del] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

181 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

182 
lemma binomial_n_n [simp]: "n choose n = 1" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

183 
by (induct n) (simp_all add: binomial_eq_0) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

184 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

185 
lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

186 
by (induct n) simp_all 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

187 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

188 
lemma binomial_1 [simp]: "n choose Suc 0 = n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

189 
by (induct n) simp_all 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

190 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

191 
lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

192 
by (induct n k rule: diff_induct) simp_all 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

193 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

194 
lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

195 
by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

196 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

197 
lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

198 
by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

199 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

200 
lemma Suc_times_binomial_eq: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

201 
"Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

202 
apply (induct n arbitrary: k, simp add: binomial.simps) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

203 
apply (case_tac k) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

204 
apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

205 
done 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

206 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

207 
lemma binomial_le_pow2: "n choose k \<le> 2^n" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

208 
apply (induction n arbitrary: k) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

209 
apply (simp add: binomial.simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

210 
apply (case_tac k) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

211 
apply (auto simp: power_Suc) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

212 
by (simp add: add_le_mono mult_2) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

213 

60758  214 
text\<open>The absorption property\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

215 
lemma Suc_times_binomial: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

216 
"Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

217 
using Suc_times_binomial_eq by auto 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

218 

60758  219 
text\<open>This is the wellknown version of absorption, but it's harder to use because of the 
220 
need to reason about division.\<close> 

59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

221 
lemma binomial_Suc_Suc_eq_times: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

222 
"(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

223 
by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

224 

60758  225 
text\<open>Another version of absorption, with 1 instead of Suc.\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

226 
lemma times_binomial_minus1_eq: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

227 
"0 < k \<Longrightarrow> k * (n choose k) = n * ((n  1) choose (k  1))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

228 
using Suc_times_binomial_eq [where n = "n  1" and k = "k  1"] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

229 
by (auto split add: nat_diff_split) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

230 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

231 

60758  232 
subsection \<open>Combinatorial theorems involving @{text "choose"}\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

233 

60758  234 
text \<open>By Florian Kamm\"uller, tidied by LCP.\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

235 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

236 
lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

237 
by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

238 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

239 
lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow> 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

240 
{s. s \<subseteq> insert x M \<and> card s = Suc k} = 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

241 
{s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

242 
apply safe 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

243 
apply (auto intro: finite_subset [THEN card_insert_disjoint]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

244 
by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

245 
card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

246 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

247 
lemma finite_bex_subset [simp]: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

248 
assumes "finite B" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

249 
and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

250 
shows "finite {x. \<exists>A \<subseteq> B. P x A}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

251 
by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

252 

60758  253 
text\<open>There are as many subsets of @{term A} having cardinality @{term k} 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

254 
as there are sets obtained from the former by inserting a fixed element 
60758  255 
@{term x} into each.\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

256 
lemma constr_bij: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

257 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

258 
card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} = 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

259 
card {B. B \<subseteq> A & card(B) = k}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

260 
apply (rule card_bij_eq [where f = "\<lambda>s. s  {x}" and g = "insert x"]) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

261 
apply (auto elim!: equalityE simp add: inj_on_def) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

262 
apply (metis card_Diff_singleton_if finite_subset in_mono) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

263 
done 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

264 

60758  265 
text \<open> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

266 
Main theorem: combinatorial statement about number of subsets of a set. 
60758  267 
\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

268 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

269 
theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

270 
proof (induct k arbitrary: A) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

271 
case 0 then show ?case by (simp add: card_s_0_eq_empty) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

272 
next 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

273 
case (Suc k) 
60758  274 
show ?case using \<open>finite A\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

275 
proof (induct A) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

276 
case empty show ?case by (simp add: card_s_0_eq_empty) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

277 
next 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

278 
case (insert x A) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

279 
then show ?case using Suc.hyps 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

280 
apply (simp add: card_s_0_eq_empty choose_deconstruct) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

281 
apply (subst card_Un_disjoint) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

282 
prefer 4 apply (force simp add: constr_bij) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

283 
prefer 3 apply force 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

284 
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

285 
finite_subset [of _ "Pow (insert x F)" for F]) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

286 
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

287 
done 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

288 
qed 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

289 
qed 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

290 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

291 

60758  292 
subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

293 

60758  294 
text\<open>Avigad's version, generalized to any commutative ring\<close> 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

295 
theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n = 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

296 
(\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(nk))" (is "?P n") 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

297 
proof (induct n) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

298 
case 0 then show "?P 0" by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

299 
next 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

300 
case (Suc n) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

301 
have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

302 
by auto 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

303 
have decomp2: "{0..n} = {0} Un {1..n}" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

304 
by auto 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

305 
have "(a+b)^(n+1) = 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

306 
(a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

307 
using Suc.hyps by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

308 
also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk)) + 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

309 
b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

310 
by (rule distrib_right) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

311 
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(nk)) + 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

312 
(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk+1))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

313 
by (auto simp add: setsum_right_distrib ac_simps) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

314 
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1k)) + 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

315 
(\<Sum>k=1..n+1. of_nat (n choose (k  1)) * a^k * b^(n+1k))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

316 
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

317 
del:setsum_cl_ivl_Suc) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

318 
also have "\<dots> = a^(n+1) + b^(n+1) + 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

319 
(\<Sum>k=1..n. of_nat (n choose (k  1)) * a^k * b^(n+1k)) + 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

320 
(\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1k))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

321 
by (simp add: decomp2) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

322 
also have 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

323 
"\<dots> = a^(n+1) + b^(n+1) + 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

324 
(\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1k))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

325 
by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

326 
also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1k))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

327 
using decomp by (simp add: field_simps) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

328 
finally show "?P (Suc n)" by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

329 
qed 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

330 

60758  331 
text\<open>Original version for the naturals\<close> 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

332 
corollary binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(nk))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

333 
using binomial_ring [of "int a" "int b" n] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

334 
by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

335 
of_nat_setsum [symmetric] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

336 
of_nat_eq_iff of_nat_id) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

337 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

338 
lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n  k) * (n choose k) = fact n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

339 
proof (induct n arbitrary: k rule: nat_less_induct) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

340 
fix n k assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m  x) * (m choose x) = 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

341 
fact m" and kn: "k \<le> n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

342 
let ?ths = "fact k * fact (n  k) * (n choose k) = fact n" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

343 
{ assume "n=0" then have ?ths using kn by simp } 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

344 
moreover 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

345 
{ assume "k=0" then have ?ths using kn by simp } 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

346 
moreover 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

347 
{ assume nk: "n=k" then have ?ths by simp } 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

348 
moreover 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

349 
{ fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

350 
from n have mn: "m < n" by arith 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

351 
from hm have hm': "h \<le> m" by arith 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

352 
from hm h n kn have km: "k \<le> m" by arith 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

353 
have "m  h = Suc (m  Suc h)" using h km hm by arith 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

354 
with km h have th0: "fact (m  h) = (m  h) * fact (m  k)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

355 
by simp 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

356 
from n h th0 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

357 
have "fact k * fact (n  k) * (n choose k) = 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

358 
k * (fact h * fact (m  h) * (m choose h)) + 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

359 
(m  h) * (fact k * fact (m  k) * (m choose k))" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

360 
by (simp add: field_simps) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

361 
also have "\<dots> = (k + (m  h)) * fact m" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

362 
using H[rule_format, OF mn hm'] H[rule_format, OF mn km] 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

363 
by (simp add: field_simps) 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

364 
finally have ?ths using h n km by simp } 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

365 
moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)" 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

366 
using kn by presburger 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

367 
ultimately show ?ths by blast 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

368 
qed 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

369 

0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

370 
lemma binomial_fact: 
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

371 
assumes kn: "k \<le> n" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

372 
shows "(of_nat (n choose k) :: 'a::field_char_0) = 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

373 
(fact n) / (fact k * fact(n  k))" 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

374 
using binomial_fact_lemma[OF kn] 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

375 
apply (simp add: field_simps) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

376 
by (metis mult.commute of_nat_fact of_nat_mult) 
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

377 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

378 
lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

379 
using binomial [of 1 "1" n] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

380 
by (simp add: numeral_2_eq_2) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

381 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

382 
lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

383 
by (induct n) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

384 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

385 
lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

386 
by (induct n) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

387 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

388 
lemma choose_alternating_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

389 
"n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

390 
using binomial_ring[of "1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

391 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

392 
lemma choose_even_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

393 
assumes "n > 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

394 
shows "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

395 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

396 
have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (1) ^ i * of_nat (n choose i) :: 'a)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

397 
using choose_row_sum[of n] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

398 
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

399 
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (1) ^ i * of_nat (n choose i))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

400 
by (simp add: setsum.distrib) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

401 
also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

402 
by (subst setsum_right_distrib, intro setsum.cong) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

403 
finally show ?thesis .. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

404 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

405 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

406 
lemma choose_odd_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

407 
assumes "n > 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

408 
shows "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

409 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

410 
have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i))  (\<Sum>i\<le>n. (1) ^ i * of_nat (n choose i) :: 'a)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

411 
using choose_row_sum[of n] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

412 
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

413 
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i)  (1) ^ i * of_nat (n choose i))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

414 
by (simp add: setsum_subtractf) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

415 
also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

416 
by (subst setsum_right_distrib, intro setsum.cong) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

417 
finally show ?thesis .. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

418 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

419 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

420 
lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

421 
using choose_row_sum[of n] by (simp add: atLeast0AtMost) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

422 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

423 
lemma natsum_reverse_index: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

424 
fixes m::nat 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

425 
shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n  k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

426 
by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+nk" and j="\<lambda>k. m+nk"]) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

427 

60758  428 
text\<open>NW diagonal sum property\<close> 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

429 
lemma sum_choose_diagonal: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

430 
assumes "m\<le>n" shows "(\<Sum>k=0..m. (nk) choose (mk)) = Suc n choose m" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

431 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

432 
have "(\<Sum>k=0..m. (nk) choose (mk)) = (\<Sum>k=0..m. (nm+k) choose k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

433 
by (rule natsum_reverse_index) (simp add: assms) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

434 
also have "... = Suc (nm+m) choose m" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

435 
by (rule sum_choose_lower) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

436 
also have "... = Suc n choose m" using assms 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

437 
by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

438 
finally show ?thesis . 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

439 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

440 

60758  441 
subsection\<open>Pochhammer's symbol : generalized rising factorial\<close> 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

442 

60758  443 
text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close> 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

444 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

445 
definition "pochhammer (a::'a::comm_semiring_1) n = 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

446 
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n  1})" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

447 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

448 
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

449 
by (simp add: pochhammer_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

450 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

451 
lemma pochhammer_1 [simp]: "pochhammer a 1 = a" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

452 
by (simp add: pochhammer_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

453 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

454 
lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

455 
by (simp add: pochhammer_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

456 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

457 
lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

458 
by (simp add: pochhammer_def) 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

459 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

460 
lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

461 
by (simp add: pochhammer_def of_nat_setprod) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

462 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

463 
lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

464 
by (simp add: pochhammer_def of_int_setprod) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

465 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

466 
lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

467 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

468 
have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

469 
then show ?thesis by (simp add: field_simps) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

470 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

471 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

472 
lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

473 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

474 
have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

475 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

476 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

477 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

478 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

479 
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

480 
proof (cases n) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

481 
case 0 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

482 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

483 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

484 
case (Suc n) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

485 
show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc .. 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

486 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

487 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

488 
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

489 
proof (cases "n = 0") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

490 
case True 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

491 
then show ?thesis by (simp add: pochhammer_Suc_setprod) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

492 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

493 
case False 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

494 
have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

495 
have eq: "insert 0 {1 .. n} = {0..n}" by auto 
61076  496 
have **: "(\<Prod>n\<in>{1::nat..n}. a + of_nat n) = (\<Prod>n\<in>{0::nat..n  1}. a + 1 + of_nat n)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

497 
apply (rule setprod.reindex_cong [where l = Suc]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

498 
using False 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

499 
apply (auto simp add: fun_eq_iff field_simps) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

500 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

501 
show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

502 
apply (simp add: pochhammer_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

503 
unfolding setprod.insert [OF *, unfolded eq] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

504 
using ** apply (simp add: field_simps) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

505 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

506 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

507 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

508 
lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

509 
proof (induction n arbitrary: z) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

510 
case (Suc n z) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

511 
have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

512 
by (simp add: pochhammer_rec) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

513 
also note Suc 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

514 
also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

515 
(z + of_nat (Suc n)) * pochhammer z (Suc n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

516 
by (simp_all add: pochhammer_rec algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

517 
finally show ?case . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

518 
qed simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

519 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

520 
lemma pochhammer_fact: "fact n = pochhammer 1 n" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

521 
unfolding fact_altdef 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

522 
apply (cases n) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

523 
apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

524 
apply (rule setprod.reindex_cong [where l = Suc]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

525 
apply (auto simp add: fun_eq_iff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

526 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

527 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

528 
lemma pochhammer_of_nat_eq_0_lemma: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

529 
assumes "k > n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

530 
shows "pochhammer ( (of_nat n :: 'a:: idom)) k = 0" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

531 
proof (cases "n = 0") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

532 
case True 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

533 
then show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

534 
using assms by (cases k) (simp_all add: pochhammer_rec) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

535 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

536 
case False 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

537 
from assms obtain h where "k = Suc h" by (cases k) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

538 
then show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

539 
by (simp add: pochhammer_Suc_setprod) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

540 
(metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1)) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

541 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

542 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

543 
lemma pochhammer_of_nat_eq_0_lemma': 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

544 
assumes kn: "k \<le> n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

545 
shows "pochhammer ( (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

546 
proof (cases k) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

547 
case 0 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

548 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

549 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

550 
case (Suc h) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

551 
then show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

552 
apply (simp add: pochhammer_Suc_setprod) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

553 
using Suc kn apply (auto simp add: algebra_simps) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

554 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

555 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

556 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

557 
lemma pochhammer_of_nat_eq_0_iff: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

558 
shows "pochhammer ( (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

559 
(is "?l = ?r") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

560 
using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

561 
pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

562 
by (auto simp add: not_le[symmetric]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

563 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

564 
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a =  of_nat k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

565 
apply (auto simp add: pochhammer_of_nat_eq_0_iff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

566 
apply (cases n) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

567 
apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

568 
apply (metis leD not_less_eq) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

569 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

570 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

571 
lemma pochhammer_eq_0_mono: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

572 
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

573 
unfolding pochhammer_eq_0_iff by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

574 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

575 
lemma pochhammer_neq_0_mono: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

576 
"pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

577 
unfolding pochhammer_eq_0_iff by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

578 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

579 
lemma pochhammer_minus: 
59862  580 
"pochhammer ( b) k = (( 1) ^ k :: 'a::comm_ring_1) * pochhammer (b  of_nat k + 1) k" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

581 
proof (cases k) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

582 
case 0 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

583 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

584 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

585 
case (Suc h) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

586 
have eq: "(( 1) ^ Suc h :: 'a) = (\<Prod>i=0..h.  1)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

587 
using setprod_constant[where A="{0 .. h}" and y=" 1 :: 'a"] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

588 
by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

589 
show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

590 
unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

591 
by (rule setprod.reindex_bij_witness[where i="op  h" and j="op  h"]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

592 
(auto simp: of_nat_diff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

593 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

594 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

595 
lemma pochhammer_minus': 
59862  596 
"pochhammer (b  of_nat k + 1) k = (( 1) ^ k :: 'a::comm_ring_1) * pochhammer ( b) k" 
597 
unfolding pochhammer_minus[where b=b] 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

598 
unfolding mult.assoc[symmetric] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

599 
unfolding power_add[symmetric] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

600 
by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

601 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

602 
lemma pochhammer_same: "pochhammer ( of_nat n) n = 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

603 
(( 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)" 
59862  604 
unfolding pochhammer_minus 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

605 
by (simp add: of_nat_diff pochhammer_fact) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

606 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

607 
lemma pochhammer_product': 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

608 
"pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

609 
proof (induction n arbitrary: z) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

610 
case (Suc n z) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

611 
have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

612 
z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

613 
by (simp add: pochhammer_rec ac_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

614 
also note Suc[symmetric] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

615 
also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

616 
by (subst pochhammer_rec) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

617 
finally show ?case by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

618 
qed simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

619 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

620 
lemma pochhammer_product: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

621 
"m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n  m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

622 
using pochhammer_product'[of z m "n  m"] by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

623 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

624 
lemma pochhammer_absorb_comp: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

625 
"((r :: 'a :: comm_ring_1)  of_nat k) * pochhammer ( r) k = r * pochhammer (r + 1) k" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

626 
(is "?lhs = ?rhs") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

627 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

628 
have "?lhs = pochhammer (r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

629 
also have "\<dots> = ?rhs" by (subst pochhammer_rec) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

630 
finally show ?thesis . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

631 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

632 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

633 

60758  634 
subsection\<open>Generalized binomial coefficients\<close> 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

635 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

636 
definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

637 
where "a gchoose n = 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

638 
(if n = 0 then 1 else (setprod (\<lambda>i. a  of_nat i) {0 .. n  1}) / (fact n))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

639 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

640 
lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset

641 
by (simp_all add: gbinomial_def) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

642 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

643 
lemma gbinomial_pochhammer: "a gchoose n = ( 1) ^ n * pochhammer ( a) n / (fact n)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

644 
proof (cases "n = 0") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

645 
case True 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

646 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

647 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

648 
case False 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

649 
from this setprod_constant[of "{0 .. n  1}" " (1:: 'a)"] 
61076  650 
have eq: "( (1::'a)) ^ n = setprod (\<lambda>i.  1) {0 .. n  1}" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

651 
by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

652 
from False show ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

653 
by (simp add: pochhammer_def gbinomial_def field_simps 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

654 
eq setprod.distrib[symmetric]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

655 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

656 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

657 
lemma binomial_gbinomial: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

658 
"of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

659 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

660 
{ assume kn: "k > n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

661 
then have ?thesis 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

662 
by (subst binomial_eq_0[OF kn]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

663 
(simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff) } 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

664 
moreover 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

665 
{ assume "k=0" then have ?thesis by simp } 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

666 
moreover 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

667 
{ assume kn: "k \<le> n" and k0: "k\<noteq> 0" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

668 
from k0 obtain h where h: "k = Suc h" by (cases k) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

669 
from h 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

670 
have eq:"( 1 :: 'a) ^ k = setprod (\<lambda>i.  1) {0..h}" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

671 
by (subst setprod_constant) auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

672 
have eq': "(\<Prod>i\<in>{0..h}. of_nat n +  (of_nat i :: 'a)) = (\<Prod>i\<in>{n  h..n}. of_nat i)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

673 
using h kn 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

674 
by (intro setprod.reindex_bij_witness[where i="op  n" and j="op  n"]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

675 
(auto simp: of_nat_diff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

676 
have th0: "finite {1..n  Suc h}" "finite {n  h .. n}" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

677 
"{1..n  Suc h} \<inter> {n  h .. n} = {}" and 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

678 
eq3: "{1..n  Suc h} \<union> {n  h .. n} = {1..n}" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

679 
using h kn by auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

680 
from eq[symmetric] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

681 
have ?thesis using kn 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

682 
apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

683 
gbinomial_pochhammer field_simps pochhammer_Suc_setprod) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

684 
apply (simp add: pochhammer_Suc_setprod fact_altdef h 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

685 
of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

686 
unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h] 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

687 
unfolding mult.assoc 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

688 
unfolding setprod.distrib[symmetric] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

689 
apply simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

690 
apply (intro setprod.reindex_bij_witness[where i="op  n" and j="op  n"]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

691 
apply (auto simp: of_nat_diff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

692 
done 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

693 
} 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

694 
moreover 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

695 
have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

696 
ultimately show ?thesis by blast 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

697 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

698 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

699 
lemma gbinomial_1[simp]: "a gchoose 1 = a" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

700 
by (simp add: gbinomial_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

701 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

702 
lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

703 
by (simp add: gbinomial_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

704 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

705 
lemma gbinomial_mult_1: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

706 
fixes a :: "'a :: field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

707 
shows "a * (a gchoose n) = 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

708 
of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

709 
proof  
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

710 
have "?r = (( 1) ^n * pochhammer ( a) n / (fact n)) * (of_nat n  ( a + of_nat n))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

711 
unfolding gbinomial_pochhammer 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

712 
pochhammer_Suc of_nat_mult right_diff_distrib power_Suc 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

713 
apply (simp del: of_nat_Suc fact.simps) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

714 
apply (auto simp add: field_simps simp del: of_nat_Suc) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

715 
done 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

716 
also have "\<dots> = ?l" unfolding gbinomial_pochhammer 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

717 
by (simp add: field_simps) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

718 
finally show ?thesis .. 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

719 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

720 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

721 
lemma gbinomial_mult_1': 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

722 
fixes a :: "'a :: field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

723 
shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

724 
by (simp add: mult.commute gbinomial_mult_1) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

725 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

726 
lemma gbinomial_Suc: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

727 
"a gchoose (Suc k) = (setprod (\<lambda>i. a  of_nat i) {0 .. k}) / (fact (Suc k))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

728 
by (simp add: gbinomial_def) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

729 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

730 
lemma gbinomial_mult_fact: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

731 
fixes a :: "'a::field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

732 
shows 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

733 
"fact (Suc k) * (a gchoose (Suc k)) = 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

734 
(setprod (\<lambda>i. a  of_nat i) {0 .. k})" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

735 
by (simp_all add: gbinomial_Suc field_simps del: fact.simps) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

736 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

737 
lemma gbinomial_mult_fact': 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

738 
fixes a :: "'a::field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

739 
shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a  of_nat i) {0 .. k})" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

740 
using gbinomial_mult_fact[of k a] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

741 
by (subst mult.commute) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

742 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

743 
lemma gbinomial_Suc_Suc: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

744 
fixes a :: "'a :: field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

745 
shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

746 
proof (cases k) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

747 
case 0 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

748 
then show ?thesis by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

749 
next 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

750 
case (Suc h) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

751 
have eq0: "(\<Prod>i\<in>{1..k}. (a + 1)  of_nat i) = (\<Prod>i\<in>{0..h}. a  of_nat i)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

752 
apply (rule setprod.reindex_cong [where l = Suc]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

753 
using Suc 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

754 
apply auto 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

755 
done 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

756 
have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) = 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

757 
(a gchoose Suc h) * (fact (Suc (Suc h))) + 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

758 
(a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

759 
by (simp add: Suc field_simps del: fact.simps) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

760 
also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

761 
(\<Prod>i = 0..Suc h. a  of_nat i)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

762 
by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

763 
also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

764 
(\<Prod>i = 0..Suc h. a  of_nat i)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

765 
by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

766 
also have "... = of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a  of_nat i) + 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

767 
(\<Prod>i = 0..Suc h. a  of_nat i)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

768 
by (metis gbinomial_mult_fact mult.commute) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

769 
also have "... = (\<Prod>i = 0..Suc h. a  of_nat i) + 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

770 
(of_nat h * (\<Prod>i = 0..h. a  of_nat i) + 2 * (\<Prod>i = 0..h. a  of_nat i))" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

771 
by (simp add: field_simps) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

772 
also have "... = 
61076  773 
((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0::nat..Suc h}. a  of_nat i)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

774 
unfolding gbinomial_mult_fact' 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

775 
by (simp add: comm_semiring_class.distrib field_simps Suc) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

776 
also have "\<dots> = (\<Prod>i\<in>{0..h}. a  of_nat i) * (a + 1)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

777 
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

778 
by (simp add: field_simps Suc) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

779 
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1)  of_nat i)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

780 
using eq0 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

781 
by (simp add: Suc setprod_nat_ivl_1_Suc) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

782 
also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

783 
unfolding gbinomial_mult_fact .. 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

784 
finally show ?thesis 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

785 
by (metis fact_nonzero mult_cancel_left) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

786 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

787 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

788 
lemma gbinomial_reduce_nat: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

789 
fixes a :: "'a :: field_char_0" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

790 
shows "0 < k \<Longrightarrow> a gchoose k = (a  1) gchoose (k  1) + ((a  1) gchoose k)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

791 
by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

792 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

793 
lemma gchoose_row_sum_weighted: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

794 
fixes r :: "'a::field_char_0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

795 
shows "(\<Sum>k = 0..m. (r gchoose k) * (r/2  of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

796 
proof (induct m) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

797 
case 0 show ?case by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

798 
next 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

799 
case (Suc m) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

800 
from Suc show ?case 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

801 
by (simp add: algebra_simps distrib gbinomial_mult_1) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

802 
qed 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

803 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

804 
lemma binomial_symmetric: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

805 
assumes kn: "k \<le> n" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

806 
shows "n choose k = n choose (n  k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

807 
proof 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

808 
from kn have kn': "n  k \<le> n" by arith 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

809 
from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

810 
have "fact k * fact (n  k) * (n choose k) = 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

811 
fact (n  k) * fact (n  (n  k)) * (n choose (n  k))" by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

812 
then show ?thesis using kn by simp 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

813 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

814 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

815 
lemma choose_rising_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

816 
"(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

817 
"(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

818 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

819 
show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

820 
also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

821 
finally show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

822 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

823 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

824 
lemma choose_linear_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

825 
"(\<Sum>i\<le>n. i * (n choose i)) = n * 2 ^ (n  1)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

826 
proof (cases n) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

827 
case (Suc m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

828 
have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

829 
also have "... = Suc m * 2 ^ m" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

830 
by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

831 
(simp add: choose_row_sum') 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

832 
finally show ?thesis using Suc by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

833 
qed simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

834 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

835 
lemma choose_alternating_linear_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

836 
assumes "n \<noteq> 1" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

837 
shows "(\<Sum>i\<le>n. (1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

838 
proof (cases n) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

839 
case (Suc m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

840 
with assms have "m > 0" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

841 
have "(\<Sum>i\<le>n. (1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

842 
(\<Sum>i\<le>Suc m. (1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

843 
also have "... = (\<Sum>i\<le>m. (1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

844 
by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

845 
also have "... = of_nat (Suc m) * (\<Sum>i\<le>m. (1) ^ i * of_nat ((m choose i)))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

846 
by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

847 
(simp add: algebra_simps of_nat_mult) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

848 
also have "(\<Sum>i\<le>m. (1 :: 'a) ^ i * of_nat ((m choose i))) = 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

849 
using choose_alternating_sum[OF `m > 0`] by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

850 
finally show ?thesis by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

851 
qed simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

852 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

853 
lemma vandermonde: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

854 
"(\<Sum>k\<le>r. (m choose k) * (n choose (r  k))) = (m + n) choose r" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

855 
proof (induction n arbitrary: r) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

856 
case 0 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

857 
have "(\<Sum>k\<le>r. (m choose k) * (0 choose (r  k))) = (\<Sum>k\<le>r. if k = r then (m choose k) else 0)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

858 
by (intro setsum.cong) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

859 
also have "... = m choose r" by (simp add: setsum.delta) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

860 
finally show ?case by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

861 
next 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

862 
case (Suc n r) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

863 
show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

864 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

865 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

866 
lemma choose_square_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

867 
"(\<Sum>k\<le>n. (n choose k)^2) = ((2*n) choose n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

868 
using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

869 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

870 
lemma pochhammer_binomial_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

871 
fixes a b :: "'a :: comm_ring_1" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

872 
shows "pochhammer (a + b) n = (\<Sum>k\<le>n. of_nat (n choose k) * pochhammer a k * pochhammer b (n  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

873 
proof (induction n arbitrary: a b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

874 
case (Suc n a b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

875 
have "(\<Sum>k\<le>Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n  k)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

876 
(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n  i)) + 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

877 
((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n  i)) + 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

878 
pochhammer b (Suc n))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

879 
by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

880 
also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n  i)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

881 
a * pochhammer ((a + 1) + b) n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

882 
by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

883 
also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n  i)) + pochhammer b (Suc n) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

884 
(\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n  i))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

885 
by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

886 
also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n  i))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

887 
using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

888 
also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n  i)))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

889 
by (intro setsum.cong) (simp_all add: Suc_diff_le) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

890 
also have "... = b * pochhammer (a + (b + 1)) n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

891 
by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

892 
also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

893 
pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

894 
finally show ?case .. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

895 
qed simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

896 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

897 

60758  898 
text\<open>Contributed by Manuel Eberl, generalised by LCP. 
899 
Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n  i) / (k  i)"}\<close> 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

900 
lemma gbinomial_altdef_of_nat: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

901 
fixes k :: nat 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset

902 
and x :: "'a :: {field_char_0,field}" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

903 
shows "x gchoose k = (\<Prod>i<k. (x  of_nat i) / of_nat (k  i) :: 'a)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

904 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

905 
have "(x gchoose k) = (\<Prod>i<k. x  of_nat i) / of_nat (fact k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

906 
unfolding gbinomial_def 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

907 
by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

908 
also have "\<dots> = (\<Prod>i<k. (x  of_nat i) / of_nat (k  i) :: 'a)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

909 
unfolding fact_eq_rev_setprod_nat of_nat_setprod 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

910 
by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric]) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

911 
finally show ?thesis . 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

912 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

913 

651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

914 
lemma gbinomial_ge_n_over_k_pow_k: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

915 
fixes k :: nat 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset

916 
and x :: "'a :: linordered_field" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

917 
assumes "of_nat k \<le> x" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

918 
shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

919 
proof  
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

920 
have x: "0 \<le> x" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

921 
using assms of_nat_0_le_iff order_trans by blast 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

922 
have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

923 
by (simp add: setprod_constant) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

924 
also have "\<dots> \<le> x gchoose k" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

925 
unfolding gbinomial_altdef_of_nat 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

926 
proof (safe intro!: setprod_mono) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

927 
fix i :: nat 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

928 
assume ik: "i < k" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

929 
from assms have "x * of_nat i \<ge> of_nat (i * k)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

930 
by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

931 
then have "x * of_nat k  x * of_nat i \<le> x * of_nat k  of_nat (i * k)" by arith 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

932 
then have "x * of_nat (k  i) \<le> (x  of_nat i) * of_nat k" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

933 
using ik 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

934 
by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

935 
then have "x * of_nat (k  i) \<le> (x  of_nat i) * (of_nat k :: 'a)" 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

936 
unfolding of_nat_mult[symmetric] of_nat_le_iff . 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

937 
with assms show "x / of_nat k \<le> (x  of_nat i) / (of_nat (k  i) :: 'a)" 
60758  938 
using \<open>i < k\<close> by (simp add: field_simps) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

939 
qed (simp add: x zero_le_divide_iff) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

940 
finally show ?thesis . 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

941 
qed 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

942 

61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

943 
lemma gbinomial_negated_upper: "(a gchoose b) = (1) ^ b * ((of_nat b  a  1) gchoose b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

944 
by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

945 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

946 
lemma gbinomial_minus: "((a) gchoose b) = (1) ^ b * ((a + of_nat b  1) gchoose b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

947 
by (subst gbinomial_negated_upper) (simp add: add_ac) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

948 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

949 
lemma Suc_times_gbinomial: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

950 
"of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

951 
proof (cases b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

952 
case (Suc b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

953 
hence "((a + 1) gchoose (Suc (Suc b))) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

954 
(\<Prod>i = 0..Suc b. a + (1  of_nat i)) / fact (b + 2)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

955 
by (simp add: field_simps gbinomial_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

956 
also have "(\<Prod>i = 0..Suc b. a + (1  of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a  of_nat i)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

957 
by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

958 
also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

959 
by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

960 
finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

961 
qed simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

962 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

963 
lemma gbinomial_factors: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

964 
"((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

965 
proof (cases b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

966 
case (Suc b) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

967 
hence "((a + 1) gchoose (Suc (Suc b))) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

968 
(\<Prod>i = 0..Suc b. a + (1  of_nat i)) / fact (b + 2)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

969 
by (simp add: field_simps gbinomial_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

970 
also have "(\<Prod>i = 0..Suc b. a + (1  of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a  of_nat i)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

971 
by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

972 
also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

973 
by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

974 
finally show ?thesis by (simp add: Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

975 
qed simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

976 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

977 
lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

978 
using gbinomial_mult_1[of r k] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

979 
by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

980 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

981 
lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n  k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

982 
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

983 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

984 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

985 
text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

986 
{r \choose k} = \frac{r}{k}{r  1 \choose k  1},\quad \textnormal{integer } k \neq 0. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

987 
\]\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

988 
lemma gbinomial_absorption': 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

989 
"k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r  1 gchoose (k  1))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

990 
using gbinomial_rec[of "r  1" "k  1"] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

991 
by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

992 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

993 
text \<open>The absorption identity is written in the following form to avoid 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

994 
division by $k$ (the lower index) and therefore remove the $k \neq 0$ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

995 
restriction\cite[p.~157]{GKP}:\[ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

996 
k{r \choose k} = r{r  1 \choose k  1}, \quad \textnormal{integer } k. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

997 
\]\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

998 
lemma gbinomial_absorption: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

999 
"of_nat (Suc k) * (r gchoose Suc k) = r * ((r  1) gchoose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1000 
using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1001 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1002 
text \<open>The absorption identity for natural number binomial coefficients:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1003 
lemma binomial_absorption: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1004 
"Suc k * (n choose Suc k) = n * ((n  1) choose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1005 
by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1006 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1007 
text \<open>The absorption companion identity for natural number coefficients, 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1008 
following the proof by GKP \cite[p.~157]{GKP}:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1009 
lemma binomial_absorb_comp: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1010 
"(n  k) * (n choose k) = n * ((n  1) choose k)" (is "?lhs = ?rhs") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1011 
proof (cases "n \<le> k") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1012 
case False 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1013 
then have "?rhs = Suc ((n  1)  k) * (n choose Suc ((n  1)  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1014 
using binomial_symmetric[of k "n  1"] binomial_absorption[of "(n  1)  k" n] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1015 
by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1016 
also from False have "Suc ((n  1)  k) = n  k" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1017 
also from False have "n choose \<dots> = n choose k" by (intro binomial_symmetric [symmetric]) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1018 
finally show ?thesis .. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1019 
qed auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1020 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1021 
text \<open>The generalised absorption companion identity:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1022 
lemma gbinomial_absorb_comp: "(r  of_nat k) * (r gchoose k) = r * ((r  1) gchoose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1023 
using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1024 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1025 
lemma gbinomial_addition_formula: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1026 
"r gchoose (Suc k) = ((r  1) gchoose (Suc k)) + ((r  1) gchoose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1027 
using gbinomial_Suc_Suc[of "r  1" k] by (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1028 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1029 
lemma binomial_addition_formula: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1030 
"0 < n \<Longrightarrow> n choose (Suc k) = ((n  1) choose (Suc k)) + ((n  1) choose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1031 
by (subst choose_reduce_nat) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1032 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1033 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1034 
text \<open> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1035 
Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1036 
summation formula, operating on both indices:\[ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1037 
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1038 
\quad \textnormal{integer } n. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1039 
\] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1040 
\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1041 
lemma gbinomial_parallel_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1042 
"(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1043 
proof (induction n) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1044 
case (Suc m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1045 
thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1046 
qed auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1047 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1048 
subsection \<open>Summation on the upper index\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1049 
text \<open> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1050 
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP}, 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1051 
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1052 
{n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1053 
\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1054 
lemma gbinomial_sum_up_index: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1055 
"(\<Sum>k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1056 
proof (induction n) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1057 
case 0 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1058 
show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1059 
next 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1060 
case (Suc n) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1061 
thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1062 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1063 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1064 
lemma gbinomial_index_swap: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1065 
"((1) ^ m) * (( (of_nat n)  1) gchoose m) = ((1) ^ n) * (( (of_nat m)  1) gchoose n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1066 
(is "?lhs = ?rhs") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1067 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1068 
have "?lhs = (of_nat (m + n) gchoose m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1069 
by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1070 
also have "\<dots> = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1071 
also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1072 
finally show ?thesis . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1073 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1074 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1075 
lemma gbinomial_sum_lower_neg: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1076 
"(\<Sum>k\<le>m. (r gchoose k) * ( 1) ^ k) = ( 1) ^ m * (r  1 gchoose m)" (is "?lhs = ?rhs") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1077 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1078 
have "?lhs = (\<Sum>k\<le>m. (r + 1) + of_nat k gchoose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1079 
by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1080 
also have "\<dots> = r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1081 
also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1082 
finally show ?thesis . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1083 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1084 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1085 
lemma gbinomial_partial_row_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1086 
"(\<Sum>k\<le>m. (r gchoose k) * ((r / 2)  of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1087 
proof (induction m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1088 
case (Suc mm) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1089 
hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2  of_nat k)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1090 
(r  of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1091 
also have "\<dots> = r * (r  1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1092 
also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1093 
by (subst gbinomial_absorption [symmetric]) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1094 
finally show ?case . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1095 
qed simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1096 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1097 
lemma setsum_bounds_lt_plus1: "(\<Sum>k<mm. f (Suc k)) = (\<Sum>k=1..mm. f k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1098 
by (induction mm) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1099 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1100 
lemma gbinomial_partial_sum_poly: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1101 
"(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(mk)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1102 
(\<Sum>k\<le>m. (r gchoose k) * (x)^k * (x + y)^(mk))" (is "?lhs m = ?rhs m") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1103 
proof (induction m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1104 
case (Suc mm) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1105 
def G \<equiv> "\<lambda>i k. (of_nat i + r gchoose k) * x^k * y^(ik)" and S \<equiv> ?lhs 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1106 
have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))" unfolding S_def G_def .. 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1107 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1108 
have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1109 
using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1110 
also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1111 
by (subst setsum_shift_bounds_cl_Suc_ivl) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1112 
also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + r gchoose (Suc k)) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1113 
+ (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1114 
unfolding G_def by (subst gbinomial_addition_formula) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1115 
also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm  k)) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1116 
+ (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1117 
by (subst setsum.distrib [symmetric]) (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1118 
also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm  k)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1119 
(\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1120 
by (simp only: atLeast0AtMost lessThan_Suc_atMost) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1121 
also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mmk)) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1122 
+ (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1123 
by (subst setsum_lessThan_Suc) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1124 
also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm  k + 1))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1125 
proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1126 
fix k assume "k < mm" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1127 
hence "mm  k = mm  Suc k + 1" by linarith 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1128 
thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm  k) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1129 
(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm  Suc k + 1)" by (simp only:) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1130 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1131 
also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1132 
unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1133 
also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm  k)) = x * (S mm)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1134 
unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1135 
also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1136 
finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k))) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1137 
+ (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1138 
by (simp add: ring_distribs) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1139 
also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1140 
by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1141 
finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1142 
by (simp add: algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1143 
also have "(of_nat mm + r gchoose (Suc mm)) = (1) ^ (Suc mm) * (r gchoose (Suc mm))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1144 
by (subst gbinomial_negated_upper) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1145 
also have "(1) ^ Suc mm * ( r gchoose Suc mm) * x ^ Suc mm = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1146 
(r gchoose (Suc mm)) * (x) ^ Suc mm" by (simp add: power_minus[of x]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1147 
also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (r gchoose (Suc mm)) * (x)^Suc mm" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1148 
unfolding S_def by (subst Suc.IH) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1149 
also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. (( r gchoose n) * ( x) ^ n * (x + y) ^ (Suc mm  n)))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1150 
by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1151 
also have "\<dots> + (r gchoose (Suc mm)) * (x)^Suc mm = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1152 
(\<Sum>n\<le>Suc mm. ( r gchoose n) * ( x) ^ n * (x + y) ^ (Suc mm  n))" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1153 
finally show ?case unfolding S_def . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1154 
qed simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1155 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1156 
lemma gbinomial_partial_sum_poly_xpos: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1157 
"(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(mk)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1158 
(\<Sum>k\<le>m. (of_nat k + r  1 gchoose k) * x^k * (x + y)^(mk))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1159 
apply (subst gbinomial_partial_sum_poly) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1160 
apply (subst gbinomial_negated_upper) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1161 
apply (intro setsum.cong, rule refl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1162 
apply (simp add: power_mult_distrib [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1163 
done 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1164 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1165 
lemma setsum_nat_symmetry: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1166 
"(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m  k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1167 
by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m  i" and j="\<lambda>i. m  i"]) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1168 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1169 
lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1170 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1171 
have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1172 
using choose_row_sum[where n="2 * m + 1"] by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1173 
also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\<Sum>k = 0..m. (2 * m + 1 choose k)) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1174 
+ (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1175 
using setsum_ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1176 
also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) = 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1177 
(\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1178 
by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1179 
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m  k)))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1180 
by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1181 
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1182 
by (subst (2) setsum_nat_symmetry) (rule refl) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1183 
also have "\<dots> + \<dots> = 2 * \<dots>" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1184 
finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1185 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1186 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1187 
lemma gbinomial_r_part_sum: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1188 
"(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1189 
proof  