author paulson Thu May 03 22:34:49 2018 +0100 (15 months ago) changeset 68077 ee8c13ae81e9 parent 68076 315043faa871 child 68078 48e188cb1591
Some tidying up (mostly regarding summations from 0)
 src/HOL/Analysis/Cartesian_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | revisions src/HOL/Analysis/Weierstrass_Theorems.thy file | annotate | diff | revisions src/HOL/Analysis/Winding_Numbers.thy file | annotate | diff | revisions src/HOL/Binomial.thy file | annotate | diff | revisions src/HOL/NthRoot.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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.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.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.14          also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
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)"