# HG changeset patch # User wenzelm # Date 1661548627 -7200 # Node ID 8f1bb89ddf4bfc974048a0aabc9d9aaee918a0f3 # Parent c8d9fbe2dedd6ea608ec541de4b481af11d3e975# Parent 1f6d79b6222296093b705ed7500b1d954d72bc70 merged diff -r 1f6d79b62222 -r 8f1bb89ddf4b NEWS --- a/NEWS Fri Aug 26 23:12:42 2022 +0200 +++ b/NEWS Fri Aug 26 23:17:07 2022 +0200 @@ -166,6 +166,9 @@ * Theory "HOL-Library.Sublist": - Added lemma map_mono_strict_suffix. +* Theory "HOL-ex.Sum_of_Powers": + - Deleted. The same material is in the AFP as Bernoulli. + * Nitpick: To avoid technical issues, prefer non-JNI solvers to JNI solvers by default. Minor INCOMPATIBILITY. diff -r 1f6d79b62222 -r 8f1bb89ddf4b src/HOL/ROOT --- a/src/HOL/ROOT Fri Aug 26 23:12:42 2022 +0200 +++ b/src/HOL/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -728,7 +728,6 @@ Specifications_with_bundle_mixins Sqrt_Script Sudoku - Sum_of_Powers Tarski Termination ThreeDivides diff -r 1f6d79b62222 -r 8f1bb89ddf4b src/HOL/ex/Sum_of_Powers.thy --- a/src/HOL/ex/Sum_of_Powers.thy Fri Aug 26 23:12:42 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -(* Author: Lukas Bulwahn *) -section \Sum of Powers\ - -theory Sum_of_Powers -imports Complex_Main -begin - -subsection \Preliminaries\ - -lemma integrals_eq: - assumes "f a = g a" - assumes "\ x. ((\x. f x - g x) has_real_derivative 0) (at x)" - shows "f x = g x" - by (metis (no_types, lifting) DERIV_isconst_all assms(1) assms(2) eq_iff_diff_eq_0) - -lemma sum_diff: "((\i\n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0" - by (induct n) (auto simp add: field_simps) - -declare One_nat_def [simp del] - -subsection \Bernoulli Numbers and Bernoulli Polynomials\ - -declare sum.cong [fundef_cong] - -fun bernoulli :: "nat \ real" -where - "bernoulli 0 = (1::real)" -| "bernoulli (Suc n) = (-1 / (n + 2)) * (\k \ n. ((n + 2 choose k) * bernoulli k))" - -declare bernoulli.simps[simp del] - -definition - "bernpoly n = (\x. \k \ n. (n choose k) * bernoulli k * x ^ (n - k))" - -subsection \Basic Observations on Bernoulli Polynomials\ - -lemma bernpoly_0: "bernpoly n 0 = bernoulli n" -proof (cases n) - case 0 - then show "bernpoly n 0 = bernoulli n" - unfolding bernpoly_def bernoulli.simps by auto -next - case (Suc n') - have "(\k\n'. real (Suc n' choose k) * bernoulli k * 0 ^ (Suc n' - k)) = 0" - by (rule sum.neutral) auto - with Suc show ?thesis - unfolding bernpoly_def by simp -qed - -lemma sum_binomial_times_bernoulli: - "(\k\n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)" -proof (cases n) - case 0 - then show ?thesis by (simp add: bernoulli.simps) -next - case Suc - then show ?thesis - by (simp add: bernoulli.simps) - (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc') -qed - -subsection \Sum of Powers with Bernoulli Polynomials\ - -lemma bernpoly_derivative [derivative_intros]: - "(bernpoly (Suc n) has_real_derivative ((n + 1) * bernpoly n x)) (at x)" -proof - - have "(bernpoly (Suc n) has_real_derivative (\k\n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k))) (at x)" - unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp) - moreover have "(\k\n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k)) = (n + 1) * bernpoly n x" - unfolding bernpoly_def - by (auto intro: sum.cong simp add: sum_distrib_left real_binomial_eq_mult_binomial_Suc[of _ n] Suc_eq_plus1 of_nat_diff) - ultimately show ?thesis by auto -qed - -lemma diff_bernpoly: - "bernpoly n (x + 1) - bernpoly n x = n * x ^ (n - 1)" -proof (induct n arbitrary: x) - case 0 - show ?case unfolding bernpoly_def by auto -next - case (Suc n) - have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = (Suc n) * 0 ^ n" - unfolding bernpoly_0 unfolding bernpoly_def by (simp add: sum_binomial_times_bernoulli zero_power) - then have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = real (Suc n) * 0 ^ n" by (simp add: power_0_left) - have hyps': "\x. (real n + 1) * bernpoly n (x + 1) - (real n + 1) * bernpoly n x = real n * x ^ (n - Suc 0) * real (Suc n)" - unfolding right_diff_distrib[symmetric] by (simp add: Suc.hyps One_nat_def) - note [derivative_intros] = DERIV_chain'[where f = "\x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"] - have derivative: "\x. ((%x. bernpoly (Suc n) (x + 1) - bernpoly (Suc n) x - real (Suc n) * x ^ n) has_real_derivative 0) (at x)" - by (rule DERIV_cong) (fast intro!: derivative_intros, simp add: hyps') - from integrals_eq[OF const derivative] show ?case by simp -qed - -lemma sum_of_powers: "(\k\n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)" -proof - - from diff_bernpoly[of "Suc m", simplified] have "(m + (1::real)) * (\k\n. (real k) ^ m) = (\k\n. bernpoly (Suc m) (real k + 1) - bernpoly (Suc m) (real k))" - by (auto simp add: sum_distrib_left intro!: sum.cong) - also have "... = (\k\n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))" - by simp - also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0" - by (simp only: sum_diff[where f="\k. bernpoly (Suc m) (real k)"]) simp - finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp) -qed - -subsection \Instances for Square And Cubic Numbers\ - -lemma binomial_unroll: - "n > 0 \ (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))" - by (auto simp add: gr0_conv_Suc) - -lemma sum_unroll: - "(\k\n::nat. f k) = (if n = 0 then f 0 else f n + (\k\n - 1. f k))" -by auto (metis One_nat_def Suc_pred add.commute sum.atMost_Suc) - -lemma bernoulli_unroll: - "n > 0 \ bernoulli n = - 1 / (real n + 1) * (\k\n - 1. real (n + 1 choose k) * bernoulli k)" -by (cases n) (simp add: bernoulli.simps One_nat_def)+ - -lemmas unroll = binomial_unroll - bernoulli.simps(1) bernoulli_unroll sum_unroll bernpoly_def - -lemma sum_of_squares: "(\k\n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6" -proof - - have "real (\k\n::nat. k ^ 2) = (\k\n::nat. (real k) ^ 2)" by simp - also have "... = (bernpoly 3 (real (n + 1)) - bernpoly 3 0) / real (3 :: nat)" - by (auto simp add: sum_of_powers) - also have "... = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6" - by (simp add: unroll algebra_simps power2_eq_square power3_eq_cube One_nat_def[symmetric]) - finally show ?thesis by simp -qed - -lemma sum_of_squares_nat: "(\k\n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6" -proof - - from sum_of_squares have "real (6 * (\k\n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)" - by (auto simp add: field_simps) - then have "6 * (\k\n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n" - using of_nat_eq_iff by blast - then show ?thesis by auto -qed - -lemma sum_of_cubes: "(\k\n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4" -proof - - have two_plus_two: "2 + 2 = 4" by simp - have power4_eq: "\x::real. x ^ 4 = x * x * x * x" - by (simp only: two_plus_two[symmetric] power_add power2_eq_square) - have "real (\k\n::nat. k ^ 3) = (\k\n::nat. (real k) ^ 3)" by simp - also have "... = ((bernpoly 4 (n + 1) - bernpoly 4 0)) / (real (4 :: nat))" - by (auto simp add: sum_of_powers) - also have "... = ((n ^ 2 + n) / 2) ^ 2" - by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube) - finally show ?thesis by (simp add: power_divide) -qed - -lemma sum_of_cubes_nat: "(\k\n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4" -proof - - from sum_of_cubes have "real (4 * (\k\n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)" - by (auto simp add: field_simps) - then have "4 * (\k\n. k ^ 3) = (n ^ 2 + n) ^ 2" - using of_nat_eq_iff by blast - then show ?thesis by auto -qed - -end