author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58917  a3be9a47e2d7 
child 59557  ebd8ecacfba6 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/Binomial.thy 
31719  2 
Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow 
3 

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

4 
Defines the "choose" function, and establishes basic properties. 
31719  5 
*) 
6 

58889  7 
section {* Binomial *} 
31719  8 

9 
theory Binomial 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

10 
imports Cong Fact Complex_Main 
31719  11 
begin 
12 

13 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

14 
text {* This development is based on the work of Andy Gordon and 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

15 
Florian Kammueller. *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

16 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

17 
subsection {* Basic definitions and lemmas *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

18 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

19 
primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

20 
where 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

21 
"0 choose k = (if k = 0 then 1 else 0)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

22 
 "Suc n choose k = (if k = 0 then 1 else (n choose (k  1)) + (n choose k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

23 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

24 
lemma binomial_n_0 [simp]: "(n choose 0) = 1" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

25 
by (cases n) simp_all 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

26 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

27 
lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

28 
by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

29 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

30 
lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

31 
by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

32 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

33 
lemma choose_reduce_nat: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

34 
"0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow> 
58833
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

35 
(n choose k) = ((n  1) choose (k  1)) + ((n  1) choose k)" 
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

36 
by (metis Suc_diff_1 binomial.simps(2) neq0_conv) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

37 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

38 
lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

39 
by (induct n arbitrary: k) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

40 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

41 
declare binomial.simps [simp del] 
31719  42 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

43 
lemma binomial_n_n [simp]: "n choose n = 1" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

44 
by (induct n) (simp_all add: binomial_eq_0) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

45 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

46 
lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

47 
by (induct n) simp_all 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

48 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

49 
lemma binomial_1 [simp]: "n choose Suc 0 = n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

50 
by (induct n) simp_all 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

51 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

52 
lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

53 
by (induct n k rule: diff_induct) simp_all 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

54 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

55 
lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

56 
by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) 
31719  57 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

58 
lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

59 
by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

60 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

61 
lemma Suc_times_binomial_eq: 
58917
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

62 
"Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" 
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

63 
apply (induct n arbitrary: k, simp add: binomial.simps) 
58841
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

64 
apply (case_tac k) 
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

65 
apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

66 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

67 

58841
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

68 
text{*The absorption property*} 
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

69 
lemma Suc_times_binomial: 
58917
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

70 
"Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" 
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

71 
using Suc_times_binomial_eq by auto 
58841
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

72 

e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

73 
text{*This is the wellknown version of absorption, but it's harder to use because of the 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

74 
need to reason about division.*} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

75 
lemma binomial_Suc_Suc_eq_times: 
58917
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

76 
"(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

77 
by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) 
31719  78 

58841
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

79 
text{*Another version of absorption, with 1 instead of Suc.*} 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

80 
lemma times_binomial_minus1_eq: 
58917
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

81 
"0 < k \<Longrightarrow> k * (n choose k) = n * ((n  1) choose (k  1))" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

82 
using Suc_times_binomial_eq [where n = "n  1" and k = "k  1"] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

83 
by (auto split add: nat_diff_split) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

84 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

85 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

86 
subsection {* Combinatorial theorems involving @{text "choose"} *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

87 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

88 
text {*By Florian Kamm\"uller, tidied by LCP.*} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

89 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

90 
lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

91 
by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

92 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

93 
lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow> 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

94 
{s. s \<subseteq> insert x M \<and> card s = Suc k} = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

95 
{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}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

96 
apply safe 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

97 
apply (auto intro: finite_subset [THEN card_insert_disjoint]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

98 
by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

99 
card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

100 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

101 
lemma finite_bex_subset [simp]: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

102 
assumes "finite B" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

103 
and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

104 
shows "finite {x. \<exists>A \<subseteq> B. P x A}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

105 
by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets) 
31719  106 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

107 
text{*There are as many subsets of @{term A} having cardinality @{term k} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

108 
as there are sets obtained from the former by inserting a fixed element 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

109 
@{term x} into each.*} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

110 
lemma constr_bij: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

111 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

112 
card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

113 
card {B. B \<subseteq> A & card(B) = k}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

114 
apply (rule card_bij_eq [where f = "\<lambda>s. s  {x}" and g = "insert x"]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

115 
apply (auto elim!: equalityE simp add: inj_on_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

116 
apply (metis card_Diff_singleton_if finite_subset in_mono) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

117 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

118 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

119 
text {* 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

120 
Main theorem: combinatorial statement about number of subsets of a set. 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

121 
*} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

122 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

123 
theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

124 
proof (induct k arbitrary: A) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

125 
case 0 then show ?case by (simp add: card_s_0_eq_empty) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

126 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

127 
case (Suc k) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

128 
show ?case using `finite A` 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

129 
proof (induct A) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

130 
case empty show ?case by (simp add: card_s_0_eq_empty) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

131 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

132 
case (insert x A) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

133 
then show ?case using Suc.hyps 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

134 
apply (simp add: card_s_0_eq_empty choose_deconstruct) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

135 
apply (subst card_Un_disjoint) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

136 
prefer 4 apply (force simp add: constr_bij) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

137 
prefer 3 apply force 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

138 
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] 
55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55130
diff
changeset

139 
finite_subset [of _ "Pow (insert x F)" for F]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

140 
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

141 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

142 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

143 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

144 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

145 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

146 
subsection {* The binomial theorem (courtesy of Tobias Nipkow): *} 
31719  147 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

148 
text{* Avigad's version, generalized to any commutative ring *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

149 
theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

150 
(\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(nk))" (is "?P n") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

151 
proof (induct n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

152 
case 0 then show "?P 0" by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

153 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

154 
case (Suc n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

155 
have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

156 
by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

157 
have decomp2: "{0..n} = {0} Un {1..n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

158 
by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

159 
have "(a+b)^(n+1) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

160 
(a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

161 
using Suc.hyps by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

162 
also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk)) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

163 
b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

164 
by (rule distrib) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

165 
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(nk)) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

166 
(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(nk+1))" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

167 
by (auto simp add: setsum_right_distrib ac_simps) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

168 
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1k)) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

169 
(\<Sum>k=1..n+1. of_nat (n choose (k  1)) * a^k * b^(n+1k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

170 
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

171 
del:setsum_cl_ivl_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

172 
also have "\<dots> = a^(n+1) + b^(n+1) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

173 
(\<Sum>k=1..n. of_nat (n choose (k  1)) * a^k * b^(n+1k)) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

174 
(\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

175 
by (simp add: decomp2) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

176 
also have 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

177 
"\<dots> = a^(n+1) + b^(n+1) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

178 
(\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1k))" 
57418  179 
by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

180 
also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

181 
using decomp by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

182 
finally show "?P (Suc n)" by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

183 
qed 
31719  184 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

185 
text{* Original version for the naturals *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

186 
corollary binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(nk))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

187 
using binomial_ring [of "int a" "int b" n] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

188 
by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

189 
of_nat_setsum [symmetric] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

190 
of_nat_eq_iff of_nat_id) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

191 

56178  192 
lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n" 
193 
using binomial [of 1 "1" n] 

194 
by (simp add: numeral_2_eq_2) 

195 

196 
lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n" 

197 
by (induct n) auto 

198 

199 
lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m" 

200 
by (induct n) auto 

201 

202 
lemma natsum_reverse_index: 

203 
fixes m::nat 

57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

204 
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)" 
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

205 
by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+nk" and j="\<lambda>k. m+nk"]) auto 
56178  206 

58841
e16712bb1d41
Some comments and a new version of a result
paulson <lp15@cam.ac.uk>
parents:
58833
diff
changeset

207 
text{*NW diagonal sum property*} 
56178  208 
lemma sum_choose_diagonal: 
209 
assumes "m\<le>n" shows "(\<Sum>k=0..m. (nk) choose (mk)) = Suc n choose m" 

210 
proof  

211 
have "(\<Sum>k=0..m. (nk) choose (mk)) = (\<Sum>k=0..m. (nm+k) choose k)" 

212 
by (rule natsum_reverse_index) (simp add: assms) 

213 
also have "... = Suc (nm+m) choose m" 

214 
by (rule sum_choose_lower) 

215 
also have "... = Suc n choose m" using assms 

216 
by simp 

217 
finally show ?thesis . 

218 
qed 

219 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

220 
subsection{* Pochhammer's symbol : generalized rising factorial *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

221 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

222 
text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

223 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

224 
definition "pochhammer (a::'a::comm_semiring_1) n = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

225 
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n  1})" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

226 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

227 
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

228 
by (simp add: pochhammer_def) 
31719  229 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

230 
lemma pochhammer_1 [simp]: "pochhammer a 1 = a" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

231 
by (simp add: pochhammer_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

232 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

233 
lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

234 
by (simp add: pochhammer_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

235 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

236 
lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

237 
by (simp add: pochhammer_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

238 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

239 
lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

240 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

241 
have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

242 
then show ?thesis by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

243 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

244 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

245 
lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

246 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

247 
have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

248 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

249 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

250 

31719  251 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

252 
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

253 
proof (cases n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

254 
case 0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

255 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

256 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

257 
case (Suc n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

258 
show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc .. 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

259 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

260 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

261 
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

262 
proof (cases "n = 0") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

263 
case True 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

264 
then show ?thesis by (simp add: pochhammer_Suc_setprod) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

265 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

266 
case False 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

267 
have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

268 
have eq: "insert 0 {1 .. n} = {0..n}" by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

269 
have **: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = (\<Prod>n\<in>{0\<Colon>nat..n  1}. a + 1 + of_nat n)" 
57418  270 
apply (rule setprod.reindex_cong [where l = Suc]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

271 
using False 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

272 
apply (auto simp add: fun_eq_iff field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

273 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

274 
show ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

275 
apply (simp add: pochhammer_def) 
57418  276 
unfolding setprod.insert [OF *, unfolded eq] 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

277 
using ** apply (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

278 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

279 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

280 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

281 
lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

282 
unfolding fact_altdef_nat 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

283 
apply (cases n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

284 
apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod) 
57418  285 
apply (rule setprod.reindex_cong [where l = Suc]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

286 
apply (auto simp add: fun_eq_iff) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

287 
done 
44872  288 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

289 
lemma pochhammer_of_nat_eq_0_lemma: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

290 
assumes "k > n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

291 
shows "pochhammer ( (of_nat n :: 'a:: idom)) k = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

292 
proof (cases "n = 0") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

293 
case True 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

294 
then show ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

295 
using assms by (cases k) (simp_all add: pochhammer_rec) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

296 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

297 
case False 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

298 
from assms obtain h where "k = Suc h" by (cases k) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

299 
then show ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

300 
by (simp add: pochhammer_Suc_setprod) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

301 
(metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1)) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

302 
qed 
31719  303 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

304 
lemma pochhammer_of_nat_eq_0_lemma': 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

305 
assumes kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

306 
shows "pochhammer ( (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

307 
proof (cases k) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

308 
case 0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

309 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

310 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

311 
case (Suc h) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

312 
then show ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

313 
apply (simp add: pochhammer_Suc_setprod) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

314 
using Suc kn apply (auto simp add: algebra_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

315 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

316 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

317 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

318 
lemma pochhammer_of_nat_eq_0_iff: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

319 
shows "pochhammer ( (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

320 
(is "?l = ?r") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

321 
using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

322 
pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

323 
by (auto simp add: not_le[symmetric]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

324 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

325 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

326 
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a =  of_nat k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

327 
apply (auto simp add: pochhammer_of_nat_eq_0_iff) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

328 
apply (cases n) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

329 
apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

330 
apply (metis leD not_less_eq) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

331 
done 
31719  332 

333 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

334 
lemma pochhammer_eq_0_mono: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

335 
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

336 
unfolding pochhammer_eq_0_iff by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

337 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

338 
lemma pochhammer_neq_0_mono: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

339 
"pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

340 
unfolding pochhammer_eq_0_iff by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

341 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

342 
lemma pochhammer_minus: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

343 
assumes kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

344 
shows "pochhammer ( b) k = (( 1) ^ k :: 'a::comm_ring_1) * pochhammer (b  of_nat k + 1) k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

345 
proof (cases k) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

346 
case 0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

347 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

348 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

349 
case (Suc h) 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

350 
have eq: "(( 1) ^ Suc h :: 'a) = (\<Prod>i=0..h.  1)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

351 
using setprod_constant[where A="{0 .. h}" and y=" 1 :: 'a"] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

352 
by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

353 
show ?thesis 
57418  354 
unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric] 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

355 
by (rule setprod.reindex_bij_witness[where i="op  h" and j="op  h"]) 
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

356 
(auto simp: of_nat_diff) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

357 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

358 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

359 
lemma pochhammer_minus': 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

360 
assumes kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

361 
shows "pochhammer (b  of_nat k + 1) k = (( 1) ^ k :: 'a::comm_ring_1) * pochhammer ( b) k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

362 
unfolding pochhammer_minus[OF kn, where b=b] 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

363 
unfolding mult.assoc[symmetric] 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

364 
unfolding power_add[symmetric] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

365 
by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

366 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

367 
lemma pochhammer_same: "pochhammer ( of_nat n) n = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

368 
(( 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

369 
unfolding pochhammer_minus[OF le_refl[of n]] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

370 
by (simp add: of_nat_diff pochhammer_fact) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

371 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

372 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

373 
subsection{* Generalized binomial coefficients *} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

374 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

375 
definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

376 
where "a gchoose n = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

377 
(if n = 0 then 1 else (setprod (\<lambda>i. a  of_nat i) {0 .. n  1}) / of_nat (fact n))" 
31719  378 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

379 
lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

380 
apply (simp_all add: gbinomial_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

381 
apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}.  of_nat i) = (0::'b)") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

382 
apply (simp del:setprod_zero_iff) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

383 
apply simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

384 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

385 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

386 
lemma gbinomial_pochhammer: "a gchoose n = ( 1) ^ n * pochhammer ( a) n / of_nat (fact n)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

387 
proof (cases "n = 0") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

388 
case True 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

389 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

390 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

391 
case False 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

392 
from this setprod_constant[of "{0 .. n  1}" " (1:: 'a)"] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

393 
have eq: "( (1\<Colon>'a)) ^ n = setprod (\<lambda>i.  1) {0 .. n  1}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

394 
by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

395 
from False show ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

396 
by (simp add: pochhammer_def gbinomial_def field_simps 
57418  397 
eq setprod.distrib[symmetric]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

398 
qed 
31719  399 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

400 
lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n  k) * (n choose k) = fact n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

401 
proof (induct n arbitrary: k rule: nat_less_induct) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

402 
fix n k assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m  x) * (m choose x) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

403 
fact m" and kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

404 
let ?ths = "fact k * fact (n  k) * (n choose k) = fact n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

405 
{ assume "n=0" then have ?ths using kn by simp } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

406 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

407 
{ assume "k=0" then have ?ths using kn by simp } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

408 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

409 
{ assume nk: "n=k" then have ?ths by simp } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

410 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

411 
{ fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

412 
from n have mn: "m < n" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

413 
from hm have hm': "h \<le> m" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

414 
from hm h n kn have km: "k \<le> m" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

415 
have "m  h = Suc (m  Suc h)" using h km hm by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

416 
with km h have th0: "fact (m  h) = (m  h) * fact (m  k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

417 
by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

418 
from n h th0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

419 
have "fact k * fact (n  k) * (n choose k) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

420 
k * (fact h * fact (m  h) * (m choose h)) + 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

421 
(m  h) * (fact k * fact (m  k) * (m choose k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

422 
by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

423 
also have "\<dots> = (k + (m  h)) * fact m" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

424 
using H[rule_format, OF mn hm'] H[rule_format, OF mn km] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

425 
by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

426 
finally have ?ths using h n km by simp } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

427 
moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

428 
using kn by presburger 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

429 
ultimately show ?ths by blast 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

430 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

431 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

432 
lemma binomial_fact: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

433 
assumes kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

434 
shows "(of_nat (n choose k) :: 'a::field_char_0) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

435 
of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n  k)))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

436 
using binomial_fact_lemma[OF kn] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

437 
by (simp add: field_simps of_nat_mult [symmetric]) 
31719  438 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

439 
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

440 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

441 
{ assume kn: "k > n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

442 
then have ?thesis 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

443 
by (subst binomial_eq_0[OF kn]) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

444 
(simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff) } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

445 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

446 
{ assume "k=0" then have ?thesis by simp } 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

447 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

448 
{ assume kn: "k \<le> n" and k0: "k\<noteq> 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

449 
from k0 obtain h where h: "k = Suc h" by (cases k) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

450 
from h 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

451 
have eq:"( 1 :: 'a) ^ k = setprod (\<lambda>i.  1) {0..h}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

452 
by (subst setprod_constant) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

453 
have eq': "(\<Prod>i\<in>{0..h}. of_nat n +  (of_nat i :: 'a)) = (\<Prod>i\<in>{n  h..n}. of_nat i)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

454 
using h kn 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

455 
by (intro setprod.reindex_bij_witness[where i="op  n" and j="op  n"]) 
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

456 
(auto simp: of_nat_diff) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

457 
have th0: "finite {1..n  Suc h}" "finite {n  h .. n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

458 
"{1..n  Suc h} \<inter> {n  h .. n} = {}" and 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

459 
eq3: "{1..n  Suc h} \<union> {n  h .. n} = {1..n}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

460 
using h kn by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

461 
from eq[symmetric] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

462 
have ?thesis using kn 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

463 
apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

464 
gbinomial_pochhammer field_simps pochhammer_Suc_setprod) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

465 
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h 
57418  466 
of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc) 
467 
unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h] 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

468 
unfolding mult.assoc[symmetric] 
57418  469 
unfolding setprod.distrib[symmetric] 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

470 
apply simp 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

471 
apply (intro setprod.reindex_bij_witness[where i="op  n" and j="op  n"]) 
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56178
diff
changeset

472 
apply (auto simp: of_nat_diff) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

473 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

474 
} 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

475 
moreover 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

476 
have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

477 
ultimately show ?thesis by blast 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

478 
qed 
31719  479 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

480 
lemma gbinomial_1[simp]: "a gchoose 1 = a" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

481 
by (simp add: gbinomial_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

482 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

483 
lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

484 
by (simp add: gbinomial_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

485 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

486 
lemma gbinomial_mult_1: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

487 
"a * (a gchoose n) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

488 
of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

489 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

490 
have "?r = (( 1) ^n * pochhammer ( a) n / of_nat (fact n)) * (of_nat n  ( a + of_nat n))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

491 
unfolding gbinomial_pochhammer 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

492 
pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

493 
by (simp add: field_simps del: of_nat_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

494 
also have "\<dots> = ?l" unfolding gbinomial_pochhammer 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

495 
by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

496 
finally show ?thesis .. 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

497 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

498 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

499 
lemma gbinomial_mult_1': 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

500 
"(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

501 
by (simp add: mult.commute gbinomial_mult_1) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

502 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

503 
lemma gbinomial_Suc: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

504 
"a gchoose (Suc k) = (setprod (\<lambda>i. a  of_nat i) {0 .. k}) / of_nat (fact (Suc k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

505 
by (simp add: gbinomial_def) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

506 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

507 
lemma gbinomial_mult_fact: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

508 
"(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

509 
(setprod (\<lambda>i. a  of_nat i) {0 .. k})" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

510 
by (simp_all add: gbinomial_Suc field_simps del: fact_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

511 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

512 
lemma gbinomial_mult_fact': 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

513 
"((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

514 
(setprod (\<lambda>i. a  of_nat i) {0 .. k})" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

515 
using gbinomial_mult_fact[of k a] 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

516 
by (subst mult.commute) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

517 

31719  518 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

519 
lemma gbinomial_Suc_Suc: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

520 
"((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

521 
proof (cases k) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

522 
case 0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

523 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

524 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

525 
case (Suc h) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

526 
have eq0: "(\<Prod>i\<in>{1..k}. (a + 1)  of_nat i) = (\<Prod>i\<in>{0..h}. a  of_nat i)" 
57418  527 
apply (rule setprod.reindex_cong [where l = Suc]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

528 
using Suc 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

529 
apply auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

530 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

531 
have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

532 
((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a  of_nat i)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

533 
apply (simp add: Suc field_simps del: fact_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

534 
unfolding gbinomial_mult_fact' 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

535 
apply (subst fact_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

536 
unfolding of_nat_mult 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

537 
apply (subst mult.commute) 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

538 
unfolding mult.assoc 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

539 
unfolding gbinomial_mult_fact 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

540 
apply (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

541 
done 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

542 
also have "\<dots> = (\<Prod>i\<in>{0..h}. a  of_nat i) * (a + 1)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

543 
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

544 
by (simp add: field_simps Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

545 
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1)  of_nat i)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

546 
using eq0 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

547 
by (simp add: Suc setprod_nat_ivl_1_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

548 
also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

549 
unfolding gbinomial_mult_fact .. 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

550 
finally show ?thesis by (simp del: fact_Suc) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

551 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

552 

58833
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

553 
lemma gbinomial_reduce_nat: 
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

554 
"0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a  1) gchoose (k  1) + ((a  1) gchoose k)" 
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

555 
by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) 
09974789e483
choose_reduce_nat: reordered operands
paulson <lp15@cam.ac.uk>
parents:
58713
diff
changeset

556 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

557 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

558 
lemma binomial_symmetric: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

559 
assumes kn: "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

560 
shows "n choose k = n choose (n  k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

561 
proof 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

562 
from kn have kn': "n  k \<le> n" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

563 
from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

564 
have "fact k * fact (n  k) * (n choose k) = 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

565 
fact (n  k) * fact (n  (n  k)) * (n choose (n  k))" by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

566 
then show ?thesis using kn by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

567 
qed 
31719  568 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

569 
(* Contributed by Manuel Eberl *) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

570 
(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n  i) / (k  i) *) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

571 
lemma binomial_altdef_of_nat: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

572 
fixes n k :: nat 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

573 
and x :: "'a :: {field_char_0,field_inverse_zero}" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

574 
assumes "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

575 
shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n  i) / of_nat (k  i) :: 'a)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

576 
proof (cases "0 < k") 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

577 
case True 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

578 
then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n  of_nat i) / of_nat (fact k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

579 
unfolding binomial_gbinomial gbinomial_def 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

580 
by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

581 
also have "\<dots> = (\<Prod>i<k. of_nat (n  i) / of_nat (k  i) :: 'a)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

582 
using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod 
57418  583 
by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric]) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

584 
finally show ?thesis . 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

585 
next 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

586 
case False 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

587 
then show ?thesis by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

588 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

589 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

590 
lemma binomial_ge_n_over_k_pow_k: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

591 
fixes k n :: nat 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

592 
and x :: "'a :: linordered_field_inverse_zero" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

593 
assumes "0 < k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

594 
and "k \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

595 
shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

596 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

597 
have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

598 
by (simp add: setprod_constant) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

599 
also have "\<dots> \<le> of_nat (n choose k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

600 
unfolding binomial_altdef_of_nat[OF `k\<le>n`] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

601 
proof (safe intro!: setprod_mono) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

602 
fix i :: nat 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

603 
assume "i < k" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

604 
from assms have "n * i \<ge> i * k" by simp 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

605 
then have "n * k  n * i \<le> n * k  i * k" by arith 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

606 
then have "n * (k  i) \<le> (n  i) * k" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

607 
by (simp add: diff_mult_distrib2 mult.commute) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

608 
then have "of_nat n * of_nat (k  i) \<le> of_nat (n  i) * (of_nat k :: 'a)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

609 
unfolding of_nat_mult[symmetric] of_nat_le_iff . 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

610 
with assms show "of_nat n / of_nat k \<le> of_nat (n  i) / (of_nat (k  i) :: 'a)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

611 
using `i < k` by (simp add: field_simps) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

612 
qed (simp add: zero_le_divide_iff) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

613 
finally show ?thesis . 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

614 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

615 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

616 
lemma binomial_le_pow: 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

617 
assumes "r \<le> n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

618 
shows "n choose r \<le> n ^ r" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

619 
proof  
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

620 
have "n choose r \<le> fact n div fact (n  r)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

621 
using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

622 
with fact_div_fact_le_pow [OF assms] show ?thesis by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

623 
qed 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

624 

70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

625 
lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

626 
n choose k = fact n div (fact k * fact (n  k))" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

627 
by (subst binomial_fact_lemma [symmetric]) auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

628 

58713  629 
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n  k) dvd fact n" 
630 
by (metis binomial_fact_lemma dvd_def) 

631 

632 
lemma choose_dvd_int: 

633 
assumes "(0::int) <= k" and "k <= n" 

634 
shows "fact k * fact (n  k) dvd fact n" 

635 
apply (subst tsub_eq [symmetric], rule assms) 

636 
apply (rule choose_dvd_nat [transferred]) 

637 
using assms apply auto 

638 
done 

56178  639 

640 
lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)" 

58713  641 
by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2) 
56178  642 

643 
lemma choose_mult_lemma: 

644 
"((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)" 

645 
proof  

646 
have "((m+r+k) choose (m+k)) * ((m+k) choose k) = 

647 
fact (m+r + k) div (fact (m + k) * fact (m+r  m)) * (fact (m + k) div (fact k * fact m))" 

648 
by (simp add: assms binomial_altdef_nat) 

649 
also have "... = fact (m+r+k) div (fact r * (fact k * fact m))" 

650 
apply (subst div_mult_div_if_dvd) 

651 
apply (auto simp: fact_fact_dvd_fact) 

58713  652 
apply (metis add.assoc add.commute fact_fact_dvd_fact) 
56178  653 
done 
654 
also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))" 

655 
apply (subst div_mult_div_if_dvd [symmetric]) 

656 
apply (auto simp: fact_fact_dvd_fact) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

657 
apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute) 
56178  658 
done 
659 
also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))" 

660 
apply (subst div_mult_div_if_dvd) 

661 
apply (auto simp: fact_fact_dvd_fact) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

662 
apply(metis mult.left_commute) 
56178  663 
done 
664 
finally show ?thesis 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

665 
by (simp add: binomial_altdef_nat mult.commute) 
56178  666 
qed 
667 

58917
a3be9a47e2d7
Tidying up. Removing unnecessary conditions from some theorems.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

668 
text{*The "Subset of a Subset" identity*} 
56178  669 
lemma choose_mult: 
670 
assumes "k\<le>m" "m\<le>n" 

671 
shows "(n choose m) * (m choose k) = (n choose k) * ((nk) choose (mk))" 

672 
using assms choose_mult_lemma [of "mk" "nm" k] 

673 
by simp 

31719  674 

675 

676 
subsection {* Binomial coefficients *} 

677 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

678 
lemma choose_one: "(n::nat) choose 1 = n" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

679 
by simp 
31719  680 

58713  681 
(*FIXME: messy and apparently unused*) 
31719  682 
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

683 
(ALL n. P (Suc n) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow> 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

684 
P (Suc n) (Suc k))) \<longrightarrow> (ALL k <= n. P n k)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

685 
apply (induct n) 
31719  686 
apply auto 
687 
apply (case_tac "k = 0") 

688 
apply auto 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

689 
apply (case_tac "k = Suc n") 
31719  690 
apply auto 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

691 
apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq) 
41541  692 
done 
31719  693 

51291  694 
lemma card_UNION: 
51292  695 
assumes "finite A" and "\<forall>k \<in> A. finite k" 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

696 
shows "card (\<Union>A) = nat (\<Sum>I  I \<subseteq> A \<and> I \<noteq> {}. ( 1) ^ (card I + 1) * int (card (\<Inter>I)))" 
51291  697 
(is "?lhs = ?rhs") 
698 
proof  

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

699 
have "?rhs = nat (\<Sum>I  I \<subseteq> A \<and> I \<noteq> {}. ( 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

700 
also have "\<dots> = nat (\<Sum>I  I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. ( 1) ^ (card I + 1)))" (is "_ = nat ?rhs") 
51292  701 
by(subst setsum_right_distrib) simp 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

702 
also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. ( 1) ^ (card I + 1))" 
57418  703 
using assms by(subst setsum.Sigma)(auto) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

704 
also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). ( 1) ^ (card I + 1))" 
57418  705 
by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

706 
also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). ( 1) ^ (card I + 1))" 
57418  707 
using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"]) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

708 
also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>II \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. ( 1) ^ (card I + 1)))" 
57418  709 
using assms by(subst setsum.Sigma) auto 
51291  710 
also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _") 
57418  711 
proof(rule setsum.cong[OF refl]) 
51291  712 
fix x 
713 
assume x: "x \<in> \<Union>A" 

714 
def K \<equiv> "{X \<in> A. x \<in> X}" 

715 
with `finite A` have K: "finite K" by auto 

716 
let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}" 

717 
have "inj_on snd (SIGMA i:{1..card A}. ?I i)" 

718 
using assms by(auto intro!: inj_onI) 

719 
moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}" 

55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55130
diff
changeset

720 
using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a] 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55130
diff
changeset

721 
simp add: card_gt_0_iff[folded Suc_le_eq] 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55130
diff
changeset

722 
dest: finite_subset intro: card_mono) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

723 
ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). ( 1) ^ (i + 1))" 
57418  724 
by (rule setsum.reindex_cong [where l = snd]) fastforce 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

725 
also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>II \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. ( 1) ^ (i + 1)))" 
57418  726 
using assms by(subst setsum.Sigma) auto 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

727 
also have "\<dots> = (\<Sum>i=1..card A. ( 1) ^ (i + 1) * (\<Sum>II \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))" 
51292  728 
by(subst setsum_right_distrib) simp 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

729 
also have "\<dots> = (\<Sum>i=1..card K. ( 1) ^ (i + 1) * (\<Sum>II \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs") 
57418  730 
proof(rule setsum.mono_neutral_cong_right[rule_format]) 
51291  731 
show "{1..card K} \<subseteq> {1..card A}" using `finite A` 
732 
by(auto simp add: K_def intro: card_mono) 

733 
next 

734 
fix i 

735 
assume "i \<in> {1..card A}  {1..card K}" 

736 
hence i: "i \<le> card A" "card K < i" by auto 

737 
have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" 

738 
by(auto simp add: K_def) 

739 
also have "\<dots> = {}" using `finite A` i 

740 
by(auto simp add: K_def dest: card_mono[rotated 1]) 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

741 
finally show "( 1) ^ (i + 1) * (\<Sum>I  I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0" 
51291  742 
by(simp only:) simp 
743 
next 

744 
fix i 

745 
have "(\<Sum>I  I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I  I \<subseteq> K \<and> card I = i. 1 :: int)" 

746 
(is "?lhs = ?rhs") 

57418  747 
by(rule setsum.cong)(auto simp add: K_def) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

748 
thus "( 1) ^ (i + 1) * ?lhs = ( 1) ^ (i + 1) * ?rhs" by simp 
51291  749 
qed simp 
750 
also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms 

751 
by(auto simp add: card_eq_0_iff K_def dest: finite_subset) 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

752 
hence "?rhs = (\<Sum>i = 0..card K. ( 1) ^ (i + 1) * (\<Sum>I  I \<subseteq> K \<and> card I = i. 1 :: int)) + 1" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

753 
by(subst (2) setsum_head_Suc)(simp_all ) 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

754 
also have "\<dots> = (\<Sum>i = 0..card K. ( 1) * (( 1) ^ i * int (card K choose i))) + 1" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
53374
diff
changeset

755 
using K by(subst n_subsets[symmetric]) simp_all 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58194
diff
changeset

756 
also have "\<dots> =  (\<Sum>i = 0..card K. ( 1) ^ i * int (card K choose i)) + 1" 
51292  757 
by(subst setsum_right_distrib[symmetric]) simp 
51291  758 
also have "\<dots> =  ((1 + 1) ^ card K) + 1" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

759 
by(subst binomial_ring)(simp add: ac_simps) 
51291  760 
also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff) 
761 
finally show "?lhs x = 1" . 

762 
qed 

763 
also have "nat \<dots> = card (\<Union>A)" by simp 

764 
finally show ?thesis .. 

765 
qed 

766 

58193  767 
text{* The number of nat lists of length @{text m} summing to @{text N} is 
768 
@{term "(N + m  1) choose N"}: *} 

769 

770 
lemma card_length_listsum_rec: 

771 
assumes "m\<ge>1" 

772 
shows "card {l::nat list. length l = m \<and> listsum l = N} = 

773 
(card {l. length l = (m  1) \<and> listsum l = N} + 

774 
card {l. length l = m \<and> listsum l + 1 = N})" 

775 
(is "card ?C = (card ?A + card ?B)") 

776 
proof  

777 
let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}" 

778 
let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}" 

779 
let ?f ="\<lambda> l. 0#l" 

780 
let ?g ="\<lambda> l. (hd l + 1) # tl l" 

781 
have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp 

782 
have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs  hd xs" 

783 
by(auto simp add: neq_Nil_conv) 

784 
have f: "bij_betw ?f ?A ?A'" 

785 
apply(rule bij_betw_byWitness[where f' = tl]) 

786 
using assms 

787 
by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv) 

788 
have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs  hd xs) = listsum xs" 

789 
by (metis 1 listsum_simps(2) 2) 

790 
have g: "bij_betw ?g ?B ?B'" 

791 
apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l  1) # tl l"]) 

792 
using assms 

793 
by (auto simp: 2 length_0_conv[symmetric] intro!: 3 

794 
simp del: length_greater_0_conv length_0_conv) 

795 
{ fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" 

796 
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto } 

797 
note fin = this 

798 
have fin_A: "finite ?A" using fin[of _ "N+1"] 

799 
by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m  1 \<and> set xs \<subseteq> {0..<N+1}}"], 

800 
auto simp: member_le_listsum_nat less_Suc_eq_le) 

801 
have fin_B: "finite ?B" 

802 
by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"], 

803 
auto simp: member_le_listsum_nat less_Suc_eq_le fin) 

804 
have uni: "?C = ?A' \<union> ?B'" by auto 

805 
have disj: "?A' \<inter> ?B' = {}" by auto 

806 
have "card ?C = card(?A' \<union> ?B')" using uni by simp 

807 
also have "\<dots> = card ?A + card ?B" 

808 
using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g] 

809 
bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B 

810 
by presburger 

811 
finally show ?thesis . 

812 
qed 

813 

58194
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

814 
lemma card_length_listsum: "By Holden Lee, tidied by Tobias Nipkow" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

815 
"card {l::nat list. size l = m \<and> listsum l = N} = (N + m  1) choose N" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

816 
proof (cases m) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

817 
case 0 then show ?thesis 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

818 
by (cases N) (auto simp: cong: conj_cong) 
58193  819 
next 
58194
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

820 
case (Suc m') 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

821 
have m: "m\<ge>1" by (simp add: Suc) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

822 
then show ?thesis 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

823 
proof (induct "N + m  1" arbitrary: N m) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

824 
case 0  "In the base case, the only solution is [0]." 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

825 
have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

826 
by (auto simp: length_Suc_conv) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

827 
have "m=1 \<and> N=0" using 0 by linarith 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

828 
then show ?case by simp 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

829 
next 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

830 
case (Suc k) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

831 

3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

832 
have c1: "card {l::nat list. size l = (m  1) \<and> listsum l = N} = 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

833 
(N + (m  1)  1) choose N" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

834 
proof cases 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

835 
assume "m = 1" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

836 
with Suc.hyps have "N\<ge>1" by auto 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

837 
with `m = 1` show ?thesis by (simp add: binomial_eq_0) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

838 
next 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

839 
assume "m \<noteq> 1" thus ?thesis using Suc by fastforce 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

840 
qed 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

841 

3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

842 
from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

843 
(if N>0 then ((N  1) + m  1) choose (N  1) else 0)" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

844 
proof  
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

845 
have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n  1" by arith 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

846 
from Suc have "N>0 \<Longrightarrow> 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

847 
card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

848 
((N  1) + m  1) choose (N  1)" by (simp add: aux) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

849 
thus ?thesis by auto 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

850 
qed 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

851 

3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

852 
from Suc.prems have "(card {l::nat list. size l = (m  1) \<and> listsum l = N} + 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

853 
card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m  1) choose N" 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

854 
by (auto simp: c1 c2 choose_reduce_nat[of "N + m  1" N] simp del: One_nat_def) 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

855 
thus ?case using card_length_listsum_rec[OF Suc.prems] by auto 
3d90a96fd6a9
Generalised card_length_listsum to all m
paulson <lp15@cam.ac.uk>
parents:
58193
diff
changeset

856 
qed 
58193  857 
qed 
858 

31719  859 
end 