# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525383289 -3600
# Node ID ee8c13ae81e96337e63343fc7b5f3203ff33286e
# Parent  315043faa871eff105e9dd7b79808fe374b29d49
Some tidying up (mostly regarding summations from 0)

diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Analysis/Starlike.thy
--- 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))"
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Analysis/Weierstrass_Theorems.thy
--- 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)
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Analysis/Winding_Numbers.thy
--- 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
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Binomial.thy
--- 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" .
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/NthRoot.thy
--- 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)
diff -r 315043faa871 -r ee8c13ae81e9 src/HOL/Transcendental.thy
--- 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: