Some tidying up (mostly regarding summations from 0)
authorpaulson <lp15@cam.ac.uk>
Thu May 03 22:34:49 2018 +0100 (15 months ago)
changeset 68077ee8c13ae81e9
parent 68076 315043faa871
child 68078 48e188cb1591
Some tidying up (mostly regarding summations from 0)
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Analysis/Winding_Numbers.thy
src/HOL/Binomial.thy
src/HOL/NthRoot.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 18:40:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 22:34:49 2018 +0100
     1.3 @@ -939,15 +939,16 @@
     1.4    fixes A :: "real^'n^'m"
     1.5    assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
     1.6    shows "orthogonal x y"
     1.7 -proof (rule span_induct [OF y])
     1.8 -  show "subspace {a. orthogonal x a}"
     1.9 +  using y
    1.10 +proof (induction rule: span_induct)
    1.11 +  case base
    1.12 +  then show ?case
    1.13      by (simp add: subspace_orthogonal_to_vector)
    1.14  next
    1.15 -  fix v
    1.16 -  assume "v \<in> rows A"
    1.17 +  case (step v)
    1.18    then obtain i where "v = row i A"
    1.19      by (auto simp: rows_def)
    1.20 -  with 0 show "orthogonal x v"
    1.21 +  with 0 show ?case
    1.22      unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
    1.23      by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
    1.24  qed
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Thu May 03 18:40:14 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu May 03 22:34:49 2018 +0100
     2.3 @@ -7030,8 +7030,7 @@
     2.4    have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     2.5      by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
     2.6    have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     2.7 -    apply (erule span_induct [OF _ subspace_hyperplane])
     2.8 -    using 1 by (simp add: )
     2.9 +    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
    2.10    then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
    2.11      by simp
    2.12    have "dim(A \<union> B) = dim (span (A \<union> B))"
     3.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu May 03 18:40:14 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu May 03 22:34:49 2018 +0100
     3.3 @@ -17,42 +17,48 @@
     3.4  lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
     3.5    by (simp add: Bernstein_def)
     3.6  
     3.7 -lemma sum_Bernstein [simp]: "(\<Sum> k = 0..n. Bernstein n k x) = 1"
     3.8 +lemma sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
     3.9    using binomial_ring [of x "1-x" n]
    3.10    by (simp add: Bernstein_def)
    3.11  
    3.12  lemma binomial_deriv1:
    3.13 -    "(\<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)"
    3.14 +    "(\<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)"
    3.15    apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a])
    3.16    apply (subst binomial_ring)
    3.17 -  apply (rule derivative_eq_intros sum.cong | simp)+
    3.18 +  apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+
    3.19    done
    3.20  
    3.21  lemma binomial_deriv2:
    3.22 -    "(\<Sum>k=0..n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
    3.23 +    "(\<Sum>k\<le>n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
    3.24       of_nat n * of_nat (n-1) * (a+b::real) ^ (n-2)"
    3.25    apply (rule DERIV_unique [where f = "\<lambda>a. of_nat n * (a+b::real) ^ (n-1)" and x=a])
    3.26    apply (subst binomial_deriv1 [symmetric])
    3.27    apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+
    3.28    done
    3.29  
    3.30 -lemma sum_k_Bernstein [simp]: "(\<Sum>k = 0..n. real k * Bernstein n k x) = of_nat n * x"
    3.31 +lemma sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x"
    3.32    apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric])
    3.33    apply (simp add: sum_distrib_right)
    3.34    apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: sum.cong)
    3.35    done
    3.36  
    3.37 -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"
    3.38 +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"
    3.39  proof -
    3.40 -  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"
    3.41 -    apply (subst binomial_deriv2 [of n x "1-x", simplified, symmetric])
    3.42 -    apply (simp add: sum_distrib_right)
    3.43 -    apply (rule sum.cong [OF refl])
    3.44 -    apply (simp add: Bernstein_def power2_eq_square algebra_simps)
    3.45 -    apply (rename_tac k)
    3.46 -    apply (subgoal_tac "k = 0 \<or> k = 1 \<or> (\<exists>k'. k = Suc (Suc k'))")
    3.47 -    apply (force simp add: field_simps of_nat_Suc power2_eq_square)
    3.48 -    by presburger
    3.49 +  have "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) =
    3.50 +        (\<Sum>k\<le>n. real k * real (k - Suc 0) * real (n choose k) * x ^ (k - 2) * (1 - x) ^ (n - k) * x\<^sup>2)"
    3.51 +  proof (rule sum.cong [OF refl], simp)
    3.52 +    fix k
    3.53 +    assume "k \<le> n"
    3.54 +    then consider "k = 0" | "k = 1" | k' where "k = Suc (Suc k')"
    3.55 +      by (metis One_nat_def not0_implies_Suc)
    3.56 +    then show "k = 0 \<or>
    3.57 +          (real k - 1) * Bernstein n k x =
    3.58 +          real (k - Suc 0) *
    3.59 +          (real (n choose k) * (x ^ (k - 2) * ((1 - x) ^ (n - k) * x\<^sup>2)))"
    3.60 +      by cases (auto simp add: Bernstein_def power2_eq_square algebra_simps)
    3.61 +  qed
    3.62 +  also have "... = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2"
    3.63 +    by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right)
    3.64    also have "... = n * (n - 1) * x\<^sup>2"
    3.65      by auto
    3.66    finally show ?thesis
    3.67 @@ -65,7 +71,7 @@
    3.68    fixes f :: "real \<Rightarrow> real"
    3.69    assumes contf: "continuous_on {0..1} f" and e: "0 < e"
    3.70      shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}
    3.71 -                    \<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e"
    3.72 +                    \<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < e"
    3.73  proof -
    3.74    have "bounded (f ` {0..1})"
    3.75      using compact_continuous_image compact_imp_bounded contf by blast
    3.76 @@ -86,22 +92,22 @@
    3.77        using \<open>0\<le>M\<close> by simp
    3.78      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>"
    3.79        using \<open>0\<le>M\<close> e \<open>0<d\<close>
    3.80 -      by (simp add: of_nat_Suc field_simps)
    3.81 +      by (simp add: field_simps)
    3.82      have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))"
    3.83 -      by (simp add: of_nat_Suc real_nat_ceiling_ge)
    3.84 +      by (simp add: real_nat_ceiling_ge)
    3.85      also have "... \<le> real n"
    3.86 -      using n by (simp add: of_nat_Suc field_simps)
    3.87 +      using n by (simp add: field_simps)
    3.88      finally have nbig: "4*M/(e*d\<^sup>2) + 1 \<le> real n" .
    3.89 -    have sum_bern: "(\<Sum>k = 0..n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n"
    3.90 +    have sum_bern: "(\<Sum>k\<le>n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n"
    3.91      proof -
    3.92        have *: "\<And>a b x::real. (a - b)\<^sup>2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x"
    3.93          by (simp add: algebra_simps power2_eq_square)
    3.94 -      have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
    3.95 +      have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
    3.96          apply (simp add: * sum.distrib)
    3.97          apply (simp add: sum_distrib_left [symmetric] mult.assoc)
    3.98          apply (simp add: algebra_simps power2_eq_square)
    3.99          done
   3.100 -      then have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
   3.101 +      then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
   3.102          by (simp add: power2_eq_square)
   3.103        then show ?thesis
   3.104          using n by (simp add: sum_divide_distrib divide_simps mult.commute power2_commute)
   3.105 @@ -137,9 +143,9 @@
   3.106          finally show ?thesis .
   3.107          qed
   3.108      } note * = this
   3.109 -    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>"
   3.110 +    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>"
   3.111        by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
   3.112 -    also have "... \<le> (\<Sum> k = 0..n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)"
   3.113 +    also have "... \<le> (\<Sum>k\<le>n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)"
   3.114        apply (rule order_trans [OF sum_abs sum_mono])
   3.115        using *
   3.116        apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono)
   3.117 @@ -154,7 +160,7 @@
   3.118        using \<open>d>0\<close> nbig e \<open>n>0\<close>
   3.119        apply (simp add: divide_simps algebra_simps)
   3.120        using ed0 by linarith
   3.121 -    finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
   3.122 +    finally have "\<bar>f x - (\<Sum>k\<le>n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
   3.123    }
   3.124    then show ?thesis
   3.125      by auto
   3.126 @@ -893,20 +899,20 @@
   3.127  
   3.128  lemma sum_max_0:
   3.129    fixes x::real (*in fact "'a::comm_ring_1"*)
   3.130 -  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)"
   3.131 +  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)"
   3.132  proof -
   3.133 -  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))"
   3.134 +  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))"
   3.135      by (auto simp: algebra_simps intro: sum.cong)
   3.136 -  also have "... = (\<Sum>i = 0..m. (if i \<le> m then x^i * a i else 0))"
   3.137 +  also have "... = (\<Sum>i\<le>m. (if i \<le> m then x^i * a i else 0))"
   3.138      by (rule sum.mono_neutral_right) auto
   3.139 -  also have "... = (\<Sum>i = 0..m. x^i * a i)"
   3.140 +  also have "... = (\<Sum>i\<le>m. x^i * a i)"
   3.141      by (auto simp: algebra_simps intro: sum.cong)
   3.142    finally show ?thesis .
   3.143  qed
   3.144  
   3.145  lemma real_polynomial_function_imp_sum:
   3.146    assumes "real_polynomial_function f"
   3.147 -    shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i)"
   3.148 +    shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i)"
   3.149  using assms
   3.150  proof (induct f)
   3.151    case (linear f)
   3.152 @@ -925,7 +931,7 @@
   3.153      done
   3.154    case (add f1 f2)
   3.155    then obtain a1 n1 a2 n2 where
   3.156 -    "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)"
   3.157 +    "f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x ^ i)"
   3.158      by auto
   3.159    then show ?case
   3.160      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)
   3.161 @@ -935,10 +941,10 @@
   3.162      done
   3.163    case (mult f1 f2)
   3.164    then obtain a1 n1 a2 n2 where
   3.165 -    "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)"
   3.166 +    "f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x ^ i)"
   3.167      by auto
   3.168    then obtain b1 b2 where
   3.169 -    "f1 = (\<lambda>x. \<Sum>i = 0..n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. b2 i * x ^ i)"
   3.170 +    "f1 = (\<lambda>x. \<Sum>i\<le>n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. b2 i * x ^ i)"
   3.171      "b1 = (\<lambda>i. if i\<le>n1 then a1 i else 0)" "b2 = (\<lambda>i. if i\<le>n2 then a2 i else 0)"
   3.172      by auto
   3.173    then show ?case
   3.174 @@ -950,7 +956,7 @@
   3.175  qed
   3.176  
   3.177  lemma real_polynomial_function_iff_sum:
   3.178 -     "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i))"
   3.179 +     "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i))"
   3.180    apply (rule iffI)
   3.181    apply (erule real_polynomial_function_imp_sum)
   3.182    apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
     4.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Thu May 03 18:40:14 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Thu May 03 22:34:49 2018 +0100
     4.3 @@ -1070,9 +1070,12 @@
     4.4              (at t within {0..1})"
     4.5        proof (rule Lim_transform_within [OF _ \<open>d > 0\<close>])
     4.6          have "continuous (at t within {0..1}) (g o p)"
     4.7 -          apply (rule continuous_within_compose)
     4.8 -          using \<open>path p\<close> continuous_on_eq_continuous_within path_def that apply blast
     4.9 -          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)
    4.10 +        proof (rule continuous_within_compose)
    4.11 +          show "continuous (at t within {0..1}) p"
    4.12 +            using \<open>path p\<close> continuous_on_eq_continuous_within path_def that by blast
    4.13 +          show "continuous (at (p t) within p ` {0..1}) g"
    4.14 +            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)
    4.15 +        qed
    4.16          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})"
    4.17            by (auto simp: subpath_def continuous_within o_def)
    4.18          then show "((\<lambda>u.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)) \<longlongrightarrow> 0)
    4.19 @@ -1255,10 +1258,10 @@
    4.20      by (auto simp: path_connected_def)
    4.21    then have "pathstart r \<noteq> \<zeta>" by blast
    4.22    have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
    4.23 -    apply (rule homotopic_paths_imp_homotopic_loops)
    4.24 -    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)
    4.25 -    using loops pas apply auto
    4.26 -    done
    4.27 +  proof (rule homotopic_paths_imp_homotopic_loops)
    4.28 +    show "homotopic_paths (- {\<zeta>}) p (r +++ q +++ reversepath r)"
    4.29 +      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)
    4.30 +  qed (use loops pas in auto)
    4.31    moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
    4.32      using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
    4.33    ultimately show ?rhs
     5.1 --- a/src/HOL/Binomial.thy	Thu May 03 18:40:14 2018 +0100
     5.2 +++ b/src/HOL/Binomial.thy	Thu May 03 22:34:49 2018 +0100
     5.3 @@ -156,7 +156,7 @@
     5.4  
     5.5  text \<open>Avigad's version, generalized to any commutative ring\<close>
     5.6  theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n =
     5.7 -  (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
     5.8 +  (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
     5.9  proof (induct n)
    5.10    case 0
    5.11    then show ?case by simp
    5.12 @@ -166,32 +166,32 @@
    5.13      by auto
    5.14    have decomp2: "{0..n} = {0} \<union> {1..n}"
    5.15      by auto
    5.16 -  have "(a + b)^(n+1) = (a + b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n - k))"
    5.17 +  have "(a + b)^(n+1) = (a + b) * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k))"
    5.18      using Suc.hyps by simp
    5.19 -  also have "\<dots> = a * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
    5.20 -      b * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    5.21 +  also have "\<dots> = a * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k)) +
    5.22 +      b * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k))"
    5.23      by (rule distrib_right)
    5.24 -  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
    5.25 -      (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n - k + 1))"
    5.26 +  also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
    5.27 +      (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k + 1))"
    5.28      by (auto simp add: sum_distrib_left ac_simps)
    5.29 -  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
    5.30 +  also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
    5.31        (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))"
    5.32 -    by (simp add:sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
    5.33 +    by (simp add: atMost_atLeast0 sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
    5.34    also have "\<dots> = a^(n + 1) + b^(n + 1) +
    5.35        (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
    5.36        (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
    5.37 -    by (simp add: decomp2)
    5.38 +    by (simp add: atMost_atLeast0 decomp2)
    5.39    also have "\<dots> = a^(n + 1) + b^(n + 1) +
    5.40        (\<Sum>k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
    5.41      by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat)
    5.42 -  also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
    5.43 -    using decomp by (simp add: field_simps)
    5.44 +  also have "\<dots> = (\<Sum>k\<le>n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
    5.45 +    using decomp by (simp add: atMost_atLeast0 field_simps)
    5.46    finally show ?case
    5.47      by simp
    5.48  qed
    5.49  
    5.50  text \<open>Original version for the naturals.\<close>
    5.51 -corollary binomial: "(a + b :: nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n - k))"
    5.52 +corollary binomial: "(a + b :: nat)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n - k))"
    5.53    using binomial_ring [of "int a" "int b" n]
    5.54    by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]
    5.55        of_nat_sum [symmetric] of_nat_eq_iff of_nat_id)
    5.56 @@ -271,13 +271,13 @@
    5.57      by (simp add: binomial_fact')
    5.58  qed
    5.59  
    5.60 -lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
    5.61 +lemma choose_row_sum: "(\<Sum>k\<le>n. n choose k) = 2^n"
    5.62    using binomial [of 1 "1" n] by (simp add: numeral_2_eq_2)
    5.63  
    5.64 -lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
    5.65 +lemma sum_choose_lower: "(\<Sum>k\<le>n. (r+k) choose k) = Suc (r+n) choose n"
    5.66    by (induct n) auto
    5.67  
    5.68 -lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
    5.69 +lemma sum_choose_upper: "(\<Sum>k\<le>n. k choose m) = Suc n choose Suc m"
    5.70    by (induct n) auto
    5.71  
    5.72  lemma choose_alternating_sum:
    5.73 @@ -313,17 +313,14 @@
    5.74    finally show ?thesis ..
    5.75  qed
    5.76  
    5.77 -lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
    5.78 -  using choose_row_sum[of n] by (simp add: atLeast0AtMost)
    5.79 -
    5.80  text\<open>NW diagonal sum property\<close>
    5.81  lemma sum_choose_diagonal:
    5.82    assumes "m \<le> n"
    5.83 -  shows "(\<Sum>k=0..m. (n - k) choose (m - k)) = Suc n choose m"
    5.84 +  shows "(\<Sum>k\<le>m. (n - k) choose (m - k)) = Suc n choose m"
    5.85  proof -
    5.86 -  have "(\<Sum>k=0..m. (n-k) choose (m - k)) = (\<Sum>k=0..m. (n - m + k) choose k)"
    5.87 +  have "(\<Sum>k\<le>m. (n-k) choose (m - k)) = (\<Sum>k\<le>m. (n - m + k) choose k)"
    5.88      using sum.atLeastAtMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms
    5.89 -      by simp
    5.90 +    by (simp add: atMost_atLeast0)
    5.91    also have "\<dots> = Suc (n - m + m) choose m"
    5.92      by (rule sum_choose_lower)
    5.93    also have "\<dots> = Suc n choose m"
    5.94 @@ -539,8 +536,8 @@
    5.95    have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))"
    5.96      by (simp add: Suc)
    5.97    also have "\<dots> = Suc m * 2 ^ m"
    5.98 -    by (simp only: sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric])
    5.99 -       (simp add: choose_row_sum')
   5.100 +    unfolding sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric]
   5.101 +    by (simp add: choose_row_sum)
   5.102    finally show ?thesis
   5.103      using Suc by simp
   5.104  qed
   5.105 @@ -917,7 +914,7 @@
   5.106  qed
   5.107  
   5.108  lemma gbinomial_partial_sum_poly_xpos:
   5.109 -  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
   5.110 +    "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
   5.111       (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
   5.112    apply (subst gbinomial_partial_sum_poly)
   5.113    apply (subst gbinomial_negated_upper)
   5.114 @@ -928,7 +925,7 @@
   5.115  lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
   5.116  proof -
   5.117    have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
   5.118 -    using choose_row_sum[where n="2 * m + 1"] by simp
   5.119 +    using choose_row_sum[where n="2 * m + 1"]  by (simp add: atMost_atLeast0)
   5.120    also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) =
   5.121        (\<Sum>k = 0..m. (2 * m + 1 choose k)) +
   5.122        (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
   5.123 @@ -1135,7 +1132,7 @@
   5.124      also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
   5.125        by (subst sum_distrib_left[symmetric]) simp
   5.126      also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
   5.127 -      by (subst binomial_ring) (simp add: ac_simps)
   5.128 +      by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
   5.129      also have "\<dots> = 1"
   5.130        using x K by (auto simp add: K_def card_gt_0_iff)
   5.131      finally show "?lhs x = 1" .
     6.1 --- a/src/HOL/NthRoot.thy	Thu May 03 18:40:14 2018 +0100
     6.2 +++ b/src/HOL/NthRoot.thy	Thu May 03 22:34:49 2018 +0100
     6.3 @@ -730,7 +730,7 @@
     6.4          by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
     6.5        also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
     6.6          by (simp add: x_def)
     6.7 -      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
     6.8 +      also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)"
     6.9          using \<open>2 < n\<close>
    6.10          by (intro sum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    6.11        also have "\<dots> = (x n + 1) ^ n"
    6.12 @@ -771,7 +771,7 @@
    6.13            by (simp add: choose_one)
    6.14          also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    6.15            by (simp add: x_def)
    6.16 -        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    6.17 +        also have "\<dots> \<le> (\<Sum>k\<le>n. of_nat (n choose k) * x n^k)"
    6.18            using \<open>1 < n\<close> \<open>1 \<le> c\<close>
    6.19            by (intro sum_mono2)
    6.20              (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
     7.1 --- a/src/HOL/Transcendental.thy	Thu May 03 18:40:14 2018 +0100
     7.2 +++ b/src/HOL/Transcendental.thy	Thu May 03 22:34:49 2018 +0100
     7.3 @@ -188,11 +188,11 @@
     7.4    shows   "4^n / (2*real n) \<le> real ((2*n) choose n)"
     7.5  proof -
     7.6    from binomial[of 1 1 "2*n"]
     7.7 -    have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)"
     7.8 +    have "4 ^ n = (\<Sum>k\<le>2*n. (2*n) choose k)"
     7.9      by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
    7.10 -  also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
    7.11 +  also have "{..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
    7.12    also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
    7.13 -               (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
    7.14 +             (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
    7.15      by (subst sum.union_disjoint) auto
    7.16    also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
    7.17      by (cases n) simp_all
    7.18 @@ -994,27 +994,21 @@
    7.19      and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
    7.20    shows "(f \<longlongrightarrow> a 0) (at 0)"
    7.21  proof -
    7.22 -  have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
    7.23 -    apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm])
    7.24 -    using s
    7.25 -    apply (auto simp: norm_divide)
    7.26 -    done
    7.27 +  have "norm (of_real s / 2 :: 'a) < s"
    7.28 +    using s  by (auto simp: norm_divide)
    7.29 +  then have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
    7.30 +    by (rule sums_summable [OF sm])
    7.31    then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)"
    7.32 -    apply (rule termdiffs_strong)
    7.33 -    using s
    7.34 -    apply (auto simp: norm_divide)
    7.35 -    done
    7.36 +    by (rule termdiffs_strong) (use s in \<open>auto simp: norm_divide\<close>)
    7.37    then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
    7.38      by (blast intro: DERIV_continuous)
    7.39    then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)"
    7.40      by (simp add: continuous_within)
    7.41    then show ?thesis
    7.42      apply (rule Lim_transform)
    7.43 -    apply (auto simp add: LIM_eq)
    7.44 +    apply (clarsimp simp: LIM_eq)
    7.45      apply (rule_tac x="s" in exI)
    7.46 -    using s
    7.47 -    apply (auto simp: sm [THEN sums_unique])
    7.48 -    done
    7.49 +    using s sm sums_unique by fastforce
    7.50  qed
    7.51  
    7.52  lemma powser_limit_0_strong: