--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu May 03 22:34:49 2018 +0100
@@ -939,15 +939,16 @@
fixes A :: "real^'n^'m"
assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
shows "orthogonal x y"
-proof (rule span_induct [OF y])
- show "subspace {a. orthogonal x a}"
+ using y
+proof (induction rule: span_induct)
+ case base
+ then show ?case
by (simp add: subspace_orthogonal_to_vector)
next
- fix v
- assume "v \<in> rows A"
+ case (step v)
then obtain i where "v = row i A"
by (auto simp: rows_def)
- with 0 show "orthogonal x v"
+ with 0 show ?case
unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
qed
--- a/src/HOL/Analysis/Starlike.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Thu May 03 22:34:49 2018 +0100
@@ -7030,8 +7030,7 @@
have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
- apply (erule span_induct [OF _ subspace_hyperplane])
- using 1 by (simp add: )
+ using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
by simp
have "dim(A \<union> B) = dim (span (A \<union> B))"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Thu May 03 22:34:49 2018 +0100
@@ -17,42 +17,48 @@
lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
by (simp add: Bernstein_def)
-lemma sum_Bernstein [simp]: "(\<Sum> k = 0..n. Bernstein n k x) = 1"
+lemma sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
using binomial_ring [of x "1-x" n]
by (simp add: Bernstein_def)
lemma binomial_deriv1:
- "(\<Sum>k=0..n. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b) ^ (n-1)"
+ "(\<Sum>k\<le>n. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b) ^ (n-1)"
apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a])
apply (subst binomial_ring)
- apply (rule derivative_eq_intros sum.cong | simp)+
+ apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+
done
lemma binomial_deriv2:
- "(\<Sum>k=0..n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
+ "(\<Sum>k\<le>n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
of_nat n * of_nat (n-1) * (a+b::real) ^ (n-2)"
apply (rule DERIV_unique [where f = "\<lambda>a. of_nat n * (a+b::real) ^ (n-1)" and x=a])
apply (subst binomial_deriv1 [symmetric])
apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+
done
-lemma sum_k_Bernstein [simp]: "(\<Sum>k = 0..n. real k * Bernstein n k x) = of_nat n * x"
+lemma sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x"
apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric])
apply (simp add: sum_distrib_right)
apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: sum.cong)
done
-lemma sum_kk_Bernstein [simp]: "(\<Sum> k = 0..n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2"
+lemma sum_kk_Bernstein [simp]: "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2"
proof -
- have "(\<Sum> k = 0..n. real k * (real k - 1) * Bernstein n k x) = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2"
- apply (subst binomial_deriv2 [of n x "1-x", simplified, symmetric])
- apply (simp add: sum_distrib_right)
- apply (rule sum.cong [OF refl])
- apply (simp add: Bernstein_def power2_eq_square algebra_simps)
- apply (rename_tac k)
- apply (subgoal_tac "k = 0 \<or> k = 1 \<or> (\<exists>k'. k = Suc (Suc k'))")
- apply (force simp add: field_simps of_nat_Suc power2_eq_square)
- by presburger
+ have "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) =
+ (\<Sum>k\<le>n. real k * real (k - Suc 0) * real (n choose k) * x ^ (k - 2) * (1 - x) ^ (n - k) * x\<^sup>2)"
+ proof (rule sum.cong [OF refl], simp)
+ fix k
+ assume "k \<le> n"
+ then consider "k = 0" | "k = 1" | k' where "k = Suc (Suc k')"
+ by (metis One_nat_def not0_implies_Suc)
+ then show "k = 0 \<or>
+ (real k - 1) * Bernstein n k x =
+ real (k - Suc 0) *
+ (real (n choose k) * (x ^ (k - 2) * ((1 - x) ^ (n - k) * x\<^sup>2)))"
+ by cases (auto simp add: Bernstein_def power2_eq_square algebra_simps)
+ qed
+ also have "... = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2"
+ by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right)
also have "... = n * (n - 1) * x\<^sup>2"
by auto
finally show ?thesis
@@ -65,7 +71,7 @@
fixes f :: "real \<Rightarrow> real"
assumes contf: "continuous_on {0..1} f" and e: "0 < e"
shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}
- \<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e"
+ \<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < e"
proof -
have "bounded (f ` {0..1})"
using compact_continuous_image compact_imp_bounded contf by blast
@@ -86,22 +92,22 @@
using \<open>0\<le>M\<close> by simp
finally have [simp]: "real_of_int (nat \<lceil>4 * M / (e * d\<^sup>2)\<rceil>) = real_of_int \<lceil>4 * M / (e * d\<^sup>2)\<rceil>"
using \<open>0\<le>M\<close> e \<open>0<d\<close>
- by (simp add: of_nat_Suc field_simps)
+ by (simp add: field_simps)
have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))"
- by (simp add: of_nat_Suc real_nat_ceiling_ge)
+ by (simp add: real_nat_ceiling_ge)
also have "... \<le> real n"
- using n by (simp add: of_nat_Suc field_simps)
+ using n by (simp add: field_simps)
finally have nbig: "4*M/(e*d\<^sup>2) + 1 \<le> real n" .
- have sum_bern: "(\<Sum>k = 0..n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n"
+ have sum_bern: "(\<Sum>k\<le>n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n"
proof -
have *: "\<And>a b x::real. (a - b)\<^sup>2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x"
by (simp add: algebra_simps power2_eq_square)
- have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
+ have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
apply (simp add: * sum.distrib)
apply (simp add: sum_distrib_left [symmetric] mult.assoc)
apply (simp add: algebra_simps power2_eq_square)
done
- then have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
+ then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
by (simp add: power2_eq_square)
then show ?thesis
using n by (simp add: sum_divide_distrib divide_simps mult.commute power2_commute)
@@ -137,9 +143,9 @@
finally show ?thesis .
qed
} note * = this
- have "\<bar>f x - (\<Sum> k = 0..n. f(k / n) * Bernstein n k x)\<bar> \<le> \<bar>\<Sum> k = 0..n. (f x - f(k / n)) * Bernstein n k x\<bar>"
+ have "\<bar>f x - (\<Sum>k\<le>n. f(k / n) * Bernstein n k x)\<bar> \<le> \<bar>\<Sum>k\<le>n. (f x - f(k / n)) * Bernstein n k x\<bar>"
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
- also have "... \<le> (\<Sum> k = 0..n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)"
+ also have "... \<le> (\<Sum>k\<le>n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)"
apply (rule order_trans [OF sum_abs sum_mono])
using *
apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono)
@@ -154,7 +160,7 @@
using \<open>d>0\<close> nbig e \<open>n>0\<close>
apply (simp add: divide_simps algebra_simps)
using ed0 by linarith
- finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
+ finally have "\<bar>f x - (\<Sum>k\<le>n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
}
then show ?thesis
by auto
@@ -893,20 +899,20 @@
lemma sum_max_0:
fixes x::real (*in fact "'a::comm_ring_1"*)
- shows "(\<Sum>i = 0..max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i = 0..m. x^i * a i)"
+ shows "(\<Sum>i\<le>max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i\<le>m. x^i * a i)"
proof -
- have "(\<Sum>i = 0..max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i = 0..max m n. (if i \<le> m then x^i * a i else 0))"
+ have "(\<Sum>i\<le>max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i\<le>max m n. (if i \<le> m then x^i * a i else 0))"
by (auto simp: algebra_simps intro: sum.cong)
- also have "... = (\<Sum>i = 0..m. (if i \<le> m then x^i * a i else 0))"
+ also have "... = (\<Sum>i\<le>m. (if i \<le> m then x^i * a i else 0))"
by (rule sum.mono_neutral_right) auto
- also have "... = (\<Sum>i = 0..m. x^i * a i)"
+ also have "... = (\<Sum>i\<le>m. x^i * a i)"
by (auto simp: algebra_simps intro: sum.cong)
finally show ?thesis .
qed
lemma real_polynomial_function_imp_sum:
assumes "real_polynomial_function f"
- shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i)"
+ shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i)"
using assms
proof (induct f)
case (linear f)
@@ -925,7 +931,7 @@
done
case (add f1 f2)
then obtain a1 n1 a2 n2 where
- "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)"
+ "f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x ^ i)"
by auto
then show ?case
apply (rule_tac x="\<lambda>i. (if i \<le> n1 then a1 i else 0) + (if i \<le> n2 then a2 i else 0)" in exI)
@@ -935,10 +941,10 @@
done
case (mult f1 f2)
then obtain a1 n1 a2 n2 where
- "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)"
+ "f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x ^ i)"
by auto
then obtain b1 b2 where
- "f1 = (\<lambda>x. \<Sum>i = 0..n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. b2 i * x ^ i)"
+ "f1 = (\<lambda>x. \<Sum>i\<le>n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. b2 i * x ^ i)"
"b1 = (\<lambda>i. if i\<le>n1 then a1 i else 0)" "b2 = (\<lambda>i. if i\<le>n2 then a2 i else 0)"
by auto
then show ?case
@@ -950,7 +956,7 @@
qed
lemma real_polynomial_function_iff_sum:
- "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i))"
+ "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i))"
apply (rule iffI)
apply (erule real_polynomial_function_imp_sum)
apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
--- a/src/HOL/Analysis/Winding_Numbers.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Thu May 03 22:34:49 2018 +0100
@@ -1070,9 +1070,12 @@
(at t within {0..1})"
proof (rule Lim_transform_within [OF _ \<open>d > 0\<close>])
have "continuous (at t within {0..1}) (g o p)"
- apply (rule continuous_within_compose)
- using \<open>path p\<close> continuous_on_eq_continuous_within path_def that apply blast
- by (metis (no_types, lifting) open_ball UNIV_I \<open>p t \<noteq> \<zeta>\<close> centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
+ proof (rule continuous_within_compose)
+ show "continuous (at t within {0..1}) p"
+ using \<open>path p\<close> continuous_on_eq_continuous_within path_def that by blast
+ show "continuous (at (p t) within p ` {0..1}) g"
+ by (metis (no_types, lifting) open_ball UNIV_I \<open>p t \<noteq> \<zeta>\<close> centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
+ qed
with LIM_zero have "((\<lambda>u. (g (subpath t u p 1) - g (subpath t u p 0))) \<longlongrightarrow> 0) (at t within {0..1})"
by (auto simp: subpath_def continuous_within o_def)
then show "((\<lambda>u. (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)) \<longlongrightarrow> 0)
@@ -1255,10 +1258,10 @@
by (auto simp: path_connected_def)
then have "pathstart r \<noteq> \<zeta>" by blast
have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
- apply (rule homotopic_paths_imp_homotopic_loops)
- apply (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
- using loops pas apply auto
- done
+ proof (rule homotopic_paths_imp_homotopic_loops)
+ show "homotopic_paths (- {\<zeta>}) p (r +++ q +++ reversepath r)"
+ by (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
+ qed (use loops pas in auto)
moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
ultimately show ?rhs
--- a/src/HOL/Binomial.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Binomial.thy Thu May 03 22:34:49 2018 +0100
@@ -156,7 +156,7 @@
text \<open>Avigad's version, generalized to any commutative ring\<close>
theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n =
- (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
+ (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
proof (induct n)
case 0
then show ?case by simp
@@ -166,32 +166,32 @@
by auto
have decomp2: "{0..n} = {0} \<union> {1..n}"
by auto
- have "(a + b)^(n+1) = (a + b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n - k))"
+ have "(a + b)^(n+1) = (a + b) * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k))"
using Suc.hyps by simp
- also have "\<dots> = a * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
- b * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+ also have "\<dots> = a * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k)) +
+ b * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k))"
by (rule distrib_right)
- also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
- (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n - k + 1))"
+ also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
+ (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k + 1))"
by (auto simp add: sum_distrib_left ac_simps)
- also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
+ also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
(\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))"
- by (simp add:sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
+ by (simp add: atMost_atLeast0 sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
also have "\<dots> = a^(n + 1) + b^(n + 1) +
(\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
(\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
- by (simp add: decomp2)
+ by (simp add: atMost_atLeast0 decomp2)
also have "\<dots> = a^(n + 1) + b^(n + 1) +
(\<Sum>k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat)
- also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
- using decomp by (simp add: field_simps)
+ also have "\<dots> = (\<Sum>k\<le>n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
+ using decomp by (simp add: atMost_atLeast0 field_simps)
finally show ?case
by simp
qed
text \<open>Original version for the naturals.\<close>
-corollary binomial: "(a + b :: nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n - k))"
+corollary binomial: "(a + b :: nat)^n = (\<Sum>k\<le>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_sum [symmetric] of_nat_eq_iff of_nat_id)
@@ -271,13 +271,13 @@
by (simp add: binomial_fact')
qed
-lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
+lemma choose_row_sum: "(\<Sum>k\<le>n. n choose k) = 2^n"
using binomial [of 1 "1" n] by (simp add: numeral_2_eq_2)
-lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
+lemma sum_choose_lower: "(\<Sum>k\<le>n. (r+k) choose k) = Suc (r+n) choose n"
by (induct n) auto
-lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
+lemma sum_choose_upper: "(\<Sum>k\<le>n. k choose m) = Suc n choose Suc m"
by (induct n) auto
lemma choose_alternating_sum:
@@ -313,17 +313,14 @@
finally show ?thesis ..
qed
-lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
- using choose_row_sum[of n] by (simp add: atLeast0AtMost)
-
text\<open>NW diagonal sum property\<close>
lemma sum_choose_diagonal:
assumes "m \<le> n"
- shows "(\<Sum>k=0..m. (n - k) choose (m - k)) = Suc n choose m"
+ shows "(\<Sum>k\<le>m. (n - k) choose (m - k)) = Suc n choose m"
proof -
- have "(\<Sum>k=0..m. (n-k) choose (m - k)) = (\<Sum>k=0..m. (n - m + k) choose k)"
+ have "(\<Sum>k\<le>m. (n-k) choose (m - k)) = (\<Sum>k\<le>m. (n - m + k) choose k)"
using sum.atLeastAtMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms
- by simp
+ by (simp add: atMost_atLeast0)
also have "\<dots> = Suc (n - m + m) choose m"
by (rule sum_choose_lower)
also have "\<dots> = Suc n choose m"
@@ -539,8 +536,8 @@
have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))"
by (simp add: Suc)
also have "\<dots> = Suc m * 2 ^ m"
- by (simp only: sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric])
- (simp add: choose_row_sum')
+ unfolding sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric]
+ by (simp add: choose_row_sum)
finally show ?thesis
using Suc by simp
qed
@@ -917,7 +914,7 @@
qed
lemma gbinomial_partial_sum_poly_xpos:
- "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
+ "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
(\<Sum>k\<le>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)
@@ -928,7 +925,7 @@
lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
proof -
have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
- using choose_row_sum[where n="2 * m + 1"] by simp
+ using choose_row_sum[where n="2 * m + 1"] by (simp add: atMost_atLeast0)
also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) =
(\<Sum>k = 0..m. (2 * m + 1 choose k)) +
(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
@@ -1135,7 +1132,7 @@
also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
by (subst sum_distrib_left[symmetric]) simp
also have "\<dots> = - ((-1 + 1) ^ card K) + 1"
- by (subst binomial_ring) (simp add: ac_simps)
+ by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
also have "\<dots> = 1"
using x K by (auto simp add: K_def card_gt_0_iff)
finally show "?lhs x = 1" .
--- a/src/HOL/NthRoot.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/NthRoot.thy Thu May 03 22:34:49 2018 +0100
@@ -730,7 +730,7 @@
by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
- also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+ also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)"
using \<open>2 < n\<close>
by (intro sum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
also have "\<dots> = (x n + 1) ^ n"
@@ -771,7 +771,7 @@
by (simp add: choose_one)
also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
- also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+ also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)"
using \<open>1 < n\<close> \<open>1 \<le> c\<close>
by (intro sum_mono2)
(auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
--- a/src/HOL/Transcendental.thy Thu May 03 18:40:14 2018 +0100
+++ b/src/HOL/Transcendental.thy Thu May 03 22:34:49 2018 +0100
@@ -188,11 +188,11 @@
shows "4^n / (2*real n) \<le> real ((2*n) choose n)"
proof -
from binomial[of 1 1 "2*n"]
- have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)"
+ have "4 ^ n = (\<Sum>k\<le>2*n. (2*n) choose k)"
by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
- also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
+ also have "{..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
- (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
+ (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
by (subst sum.union_disjoint) auto
also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
by (cases n) simp_all
@@ -994,27 +994,21 @@
and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
shows "(f \<longlongrightarrow> a 0) (at 0)"
proof -
- have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
- apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm])
- using s
- apply (auto simp: norm_divide)
- done
+ have "norm (of_real s / 2 :: 'a) < s"
+ using s by (auto simp: norm_divide)
+ then have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
+ by (rule sums_summable [OF sm])
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)"
- apply (rule termdiffs_strong)
- using s
- apply (auto simp: norm_divide)
- done
+ by (rule termdiffs_strong) (use s in \<open>auto simp: norm_divide\<close>)
then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
by (blast intro: DERIV_continuous)
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)"
by (simp add: continuous_within)
then show ?thesis
apply (rule Lim_transform)
- apply (auto simp add: LIM_eq)
+ apply (clarsimp simp: LIM_eq)
apply (rule_tac x="s" in exI)
- using s
- apply (auto simp: sm [THEN sums_unique])
- done
+ using s sm sums_unique by fastforce
qed
lemma powser_limit_0_strong: