diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Fri Feb 12 16:09:07 2016 +0100 +++ b/src/HOL/Binomial.thy Fri Feb 19 13:40:50 2016 +0100 @@ -28,7 +28,7 @@ lemma of_nat_fact [simp]: "of_nat (fact n) = fact n" by (induct n) (auto simp add: algebra_simps of_nat_mult) - + lemma of_int_fact [simp]: "of_int (fact n) = fact n" proof - @@ -56,22 +56,22 @@ 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_ge_1 [simp]: "fact n \ (1 :: 'a)" by (metis le0 fact.simps(1) 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_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_le_power: "fact n \ (of_nat (n^n) ::'a)" proof (induct n) @@ -86,7 +86,7 @@ by (metis of_nat_mult order_refl power_Suc) finally show ?case . qed simp - + end text\Note that @{term "fact 0 = fact 1"}\ @@ -100,7 +100,7 @@ lemma fact_ge_Suc_0_nat [simp]: "fact n \ Suc 0" by (metis One_nat_def fact_ge_1) -lemma dvd_fact: +lemma dvd_fact: shows "1 \ m \ m \ n \ m dvd fact n" by (induct n) (auto simp: dvdI le_Suc_eq) @@ -112,7 +112,7 @@ lemma fact_altdef: "fact n = (\i=1..n. of_nat i)" by (induct n) (auto simp: atLeastAtMostSuc_conv) - + lemma fact_altdef': "fact n = of_nat (\{1..n})" by (subst fact_altdef_nat [symmetric]) simp @@ -145,7 +145,7 @@ from this \m = n + d\ show ?thesis by simp qed -lemma fact_num_eq_if: +lemma fact_num_eq_if: "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))" by (cases m) auto @@ -402,20 +402,20 @@ lemma sum_choose_upper: "(\k=0..n. k choose m) = Suc n choose Suc m" by (induct n) auto -lemma choose_alternating_sum: +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) 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)" -proof - +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] by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power) also have "\ = (\i\n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))" by (simp add: setsum.distrib) - also have "\ = 2 * (\i\n. if even i then of_nat (n choose i) else 0)" + also have "\ = 2 * (\i\n. if even i then of_nat (n choose i) else 0)" by (subst setsum_right_distrib, intro setsum.cong) simp_all finally show ?thesis .. qed @@ -423,13 +423,13 @@ 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)" -proof - +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] by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power) also have "\ = (\i\n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))" by (simp add: setsum_subtractf) - also have "\ = 2 * (\i\n. if odd i then of_nat (n choose i) else 0)" + also have "\ = 2 * (\i\n. if odd i then of_nat (n choose i) else 0)" by (subst setsum_right_distrib, intro setsum.cong) simp_all finally show ?thesis .. qed @@ -473,7 +473,7 @@ lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\n. a + of_nat n) {0 .. n}" by (simp add: pochhammer_def) - + lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)" by (simp add: pochhammer_def of_nat_setprod) @@ -525,10 +525,10 @@ lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n" proof (induction n arbitrary: z) case (Suc n z) - have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" + have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" by (simp add: pochhammer_rec) also note Suc - also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = + also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = (z + of_nat (Suc n)) * pochhammer z (Suc n)" by (simp_all add: pochhammer_rec algebra_simps) finally show ?case . @@ -621,11 +621,11 @@ unfolding pochhammer_minus by (simp add: of_nat_diff pochhammer_fact) -lemma pochhammer_product': +lemma pochhammer_product': "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m" proof (induction n arbitrary: z) case (Suc n z) - have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = + have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc 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] @@ -634,7 +634,7 @@ finally show ?case by simp qed simp -lemma pochhammer_product: +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 @@ -645,7 +645,7 @@ case (Suc n) def n' \ "Suc n" have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') = - (pochhammer z n' * pochhammer (z + 1 / 2) 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) also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)" @@ -661,7 +661,7 @@ shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n" proof (induction n) case (Suc n) - have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * + have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)" by (simp add: pochhammer_rec' ac_simps of_nat_mult) also note Suc @@ -673,7 +673,7 @@ qed simp lemma pochhammer_absorb_comp: - "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" + "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" (is "?lhs = ?rhs") proof - have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps) @@ -714,7 +714,7 @@ finally show ?thesis by simp qed -lemma binomial_gbinomial: +lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)" proof - { assume kn: "k > n" @@ -741,7 +741,7 @@ have ?thesis using kn apply (simp add: binomial_fact[OF kn, where ?'a = 'a] gbinomial_pochhammer field_simps pochhammer_Suc_setprod) - apply (simp add: pochhammer_Suc_setprod fact_altdef h + apply (simp add: pochhammer_Suc_setprod fact_altdef h of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc) unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] unfolding mult.assoc @@ -817,19 +817,19 @@ (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.simps) - also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + + also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\i = 0..Suc h. a - of_nat i)" by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id) - also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + + 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.simps(2) 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) + + also have "... = of_nat (Suc (Suc h)) * (\i = 0..h. a - of_nat i) + (\i = 0..Suc h. a - of_nat i)" by (metis gbinomial_mult_fact mult.commute) 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::nat..Suc h}. a - of_nat i)" unfolding gbinomial_mult_fact' by (simp add: comm_semiring_class.distrib field_simps Suc) @@ -842,7 +842,7 @@ also have "\ = (fact (Suc k)) * ((a + 1) gchoose (Suc k))" unfolding gbinomial_mult_fact .. finally show ?thesis - by (metis fact_nonzero mult_cancel_left) + by (metis fact_nonzero mult_cancel_left) qed lemma gbinomial_reduce_nat: @@ -887,7 +887,7 @@ 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" - by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) + 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 @@ -898,7 +898,7 @@ proof (cases n) case (Suc m) with assms have "m > 0" by simp - have "(\i\n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = + 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)))" by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp @@ -940,7 +940,7 @@ also have "(\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) = 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) = + 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))" @@ -1010,7 +1010,7 @@ "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)" proof (cases b) case (Suc b) - hence "((a + 1) gchoose (Suc (Suc b))) = + hence "((a + 1) gchoose (Suc (Suc b))) = (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)" by (simp add: field_simps gbinomial_def) also have "(\i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)" @@ -1024,7 +1024,7 @@ "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)" proof (cases b) case (Suc b) - hence "((a + 1) gchoose (Suc (Suc b))) = + hence "((a + 1) gchoose (Suc (Suc b))) = (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)" by (simp add: field_simps gbinomial_def) also have "(\i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)" @@ -1045,9 +1045,9 @@ 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': +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"] + 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 @@ -1096,7 +1096,7 @@ 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" @@ -1108,7 +1108,7 @@ subsection \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} = + 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: @@ -1121,7 +1121,7 @@ thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac) qed -lemma gbinomial_index_swap: +lemma gbinomial_index_swap: "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)" (is "?lhs = ?rhs") proof - @@ -1132,7 +1132,7 @@ finally show ?thesis . qed -lemma gbinomial_sum_lower_neg: +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)" @@ -1146,7 +1146,7 @@ "(\k\m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))" proof (induction m) case (Suc mm) - hence "(\k\Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = + 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) also have "\ = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))" @@ -1175,10 +1175,10 @@ 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)) = + also have "(\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = (\k = (\k = (\kk=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))" @@ -1188,17 +1188,17 @@ 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:) qed - also have "\ + ?B = y * (\k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" + 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))) + 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)" + 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))" by (subst gbinomial_negated_upper) simp @@ -1208,13 +1208,13 @@ 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 = + 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 lemma gbinomial_partial_sum_poly_xpos: - "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = + "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = (\k\m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))" apply (subst gbinomial_partial_sum_poly) apply (subst gbinomial_negated_upper) @@ -1222,7 +1222,7 @@ apply (simp add: power_mult_distrib [symmetric]) done -lemma setsum_nat_symmetry: +lemma setsum_nat_symmetry: "(\k = 0..(m::nat). f k) = (\k = 0..m. f (m - k))" by (rule setsum.reindex_bij_witness[where i="\i. m - i" and j="\i. m - i"]) auto @@ -1247,7 +1247,7 @@ 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)" + have "?lhs = of_nat (\k\m. (2 * m + 1) choose k)" by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum) also have "\ = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl) finally show ?thesis by (simp add: of_nat_power) @@ -1270,7 +1270,7 @@ assumes "k \ m" 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) = + 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 @@ -1315,7 +1315,7 @@ apply (auto simp: of_nat_mult) done -lemma fact_fact_dvd_fact: +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) @@ -1568,12 +1568,12 @@ qed lemma pochhammer_code [code]: - "pochhammer a n = (if n = 0 then 1 else + "pochhammer a n = (if n = 0 then 1 else fold_atLeastAtMost_nat (\n acc. (a + of_nat n) * acc) 0 (n - 1) 1)" by (simp add: setprod_atLeastAtMost_code pochhammer_def) lemma gbinomial_code [code]: - "a gchoose n = (if n = 0 then 1 else + "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 (simp add: setprod_atLeastAtMost_code gbinomial_def) @@ -1593,7 +1593,7 @@ by (simp add: setprod.union_disjoint fact_altdef_nat) } thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code) -qed +qed *) end