author  eberlm 
Thu, 16 Jun 2016 17:57:09 +0200  
changeset 63306  ca187a9f66da 
parent 63092  a949b2a5f51d 
child 63363  bd483ddb17f2 
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. 
61554  6 
Additional binomial identities by Chaitanya Mangla and Manuel Eberl 
12196  7 
*) 
8 

60758  9 
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

10 

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

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

14 

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

16 

61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

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

18 
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

19 

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

20 
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

21 

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

22 
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

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

24 

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

25 
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

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

27 

62347  28 
lemma of_nat_fact [simp]: 
29 
"of_nat (fact n) = fact n" 

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

30 
by (induct n) (auto simp add: algebra_simps of_nat_mult) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

31 

62347  32 
lemma of_int_fact [simp]: 
33 
"of_int (fact n) = fact n" 

34 
proof  

35 
have "of_int (of_nat (fact n)) = fact n" 

36 
unfolding of_int_of_nat_eq by simp 

37 
then show ?thesis 

38 
by simp 

39 
qed 

40 

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

41 
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

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

43 

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

44 
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

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

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

47 
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

48 

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

49 
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

50 
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

51 

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

52 
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

53 

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

54 
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

55 

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

56 
context 
60241  57 
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

58 
begin 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

59 

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

60 
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

61 
by (metis of_nat_fact of_nat_le_iff fact_mono_nat) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

62 

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

63 
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

64 
by (metis le0 fact.simps(1) fact_mono) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

65 

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

66 
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

67 
using fact_ge_1 less_le_trans zero_less_one by blast 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

68 

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

69 
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

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

71 

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

72 
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

73 
by (simp add: not_less_iff_gr_or_eq) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

74 

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

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

76 
"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

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

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

79 
then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61554
diff
changeset

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

81 
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

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

83 
also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61554
diff
changeset

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

85 
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

86 
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

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

88 
qed simp 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

89 

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

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

91 

60758  92 
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

93 
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

94 
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

95 

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

96 
lemma fact_less_mono: 
60241  97 
"\<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

98 
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

99 

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

100 
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

101 
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

102 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

104 
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

105 
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

106 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

107 
lemma fact_ge_self: "fact n \<ge> n" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

108 
by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

109 

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

110 
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

111 
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

112 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

113 
lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

114 
by (induct n) (auto simp: atLeastAtMostSuc_conv) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

115 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

116 
lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61799
diff
changeset

117 
by (subst fact_altdef_nat [symmetric]) simp 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

118 

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

119 
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

120 
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

121 

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

122 
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

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

124 

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

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

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

127 
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

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

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

130 
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

131 
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

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

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

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

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

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

137 
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

138 
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

139 
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

140 
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

141 
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

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

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

144 
qed 
60758  145 
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

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

147 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

149 
"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

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

151 

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

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

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

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

156 
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

157 
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

158 
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

159 
have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n  r..n} = (n  r) * \<Prod>{Suc (n  r)..n}" 
57418  160 
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

161 
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

162 
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

163 
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

164 

61799  165 
lemma fact_numeral: \<comment>\<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

166 
"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

167 
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

168 

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

169 

60758  170 
text \<open>This development is based on the work of Andy Gordon and 
171 
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

172 

60758  173 
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

174 

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 
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

176 
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

177 
"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

178 
 "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

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 
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

181 
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

182 

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 
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

184 
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

185 

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 
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

187 
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

188 

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

189 
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

190 
"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

191 
(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

192 
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

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: "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

195 
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

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 
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

198 

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 
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

200 
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

201 

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 
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

203 
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

204 

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 
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

206 
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

207 

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

208 
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

209 
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

210 

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

211 
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

212 
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

213 

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

214 
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

215 
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

216 

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 
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

218 
"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

219 
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

220 
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

221 
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

222 
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

223 

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

224 
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

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

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

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

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

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

230 

60758  231 
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

232 
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

233 
"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

234 
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

235 

60758  236 
text\<open>This is the wellknown version of absorption, but it's harder to use because of the 
237 
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

238 
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

239 
"(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

240 
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

241 

60758  242 
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

243 
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

244 
"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

245 
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

246 
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

247 

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 

61799  249 
subsection \<open>Combinatorial theorems involving \<open>choose\<close>\<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

250 

60758  251 
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

252 

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

253 
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

254 
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

255 

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 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

257 
{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

258 
{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

259 
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

260 
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

261 
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

262 
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

263 

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 
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

265 
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

266 
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

267 
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

268 
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

269 

60758  270 
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

271 
as there are sets obtained from the former by inserting a fixed element 
60758  272 
@{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

273 
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

274 
"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

275 
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

276 
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

277 
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

278 
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

279 
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

280 
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

281 

60758  282 
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

283 
Main theorem: combinatorial statement about number of subsets of a set. 
60758  284 
\<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

285 

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 
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

287 
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

288 
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

289 
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

290 
case (Suc k) 
60758  291 
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

292 
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

293 
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

294 
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

295 
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

296 
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

297 
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

298 
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

299 
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

300 
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

301 
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

302 
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

303 
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

304 
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

305 
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

306 
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

307 

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 

60758  309 
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

310 

60758  311 
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

312 
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

313 
(\<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

314 
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

315 
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

316 
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

317 
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

318 
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

319 
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

320 
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

321 
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

322 
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

323 
(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

324 
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

325 
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

326 
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

327 
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

328 
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

329 
(\<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

330 
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

331 
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

332 
(\<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

333 
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

334 
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

335 
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

336 
(\<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

337 
(\<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

338 
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

339 
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

340 
"\<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

341 
(\<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

342 
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

343 
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

344 
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

345 
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

346 
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

347 

60758  348 
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

349 
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

350 
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

351 
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

352 
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

353 
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

354 

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 
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

356 
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

357 
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

358 
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

359 
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

360 
{ 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

361 
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

362 
{ 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

363 
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

364 
{ 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

365 
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

366 
{ 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

367 
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

368 
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

369 
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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
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

376 
(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

377 
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

378 
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

379 
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

380 
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

381 
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

382 
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

383 
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

384 
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

385 
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

386 

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

387 
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

388 
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

389 
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

390 
(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

391 
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

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

393 
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

394 

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

395 
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

396 
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

397 
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

398 

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

399 
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

400 
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

401 

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

402 
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

403 
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

404 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

406 
"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

407 
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

408 

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

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

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

411 
shows "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

413 
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

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

415 
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

416 
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

417 
by (simp add: setsum.distrib) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

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

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

422 

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

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

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

425 
shows "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

427 
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

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

429 
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

430 
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

431 
by (simp add: setsum_subtractf) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

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

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

436 

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

437 
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

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

439 

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

440 
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

441 
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

442 
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

443 
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

444 

60758  445 
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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

456 
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

457 

60758  458 
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

459 

60758  460 
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

461 

61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

462 
definition (in comm_semiring_1) "pochhammer (a :: 'a) 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

463 
(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

464 

651ea265d568
Removal of the 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 
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

466 
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

467 

651ea265d568
Removal of the 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 
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

469 
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

470 

651ea265d568
Removal of the 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 
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

472 
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

473 

651ea265d568
Removal of the 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 
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

475 
by (simp add: pochhammer_def) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

476 

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

477 
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

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

479 

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

480 
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

481 
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

482 

651ea265d568
Removal of the 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 
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

484 
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

485 
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

486 
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

487 
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

488 

651ea265d568
Removal of the 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 
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

490 
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

491 
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

492 
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

493 
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

494 

651ea265d568
Removal of the 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 

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

496 
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

497 
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

498 
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

499 
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

500 
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

501 
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

502 
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

503 
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

504 

651ea265d568
Removal of the 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 
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

506 
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

507 
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

508 
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

509 
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

510 
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

511 
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

512 
have eq: "insert 0 {1 .. n} = {0..n}" by auto 
61076  513 
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

514 
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

515 
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

516 
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

517 
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

518 
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

519 
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

520 
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

521 
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

522 
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

523 
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

524 

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

525 
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

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

527 
case (Suc n z) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

530 
also note Suc 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

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

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

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

536 

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

537 
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

538 
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

539 
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

540 
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

541 
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

542 
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

543 
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

544 

651ea265d568
Removal of the 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 
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

546 
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

547 
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

548 
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

549 
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

550 
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

551 
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

552 
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

553 
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

554 
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

555 
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

556 
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

557 
(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

558 
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

559 

651ea265d568
Removal of the 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 
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

561 
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

562 
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

563 
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

564 
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

565 
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

566 
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

567 
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

568 
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

569 
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

570 
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

571 
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

572 
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

573 

651ea265d568
Removal of the 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 
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

575 
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

576 
(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

577 
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

578 
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

579 
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

580 

651ea265d568
Removal of the 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 
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

582 
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

583 
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

584 
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

585 
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

586 
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

587 

651ea265d568
Removal of the 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 
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

589 
"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

590 
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

591 

651ea265d568
Removal of the 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 
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

593 
"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

594 
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

595 

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

596 
lemma pochhammer_minus: 
59862  597 
"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

598 
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

599 
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

600 
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

601 
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

602 
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

603 
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

604 
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

605 
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

606 
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

607 
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

608 
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

609 
(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

610 
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

611 

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

612 
lemma pochhammer_minus': 
59862  613 
"pochhammer (b  of_nat k + 1) k = (( 1) ^ k :: 'a::comm_ring_1) * pochhammer ( b) k" 
614 
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

615 
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

616 
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

617 
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

618 

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

619 
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

620 
(( 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)" 
59862  621 
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

622 
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

623 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

625 
"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

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

627 
case (Suc n z) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

629 
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

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

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

632 
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

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

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

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

636 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

638 
"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

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

640 

61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

641 
lemma pochhammer_times_pochhammer_half: 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

642 
fixes z :: "'a :: field_char_0" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

643 
shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

644 
proof (induction n) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

645 
case (Suc n) 
63044  646 
define n' where "n' = Suc n" 
61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

647 
have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') = 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

648 
(pochhammer z n' * pochhammer (z + 1 / 2) n') * 
61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

649 
((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A") 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

650 
by (simp_all add: pochhammer_rec' mult_ac) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

651 
also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

652 
(is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

653 
also note Suc[folded n'_def] 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

654 
also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

655 
by (simp add: setprod_nat_ivl_Suc) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

656 
finally show ?case by (simp add: n'_def) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

657 
qed (simp add: setprod_nat_ivl_Suc) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

658 

980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

659 
lemma pochhammer_double: 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

660 
fixes z :: "'a :: field_char_0" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

661 
shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

662 
proof (induction n) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

663 
case (Suc n) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

664 
have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * 
61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

665 
(2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

666 
by (simp add: pochhammer_rec' ac_simps of_nat_mult) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

667 
also note Suc 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

668 
also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n * 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

669 
(2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) = 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

670 
of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

671 
by (simp add: of_nat_mult field_simps pochhammer_rec') 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

672 
finally show ?case . 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

673 
qed simp 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

674 

63306
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63092
diff
changeset

675 
lemma fact_double: 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63092
diff
changeset

676 
"fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63092
diff
changeset

677 
using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63092
diff
changeset

678 

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

679 
lemma pochhammer_absorb_comp: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

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

683 
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

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

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

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

687 

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 

60758  689 
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

690 

61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

691 
definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65) 
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

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

693 
(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

694 

651ea265d568
Removal of the 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 
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

696 
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

697 

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

698 
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

699 
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

700 
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

701 
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

702 
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

703 
case False 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

704 
then have eq: "( 1) ^ n = (\<Prod>i = 0..n  1.  1)" 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

705 
by (auto simp add: setprod_constant) 
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

706 
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

707 
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

708 
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

709 
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

710 

61533
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

711 
lemma gbinomial_pochhammer': 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

712 
"(s :: 'a :: field_char_0) gchoose n = pochhammer (s  of_nat n + 1) n / fact n" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

713 
proof  
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

714 
have "s gchoose n = ((1)^n * (1)^n) * pochhammer (s  of_nat n + 1) n / fact n" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

715 
by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

716 
also have "(1 :: 'a)^n * (1)^n = 1" by (subst power_add [symmetric]) simp 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

717 
finally show ?thesis by simp 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

718 
qed 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61525
diff
changeset

719 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

721 
"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

722 
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

723 
{ 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

724 
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

725 
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

726 
(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

727 
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

728 
{ 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

729 
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

730 
{ 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

731 
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

732 
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

733 
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

734 
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

735 
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

736 
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

737 
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

738 
(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

739 
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

740 
"{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

741 
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

742 
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

743 
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

744 
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

745 
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

746 
gbinomial_pochhammer field_simps pochhammer_Suc_setprod) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

747 
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

748 
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

749 
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

750 
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

751 
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

752 
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

753 
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

754 
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

755 
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

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

757 
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

758 
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

759 
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

760 
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

761 

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

762 
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

763 
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

764 

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

765 
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

766 
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

767 

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

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

769 
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

770 
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

771 
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

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

773 
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

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

775 
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

776 
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

777 
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

778 
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

779 
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

780 
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

781 
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

782 
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

783 

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

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

785 
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

786 
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

787 
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

788 

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

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

790 
"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

791 
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

792 

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

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

794 
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

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

796 
"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

797 
(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

798 
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

799 

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

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

801 
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

802 
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

803 
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

804 
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

805 

651ea265d568
Removal of the 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 
lemma gbinomial_Suc_Suc: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

807 
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

808 
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

809 
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

810 
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

811 
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

812 
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

813 
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

814 
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

815 
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

816 
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

817 
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

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

819 
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

820 
(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

821 
(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

822 
by (simp add: Suc field_simps del: fact.simps) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

824 
(\<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

825 
by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

827 
(\<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

828 
by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

830 
(\<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

831 
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

832 
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

833 
(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

834 
by (simp add: field_simps) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

835 
also have "... = 
61076  836 
((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

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

838 
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

839 
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

840 
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

841 
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

842 
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

843 
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

844 
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

845 
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

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

847 
finally show ?thesis 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

848 
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

849 
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

850 

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

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

852 
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

853 
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

854 
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

855 

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

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

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

858 
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

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

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

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

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

863 
from Suc show ?case 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61649
diff
changeset

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

865 
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

866 

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

867 
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

868 
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

869 
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

870 
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

871 
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

872 
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

873 
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

874 
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

875 
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

876 
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

877 

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

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

879 
"(\<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

880 
"(\<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

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

882 
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

883 
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

884 
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

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

886 

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

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

888 
"(\<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

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

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

891 
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

892 
also have "... = Suc m * 2 ^ m" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

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

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

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

897 

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

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

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

900 
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

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

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

903 
with assms have "m > 0" by simp 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

905 
(\<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

906 
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

907 
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

908 
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

909 
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

910 
(simp add: algebra_simps of_nat_mult) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

911 
also have "(\<Sum>i\<le>m. (1 :: 'a) ^ i * of_nat ((m choose i))) = 0" 
61799  912 
using choose_alternating_sum[OF \<open>m > 0\<close>] by simp 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

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

915 

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

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

917 
"(\<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

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

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

920 
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

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

922 
also have "... = m choose r" by (simp add: setsum.delta) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

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

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

926 
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

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

928 

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

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

930 
"(\<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

931 
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

932 

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

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

934 
fixes a b :: "'a :: comm_ring_1" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

935 
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

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

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

938 
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

939 
(\<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

940 
((\<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

941 
pochhammer b (Suc n))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

942 
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

943 
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

944 
a * pochhammer ((a + 1) + b) n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

945 
by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

946 
also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n  i)) + pochhammer b (Suc n) = 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

947 
(\<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

948 
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

949 
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

950 
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

951 
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

952 
by (intro setsum.cong) (simp_all add: Suc_diff_le) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

953 
also have "... = b * pochhammer (a + (b + 1)) n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

954 
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

955 
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

956 
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

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

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

959 

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

960 

60758  961 
text\<open>Contributed by Manuel Eberl, generalised by LCP. 
962 
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

963 
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

964 
fixes k :: nat 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset

965 
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

966 
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

967 
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

968 
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

969 
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

970 
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

971 
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

972 
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

973 
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

974 
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

975 
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

976 

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

977 
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

978 
fixes k :: nat 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset

979 
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

980 
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

981 
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

982 
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

983 
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

984 
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

985 
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

986 
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

987 
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

988 
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

989 
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

990 
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

991 
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

992 
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

993 
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

994 
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

995 
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

996 
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

997 
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

998 
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

999 
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

1000 
with assms show "x / of_nat k \<le> (x  of_nat i) / (of_nat (k  i) :: 'a)" 
60758  1001 
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

1002 
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

1003 
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

1004 
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

1005 

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

1006 
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

1007 
by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1008 

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

1009 
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

1010 
by (subst gbinomial_negated_upper) (simp add: add_ac) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1011 

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

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

1013 
"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

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

1015 
case (Suc b) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1016 
hence "((a + 1) gchoose (Suc (Suc b))) = 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1017 
(\<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

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

1019 
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

1020 
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

1021 
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

1022 
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

1023 
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

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

1025 

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

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

1027 
"((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

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

1029 
case (Suc b) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1030 
hence "((a + 1) gchoose (Suc (Suc b))) = 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1031 
(\<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

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

1033 
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

1034 
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

1035 
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

1036 
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

1037 
finally show ?thesis by (simp add: Suc) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1038 
qed simp 
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 
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

1041 
using gbinomial_mult_1[of r k] 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1042 
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

1043 

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

1044 
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

1045 
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

1046 

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 
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

1049 
{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

1050 
\]\<close> 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

1052 
"k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r  1 gchoose (k  1))" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1053 
using gbinomial_rec[of "r  1" "k  1"] 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1054 
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

1055 

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

1056 
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

1057 
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

1058 
restriction\cite[p.~157]{GKP}:\[ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1059 
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

1060 
\]\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1062 
"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

1063 
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

1064 

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

1065 
text \<open>The absorption identity for natural number binomial coefficients:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1067 
"Suc k * (n choose Suc k) = n * ((n  1) choose k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1068 
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

1069 

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

1070 
text \<open>The absorption companion identity for natural number coefficients, 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1071 
following the proof by GKP \cite[p.~157]{GKP}:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1073 
"(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

1074 
proof (cases "n \<le> k") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1076 
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

1077 
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

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

1079 
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

1080 
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

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

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

1083 

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

1084 
text \<open>The generalised absorption companion identity:\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1085 
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

1086 
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

1087 

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

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

1089 
"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

1090 
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

1091 

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

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

1093 
"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

1094 
by (subst choose_reduce_nat) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1095 

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 
text \<open> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1098 
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

1099 
summation formula, operating on both indices:\[ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1100 
\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

1101 
\quad \textnormal{integer } n. 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

1103 
\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1105 
"(\<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

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

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

1108 
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

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

1110 

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

1111 
subsection \<open>Summation on the upper index\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1112 
text \<open> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1113 
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP}, 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1114 
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1115 
{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

1116 
\<close> 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

1118 
"(\<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

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

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

1121 
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

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

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

1124 
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

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

1126 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

1128 
"((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

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

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

1131 
have "?lhs = (of_nat (m + n) gchoose m)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1132 
by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1133 
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

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

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

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

1137 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

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

1139 
"(\<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

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

1141 
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

1142 
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

1143 
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

1144 
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

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

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

1147 

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

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

1149 
"(\<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

1150 
proof (induction m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1151 
case (Suc mm) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1152 
hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2  of_nat k)) = 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61649
diff
changeset

1153 
(r  of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps) 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1154 
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

1155 
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

1156 
by (subst gbinomial_absorption [symmetric]) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

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

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

1159 

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

1160 
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

1161 
by (induction mm) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1162 

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

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

1164 
"(\<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

1165 
(\<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

1166 
proof (induction m) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1167 
case (Suc mm) 
63044  1168 
define G where "G i k = (of_nat i + r gchoose k) * x^k * y^(ik)" for i k 
1169 
define S where "S = ?lhs" 

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

1170 
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

1171 

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

1172 
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

1173 
using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1174 
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

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

1176 
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

1177 
+ (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

1178 
unfolding G_def by (subst gbinomial_addition_formula) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1179 
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

1180 
+ (\<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

1181 
by (subst setsum.distrib [symmetric]) (simp add: algebra_simps) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1182 
also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm  k)) = 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1183 
(\<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

1184 
by (simp only: atLeast0AtMost lessThan_Suc_atMost) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62347
diff
changeset

1185 
also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mmk)) 
61525
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61076
diff
changeset

1186 
+ (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

1187 
by (subst setsum_lessThan_Suc) simp 