# HG changeset patch # User wenzelm # Date 1468353236 -7200 # Node ID 2100fbbdc3f1d66e43a319e0882dad08521601d1 # Parent d7610beb98bc978edb8b8721d7755d77f6b28fe4 misc tuning and modernization; diff -r d7610beb98bc -r 2100fbbdc3f1 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Tue Jul 12 20:03:18 2016 +0200 +++ b/src/HOL/Binomial.thy Tue Jul 12 21:53:56 2016 +0200 @@ -1,15 +1,15 @@ -(* Title : Binomial.thy - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Conversion to Isar and new proofs by Lawrence C Paulson, 2004 - Various additions by Jeremy Avigad. - Additional binomial identities by Chaitanya Mangla and Manuel Eberl +(* Title: HOL/Binomial.thy + Author: Jacques D. Fleuriot + Author: Lawrence C Paulson + Author: Jeremy Avigad + Author: Chaitanya Mangla + Author: Manuel Eberl *) section \Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\ theory Binomial -imports Main + imports Main begin subsection \Factorial\ @@ -18,17 +18,18 @@ begin definition fact :: "nat \ 'a" -where - fact_setprod: "fact n = of_nat (\{1..n})" + where fact_setprod: "fact n = of_nat (\{1..n})" -lemma fact_setprod_Suc: - "fact n = of_nat (setprod Suc {0..i = 0..i = 0..i. i" 1 n] - by (cases n) (simp_all add: fact_setprod_Suc setprod.atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost) + by (cases n) + (simp_all add: fact_setprod_Suc setprod.atLeast_Suc_atMost_Suc_shift + atLeastLessThanSuc_atLeastAtMost) lemma fact_0 [simp]: "fact 0 = 1" by (simp add: fact_setprod) @@ -42,24 +43,19 @@ lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n" by (simp add: fact_setprod atLeastAtMostSuc_conv algebra_simps) -lemma fact_2 [simp]: - "fact 2 = 2" +lemma fact_2 [simp]: "fact 2 = 2" by (simp add: numeral_2_eq_2) -lemma fact_split: - assumes "k \ n" - shows "fact n = of_nat (setprod Suc {n - k.. n \ fact n = of_nat (setprod Suc {n - k.. 0 \ fact n = of_nat n * fact (n - 1)" @@ -68,81 +64,87 @@ lemma fact_nonzero [simp]: "fact n \ (0::'a::{semiring_char_0,semiring_no_zero_divisors})" apply (induct n) apply auto - using of_nat_eq_0_iff by fastforce + using of_nat_eq_0_iff + apply fastforce + done lemma fact_mono_nat: "m \ n \ fact m \ (fact n :: nat)" by (induct n) (auto simp: le_Suc_eq) -lemma fact_in_Nats: "fact n \ \" by (induction n) auto +lemma fact_in_Nats: "fact n \ \" + by (induct n) auto -lemma fact_in_Ints: "fact n \ \" by (induction n) auto +lemma fact_in_Ints: "fact n \ \" + by (induct n) auto context assumes "SORT_CONSTRAINT('a::linordered_semidom)" begin - lemma fact_mono: "m \ n \ fact m \ (fact n :: 'a)" - by (metis of_nat_fact of_nat_le_iff fact_mono_nat) +lemma fact_mono: "m \ n \ fact m \ (fact n :: 'a)" + by (metis of_nat_fact of_nat_le_iff fact_mono_nat) - lemma fact_ge_1 [simp]: "fact n \ (1 :: 'a)" - by (metis le0 fact_0 fact_mono) +lemma fact_ge_1 [simp]: "fact n \ (1 :: 'a)" + by (metis le0 fact_0 fact_mono) - lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)" - using fact_ge_1 less_le_trans zero_less_one by blast +lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)" + using fact_ge_1 less_le_trans zero_less_one by blast - lemma fact_ge_zero [simp]: "fact n \ (0 :: 'a)" - by (simp add: less_imp_le) +lemma fact_ge_zero [simp]: "fact n \ (0 :: 'a)" + by (simp add: less_imp_le) - lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))" - by (simp add: not_less_iff_gr_or_eq) +lemma fact_not_neg [simp]: "\ fact n < (0 :: 'a)" + by (simp add: not_less_iff_gr_or_eq) - lemma fact_le_power: - "fact n \ (of_nat (n^n) ::'a)" - proof (induct n) - case (Suc n) - then have *: "fact n \ (of_nat (Suc n ^ n) ::'a)" - by (rule order_trans) (simp add: power_mono del: of_nat_power) - have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)" - by (simp add: algebra_simps) - also have "... \ (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)" - by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power) - also have "... \ (of_nat (Suc n ^ Suc n) ::'a)" - by (metis of_nat_mult order_refl power_Suc) - finally show ?case . - qed simp +lemma fact_le_power: "fact n \ (of_nat (n^n) :: 'a)" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + then have *: "fact n \ (of_nat (Suc n ^ n) ::'a)" + by (rule order_trans) (simp add: power_mono del: of_nat_power) + have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)" + by (simp add: algebra_simps) + also have "\ \ of_nat (Suc n) * of_nat (Suc n ^ n)" + by (simp add: * ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power) + also have "\ \ of_nat (Suc n ^ Suc n)" + by (metis of_nat_mult order_refl power_Suc) + finally show ?case . +qed end -text\Note that @{term "fact 0 = fact 1"}\ -lemma fact_less_mono_nat: "\0 < m; m < n\ \ fact m < (fact n :: nat)" +text \Note that @{term "fact 0 = fact 1"}\ +lemma fact_less_mono_nat: "0 < m \ m < n \ fact m < (fact n :: nat)" by (induct n) (auto simp: less_Suc_eq) -lemma fact_less_mono: - "\0 < m; m < n\ \ fact m < (fact n :: 'a::linordered_semidom)" +lemma fact_less_mono: "0 < m \ m < n \ fact m < (fact n :: 'a::linordered_semidom)" by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat) lemma fact_ge_Suc_0_nat [simp]: "fact n \ Suc 0" by (metis One_nat_def fact_ge_1) -lemma dvd_fact: - shows "1 \ m \ m \ n \ m dvd fact n" +lemma dvd_fact: "1 \ m \ m \ n \ m dvd fact n" by (induct n) (auto simp: dvdI le_Suc_eq) lemma fact_ge_self: "fact n \ n" by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact) -lemma fact_dvd: "n \ m \ fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})" +lemma fact_dvd: "n \ m \ fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})" by (induct m) (auto simp: le_Suc_eq) -lemma fact_mod: "m \ n \ fact n mod (fact m :: 'a :: {semiring_div,linordered_semidom}) = 0" +lemma fact_mod: "m \ n \ fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0" by (auto simp add: fact_dvd) lemma fact_div_fact: assumes "m \ n" - shows "(fact m) div (fact n) = \{n + 1..m}" + shows "fact m div fact n = \{n + 1..m}" proof - - obtain d where "d = m - n" by auto - from assms this have "m = n + d" by auto + obtain d where "d = m - n" + by auto + with assms have "m = n + d" + by auto have "fact (n + d) div (fact n) = \{n + 1..n + d}" proof (induct d) case 0 @@ -151,44 +153,41 @@ case (Suc d') have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n" by simp - also from Suc.hyps have "... = Suc (n + d') * \{n + 1..n + d'}" + also from Suc.hyps have "\ = Suc (n + d') * \{n + 1..n + d'}" unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod) - also have "... = \{n + 1..n + Suc d'}" + also have "\ = \{n + 1..n + Suc d'}" by (simp add: atLeastAtMostSuc_conv) finally show ?case . qed - from this \m = n + d\ show ?thesis by simp + with \m = n + d\ show ?thesis by simp qed -lemma fact_num_eq_if: - "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))" -by (cases m) auto +lemma fact_num_eq_if: "fact m = (if m = 0 then 1 else of_nat m * fact (m - 1))" + by (cases m) auto lemma fact_div_fact_le_pow: - assumes "r \ n" shows "fact n div fact (n - r) \ n ^ r" + assumes "r \ n" + shows "fact n div fact (n - r) \ n ^ r" proof - - have "\r. r \ n \ \{n - r..n} = (n - r) * \{Suc (n - r)..n}" + have "r \ n \ \{n - r..n} = (n - r) * \{Suc (n - r)..n}" for r by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL) with assms show ?thesis by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono) qed -lemma fact_numeral: \\Evaluation for specific numerals\ - "fact (numeral k) = (numeral k) * (fact (pred_numeral k))" +lemma fact_numeral: "fact (numeral k) = numeral k * fact (pred_numeral k)" + \ \Evaluation for specific numerals\ by (metis fact_Suc numeral_eq_Suc of_nat_numeral) -text \This development is based on the work of Andy Gordon and - Florian Kammueller.\ - - subsection \Binomial coefficients\ +text \This development is based on the work of Andy Gordon and Florian Kammueller.\ + text \Combinatorial definition\ -definition binomial :: "nat \ nat \ nat" (infixl "choose" 65) -where - "n choose k = card {K\Pow {0.. nat \ nat" (infixl "choose" 65) + where "n choose k = card {K\Pow {0.. {0.. card K = k}" by (rule inj_on_subset) then have "card {K. K \ {0.. card K = k} = - card (image f ` {K. K \ {0.. card K = k})" (is "_ = card ?C") + card (image f ` {K. K \ {0.. card K = k})" (is "_ = card ?C") by (simp add: card_image) also have "?C = {K. K \ f ` {0.. card K = k}" by (auto elim!: subset_imageE) @@ -216,11 +215,10 @@ finally show ?thesis by (simp add: binomial_def) qed - + text \Recursive characterization\ -lemma binomial_n_0 [simp, code]: - "n choose 0 = 1" +lemma binomial_n_0 [simp, code]: "n choose 0 = 1" proof - have "{K \ Pow {0.. ?P n (Suc k) = {}" by auto have "?Q = {K\?Q. n \ K} \ {K\?Q. n \ K}" @@ -257,27 +253,25 @@ qed show "K \ ?A \ K \ ?B" by (subst in_image_insert_iff) - (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite Diff_subset_conv K_finite Suc_card_K) - qed + (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite + Diff_subset_conv K_finite Suc_card_K) + qed also have "{K\?Q. n \ K} = ?P n (Suc k)" by (auto simp add: atLeast0_lessThan_Suc) finally show ?thesis using inj disjoint by (simp add: binomial_def card_Un_disjoint card_image) qed -lemma binomial_eq_0: - "n < k \ n choose k = 0" +lemma binomial_eq_0: "n < k \ n choose k = 0" by (auto simp add: binomial_def dest: subset_eq_atLeast0_lessThan_card) lemma zero_less_binomial: "k \ n \ n choose k > 0" by (induct n k rule: diff_induct) simp_all -lemma binomial_eq_0_iff [simp]: - "n choose k = 0 \ n < k" +lemma binomial_eq_0_iff [simp]: "n choose k = 0 \ n < k" by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) -lemma zero_less_binomial_iff [simp]: - "n choose k > 0 \ k \ n" +lemma zero_less_binomial_iff [simp]: "n choose k > 0 \ k \ n" by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial) lemma binomial_n_n [simp]: "n choose n = 1" @@ -290,120 +284,123 @@ by (induct n) simp_all lemma choose_reduce_nat: - "0 < (n::nat) \ 0 < k \ - (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)" + "0 < n \ 0 < k \ + n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)" using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp -lemma Suc_times_binomial_eq: - "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" +lemma Suc_times_binomial_eq: "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" apply (induct n arbitrary: k) - apply simp apply arith + apply simp + apply arith apply (case_tac k) apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) done lemma binomial_le_pow2: "n choose k \ 2^n" apply (induct n arbitrary: k) - apply (case_tac k) apply simp_all + apply (case_tac k) + apply simp_all apply (case_tac k) - apply auto + apply auto apply (simp add: add_le_mono mult_2) done -text\The absorption property\ -lemma Suc_times_binomial: - "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" +text \The absorption property.\ +lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" using Suc_times_binomial_eq by auto -text\This is the well-known version of absorption, but it's harder to use because of the - need to reason about division.\ -lemma binomial_Suc_Suc_eq_times: - "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" +text \This is the well-known version of absorption, but it's harder to use + because of the need to reason about division.\ +lemma binomial_Suc_Suc_eq_times: "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) -text\Another version of absorption, with -1 instead of Suc.\ -lemma times_binomial_minus1_eq: - "0 < k \ k * (n choose k) = n * ((n - 1) choose (k - 1))" +text \Another version of absorption, with \-1\ instead of \Suc\.\ +lemma times_binomial_minus1_eq: "0 < k \ k * (n choose k) = n * ((n - 1) choose (k - 1))" using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"] by (auto split add: nat_diff_split) subsection \The binomial theorem (courtesy of Tobias Nipkow):\ -text\Avigad's version, generalized to any commutative ring\ -theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n = - (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n") +text \Avigad's version, generalized to any commutative ring\ +theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n = + (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" proof (induct n) - case 0 then show "?P 0" by simp + case 0 + then show ?case by simp next case (Suc n) - have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" + have decomp: "{0..n+1} = {0} \ {n + 1} \ {1..n}" by auto - have decomp2: "{0..n} = {0} Un {1..n}" + have decomp2: "{0..n} = {0} \ {1..n}" by auto - have "(a+b)^(n+1) = - (a+b) * (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" + have "(a + b)^(n+1) = (a + b) * (\k=0..n. of_nat (n choose k) * a^k * b^(n - k))" using Suc.hyps by simp - also have "\ = a*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k)) + - b*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" + also have "\ = a * (\k=0..n. of_nat (n choose k) * a^k * b^(n-k)) + + b * (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" by (rule distrib_right) also have "\ = (\k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + - (\k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))" + (\k=0..n. of_nat (n choose k) * a^k * b^(n - k + 1))" by (auto simp add: setsum_right_distrib ac_simps) - also have "\ = (\k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) + - (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))" - by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps - del:setsum_cl_ivl_Suc) - also have "\ = a^(n+1) + b^(n+1) + - (\k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) + - (\k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))" + also have "\ = (\k=0..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + + (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))" + by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: setsum_cl_ivl_Suc) + also have "\ = a^(n + 1) + b^(n + 1) + + (\k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) + + (\k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))" by (simp add: decomp2) - also have - "\ = a^(n+1) + b^(n+1) + - (\k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))" + also have "\ = a^(n + 1) + b^(n + 1) + + (\k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat) - also have "\ = (\k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))" + also have "\ = (\k=0..n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" using decomp by (simp add: field_simps) - finally show "?P (Suc n)" by simp + finally show ?case + by simp qed -text\Original version for the naturals\ -corollary binomial: "(a+b::nat)^n = (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" - using binomial_ring [of "int a" "int b" n] +text \Original version for the naturals.\ +corollary binomial: "(a + b :: nat)^n = (\k=0..n. (of_nat (n choose k)) * a^k * b^(n - k))" + using binomial_ring [of "int a" "int b" n] by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric] - of_nat_setsum [symmetric] - of_nat_eq_iff of_nat_id) + of_nat_setsum [symmetric] of_nat_eq_iff of_nat_id) lemma binomial_fact_lemma: "k \ n \ fact k * fact (n - k) * (n choose k) = fact n" proof (induct n arbitrary: k rule: nat_less_induct) - fix n k assume H: "\mx\m. fact x * fact (m - x) * (m choose x) = - fact m" and kn: "k \ n" + fix n k + assume H: "\mx\m. fact x * fact (m - x) * (m choose x) = fact m" + assume kn: "k \ n" let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" - { assume "n=0" then have ?ths using kn by simp } - moreover - { assume "k=0" then have ?ths using kn by simp } - moreover - { assume nk: "n=k" then have ?ths by simp } - moreover - { fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" - from n have mn: "m < n" by arith - from hm have hm': "h \ m" by arith - from hm h n kn have km: "k \ m" by arith - have "m - h = Suc (m - Suc h)" using h km hm by arith - with km h have th0: "fact (m - h) = (m - h) * fact (m - k)" + consider "n = 0 \ k = 0 \ n = k" | m h where "n = Suc m" "k = Suc h" "h < m" + using kn by atomize_elim presburger + then show "fact k * fact (n - k) * (n choose k) = fact n" + proof cases + case 1 + with kn show ?thesis by auto + next + case 2 + note n = \n = Suc m\ + note k = \k = Suc h\ + note hm = \h < m\ + have mn: "m < n" + using n by arith + have hm': "h \ m" + using hm by arith + have km: "k \ m" + using hm k n kn by arith + have "m - h = Suc (m - Suc h)" + using k km hm by arith + with km k have "fact (m - h) = (m - h) * fact (m - k)" by simp - from n h th0 - have "fact k * fact (n - k) * (n choose k) = + with n k have "fact k * fact (n - k) * (n choose k) = k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" by (simp add: field_simps) also have "\ = (k + (m - h)) * fact m" using H[rule_format, OF mn hm'] H[rule_format, OF mn km] by (simp add: field_simps) - finally have ?ths using h n km by simp } - moreover have "n=0 \ k = 0 \ k = n \ (\m h. n = Suc m \ k = Suc h \ h < m)" - using kn by presburger - ultimately show ?ths by blast + finally show ?thesis + using k n km by simp + qed qed lemma binomial_fact': @@ -414,19 +411,18 @@ lemma binomial_fact: assumes kn: "k \ n" - shows "(of_nat (n choose k) :: 'a::field_char_0) = - (fact n) / (fact k * fact(n - k))" + shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))" using binomial_fact_lemma[OF kn] apply (simp add: field_simps) - by (metis mult.commute of_nat_fact of_nat_mult) + apply (metis mult.commute of_nat_fact of_nat_mult) + done lemma fact_binomial: assumes "k \ n" shows "fact k * of_nat (n choose k) = (fact n / fact (n - k) :: 'a::field_char_0)" unfolding binomial_fact [OF assms] by (simp add: field_simps) -lemma choose_two: - "n choose 2 = n * (n - 1) div 2" +lemma choose_two: "n choose 2 = n * (n - 1) div 2" proof (cases "n \ 2") case False then have "n = 0 \ n = 1" @@ -444,8 +440,7 @@ qed lemma choose_row_sum: "(\k=0..n. n choose k) = 2^n" - using binomial [of 1 "1" n] - by (simp add: numeral_2_eq_2) + using binomial [of 1 "1" n] by (simp add: numeral_2_eq_2) lemma sum_choose_lower: "(\k=0..n. (r+k) choose k) = Suc (r+n) choose n" by (induct n) auto @@ -454,12 +449,13 @@ by (induct n) auto lemma choose_alternating_sum: - "n > 0 \ (\i\n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)" - using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power) + "n > 0 \ (\i\n. (-1)^i * of_nat (n choose i)) = (0 :: 'a::comm_ring_1)" + using binomial_ring[of "-1 :: 'a" 1 n] + by (simp add: atLeast0AtMost mult_of_nat_commute zero_power) lemma choose_even_sum: assumes "n > 0" - shows "2 * (\i\n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" + shows "2 * (\i\n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)" proof - have "2 ^ n = (\i\n. of_nat (n choose i)) + (\i\n. (-1) ^ i * of_nat (n choose i) :: 'a)" using choose_row_sum[of n] @@ -473,7 +469,7 @@ lemma choose_odd_sum: assumes "n > 0" - shows "2 * (\i\n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)" + shows "2 * (\i\n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)" proof - have "2 ^ n = (\i\n. of_nat (n choose i)) - (\i\n. (-1) ^ i * of_nat (n choose i) :: 'a)" using choose_row_sum[of n] @@ -490,20 +486,21 @@ text\NW diagonal sum property\ lemma sum_choose_diagonal: - assumes "m\n" shows "(\k=0..m. (n-k) choose (m-k)) = Suc n choose m" + assumes "m \ n" + shows "(\k=0..m. (n - k) choose (m - k)) = Suc n choose m" proof - - have "(\k=0..m. (n-k) choose (m-k)) = (\k=0..m. (n-m+k) choose k)" + have "(\k=0..m. (n-k) choose (m - k)) = (\k=0..m. (n - m + k) choose k)" using setsum.atLeast_atMost_rev [of "\k. (n - k) choose (m - k)" 0 m] assms by simp - also have "... = Suc (n-m+m) choose m" + also have "\ = Suc (n - m + m) choose m" by (rule sum_choose_lower) - also have "... = Suc n choose m" using assms - by simp + also have "\ = Suc n choose m" + using assms by simp finally show ?thesis . qed -subsection \Pochhammer's symbol : generalized rising factorial\ +subsection \Pochhammer's symbol: generalized rising factorial\ text \See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\ @@ -511,34 +508,30 @@ begin definition pochhammer :: "'a \ nat \ 'a" -where - pochhammer_setprod: "pochhammer a n = setprod (\i. a + of_nat i) {0..i. a + of_nat i) {0..i. a + of_nat (n - i)) {1..n}" +lemma pochhammer_setprod_rev: "pochhammer a n = setprod (\i. a + of_nat (n - i)) {1..n}" using setprod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\i. a + of_nat i" 0 n] by (simp add: pochhammer_setprod) -lemma pochhammer_Suc_setprod: - "pochhammer a (Suc n) = setprod (\i. a + of_nat i) {0..n}" +lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\i. a + of_nat i) {0..n}" by (simp add: pochhammer_setprod atLeastLessThanSuc_atLeastAtMost) -lemma pochhammer_Suc_setprod_rev: - "pochhammer a (Suc n) = setprod (\i. a + of_nat (n - i)) {0..n}" +lemma pochhammer_Suc_setprod_rev: "pochhammer a (Suc n) = setprod (\i. a + of_nat (n - i)) {0..n}" by (simp add: pochhammer_setprod_rev setprod.atLeast_Suc_atMost_Suc_shift) lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" by (simp add: pochhammer_setprod) - + lemma pochhammer_1 [simp]: "pochhammer a 1 = a" by (simp add: pochhammer_setprod lessThan_Suc) - + lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a" by (simp add: pochhammer_setprod lessThan_Suc) - + lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" by (simp add: pochhammer_setprod atLeast0_lessThan_Suc ac_simps) - + end lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)" @@ -556,14 +549,12 @@ lemma pochhammer_fact: "fact n = pochhammer 1 n" by (simp add: pochhammer_setprod fact_setprod_Suc) -lemma pochhammer_of_nat_eq_0_lemma: - assumes "k > n" - shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0" - using assms by (auto simp add: pochhammer_setprod) +lemma pochhammer_of_nat_eq_0_lemma: "k > n \ pochhammer (- (of_nat n :: 'a:: idom)) k = 0" + by (auto simp add: pochhammer_setprod) lemma pochhammer_of_nat_eq_0_lemma': assumes kn: "k \ n" - shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \ 0" + shows "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k \ 0" proof (cases k) case 0 then show ?thesis by simp @@ -571,12 +562,13 @@ case (Suc h) then show ?thesis apply (simp add: pochhammer_Suc_setprod) - using Suc kn apply (auto simp add: algebra_simps) + using Suc kn + apply (auto simp add: algebra_simps) done qed lemma pochhammer_of_nat_eq_0_iff: - shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \ k > n" + "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k = 0 \ k > n" (is "?l = ?r") using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] @@ -609,131 +601,142 @@ qed lemma pochhammer_minus': - "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" - unfolding pochhammer_minus[where b=b] - unfolding mult.assoc[symmetric] - unfolding power_add[symmetric] - by simp + "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" + apply (simp only: pochhammer_minus [where b = b]) + apply (simp only: mult.assoc [symmetric]) + apply (simp only: power_add [symmetric]) + apply simp + done lemma pochhammer_same: "pochhammer (- of_nat n) n = - ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)" + ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n" unfolding pochhammer_minus by (simp add: of_nat_diff pochhammer_fact) -lemma pochhammer_product': - "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m" -proof (induction n arbitrary: z) +lemma pochhammer_product': "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m" +proof (induct n arbitrary: z) + case 0 + then show ?case by simp +next case (Suc n z) have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = - z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)" + z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)" by (simp add: pochhammer_rec ac_simps) also note Suc[symmetric] also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))" by (subst pochhammer_rec) simp - finally show ?case by simp -qed simp + finally show ?case + by simp +qed lemma pochhammer_product: "m \ n \ pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)" using pochhammer_product'[of z m "n - m"] by simp lemma pochhammer_times_pochhammer_half: - fixes z :: "'a :: field_char_0" + fixes z :: "'a::field_char_0" shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\k=0..2*n+1. z + of_nat k / 2)" -proof (induction n) +proof (induct n) + case 0 + then show ?case + by (simp add: atLeast0_atMost_Suc) +next case (Suc n) define n' where "n' = Suc n" have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') = - (pochhammer z n' * pochhammer (z + 1 / 2) n') * - ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A") - by (simp_all add: pochhammer_rec' mult_ac) + (pochhammer z n' * pochhammer (z + 1 / 2) n') * ((z + of_nat n') * (z + 1/2 + of_nat n'))" + (is "_ = _ * ?A") + by (simp_all add: pochhammer_rec' mult_ac) also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)" - (is "_ = ?A") by (simp add: field_simps n'_def) + (is "_ = ?B") + by (simp add: field_simps n'_def) also note Suc[folded n'_def] - also have "(\k=0..2 * n + 1. z + of_nat k / 2) * ?A = (\k=0..2 * Suc n + 1. z + of_nat k / 2)" + also have "(\k=0..2 * n + 1. z + of_nat k / 2) * ?B = (\k=0..2 * Suc n + 1. z + of_nat k / 2)" by (simp add: atLeast0_atMost_Suc) - finally show ?case by (simp add: n'_def) -qed (simp add: atLeast0_atMost_Suc) + finally show ?case + by (simp add: n'_def) +qed lemma pochhammer_double: - fixes z :: "'a :: field_char_0" + fixes z :: "'a::field_char_0" shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n" -proof (induction n) +proof (induct n) + case 0 + then show ?case by simp +next case (Suc n) have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * - (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)" + (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)" by (simp add: pochhammer_rec' ac_simps) also note Suc also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n * - (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) = - of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)" + (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) = + of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)" by (simp add: field_simps pochhammer_rec') finally show ?case . -qed simp +qed lemma fact_double: - "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)" + "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a::field_char_0)" using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact) -lemma pochhammer_absorb_comp: - "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" +lemma pochhammer_absorb_comp: "(r - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" (is "?lhs = ?rhs") + for r :: "'a::comm_ring_1" proof - - have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps) - also have "\ = ?rhs" by (subst pochhammer_rec) simp + have "?lhs = - pochhammer (- r) (Suc k)" + by (subst pochhammer_rec') (simp add: algebra_simps) + also have "\ = ?rhs" + by (subst pochhammer_rec) simp finally show ?thesis . qed subsection \Generalized binomial coefficients\ -definition gbinomial :: "'a :: {semidom_divide, semiring_char_0} \ nat \ 'a" (infixl "gchoose" 65) -where - gbinomial_setprod_rev: "a gchoose n = setprod (\i. a - of_nat i) {0.. nat \ 'a" (infixl "gchoose" 65) + where gbinomial_setprod_rev: "a gchoose n = setprod (\i. a - of_nat i) {0..i. a - of_nat i) {0..k} div fact (Suc k)" +lemma gbinomial_Suc: "a gchoose (Suc k) = setprod (\i. a - of_nat i) {0..k} div fact (Suc k)" by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) -lemma gbinomial_mult_fact: - fixes a :: "'a::field_char_0" - shows - "fact n * (a gchoose n) = (\i = 0..i = 0..i = 0..i = 0.. n") case False - then have "n < k" by (simp add: not_le) + then have "n < k" + by (simp add: not_le) then have "0 \ (op - n) ` {0..(op - n ` {0..q. n - q) {0..{Suc (n - k)..n}" .. - from True have "(n choose k) = fact n div (fact k * fact (n - k))" + from True have "n choose k = fact n div (fact k * fact (n - k))" by (rule binomial_fact') with * show ?thesis by (simp add: gbinomial_setprod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact) qed -lemma of_nat_gbinomial: - "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)" +lemma of_nat_gbinomial: "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)" proof (cases "k \ n") - case False then show ?thesis + case False + then show ?thesis by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_setprod_rev) next - case True - moreover define m where "m = n - k" - ultimately have n: "n = m + k" + case True + define m where "m = n - k" + with True have n: "n = m + k" by arith from n have "fact n = ((\i = 0.. = ((\i\{0.. {k..i = 0..i = 0..i. of_nat (m + k - i) :: 'a" 0 k m] by (simp add: fact_setprod_rev [of m] setprod.union_disjoint of_nat_diff) - then have "fact n / fact (n - k) = - ((\i = 0..i = 0..Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \ nat \ 'a"})\ +setup + \Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \ nat \ 'a"})\ lemma gbinomial_1[simp]: "a gchoose 1 = a" by (simp add: gbinomial_setprod_rev lessThan_Suc) @@ -796,29 +796,27 @@ by (simp add: gbinomial_setprod_rev lessThan_Suc) lemma gbinomial_mult_1: - fixes a :: "'a :: field_char_0" - shows "a * (a gchoose n) = - of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") + fixes a :: "'a::field_char_0" + shows "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" + (is "?l = ?r") proof - have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))" - unfolding gbinomial_pochhammer - pochhammer_Suc right_diff_distrib power_Suc + apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc) apply (simp del: of_nat_Suc fact_Suc) apply (auto simp add: field_simps simp del: of_nat_Suc) done - also have "\ = ?l" unfolding gbinomial_pochhammer - by (simp add: field_simps) + also have "\ = ?l" + by (simp add: field_simps gbinomial_pochhammer) finally show ?thesis .. qed lemma gbinomial_mult_1': - fixes a :: "'a :: field_char_0" - shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" + "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" + for a :: "'a::field_char_0" by (simp add: mult.commute gbinomial_mult_1) -lemma gbinomial_Suc_Suc: - fixes a :: "'a :: field_char_0" - shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" +lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" + for a :: "'a::field_char_0" proof (cases k) case 0 then show ?thesis by simp @@ -830,24 +828,25 @@ apply (auto simp add: image_Suc_atMost) done have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) = - (a gchoose Suc h) * (fact (Suc (Suc h))) + - (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))" + (a gchoose Suc h) * (fact (Suc (Suc h))) + + (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))" by (simp add: Suc field_simps del: fact_Suc) - also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + - (\i=0..Suc h. a - of_nat i)" + also have "\ = + (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\i=0..Suc h. a - of_nat i)" apply (simp del: fact_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"]) - apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost) + apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact + mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost) done - also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + - (\i=0..Suc h. a - of_nat i)" + also have "\ = + (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + (\i=0..Suc h. a - of_nat i)" by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult) - also have "... = of_nat (Suc (Suc h)) * (\i=0..h. a - of_nat i) + - (\i=0..Suc h. a - of_nat i)" + also have "\ = + of_nat (Suc (Suc h)) * (\i=0..h. a - of_nat i) + (\i=0..Suc h. a - of_nat i)" unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost by auto - also have "... = (\i=0..Suc h. a - of_nat i) + - (of_nat h * (\i=0..h. a - of_nat i) + 2 * (\i=0..h. a - of_nat i))" + also have "\ = + (\i=0..Suc h. a - of_nat i) + (of_nat h * (\i=0..h. a - of_nat i) + 2 * (\i=0..h. a - of_nat i))" by (simp add: field_simps) - also have "... = + also have "\ = ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\i\{0..Suc h}. a - of_nat i)" unfolding gbinomial_mult_fact' by (simp add: comm_semiring_class.distrib field_simps Suc atLeastLessThanSuc_atLeastAtMost) @@ -858,132 +857,147 @@ using eq0 by (simp add: Suc setprod.atLeast0_atMost_Suc_shift) also have "\ = (fact (Suc k)) * ((a + 1) gchoose (Suc k))" - unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost .. + by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost) finally show ?thesis using fact_nonzero [of "Suc k"] by auto qed -lemma gbinomial_reduce_nat: - fixes a :: "'a :: field_char_0" - shows "0 < k \ a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)" +lemma gbinomial_reduce_nat: "0 < k \ a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)" + for a :: "'a::field_char_0" by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) lemma gchoose_row_sum_weighted: - fixes r :: "'a::field_char_0" - shows "(\k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))" -proof (induct m) - case 0 show ?case by simp -next - case (Suc m) - from Suc show ?case - by (simp add: field_simps distrib gbinomial_mult_1) -qed + "(\k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))" + for r :: "'a::field_char_0" + by (induct m) (simp_all add: field_simps distrib gbinomial_mult_1) lemma binomial_symmetric: assumes kn: "k \ n" shows "n choose k = n choose (n - k)" -proof- - from kn have kn': "n - k \ n" by arith +proof - + have kn': "n - k \ n" + using kn by arith from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] - have "fact k * fact (n - k) * (n choose k) = - fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp - then show ?thesis using kn by simp + have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" + by simp + then show ?thesis + using kn by simp qed lemma choose_rising_sum: "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose m)" proof - - show "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all - also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all - finally show "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose m)" . + show "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" + by (induct m) simp_all + also have "\ = (n + m + 1) choose m" + by (subst binomial_symmetric) simp_all + finally show "(\j\m. ((n + j) choose n)) = (n + m + 1) choose m" . qed -lemma choose_linear_sum: - "(\i\n. i * (n choose i)) = n * 2 ^ (n - 1)" +lemma choose_linear_sum: "(\i\n. i * (n choose i)) = n * 2 ^ (n - 1)" proof (cases n) + case 0 + then show ?thesis by simp +next case (Suc m) - have "(\i\n. i * (n choose i)) = (\i\Suc m. i * (Suc m choose i))" by (simp add: Suc) - also have "... = Suc m * 2 ^ m" + have "(\i\n. i * (n choose i)) = (\i\Suc m. i * (Suc m choose i))" + by (simp add: Suc) + also have "\ = Suc m * 2 ^ m" by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) (simp add: choose_row_sum') - finally show ?thesis using Suc by simp -qed simp_all + finally show ?thesis + using Suc by simp +qed lemma choose_alternating_linear_sum: assumes "n \ 1" - shows "(\i\n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0" + shows "(\i\n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a::comm_ring_1) = 0" proof (cases n) + case 0 + then show ?thesis by simp +next case (Suc m) - with assms have "m > 0" by simp + with assms have "m > 0" + by simp have "(\i\n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = - (\i\Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc) - also have "... = (\i\m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))" + (\i\Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" + by (simp add: Suc) + also have "\ = (\i\m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))" by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] mult_ac of_nat_mult) simp - also have "... = -of_nat (Suc m) * (\i\m. (-1) ^ i * of_nat ((m choose i)))" + also have "\ = - of_nat (Suc m) * (\i\m. (-1) ^ i * of_nat (m choose i))" by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial) (simp add: algebra_simps) also have "(\i\m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0" using choose_alternating_sum[OF \m > 0\] by simp - finally show ?thesis by simp -qed simp + finally show ?thesis + by simp +qed -lemma vandermonde: - "(\k\r. (m choose k) * (n choose (r - k))) = (m + n) choose r" -proof (induction n arbitrary: r) +lemma vandermonde: "(\k\r. (m choose k) * (n choose (r - k))) = (m + n) choose r" +proof (induct n arbitrary: r) case 0 have "(\k\r. (m choose k) * (0 choose (r - k))) = (\k\r. if k = r then (m choose k) else 0)" by (intro setsum.cong) simp_all - also have "... = m choose r" by (simp add: setsum.delta) - finally show ?case by simp + also have "\ = m choose r" + by (simp add: setsum.delta) + finally show ?case + by simp next case (Suc n r) - show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le) + show ?case + by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le) qed -lemma choose_square_sum: - "(\k\n. (n choose k)^2) = ((2*n) choose n)" - using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric]) +lemma choose_square_sum: "(\k\n. (n choose k)^2) = ((2*n) choose n)" + using vandermonde[of n n n] + by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric]) lemma pochhammer_binomial_sum: - fixes a b :: "'a :: comm_ring_1" + fixes a b :: "'a::comm_ring_1" shows "pochhammer (a + b) n = (\k\n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))" proof (induction n arbitrary: a b) + case 0 + then show ?case by simp +next case (Suc n a b) have "(\k\Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) = - (\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) + - ((\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + - pochhammer b (Suc n))" + (\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) + + ((\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + + pochhammer b (Suc n))" by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib) also have "(\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) = - a * pochhammer ((a + 1) + b) n" + a * pochhammer ((a + 1) + b) n" by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac) - also have "(\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) = - (\i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" - by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost) - also have "... = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" + also have "(\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + + pochhammer b (Suc n) = + (\i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" + apply (subst setsum_head_Suc) + apply simp + apply (subst setsum_shift_bounds_cl_Suc_ivl) + apply (simp add: atLeast0AtMost) + done + also have "\ = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0) - also have "... = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))" + also have "\ = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))" by (intro setsum.cong) (simp_all add: Suc_diff_le) - also have "... = b * pochhammer (a + (b + 1)) n" + also have "\ = b * pochhammer (a + (b + 1)) n" by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec) also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n = - pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps) + pochhammer (a + b) (Suc n)" + by (simp add: pochhammer_rec algebra_simps) finally show ?case .. -qed simp_all - +qed -text\Contributed by Manuel Eberl, generalised by LCP. - Alternative definition of the binomial coefficient as @{term "\i -lemma gbinomial_altdef_of_nat: - fixes k :: nat - and x :: "'a :: field_char_0" - shows "x gchoose k = (\i = 0..Contributed by Manuel Eberl, generalised by LCP. + Alternative definition of the binomial coefficient as @{term "\i +lemma gbinomial_altdef_of_nat: "x gchoose k = (\i = 0.. x" shows "(x / of_nat k :: 'a) ^ k \ x gchoose k" proof - @@ -991,22 +1005,26 @@ using assms of_nat_0_le_iff order_trans by blast have "(x / of_nat k :: 'a) ^ k = (\i = 0.. \ x gchoose k" + also have "\ \ x gchoose k" (* FIXME *) unfolding gbinomial_altdef_of_nat - proof (safe intro!: setprod_mono, simp_all) -- \FIXME\ - fix i :: nat - assume ik: "i < k" - from assms have "x * of_nat i \ of_nat (i * k)" - by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult) - then have "x * of_nat k - x * of_nat i \ x * of_nat k - of_nat (i * k)" by arith - then have "x * of_nat (k - i) \ (x - of_nat i) * of_nat k" - using ik - by (simp add: algebra_simps zero_less_mult_iff of_nat_diff) - then have "x * of_nat (k - i) \ (x - of_nat i) * (of_nat k :: 'a)" - unfolding of_nat_mult[symmetric] of_nat_le_iff . - with assms show "x / of_nat k \ (x - of_nat i) / (of_nat (k - i) :: 'a)" - using \i < k\ by (simp add: field_simps) - qed (simp add: x zero_le_divide_iff) + apply (safe intro!: setprod_mono) + apply simp_all + prefer 2 + subgoal premises for i + proof - + from assms have "x * of_nat i \ of_nat (i * k)" + by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult) + then have "x * of_nat k - x * of_nat i \ x * of_nat k - of_nat (i * k)" + by arith + then have "x * of_nat (k - i) \ (x - of_nat i) * of_nat k" + using \i < k\ by (simp add: algebra_simps zero_less_mult_iff of_nat_diff) + then have "x * of_nat (k - i) \ (x - of_nat i) * (of_nat k :: 'a)" + by (simp only: of_nat_mult[symmetric] of_nat_le_iff) + with assms show ?thesis + using \i < k\ by (simp add: field_simps) + qed + apply (simp add: x zero_le_divide_iff) + done finally show ?thesis . qed @@ -1016,33 +1034,36 @@ lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)" by (subst gbinomial_negated_upper) (simp add: add_ac) -lemma Suc_times_gbinomial: - "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)" +lemma Suc_times_gbinomial: "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)" proof (cases b) + case 0 + then show ?thesis by simp +next case (Suc b) - hence "((a + 1) gchoose (Suc (Suc b))) = - (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)" + then have "((a + 1) gchoose (Suc (Suc b))) = (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)" by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) also have "(\i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)" by (simp add: setprod.atLeast0_atMost_Suc_shift) - also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" + also have "\ / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc) -qed simp +qed -lemma gbinomial_factors: - "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)" +lemma gbinomial_factors: "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)" proof (cases b) + case 0 + then show ?thesis by simp +next case (Suc b) - hence "((a + 1) gchoose (Suc (Suc b))) = - (\i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)" + then have "((a + 1) gchoose (Suc (Suc b))) = (\i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)" by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) also have "(\i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)" by (simp add: setprod.atLeast0_atMost_Suc_shift) - also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" + also have "\ / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) - finally show ?thesis by (simp add: Suc) -qed simp + finally show ?thesis + by (simp add: Suc) +qed lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))" using gbinomial_mult_1[of r k] @@ -1052,41 +1073,45 @@ using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric]) -text \The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[ +text \The absorption identity (equation 5.5 \cite[p.~157]{GKP}): +\[ {r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0. \]\ -lemma gbinomial_absorption': - "k > 0 \ (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))" +lemma gbinomial_absorption': "k > 0 \ r gchoose k = (r / of_nat k) * (r - 1 gchoose (k - 1))" using gbinomial_rec[of "r - 1" "k - 1"] by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc) text \The absorption identity is written in the following form to avoid division by $k$ (the lower index) and therefore remove the $k \neq 0$ -restriction\cite[p.~157]{GKP}:\[ +restriction\cite[p.~157]{GKP}: +\[ k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k. \]\ -lemma gbinomial_absorption: - "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)" +lemma gbinomial_absorption: "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)" using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc) text \The absorption identity for natural number binomial coefficients:\ -lemma binomial_absorption: - "Suc k * (n choose Suc k) = n * ((n - 1) choose k)" +lemma binomial_absorption: "Suc k * (n choose Suc k) = n * ((n - 1) choose k)" by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc) text \The absorption companion identity for natural number coefficients, -following the proof by GKP \cite[p.~157]{GKP}:\ -lemma binomial_absorb_comp: - "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs") + following the proof by GKP \cite[p.~157]{GKP}:\ +lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)" + (is "?lhs = ?rhs") proof (cases "n \ k") + case True + then show ?thesis by auto +next case False then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))" using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n] by simp - also from False have "Suc ((n - 1) - k) = n - k" by simp - also from False have "n choose \ = n choose k" by (intro binomial_symmetric [symmetric]) simp_all + also have "Suc ((n - 1) - k) = n - k" + using False by simp + also have "n choose \ = n choose k" + using False by (intro binomial_symmetric [symmetric]) simp_all finally show ?thesis .. -qed auto +qed text \The generalised absorption companion identity:\ lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)" @@ -1100,35 +1125,45 @@ "0 < n \ n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)" by (subst choose_reduce_nat) simp_all - text \ Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful - summation formula, operating on both indices:\[ - \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, + summation formula, operating on both indices: + \[ + \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, \quad \textnormal{integer } n. \] \ -lemma gbinomial_parallel_sum: -"(\k\n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n" -proof (induction n) +lemma gbinomial_parallel_sum: "(\k\n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n" +proof (induct n) + case 0 + then show ?case by simp +next case (Suc m) - thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac) -qed auto + then show ?case + using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] + by (simp add: add_ac) +qed + subsubsection \Summation on the upper index\ + text \ Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP}, aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\] \ lemma gbinomial_sum_up_index: - "(\k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)" -proof (induction n) + "(\k = 0..n. (of_nat k gchoose m) :: 'a::field_char_0) = (of_nat n + 1) gchoose (m + 1)" +proof (induct n) case 0 - show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto + show ?case + using gbinomial_Suc_Suc[of 0 m] + by (cases m) auto next case (Suc n) - thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac) + then show ?case + using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] + by (simp add: add_ac) qed lemma gbinomial_index_swap: @@ -1137,92 +1172,114 @@ proof - have "?lhs = (of_nat (m + n) gchoose m)" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric]) - also have "\ = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all - also have "\ = ?rhs" by (subst gbinomial_negated_upper) simp + also have "\ = (of_nat (m + n) gchoose n)" + by (subst gbinomial_of_nat_symmetric) simp_all + also have "\ = ?rhs" + by (subst gbinomial_negated_upper) simp finally show ?thesis . qed -lemma gbinomial_sum_lower_neg: - "(\k\m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs") +lemma gbinomial_sum_lower_neg: "(\k\m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" + (is "?lhs = ?rhs") proof - have "?lhs = (\k\m. -(r + 1) + of_nat k gchoose k)" by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib) - also have "\ = -r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp - also have "\ = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib) + also have "\ = - r + of_nat m gchoose m" + by (subst gbinomial_parallel_sum) simp + also have "\ = ?rhs" + by (subst gbinomial_negated_upper) (simp add: power_mult_distrib) finally show ?thesis . qed lemma gbinomial_partial_row_sum: -"(\k\m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))" -proof (induction m) + "(\k\m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))" +proof (induct m) + case 0 + then show ?case by simp +next case (Suc mm) - hence "(\k\Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = - (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps) - also have "\ = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl) + then have "(\k\Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = + (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" + by (simp add: field_simps) + also have "\ = r * (r - 1 gchoose Suc mm) / 2" + by (subst gbinomial_absorb_comp) (rule refl) also have "\ = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))" by (subst gbinomial_absorption [symmetric]) simp finally show ?case . -qed simp_all +qed lemma setsum_bounds_lt_plus1: "(\kk=1..mm. f k)" - by (induction mm) simp_all + by (induct mm) simp_all lemma gbinomial_partial_sum_poly: "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = - (\k\m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" (is "?lhs m = ?rhs m") + (\k\m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" + (is "?lhs m = ?rhs m") proof (induction m) + case 0 + then show ?case by simp +next case (Suc mm) - define G where "G i k = (of_nat i + r gchoose k) * x^k * y^(i-k)" for i k + define G where "G i k = (of_nat i + r gchoose k) * x^k * y^(i - k)" for i k define S where "S = ?lhs" - have SG_def: "S = (\i. (\k\i. (G i k)))" unfolding S_def G_def .. + have SG_def: "S = (\i. (\k\i. (G i k)))" + unfolding S_def G_def .. have "S (Suc mm) = G (Suc mm) 0 + (\k=Suc 0..Suc mm. G (Suc mm) k)" using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric]) also have "(\k=Suc 0..Suc mm. G (Suc mm) k) = (\k=0..mm. G (Suc mm) (Suc k))" by (subst setsum_shift_bounds_cl_Suc_ivl) simp - also have "\ = (\k=0..mm. ((of_nat mm + r gchoose (Suc k)) - + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))" + also have "\ = (\k=0..mm. ((of_nat mm + r gchoose (Suc k)) + + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))" unfolding G_def by (subst gbinomial_addition_formula) simp - also have "\ = (\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) - + (\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))" + also have "\ = (\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) + + (\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))" by (subst setsum.distrib [symmetric]) (simp add: algebra_simps) also have "(\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = - (\kk = (\k = (\kk=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))" proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify) - fix k assume "k < mm" - hence "mm - k = mm - Suc k + 1" by linarith - thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) = - (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:) + fix k + assume "k < mm" + then have "mm - k = mm - Suc k + 1" + by linarith + then show "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) = + (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" + by (simp only:) qed also have "\ + ?B = y * (\k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps) also have "(\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)" - unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps) - also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def) - finally have "S (Suc mm) = y * ((G mm 0) + (\k=1..mm. (G mm k))) - + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)" + unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps) + also have "(G (Suc mm) 0) = y * (G mm 0)" + by (simp add: G_def) + finally have "S (Suc mm) = + y * (G mm 0 + (\k=1..mm. (G mm k))) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)" by (simp add: ring_distribs) - also have "(G mm 0) + (\k=1..mm. (G mm k)) = S mm" + also have "G mm 0 + (\k=1..mm. (G mm k)) = S mm" by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost) finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" by (simp add: algebra_simps) - also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))" + also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- r gchoose (Suc mm))" by (subst gbinomial_negated_upper) simp also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm = - (-r gchoose (Suc mm)) * (-x) ^ Suc mm" by (simp add: power_minus[of x]) - also have "(x + y) * S mm + \ = (x + y) * ?rhs mm + (-r gchoose (Suc mm)) * (-x)^Suc mm" + (- r gchoose (Suc mm)) * (-x) ^ Suc mm" + by (simp add: power_minus[of x]) + also have "(x + y) * S mm + \ = (x + y) * ?rhs mm + (- r gchoose (Suc mm)) * (- x)^Suc mm" unfolding S_def by (subst Suc.IH) simp also have "(x + y) * ?rhs mm = (\n\mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))" by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le) also have "\ + (-r gchoose (Suc mm)) * (-x)^Suc mm = - (\n\Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp - finally show ?case unfolding S_def . -qed simp_all + (\n\Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" + by simp + finally show ?case + by (simp only: S_def) +qed lemma gbinomial_partial_sum_poly_xpos: "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = @@ -1237,85 +1294,89 @@ proof - have "2 * 2^(2*m) = (\k = 0..(2 * m + 1). (2 * m + 1 choose k))" using choose_row_sum[where n="2 * m + 1"] by simp - also have "(\k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\k = 0..m. (2 * m + 1 choose k)) - + (\k = m+1..2*m+1. (2 * m + 1 choose k))" - using setsum_ub_add_nat[of 0 m "\k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2) + also have "(\k = 0..(2 * m + 1). (2 * m + 1 choose k)) = + (\k = 0..m. (2 * m + 1 choose k)) + + (\k = m+1..2*m+1. (2 * m + 1 choose k))" + using setsum_ub_add_nat[of 0 m "\k. 2 * m + 1 choose k" "m+1"] + by (simp add: mult_2) also have "(\k = m+1..2*m+1. (2 * m + 1 choose k)) = - (\k = 0..m. (2 * m + 1 choose (k + (m + 1))))" + (\k = 0..m. (2 * m + 1 choose (k + (m + 1))))" by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2) also have "\ = (\k = 0..m. (2 * m + 1 choose (m - k)))" by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all also have "\ = (\k = 0..m. (2 * m + 1 choose k))" using setsum.atLeast_atMost_rev [of "\k. 2 * m + 1 choose (m - k)" 0 m] by simp - also have "\ + \ = 2 * \" by simp - finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost) + also have "\ + \ = 2 * \" + by simp + finally show ?thesis + by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost) qed -lemma gbinomial_r_part_sum: - "(\k\m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs") +lemma gbinomial_r_part_sum: "(\k\m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" + (is "?lhs = ?rhs") proof - have "?lhs = of_nat (\k\m. (2 * m + 1) choose k)" by (simp add: binomial_gbinomial add_ac) - also have "\ = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl) + also have "\ = of_nat (2 ^ (2 * m))" + by (subst binomial_r_part_sum) (rule refl) finally show ?thesis by simp qed lemma gbinomial_sum_nat_pow2: - "(\k\m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs") + "(\k\m. (of_nat (m + k) gchoose k :: 'a::field_char_0) / 2 ^ k) = 2 ^ m" + (is "?lhs = ?rhs") proof - - have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" by (induction m) simp_all - also have "\ = (\k\m. (2 * (of_nat m) + 1 gchoose k))" using gbinomial_r_part_sum .. + have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" + by (induct m) simp_all + also have "\ = (\k\m. (2 * (of_nat m) + 1 gchoose k))" + using gbinomial_r_part_sum .. also have "\ = (\k\m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))" using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"] by (simp add: add_ac) also have "\ = 2 ^ m * (\k\m. (of_nat (m + k) gchoose k) / 2 ^ k)" by (subst setsum_right_distrib) (simp add: algebra_simps power_diff) - finally show ?thesis by (subst (asm) mult_left_cancel) simp_all + finally show ?thesis + by (subst (asm) mult_left_cancel) simp_all qed lemma gbinomial_trinomial_revision: assumes "k \ m" - shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))" + shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))" proof - - have "(r gchoose m) * (of_nat m gchoose k) = - (r gchoose m) * fact m / (fact k * fact (m - k))" + have "(r gchoose m) * (of_nat m gchoose k) = (r gchoose m) * fact m / (fact k * fact (m - k))" using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact) - also have "\ = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms - by (simp add: gbinomial_pochhammer power_diff pochhammer_product) + also have "\ = (r gchoose k) * (r - of_nat k gchoose (m - k))" + using assms by (simp add: gbinomial_pochhammer power_diff pochhammer_product) finally show ?thesis . qed - -text\Versions of the theorems above for the natural-number version of "choose"\ +text \Versions of the theorems above for the natural-number version of "choose"\ lemma binomial_altdef_of_nat: - fixes n k :: nat - and x :: "'a :: field_char_0" - assumes "k \ n" - shows "of_nat (n choose k) = (\i = 0.. n \ of_nat (n choose k) = (\i = 0.. n" - shows "(of_nat n / of_nat k :: 'a) ^ k \ of_nat (n choose k)" -by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff) +lemma binomial_ge_n_over_k_pow_k: "k \ n \ (of_nat n / of_nat k :: 'a) ^ k \ of_nat (n choose k)" + for k n :: nat and x :: "'a::linordered_field" + by (simp add: gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff) lemma binomial_le_pow: assumes "r \ n" shows "n choose r \ n ^ r" proof - have "n choose r \ fact n div fact (n - r)" - using \r \ n\ by (subst binomial_fact_lemma[symmetric]) auto - with fact_div_fact_le_pow [OF assms] show ?thesis by auto + using assms by (subst binomial_fact_lemma[symmetric]) auto + with fact_div_fact_le_pow [OF assms] show ?thesis + by auto qed -lemma binomial_altdef_nat: "(k::nat) \ n \ - n choose k = fact n div (fact k * fact (n - k))" - by (subst binomial_fact_lemma [symmetric]) auto +lemma binomial_altdef_nat: "k \ n \ n choose k = fact n div (fact k * fact (n - k))" + for k n :: nat + by (subst binomial_fact_lemma [symmetric]) auto -lemma choose_dvd: "k \ n \ fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})" +lemma choose_dvd: + "k \ n \ fact k * fact (n - k) dvd (fact n :: 'a::{semiring_div,linordered_semidom})" unfolding dvd_def apply (rule exI [where x="of_nat (n choose k)"]) using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]] @@ -1323,26 +1384,28 @@ done lemma fact_fact_dvd_fact: - "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})" -by (metis add.commute add_diff_cancel_left' choose_dvd le_add2) + "fact k * fact n dvd (fact (k + n) :: 'a::{semiring_div,linordered_semidom})" + by (metis add.commute add_diff_cancel_left' choose_dvd le_add2) lemma choose_mult_lemma: - "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)" + "((m + r + k) choose (m + k)) * ((m + k) choose k) = ((m + r + k) choose k) * ((m + r) choose m)" + (is "?lhs = _") proof - - have "((m+r+k) choose (m+k)) * ((m+k) choose k) = - fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))" + have "?lhs = + fact (m + r + k) div (fact (m + k) * fact (m + r - m)) * (fact (m + k) div (fact k * fact m))" by (simp add: binomial_altdef_nat) - also have "... = fact (m+r+k) div (fact r * (fact k * fact m))" + also have "\ = fact (m + r + k) div (fact r * (fact k * fact m))" apply (subst div_mult_div_if_dvd) apply (auto simp: algebra_simps fact_fact_dvd_fact) apply (metis add.assoc add.commute fact_fact_dvd_fact) done - also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))" + also have "\ = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))" apply (subst div_mult_div_if_dvd [symmetric]) apply (auto simp add: algebra_simps) apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj) done - also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))" + also have "\ = + (fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))" apply (subst div_mult_div_if_dvd) apply (auto simp: fact_fact_dvd_fact algebra_simps) done @@ -1350,23 +1413,21 @@ by (simp add: binomial_altdef_nat mult.commute) qed -text\The "Subset of a Subset" identity\ +text \The "Subset of a Subset" identity.\ lemma choose_mult: - assumes "k\m" "m\n" - shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))" -using assms choose_mult_lemma [of "m-k" "n-m" k] -by simp + "k \ m \ m \ n \ (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))" + using choose_mult_lemma [of "m-k" "n-m" k] by simp subsection \More on Binomial Coefficients\ -lemma choose_one: "(n::nat) choose 1 = n" +lemma choose_one: "n choose 1 = n" for n :: nat by simp (*FIXME: messy and apparently unused*) -lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \ - (ALL n. P (Suc n) 0) \ (ALL n. (ALL k < n. P n k \ P n (Suc k) \ - P (Suc n) (Suc k))) \ (ALL k <= n. P n k)" +lemma binomial_induct [rule_format]: "(\n::nat. P n n) \ + (\n. P (Suc n) 0) \ (\n. (\k < n. P n k \ P n (Suc k) \ + P (Suc n) (Suc k))) \ (\k \ n. P n k)" apply (induct n) apply auto apply (case_tac "k = 0") @@ -1376,118 +1437,133 @@ done lemma card_UNION: - assumes "finite A" and "\k \ A. finite k" + assumes "finite A" + and "\k \ A. finite k" shows "card (\A) = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * int (card (\I)))" (is "?lhs = ?rhs") proof - - have "?rhs = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * (\_\\I. 1))" by simp - also have "\ = nat (\I | I \ A \ I \ {}. (\_\\I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs") - by(subst setsum_right_distrib) simp + have "?rhs = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * (\_\\I. 1))" + by simp + also have "\ = nat (\I | I \ A \ I \ {}. (\_\\I. (- 1) ^ (card I + 1)))" + (is "_ = nat ?rhs") + by (subst setsum_right_distrib) simp also have "?rhs = (\(I, _)\Sigma {I. I \ A \ I \ {}} Inter. (- 1) ^ (card I + 1))" - using assms by(subst setsum.Sigma)(auto) + using assms by (subst setsum.Sigma) auto also have "\ = (\(x, I)\(SIGMA x:UNIV. {I. I \ A \ I \ {} \ x \ \I}). (- 1) ^ (card I + 1))" by (rule setsum.reindex_cong [where l = "\(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta) also have "\ = (\(x, I)\(SIGMA x:\A. {I. I \ A \ I \ {} \ x \ \I}). (- 1) ^ (card I + 1))" - using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\A"]) + using assms + by (auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\A"]) also have "\ = (\x\\A. (\I|I \ A \ I \ {} \ x \ \I. (- 1) ^ (card I + 1)))" - using assms by(subst setsum.Sigma) auto + using assms by (subst setsum.Sigma) auto also have "\ = (\_\\A. 1)" (is "setsum ?lhs _ = _") - proof(rule setsum.cong[OF refl]) + proof (rule setsum.cong[OF refl]) fix x assume x: "x \ \A" define K where "K = {X \ A. x \ X}" - with \finite A\ have K: "finite K" by auto + with \finite A\ have K: "finite K" + by auto let ?I = "\i. {I. I \ A \ card I = i \ x \ \I}" have "inj_on snd (SIGMA i:{1..card A}. ?I i)" - using assms by(auto intro!: inj_onI) + using assms by (auto intro!: inj_onI) moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \ A \ I \ {} \ x \ \I}" - using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a] + using assms + by (auto intro!: rev_image_eqI[where x="(card a, a)" for a] simp add: card_gt_0_iff[folded Suc_le_eq] dest: finite_subset intro: card_mono) ultimately have "?lhs x = (\(i, I)\(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))" by (rule setsum.reindex_cong [where l = snd]) fastforce also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. (- 1) ^ (i + 1)))" - using assms by(subst setsum.Sigma) auto + using assms by (subst setsum.Sigma) auto also have "\ = (\i=1..card A. (- 1) ^ (i + 1) * (\I|I \ A \ card I = i \ x \ \I. 1))" - by(subst setsum_right_distrib) simp - also have "\ = (\i=1..card K. (- 1) ^ (i + 1) * (\I|I \ K \ card I = i. 1))" (is "_ = ?rhs") - proof(rule setsum.mono_neutral_cong_right[rule_format]) - show "{1..card K} \ {1..card A}" using \finite A\ - by(auto simp add: K_def intro: card_mono) + by (subst setsum_right_distrib) simp + also have "\ = (\i=1..card K. (- 1) ^ (i + 1) * (\I|I \ K \ card I = i. 1))" + (is "_ = ?rhs") + proof (rule setsum.mono_neutral_cong_right[rule_format]) + show "finite {1..card A}" + by simp + show "{1..card K} \ {1..card A}" + using \finite A\ by (auto simp add: K_def intro: card_mono) next fix i assume "i \ {1..card A} - {1..card K}" - hence i: "i \ card A" "card K < i" by auto + then have i: "i \ card A" "card K < i" + by auto have "{I. I \ A \ card I = i \ x \ \I} = {I. I \ K \ card I = i}" - by(auto simp add: K_def) - also have "\ = {}" using \finite A\ i - by(auto simp add: K_def dest: card_mono[rotated 1]) + by (auto simp add: K_def) + also have "\ = {}" + using \finite A\ i by (auto simp add: K_def dest: card_mono[rotated 1]) finally show "(- 1) ^ (i + 1) * (\I | I \ A \ card I = i \ x \ \I. 1 :: int) = 0" - by(simp only:) simp + by (simp only:) simp next fix i have "(\I | I \ A \ card I = i \ x \ \I. 1) = (\I | I \ K \ card I = i. 1 :: int)" (is "?lhs = ?rhs") - by(rule setsum.cong)(auto simp add: K_def) - thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp - qed simp - also have "{I. I \ K \ card I = 0} = {{}}" using assms - by(auto simp add: card_eq_0_iff K_def dest: finite_subset) - hence "?rhs = (\i = 0..card K. (- 1) ^ (i + 1) * (\I | I \ K \ card I = i. 1 :: int)) + 1" - by(subst (2) setsum_head_Suc)(simp_all ) + by (rule setsum.cong) (auto simp add: K_def) + then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" + by simp + qed + also have "{I. I \ K \ card I = 0} = {{}}" + using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset) + then have "?rhs = (\i = 0..card K. (- 1) ^ (i + 1) * (\I | I \ K \ card I = i. 1 :: int)) + 1" + by (subst (2) setsum_head_Suc) simp_all also have "\ = (\i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1" - using K by(subst n_subsets[symmetric]) simp_all + using K by (subst n_subsets[symmetric]) simp_all also have "\ = - (\i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1" - by(subst setsum_right_distrib[symmetric]) simp + by (subst setsum_right_distrib[symmetric]) simp also have "\ = - ((-1 + 1) ^ card K) + 1" - by(subst binomial_ring)(simp add: ac_simps) - also have "\ = 1" using x K by(auto simp add: K_def card_gt_0_iff) + by (subst binomial_ring) (simp add: ac_simps) + also have "\ = 1" + using x K by (auto simp add: K_def card_gt_0_iff) finally show "?lhs x = 1" . qed - also have "nat \ = card (\A)" by simp + also have "nat \ = card (\A)" + by simp finally show ?thesis .. qed -text\The number of nat lists of length \m\ summing to \N\ is -@{term "(N + m - 1) choose N"}:\ - +text \The number of nat lists of length \m\ summing to \N\ is @{term "(N + m - 1) choose N"}:\ lemma card_length_listsum_rec: - assumes "m\1" + assumes "m \ 1" shows "card {l::nat list. length l = m \ listsum l = N} = - (card {l. length l = (m - 1) \ listsum l = N} + - card {l. length l = m \ listsum l + 1 = N})" - (is "card ?C = (card ?A + card ?B)") + card {l. length l = (m - 1) \ listsum l = N} + + card {l. length l = m \ listsum l + 1 = N}" + (is "card ?C = card ?A + card ?B") proof - - let ?A'="{l. length l = m \ listsum l = N \ hd l = 0}" - let ?B'="{l. length l = m \ listsum l = N \ hd l \ 0}" - let ?f ="\ l. 0#l" - let ?g ="\ l. (hd l + 1) # tl l" - have 1: "\xs x. xs \ [] \ x = hd xs \ x # tl xs = xs" by simp - have 2: "\xs. (xs::nat list) \ [] \ listsum(tl xs) = listsum xs - hd xs" - by(auto simp add: neq_Nil_conv) + let ?A' = "{l. length l = m \ listsum l = N \ hd l = 0}" + let ?B' = "{l. length l = m \ listsum l = N \ hd l \ 0}" + let ?f = "\l. 0 # l" + let ?g = "\l. (hd l + 1) # tl l" + have 1: "xs \ [] \ x = hd xs \ x # tl xs = xs" for x xs + by simp + have 2: "xs \ [] \ listsum(tl xs) = listsum xs - hd xs" for xs :: "nat list" + by (auto simp add: neq_Nil_conv) have f: "bij_betw ?f ?A ?A'" - apply(rule bij_betw_byWitness[where f' = tl]) + apply (rule bij_betw_byWitness[where f' = tl]) using assms - by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv) - have 3: "\xs:: nat list. xs \ [] \ hd xs + (listsum xs - hd xs) = listsum xs" + apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv) + done + have 3: "xs \ [] \ hd xs + (listsum xs - hd xs) = listsum xs" for xs :: "nat list" by (metis 1 listsum_simps(2) 2) have g: "bij_betw ?g ?B ?B'" - apply(rule bij_betw_byWitness[where f' = "\ l. (hd l - 1) # tl l"]) + apply (rule bij_betw_byWitness[where f' = "\l. (hd l - 1) # tl l"]) using assms by (auto simp: 2 length_0_conv[symmetric] intro!: 3 - simp del: length_greater_0_conv length_0_conv) - { fix M N :: nat have "finite {xs. size xs = M \ set xs \ {0.. set xs \ {0.. ?B'" by auto - have disj: "?A' \ ?B' = {}" by auto - have "card ?C = card(?A' \ ?B')" using uni by simp + by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \ set xs \ {0.. ?B'" + by auto + have disj: "?A' \ ?B' = {}" + by auto + have "card ?C = card(?A' \ ?B')" + using uni by simp also have "\ = card ?A + card ?B" using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g] bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B @@ -1495,59 +1571,65 @@ finally show ?thesis . qed -lemma card_length_listsum: \"By Holden Lee, tidied by Tobias Nipkow" - "card {l::nat list. size l = m \ listsum l = N} = (N + m - 1) choose N" +lemma card_length_listsum: "card {l::nat list. size l = m \ listsum l = N} = (N + m - 1) choose N" + \ "by Holden Lee, tidied by Tobias Nipkow" proof (cases m) - case 0 then show ?thesis - by (cases N) (auto simp: cong: conj_cong) + case 0 + then show ?thesis + by (cases N) (auto cong: conj_cong) next case (Suc m') - have m: "m\1" by (simp add: Suc) - then show ?thesis - proof (induct "N + m - 1" arbitrary: N m) - case 0 \ "In the base case, the only solution is [0]." - have [simp]: "{l::nat list. length l = Suc 0 \ (\n\set l. n = 0)} = {[0]}" - by (auto simp: length_Suc_conv) - have "m=1 \ N=0" using 0 by linarith - then show ?case by simp + have m: "m \ 1" + by (simp add: Suc) + then show ?thesis + proof (induct "N + m - 1" arbitrary: N m) + case 0 \ "In the base case, the only solution is [0]." + have [simp]: "{l::nat list. length l = Suc 0 \ (\n\set l. n = 0)} = {[0]}" + by (auto simp: length_Suc_conv) + have "m = 1 \ N = 0" + using 0 by linarith + then show ?case + by simp + next + case (Suc k) + have c1: "card {l::nat list. size l = (m - 1) \ listsum l = N} = (N + (m - 1) - 1) choose N" + proof (cases "m = 1") + case True + with Suc.hyps have "N \ 1" + by auto + with True show ?thesis + by (simp add: binomial_eq_0) next - case (Suc k) - - have c1: "card {l::nat list. size l = (m - 1) \ listsum l = N} = - (N + (m - 1) - 1) choose N" - proof cases - assume "m = 1" - with Suc.hyps have "N\1" by auto - with \m = 1\ show ?thesis by (simp add: binomial_eq_0) - next - assume "m \ 1" thus ?thesis using Suc by fastforce - qed - - from Suc have c2: "card {l::nat list. size l = m \ listsum l + 1 = N} = - (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)" - proof - - have aux: "\m n. n > 0 \ Suc m = n \ m = n - 1" by arith - from Suc have "N>0 \ - card {l::nat list. size l = m \ listsum l + 1 = N} = - ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux) - thus ?thesis by auto - qed - - from Suc.prems have "(card {l::nat list. size l = (m - 1) \ listsum l = N} + + case False + then show ?thesis + using Suc by fastforce + qed + from Suc have c2: "card {l::nat list. size l = m \ listsum l + 1 = N} = + (if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)" + proof - + have *: "n > 0 \ Suc m = n \ m = n - 1" for m n + by arith + from Suc have "N > 0 \ + card {l::nat list. size l = m \ listsum l + 1 = N} = + ((N - 1) + m - 1) choose (N - 1)" + by (simp add: *) + then show ?thesis + by auto + qed + from Suc.prems have "(card {l::nat list. size l = (m - 1) \ listsum l = N} + card {l::nat list. size l = m \ listsum l + 1 = N}) = (N + m - 1) choose N" - by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def) - thus ?case using card_length_listsum_rec[OF Suc.prems] by auto - qed + by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def) + then show ?case + using card_length_listsum_rec[OF Suc.prems] by auto + qed qed - -lemma Suc_times_binomial_add: \ \by Lukas Bulwahn\ - "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)" +lemma Suc_times_binomial_add: "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)" + \ \by Lukas Bulwahn\ proof - have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat] by (simp only: fact_Suc add_Suc[symmetric] of_nat_id mult.assoc) - have "Suc a * (fact (Suc (a + b)) div (Suc a * fact a * fact b)) = Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))" by (subst div_mult_swap[symmetric]; simp only: mult.assoc dvd) @@ -1557,14 +1639,14 @@ using dvd[of b a] by (subst div_mult_swap[symmetric]; simp only: ac_simps dvd) finally show ?thesis by (subst (1 2) binomial_altdef_nat) - (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id) + (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id) qed subsection \Misc\ lemma fact_code [code]: - "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)" + "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)" proof - have "fact n = (of_nat (\{1..n}) :: 'a)" by (simp add: fact_setprod) @@ -1576,15 +1658,22 @@ qed lemma pochhammer_code [code]: - "pochhammer a n = (if n = 0 then 1 else - fold_atLeastAtMost_nat (\n acc. (a + of_nat n) * acc) 0 (n - 1) 1)" - by (cases n) (simp_all add: pochhammer_setprod setprod_atLeastAtMost_code [symmetric] atLeastLessThanSuc_atLeastAtMost) + "pochhammer a n = + (if n = 0 then 1 + else fold_atLeastAtMost_nat (\n acc. (a + of_nat n) * acc) 0 (n - 1) 1)" + by (cases n) + (simp_all add: pochhammer_setprod setprod_atLeastAtMost_code [symmetric] + atLeastLessThanSuc_atLeastAtMost) lemma gbinomial_code [code]: - "a gchoose n = (if n = 0 then 1 else - fold_atLeastAtMost_nat (\n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)" - by (cases n) (simp_all add: gbinomial_setprod_rev setprod_atLeastAtMost_code [symmetric] atLeastLessThanSuc_atLeastAtMost) + "a gchoose n = + (if n = 0 then 1 + else fold_atLeastAtMost_nat (\n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)" + by (cases n) + (simp_all add: gbinomial_setprod_rev setprod_atLeastAtMost_code [symmetric] + atLeastLessThanSuc_atLeastAtMost) +(* FIXME *) (*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *) (* @@ -1596,11 +1685,11 @@ proof - { assume "k \ n" - hence "{1..n} = {1..n-k} \ {n-k+1..n}" by auto - hence "(fact n :: nat) = fact (n-k) * \{n-k+1..n}" + then have "{1..n} = {1..n-k} \ {n-k+1..n}" by auto + then have "(fact n :: nat) = fact (n-k) * \{n-k+1..n}" by (simp add: setprod.union_disjoint fact_altdef_nat) } - thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code) + then show ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code) qed *)