src/HOL/Series.thy
changeset 64267 b9a1486e79be
parent 63952 354808e9f44b
child 65680 378a2f11bec9
     1.1 --- a/src/HOL/Series.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Series.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Copyright   : 1998  University of Cambridge
     1.5  
     1.6  Converted to Isar and polished by lcp
     1.7 -Converted to setsum and polished yet more by TNN
     1.8 +Converted to sum and polished yet more by TNN
     1.9  Additional contributions by Jeremy Avigad
    1.10  *)
    1.11  
    1.12 @@ -51,9 +51,9 @@
    1.13  lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)"
    1.14    by (simp add: summable_def sums_def convergent_def)
    1.15  
    1.16 -lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
    1.17 +lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. sum f {..n})"
    1.18    by (simp_all only: summable_iff_convergent convergent_def
    1.19 -        lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"])
    1.20 +        lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. sum f {..<n}"])
    1.21  
    1.22  lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
    1.23    by (simp add: suminf_def sums_def lim_def)
    1.24 @@ -64,8 +64,8 @@
    1.25  lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    1.26    by (rule sums_zero [THEN sums_summable])
    1.27  
    1.28 -lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
    1.29 -  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
    1.30 +lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s"
    1.31 +  apply (simp only: sums_def sum_nat_group tendsto_def eventually_sequentially)
    1.32    apply safe
    1.33    apply (erule_tac x=S in allE)
    1.34    apply safe
    1.35 @@ -88,22 +88,22 @@
    1.36      by (auto simp: eventually_at_top_linorder)
    1.37    define C where "C = (\<Sum>k<N. f k - g k)"
    1.38    from eventually_ge_at_top[of N]
    1.39 -  have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
    1.40 +  have "eventually (\<lambda>n. sum f {..<n} = C + sum g {..<n}) sequentially"
    1.41    proof eventually_elim
    1.42      case (elim n)
    1.43      then have "{..<n} = {..<N} \<union> {N..<n}"
    1.44        by auto
    1.45 -    also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}"
    1.46 -      by (intro setsum.union_disjoint) auto
    1.47 -    also from N have "setsum f {N..<n} = setsum g {N..<n}"
    1.48 -      by (intro setsum.cong) simp_all
    1.49 -    also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})"
    1.50 -      unfolding C_def by (simp add: algebra_simps setsum_subtractf)
    1.51 -    also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})"
    1.52 -      by (intro setsum.union_disjoint [symmetric]) auto
    1.53 +    also have "sum f ... = sum f {..<N} + sum f {N..<n}"
    1.54 +      by (intro sum.union_disjoint) auto
    1.55 +    also from N have "sum f {N..<n} = sum g {N..<n}"
    1.56 +      by (intro sum.cong) simp_all
    1.57 +    also have "sum f {..<N} + sum g {N..<n} = C + (sum g {..<N} + sum g {N..<n})"
    1.58 +      unfolding C_def by (simp add: algebra_simps sum_subtractf)
    1.59 +    also have "sum g {..<N} + sum g {N..<n} = sum g ({..<N} \<union> {N..<n})"
    1.60 +      by (intro sum.union_disjoint [symmetric]) auto
    1.61      also from elim have "{..<N} \<union> {N..<n} = {..<n}"
    1.62        by auto
    1.63 -    finally show "setsum f {..<n} = C + setsum g {..<n}" .
    1.64 +    finally show "sum f {..<n} = C + sum g {..<n}" .
    1.65    qed
    1.66    from convergent_cong[OF this] show ?thesis
    1.67      by (simp add: summable_iff_convergent convergent_add_const_iff)
    1.68 @@ -114,7 +114,7 @@
    1.69      and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    1.70    shows "f sums (\<Sum>n\<in>N. f n)"
    1.71  proof -
    1.72 -  have eq: "setsum f {..<n + Suc (Max N)} = setsum f N" for n
    1.73 +  have eq: "sum f {..<n + Suc (Max N)} = sum f N" for n
    1.74    proof (cases "N = {}")
    1.75      case True
    1.76      with f have "f = (\<lambda>x. 0)" by auto
    1.77 @@ -122,7 +122,7 @@
    1.78    next
    1.79      case [simp]: False
    1.80      show ?thesis
    1.81 -    proof (safe intro!: setsum.mono_neutral_right f)
    1.82 +    proof (safe intro!: sum.mono_neutral_right f)
    1.83        fix i
    1.84        assume "i \<in> N"
    1.85        then have "i \<le> Max N" by simp
    1.86 @@ -136,7 +136,7 @@
    1.87  qed
    1.88  
    1.89  corollary sums_0: "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"
    1.90 -    by (metis (no_types) finite.emptyI setsum.empty sums_finite)
    1.91 +    by (metis (no_types) finite.emptyI sum.empty sums_finite)
    1.92  
    1.93  lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
    1.94    by (rule sums_summable) (rule sums_finite)
    1.95 @@ -199,7 +199,7 @@
    1.96  
    1.97  lemma sums_le: "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
    1.98    for f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
    1.99 -  by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
   1.100 +  by (rule LIMSEQ_le) (auto intro: sum_mono simp: sums_def)
   1.101  
   1.102  context
   1.103    fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
   1.104 @@ -208,13 +208,13 @@
   1.105  lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
   1.106    by (auto dest: sums_summable intro: sums_le)
   1.107  
   1.108 -lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
   1.109 +lemma sum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> sum f {..<n} \<le> suminf f"
   1.110    by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
   1.111  
   1.112  lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
   1.113 -  using setsum_le_suminf[of 0] by simp
   1.114 +  using sum_le_suminf[of 0] by simp
   1.115  
   1.116 -lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   1.117 +lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. sum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   1.118    by (metis LIMSEQ_le_const2 summable_LIMSEQ)
   1.119  
   1.120  lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
   1.121 @@ -224,24 +224,24 @@
   1.122      using summable_LIMSEQ[of f] by simp
   1.123    then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
   1.124    proof (rule LIMSEQ_le_const)
   1.125 -    show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}" for i
   1.126 -      using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
   1.127 +    show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> sum f {..<n}" for i
   1.128 +      using pos by (intro exI[of _ "Suc i"] allI impI sum_mono2) auto
   1.129    qed
   1.130    with pos show "\<forall>n. f n = 0"
   1.131      by (auto intro!: antisym)
   1.132  qed (metis suminf_zero fun_eq_iff)
   1.133  
   1.134  lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   1.135 -  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   1.136 +  using sum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   1.137  
   1.138  lemma suminf_pos2:
   1.139    assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
   1.140    shows "0 < suminf f"
   1.141  proof -
   1.142    have "0 < (\<Sum>n<Suc i. f n)"
   1.143 -    using assms by (intro setsum_pos2[where i=i]) auto
   1.144 +    using assms by (intro sum_pos2[where i=i]) auto
   1.145    also have "\<dots> \<le> suminf f"
   1.146 -    using assms by (intro setsum_le_suminf) auto
   1.147 +    using assms by (intro sum_le_suminf) auto
   1.148    finally show ?thesis .
   1.149  qed
   1.150  
   1.151 @@ -254,15 +254,15 @@
   1.152    fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add,linorder_topology}"
   1.153  begin
   1.154  
   1.155 -lemma setsum_less_suminf2:
   1.156 -  "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
   1.157 -  using setsum_le_suminf[of f "Suc i"]
   1.158 -    and add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   1.159 -    and setsum_mono2[of "{..<i}" "{..<n}" f]
   1.160 +lemma sum_less_suminf2:
   1.161 +  "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
   1.162 +  using sum_le_suminf[of f "Suc i"]
   1.163 +    and add_strict_increasing[of "f i" "sum f {..<n}" "sum f {..<i}"]
   1.164 +    and sum_mono2[of "{..<i}" "{..<n}" f]
   1.165    by (auto simp: less_imp_le ac_simps)
   1.166  
   1.167 -lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   1.168 -  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
   1.169 +lemma sum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> sum f {..<n} < suminf f"
   1.170 +  using sum_less_suminf2[of n n] by (simp add: less_imp_le)
   1.171  
   1.172  end
   1.173  
   1.174 @@ -273,10 +273,10 @@
   1.175    shows "summable f"
   1.176    unfolding summable_def sums_def [abs_def]
   1.177  proof (rule exI LIMSEQ_incseq_SUP)+
   1.178 -  show "bdd_above (range (\<lambda>n. setsum f {..<n}))"
   1.179 +  show "bdd_above (range (\<lambda>n. sum f {..<n}))"
   1.180      using le by (auto simp: bdd_above_def)
   1.181 -  show "incseq (\<lambda>n. setsum f {..<n})"
   1.182 -    by (auto simp: mono_def intro!: setsum_mono2)
   1.183 +  show "incseq (\<lambda>n. sum f {..<n})"
   1.184 +    by (auto simp: mono_def intro!: sum_mono2)
   1.185  qed
   1.186  
   1.187  lemma summableI[intro, simp]: "summable f"
   1.188 @@ -298,13 +298,13 @@
   1.189      using assms by (auto intro!: tendsto_add simp: sums_def)
   1.190    moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
   1.191      unfolding lessThan_Suc_eq_insert_0
   1.192 -    by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
   1.193 +    by (simp add: ac_simps sum_atLeast1_atMost_eq image_Suc_lessThan)
   1.194    ultimately show ?thesis
   1.195 -    by (auto simp: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
   1.196 +    by (auto simp: sums_def simp del: sum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
   1.197  qed
   1.198  
   1.199  lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
   1.200 -  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
   1.201 +  unfolding sums_def by (simp add: sum.distrib tendsto_add)
   1.202  
   1.203  lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
   1.204    unfolding summable_def by (auto intro: sums_add)
   1.205 @@ -319,14 +319,14 @@
   1.206      and I :: "'i set"
   1.207  begin
   1.208  
   1.209 -lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
   1.210 +lemma sums_sum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
   1.211    by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
   1.212  
   1.213 -lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
   1.214 -  using sums_unique[OF sums_setsum, OF summable_sums] by simp
   1.215 +lemma suminf_sum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
   1.216 +  using sums_unique[OF sums_sum, OF summable_sums] by simp
   1.217  
   1.218 -lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
   1.219 -  using sums_summable[OF sums_setsum[OF summable_sums]] .
   1.220 +lemma summable_sum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
   1.221 +  using sums_summable[OF sums_sum[OF summable_sums]] .
   1.222  
   1.223  end
   1.224  
   1.225 @@ -341,7 +341,7 @@
   1.226    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
   1.227      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
   1.228    also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
   1.229 -    by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan setsum_atLeast1_atMost_eq)
   1.230 +    by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan sum_atLeast1_atMost_eq)
   1.231    also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
   1.232    proof
   1.233      assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
   1.234 @@ -372,7 +372,7 @@
   1.235  begin
   1.236  
   1.237  lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)"
   1.238 -  unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
   1.239 +  unfolding sums_def by (simp add: sum_subtractf tendsto_diff)
   1.240  
   1.241  lemma summable_diff: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n - g n)"
   1.242    unfolding summable_def by (auto intro: sums_diff)
   1.243 @@ -381,7 +381,7 @@
   1.244    by (intro sums_unique sums_diff summable_sums)
   1.245  
   1.246  lemma sums_minus: "f sums a \<Longrightarrow> (\<lambda>n. - f n) sums (- a)"
   1.247 -  unfolding sums_def by (simp add: setsum_negf tendsto_minus)
   1.248 +  unfolding sums_def by (simp add: sum_negf tendsto_minus)
   1.249  
   1.250  lemma summable_minus: "summable f \<Longrightarrow> summable (\<lambda>n. - f n)"
   1.251    unfolding summable_def by (auto intro: sums_minus)
   1.252 @@ -433,7 +433,7 @@
   1.253    shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
   1.254  proof -
   1.255    from LIMSEQ_D[OF summable_LIMSEQ[OF \<open>summable f\<close>] \<open>0 < r\<close>]
   1.256 -  obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n} - suminf f) < r"
   1.257 +  obtain N :: nat where "\<forall> n \<ge> N. norm (sum f {..<n} - suminf f) < r"
   1.258      by auto
   1.259    then show ?thesis
   1.260      by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
   1.261 @@ -467,7 +467,7 @@
   1.262    by (auto dest: summable_minus)  (* used two ways, hence must be outside the context above *)
   1.263  
   1.264  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   1.265 -  unfolding sums_def by (drule tendsto) (simp only: setsum)
   1.266 +  unfolding sums_def by (drule tendsto) (simp only: sum)
   1.267  
   1.268  lemma (in bounded_linear) summable: "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
   1.269    unfolding summable_def by (auto intro: sums)
   1.270 @@ -497,7 +497,7 @@
   1.271          (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
   1.272      then have "\<not> convergent (\<lambda>n. norm (\<Sum>k<n. c))"
   1.273        by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity)
   1.274 -        (simp_all add: setsum_constant_scaleR)
   1.275 +        (simp_all add: sum_constant_scaleR)
   1.276      then show ?thesis
   1.277        unfolding summable_iff_convergent using convergent_norm by blast
   1.278    qed
   1.279 @@ -546,7 +546,7 @@
   1.280  
   1.281  lemma sums_of_real_iff:
   1.282    "(\<lambda>n. of_real (f n) :: 'a::real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
   1.283 -  by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum)
   1.284 +  by (simp add: sums_def of_real_sum[symmetric] tendsto_of_real_iff del: of_real_sum)
   1.285  
   1.286  
   1.287  subsection \<open>Infinite summability on real normed fields\<close>
   1.288 @@ -628,7 +628,7 @@
   1.289    unfolding sums_def
   1.290  proof (subst LIMSEQ_Suc_iff [symmetric])
   1.291    have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
   1.292 -    by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
   1.293 +    by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] sum_Suc_diff)
   1.294    also have "\<dots> \<longlonglongrightarrow> c - f 0"
   1.295      by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
   1.296    finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0" .
   1.297 @@ -657,7 +657,7 @@
   1.298  
   1.299  text \<open>Cauchy-type criterion for convergence of series (c.f. Harrison).\<close>
   1.300  
   1.301 -lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (setsum f {m..<n}) < e)"
   1.302 +lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e)"
   1.303    for f :: "nat \<Rightarrow> 'a::banach"
   1.304    apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
   1.305    apply safe
   1.306 @@ -672,7 +672,7 @@
   1.307      apply (drule (1) mp)
   1.308      apply (drule_tac x="m" in spec)
   1.309      apply (drule (1) mp)
   1.310 -    apply (simp_all add: setsum_diff [symmetric])
   1.311 +    apply (simp_all add: sum_diff [symmetric])
   1.312    apply (drule spec)
   1.313    apply (drule (1) mp)
   1.314    apply (erule exE)
   1.315 @@ -680,7 +680,7 @@
   1.316    apply clarify
   1.317    apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.318     apply (subst norm_minus_commute)
   1.319 -   apply (simp_all add: setsum_diff [symmetric])
   1.320 +   apply (simp_all add: sum_diff [symmetric])
   1.321    done
   1.322  
   1.323  context
   1.324 @@ -698,13 +698,13 @@
   1.325    apply safe
   1.326    apply (drule_tac x="m" in spec)
   1.327    apply safe
   1.328 -  apply (rule order_le_less_trans [OF norm_setsum])
   1.329 +  apply (rule order_le_less_trans [OF norm_sum])
   1.330    apply (rule order_le_less_trans [OF abs_ge_self])
   1.331    apply simp
   1.332    done
   1.333  
   1.334  lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
   1.335 -  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_setsum)
   1.336 +  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_sum)
   1.337  
   1.338  text \<open>Comparison tests.\<close>
   1.339  
   1.340 @@ -721,9 +721,9 @@
   1.341    apply (rotate_tac 2)
   1.342    apply (drule_tac x = n in spec)
   1.343    apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
   1.344 -   apply (rule norm_setsum)
   1.345 -  apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   1.346 -   apply (auto intro: setsum_mono simp add: abs_less_iff)
   1.347 +   apply (rule norm_sum)
   1.348 +  apply (rule_tac y = "sum g {m..<n}" in order_le_less_trans)
   1.349 +   apply (auto intro: sum_mono simp add: abs_less_iff)
   1.350    done
   1.351  
   1.352  lemma summable_comparison_test_ev:
   1.353 @@ -841,58 +841,58 @@
   1.354    let ?g = "\<lambda>(i,j). a i * b j"
   1.355    let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
   1.356    have f_nonneg: "\<And>x. 0 \<le> ?f x" by auto
   1.357 -  then have norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
   1.358 +  then have norm_sum_f: "\<And>A. norm (sum ?f A) = sum ?f A"
   1.359      unfolding real_norm_def
   1.360 -    by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
   1.361 +    by (simp only: abs_of_nonneg sum_nonneg [rule_format])
   1.362  
   1.363    have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.364      by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b])
   1.365 -  then have 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.366 -    by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
   1.367 +  then have 1: "(\<lambda>n. sum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.368 +    by (simp only: sum_product sum.Sigma [rule_format] finite_lessThan)
   1.369  
   1.370    have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.371      using a b by (intro tendsto_mult summable_LIMSEQ)
   1.372 -  then have "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.373 -    by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
   1.374 -  then have "convergent (\<lambda>n. setsum ?f (?S1 n))"
   1.375 +  then have "(\<lambda>n. sum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.376 +    by (simp only: sum_product sum.Sigma [rule_format] finite_lessThan)
   1.377 +  then have "convergent (\<lambda>n. sum ?f (?S1 n))"
   1.378      by (rule convergentI)
   1.379 -  then have Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
   1.380 +  then have Cauchy: "Cauchy (\<lambda>n. sum ?f (?S1 n))"
   1.381      by (rule convergent_Cauchy)
   1.382 -  have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially"
   1.383 -  proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)
   1.384 +  have "Zfun (\<lambda>n. sum ?f (?S1 n - ?S2 n)) sequentially"
   1.385 +  proof (rule ZfunI, simp only: eventually_sequentially norm_sum_f)
   1.386      fix r :: real
   1.387      assume r: "0 < r"
   1.388      from CauchyD [OF Cauchy r] obtain N
   1.389 -      where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" ..
   1.390 -    then have "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> norm (setsum ?f (?S1 m - ?S1 n)) < r"
   1.391 -      by (simp only: setsum_diff finite_S1 S1_mono)
   1.392 -    then have N: "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> setsum ?f (?S1 m - ?S1 n) < r"
   1.393 -      by (simp only: norm_setsum_f)
   1.394 -    show "\<exists>N. \<forall>n\<ge>N. setsum ?f (?S1 n - ?S2 n) < r"
   1.395 +      where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (sum ?f (?S1 m) - sum ?f (?S1 n)) < r" ..
   1.396 +    then have "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> norm (sum ?f (?S1 m - ?S1 n)) < r"
   1.397 +      by (simp only: sum_diff finite_S1 S1_mono)
   1.398 +    then have N: "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> sum ?f (?S1 m - ?S1 n) < r"
   1.399 +      by (simp only: norm_sum_f)
   1.400 +    show "\<exists>N. \<forall>n\<ge>N. sum ?f (?S1 n - ?S2 n) < r"
   1.401      proof (intro exI allI impI)
   1.402        fix n
   1.403        assume "2 * N \<le> n"
   1.404        then have n: "N \<le> n div 2" by simp
   1.405 -      have "setsum ?f (?S1 n - ?S2 n) \<le> setsum ?f (?S1 n - ?S1 (n div 2))"
   1.406 -        by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg Diff_mono subset_refl S1_le_S2)
   1.407 +      have "sum ?f (?S1 n - ?S2 n) \<le> sum ?f (?S1 n - ?S1 (n div 2))"
   1.408 +        by (intro sum_mono2 finite_Diff finite_S1 f_nonneg Diff_mono subset_refl S1_le_S2)
   1.409        also have "\<dots> < r"
   1.410          using n div_le_dividend by (rule N)
   1.411 -      finally show "setsum ?f (?S1 n - ?S2 n) < r" .
   1.412 +      finally show "sum ?f (?S1 n - ?S2 n) < r" .
   1.413      qed
   1.414    qed
   1.415 -  then have "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
   1.416 +  then have "Zfun (\<lambda>n. sum ?g (?S1 n - ?S2 n)) sequentially"
   1.417      apply (rule Zfun_le [rule_format])
   1.418 -    apply (simp only: norm_setsum_f)
   1.419 -    apply (rule order_trans [OF norm_setsum setsum_mono])
   1.420 +    apply (simp only: norm_sum_f)
   1.421 +    apply (rule order_trans [OF norm_sum sum_mono])
   1.422      apply (auto simp add: norm_mult_ineq)
   1.423      done
   1.424 -  then have 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \<longlonglongrightarrow> 0"
   1.425 +  then have 2: "(\<lambda>n. sum ?g (?S1 n) - sum ?g (?S2 n)) \<longlonglongrightarrow> 0"
   1.426      unfolding tendsto_Zfun_iff diff_0_right
   1.427 -    by (simp only: setsum_diff finite_S1 S2_le_S1)
   1.428 -  with 1 have "(\<lambda>n. setsum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.429 +    by (simp only: sum_diff finite_S1 S2_le_S1)
   1.430 +  with 1 have "(\<lambda>n. sum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.431      by (rule Lim_transform2)
   1.432    then show ?thesis
   1.433 -    by (simp only: sums_def setsum_triangle_reindex)
   1.434 +    by (simp only: sums_def sum_triangle_reindex)
   1.435  qed
   1.436  
   1.437  lemma Cauchy_product:
   1.438 @@ -1021,7 +1021,7 @@
   1.439      with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e"
   1.440        by (intro N) simp_all
   1.441      also from True have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
   1.442 -      by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
   1.443 +      by (subst sum_diff [symmetric]) (simp_all add: sum_last_plus)
   1.444      finally show ?thesis .
   1.445    next
   1.446      case False
   1.447 @@ -1059,12 +1059,12 @@
   1.448      then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m"
   1.449        by blast
   1.450  
   1.451 -    have "(\<Sum>i<n. f (g i)) = setsum f (g ` {..<n})"
   1.452 -      by (simp add: setsum.reindex)
   1.453 +    have "(\<Sum>i<n. f (g i)) = sum f (g ` {..<n})"
   1.454 +      by (simp add: sum.reindex)
   1.455      also have "\<dots> \<le> (\<Sum>i<m. f i)"
   1.456 -      by (rule setsum_mono3) (auto simp add: pos n[rule_format])
   1.457 +      by (rule sum_mono3) (auto simp add: pos n[rule_format])
   1.458      also have "\<dots> \<le> suminf f"
   1.459 -      using \<open>summable f\<close> by (rule setsum_le_suminf) (simp add: pos)
   1.460 +      using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
   1.461      finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
   1.462        by simp
   1.463    qed
   1.464 @@ -1093,14 +1093,14 @@
   1.465      then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m"
   1.466        by blast
   1.467      have "(\<Sum>i<n. f i) = (\<Sum>i\<in>{..<n} \<inter> range g. f i)"
   1.468 -      using f by(auto intro: setsum.mono_neutral_cong_right)
   1.469 +      using f by(auto intro: sum.mono_neutral_cong_right)
   1.470      also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
   1.471 -      by (rule setsum.reindex_cong[where l=g])(auto)
   1.472 +      by (rule sum.reindex_cong[where l=g])(auto)
   1.473      also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
   1.474 -      by (rule setsum_mono3)(auto simp add: pos n)
   1.475 +      by (rule sum_mono3)(auto simp add: pos n)
   1.476      also have "\<dots> \<le> suminf (f \<circ> g)"
   1.477 -      using \<open>summable (f \<circ> g)\<close> by (rule setsum_le_suminf) (simp add: pos)
   1.478 -    finally show "setsum f {..<n} \<le> suminf (f \<circ> g)" .
   1.479 +      using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
   1.480 +    finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
   1.481    qed
   1.482    with le show "suminf (f \<circ> g) = suminf f"
   1.483      by (rule antisym)
   1.484 @@ -1117,9 +1117,9 @@
   1.485    proof
   1.486      fix n :: nat
   1.487      from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
   1.488 -      by (subst setsum.reindex) (auto intro: subseq_imp_inj_on)
   1.489 +      by (subst sum.reindex) (auto intro: subseq_imp_inj_on)
   1.490      also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
   1.491 -      by (intro setsum.mono_neutral_left ballI zero)
   1.492 +      by (intro sum.mono_neutral_left ballI zero)
   1.493          (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
   1.494      finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
   1.495    qed
   1.496 @@ -1158,9 +1158,9 @@
   1.497          by (rule zero)
   1.498      }
   1.499      with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
   1.500 -      by (intro setsum.mono_neutral_right) auto
   1.501 +      by (intro sum.mono_neutral_right) auto
   1.502      also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
   1.503 -      using subseq_imp_inj_on by (subst setsum.reindex) simp_all
   1.504 +      using subseq_imp_inj_on by (subst sum.reindex) simp_all
   1.505      finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
   1.506    qed
   1.507    also {