# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395240947 0
# Node ID 76ff0a15d2027c72a39cdba09c8c8dea5cf497ac
# Parent  fcf90317383dfb4645b4b55c556eeaaf6e8b6e45# Parent  d503c51e869af901c4c6f3042e017d275333ca9c
Merge

diff -r fcf90317383d -r 76ff0a15d202 NEWS
--- a/NEWS	Wed Mar 19 14:54:45 2014 +0000
+++ b/NEWS	Wed Mar 19 14:55:47 2014 +0000
@@ -412,6 +412,53 @@
 shows up as additional case in fixpoint induction proofs.
 INCOMPATIBILITY
 
+* Removed and renamed theorems in Series:
+  summable_le         ~>  suminf_le
+  suminf_le           ~>  suminf_le_const
+  series_pos_le       ~>  setsum_le_suminf
+  series_pos_less     ~>  setsum_less_suminf
+  suminf_ge_zero      ~>  suminf_nonneg
+  suminf_gt_zero      ~>  suminf_pos
+  suminf_gt_zero_iff  ~>  suminf_pos_iff
+  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
+  suminf_0_le         ~>  suminf_nonneg [rotate]
+  pos_summable        ~>  summableI_nonneg_bounded
+  ratio_test          ~>  summable_ratio_test
+
+  removed series_zero, replaced by sums_finite
+
+  removed auxiliary lemmas:
+    sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
+    half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded,
+    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
+    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const
+INCOMPATIBILITY.
+
+* Replace (F)DERIV syntax by has_derivative:
+  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"
+
+  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"
+
+  - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax
+
+  - removed constant isDiff
+
+  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input
+    syntax.
+
+  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed
+
+  - Renamed FDERIV_... lemmas to has_derivative_...
+
+  - Other renamings:
+    differentiable_def        ~>  real_differentiable_def
+    differentiableE           ~>  real_differentiableE
+    fderiv_def                ~>  has_derivative_at
+    field_fderiv_def          ~>  field_has_derivative_at
+    isDiff_der                ~>  differentiable_def
+    deriv_fderiv              ~>  has_field_derivative_def
+INCOMPATIBILITY.
+
 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
 
 * Nitpick:
diff -r fcf90317383d -r 76ff0a15d202 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 14:54:45 2014 +0000
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 14:55:47 2014 +0000
@@ -2239,7 +2239,7 @@
   proof eventually_elim
     fix j x assume [simp]: "x \<in> space M"
     have "\<bar>\<Sum>i<j. f i x\<bar> \<le> (\<Sum>i<j. \<bar>f i x\<bar>)" by (rule setsum_abs)
-    also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
+    also have "\<dots> \<le> w x" using w[of x] setsum_le_suminf[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
     finally show "\<bar>\<Sum>i<j. f i x\<bar> \<le> ?w x" by simp
   qed
 
diff -r fcf90317383d -r 76ff0a15d202 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Mar 19 14:54:45 2014 +0000
+++ b/src/HOL/Series.thy	Wed Mar 19 14:55:47 2014 +0000
@@ -7,12 +7,14 @@
 Additional contributions by Jeremy Avigad
 *)
 
-header {* Finite Summation and Infinite Series *}
+header {* Infinite Series *}
 
 theory Series
 imports Limits
 begin
 
+subsection {* Definition of infinite summability *}
+
 definition
   sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
   (infixr "sums" 80)
@@ -28,6 +30,8 @@
 where
   "suminf f = (THE s. f sums s)"
 
+subsection {* Infinite summability on topological monoids *}
+
 lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
   by simp
 
@@ -40,6 +44,24 @@
 lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
   by (simp add: suminf_def sums_def lim_def)
 
+lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
+  unfolding sums_def by (simp add: tendsto_const)
+
+lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
+  by (rule sums_zero [THEN sums_summable])
+
+lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
+  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
+  apply safe
+  apply (erule_tac x=S in allE)
+  apply safe
+  apply (rule_tac x="N" in exI, safe)
+  apply (drule_tac x="n*k" in spec)
+  apply (erule mp)
+  apply (erule order_trans)
+  apply simp
+  done
+
 lemma sums_finite:
   assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   shows "f sums (\<Sum>n\<in>N. f n)"
@@ -65,36 +87,26 @@
        (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
 qed
 
+lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
+  by (rule sums_summable) (rule sums_finite)
+
 lemma sums_If_finite_set: "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0) sums (\<Sum>r\<in>A. f r)"
   using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
 
+lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)"
+  by (rule sums_summable) (rule sums_If_finite_set)
+
 lemma sums_If_finite: "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0) sums (\<Sum>r | P r. f r)"
   using sums_If_finite_set[of "{r. P r}"] by simp
 
+lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)"
+  by (rule sums_summable) (rule sums_If_finite)
+
 lemma sums_single: "(\<lambda>r. if r = i then f r else 0) sums f i"
   using sums_If_finite[of "\<lambda>r. r = i"] by simp
 
-lemma series_zero: (* REMOVE *)
-  "(\<And>m. n \<le> m \<Longrightarrow> f m = 0) \<Longrightarrow> f sums (\<Sum>i<n. f i)"
-  by (rule sums_finite) auto
-
-lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
-  unfolding sums_def by (simp add: tendsto_const)
-
-lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
-  by (rule sums_zero [THEN sums_summable])
-
-lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
-  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
-  apply safe
-  apply (erule_tac x=S in allE)
-  apply safe
-  apply (rule_tac x="N" in exI, safe)
-  apply (drule_tac x="n*k" in spec)
-  apply (erule mp)
-  apply (erule order_trans)
-  apply simp
-  done
+lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)"
+  by (rule sums_summable) (rule sums_single)
 
 context
   fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
@@ -123,26 +135,53 @@
 lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0"
   by (rule sums_zero [THEN sums_unique, symmetric])
 
+
+subsection {* Infinite summability on ordered, topological monoids *}
+
+lemma sums_le:
+  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+  shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
+  by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
+
 context
   fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
 begin
 
-lemma series_pos_le: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
-  apply (rule LIMSEQ_le_const[OF summable_LIMSEQ])
-  apply assumption
-  apply (intro exI[of _ n])
-  apply (auto intro!: setsum_mono2 simp: not_le[symmetric])
-  done
+lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
+  by (auto dest: sums_summable intro: sums_le)
+
+lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
+  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
+
+lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
+  using setsum_le_suminf[of 0] by simp
+
+lemma setsum_less_suminf2: "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"
+  using
+    setsum_le_suminf[of "Suc i"]
+    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
+    setsum_mono2[of "{..<i}" "{..<n}" f]
+  by (auto simp: less_imp_le ac_simps)
+
+lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
+  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
+
+lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
+  using setsum_less_suminf2[of 0 i] by simp
+
+lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
+  using suminf_pos2[of 0] by (simp add: less_imp_le)
+
+lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
+  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
 
 lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
 proof
   assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
-  then have "f sums 0"
-    by (simp add: sums_iff)
   then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
-    by (simp add: sums_def atLeast0LessThan)
-  have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
-  proof (rule LIMSEQ_le_const[OF f])
+    using summable_LIMSEQ[of f] by simp
+  then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
+  proof (rule LIMSEQ_le_const)
     fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
       using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
   qed
@@ -150,33 +189,34 @@
     by (auto intro!: antisym)
 qed (metis suminf_zero fun_eq_iff)
 
-lemma suminf_gt_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
-  using series_pos_le[of 0] suminf_eq_zero_iff by (simp add: less_le)
-
-lemma suminf_gt_zero: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
-  using suminf_gt_zero_iff by (simp add: less_imp_le)
-
-lemma suminf_ge_zero: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
-  by (drule_tac n="0" in series_pos_le) simp_all
-
-lemma suminf_le: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
-  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
-
-lemma summable_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
-  by (rule LIMSEQ_le) (auto intro: setsum_mono summable_LIMSEQ)
+lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
 
 end
 
-lemma series_pos_less:
-  fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
-  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {..<n} < suminf f"
-  apply simp
-  apply (rule_tac y="setsum f {..<Suc n}" in order_less_le_trans)
-  using add_less_cancel_left [of "setsum f {..<n}" 0 "f n"]
-  apply simp
-  apply (erule series_pos_le)
-  apply (simp add: order_less_imp_le)
-  done
+lemma summableI_nonneg_bounded:
+  fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}"
+  assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
+  shows "summable f"
+  unfolding summable_def sums_def[abs_def]
+proof (intro exI order_tendstoI)
+  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
+    using le by (auto simp: bdd_above_def)
+  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
+    then obtain n where "a < (\<Sum>i<n. f i)"
+      by (auto simp add: less_cSUP_iff)
+    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
+      by (rule less_le_trans) (auto intro!: setsum_mono2)
+    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
+      by (auto simp: eventually_sequentially) }
+  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
+    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
+      by (auto intro: cSUP_upper)
+    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
+      by (auto intro: le_less_trans simp: eventually_sequentially) }
+qed
+
+subsection {* Infinite summability on real normed vector spaces *}
 
 lemma sums_Suc_iff:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -289,6 +329,8 @@
 lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
 lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
 
+subsection {* Infinite summability on real normed algebras *}
+
 context
   fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra"
 begin
@@ -313,6 +355,8 @@
 
 end
 
+subsection {* Infinite summability on real normed fields *}
+
 context
   fixes c :: "'a::real_normed_field"
 begin
@@ -361,6 +405,8 @@
     by simp
 qed
 
+subsection {* Infinite summability on Banach spaces *}
+
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
 
 lemma summable_Cauchy:
@@ -452,12 +498,6 @@
 
 end
 
-lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
-  by (rule summable_comparison_test) auto
-
-lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
-  by (rule summable_norm_cancel) simp
-
 text{*Summability of geometric series for real algebras*}
 
 lemma complete_algebra_summable_geometric:
@@ -470,34 +510,6 @@
     by (simp add: summable_geometric)
 qed
 
-
-text{*A summable series of positive terms has limit that is at least as
-great as any partial sum.*}
-
-lemma pos_summable:
-  fixes f:: "nat \<Rightarrow> real"
-  assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {..<n} \<le> x"
-  shows "summable f"
-proof -
-  have "convergent (\<lambda>n. setsum f {..<n})"
-  proof (rule Bseq_mono_convergent)
-    show "Bseq (\<lambda>n. setsum f {..<n})"
-      by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
-  qed (auto intro: setsum_mono2 pos)
-  thus ?thesis
-    by (force simp add: summable_def sums_def convergent_def)
-qed
-
-lemma summable_rabs_comparison_test:
-  fixes f :: "nat \<Rightarrow> real"
-  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
-  by (rule summable_comparison_test) auto
-
-lemma summable_rabs:
-  fixes f :: "nat \<Rightarrow> real"
-  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
-by (fold real_norm_def, rule summable_norm)
-
 subsection {* Cauchy Product Formula *}
 
 text {*
@@ -507,14 +519,14 @@
 
 lemma setsum_triangle_reindex:
   fixes n :: nat
-  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i=0..k. f i (k - i))"
+  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
 proof -
   have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
-    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {0..k}). f i (k - i))"
+    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
   proof (rule setsum_reindex_cong)
-    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {0..k})"
+    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
       by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
-    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {0..k})"
+    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
       by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
     show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
       by clarify
@@ -526,7 +538,7 @@
   fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   assumes a: "summable (\<lambda>k. norm (a k))"
   assumes b: "summable (\<lambda>k. norm (b k))"
-  shows "(\<lambda>k. \<Sum>i=0..k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
+  shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
 proof -
   let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}"
   let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}"
@@ -598,8 +610,22 @@
   fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   assumes a: "summable (\<lambda>k. norm (a k))"
   assumes b: "summable (\<lambda>k. norm (b k))"
-  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
-using a b
-by (rule Cauchy_product_sums [THEN sums_unique])
+  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))"
+  using a b
+  by (rule Cauchy_product_sums [THEN sums_unique])
+
+subsection {* Series on @{typ real}s *}
+
+lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
+  by (rule summable_comparison_test) auto
+
+lemma summable_rabs_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n :: real\<bar>)"
+  by (rule summable_comparison_test) auto
+
+lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
+  by (rule summable_norm_cancel) simp
+
+lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
+  by (fold real_norm_def) (rule summable_norm)
 
 end
diff -r fcf90317383d -r 76ff0a15d202 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Mar 19 14:54:45 2014 +0000
+++ b/src/HOL/Transcendental.thy	Wed Mar 19 14:55:47 2014 +0000
@@ -552,7 +552,7 @@
   hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
     by (rule summable_norm)
   also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
-    by (rule summable_le)
+    by (rule suminf_le)
   also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
     by (rule suminf_mult2 [symmetric])
   finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
@@ -737,7 +737,7 @@
         using `x \<noteq> 0` by auto }
     note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
-      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] summable_le[OF _ 2 ign[OF `summable L`]]])
+      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
       using L_estimate by auto
 
@@ -1006,22 +1006,17 @@
   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
 proof -
   have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
-    by (rule sums_unique [OF series_zero], simp add: power_0_left)
+    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
   thus ?thesis unfolding One_nat_def by simp
 qed
 
 lemma exp_zero [simp]: "exp 0 = 1"
   unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
 
-lemma setsum_cl_ivl_Suc2:
-  "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
-  by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
-           del: setsum_cl_ivl_Suc)
-
 lemma exp_series_add:
   fixes x y :: "'a::{real_field}"
   defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
-  shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
+  shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
 proof (induct n)
   case 0
   show ?case
@@ -1035,32 +1030,32 @@
 
   have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
     by (simp only: times_S)
-  also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
+  also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
     by (simp only: Suc)
-  also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
-                + y * (\<Sum>i=0..n. S x i * S y (n-i))"
+  also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
+                + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
     by (rule distrib_right)
-  also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
-                + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
+  also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
+                + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
     by (simp only: setsum_right_distrib mult_ac)
-  also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
-                + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
+  also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
+                + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp add: times_S Suc_diff_le)
-  also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
-             (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
-    by (subst setsum_cl_ivl_Suc2, simp)
-  also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
-             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
-    by (subst setsum_cl_ivl_Suc, simp)
-  also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
-             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
-             (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
+  also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
+             (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
+    by (subst setsum_atMost_Suc_shift) simp
+  also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
+    by simp
+  also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
+             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+             (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
-              real_of_nat_add [symmetric], simp)
-  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
+                   real_of_nat_add [symmetric]) simp
+  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
     by (simp only: scaleR_right.setsum)
   finally show
-    "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
+    "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
     by (simp del: setsum_cl_ivl_Suc)
 qed
 
@@ -1128,7 +1123,7 @@
   have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
     by (auto simp add: numeral_2_eq_2)
   also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
-    apply (rule series_pos_le [OF summable_exp])
+    apply (rule setsum_le_suminf [OF summable_exp])
     using `0 < x`
     apply (auto  simp add:  zero_le_mult_iff)
     done
@@ -1412,7 +1407,7 @@
   proof -
     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
-      apply (rule summable_le)
+      apply (rule suminf_le)
       apply (rule allI, rule aux1)
       apply (rule summable_exp [THEN summable_ignore_initial_segment])
       by (rule sums_summable, rule aux2)
@@ -2388,7 +2383,7 @@
   show "0 < sin x"
     unfolding sums_unique [OF sums]
     using sums_summable [OF sums] pos
-    by (rule suminf_gt_zero)
+    by (rule suminf_pos)
 qed
 
 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
@@ -2427,7 +2422,7 @@
 apply (frule sums_unique)
 apply (drule sums_summable)
 apply simp
-apply (erule suminf_gt_zero)
+apply (erule suminf_pos)
 apply (simp add: add_ac)
 done
 
diff -r fcf90317383d -r 76ff0a15d202 src/HOL/ex/HarmonicSeries.thy
--- a/src/HOL/ex/HarmonicSeries.thy	Wed Mar 19 14:54:45 2014 +0000
+++ b/src/HOL/ex/HarmonicSeries.thy	Wed Mar 19 14:55:47 2014 +0000
@@ -268,8 +268,8 @@
 
 text {* The final theorem shows that as we take more and more elements
 (see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
-the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm
-series_pos_less} ) states that each sum is bounded above by the
+the sum converges, the lemma @{thm [source] setsum_less_suminf} ( @{thm
+setsum_less_suminf} ) states that each sum is bounded above by the
 series' limit. This contradicts our first statement and thus we prove
 that the harmonic series is divergent. *}
 
@@ -284,7 +284,7 @@
   proof -
     have "\<forall>n. 0 \<le> ?f n" by simp
     with sf have "?s \<ge> 0"
-      by - (rule suminf_ge_zero, simp_all)
+      by (rule suminf_nonneg)
     then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
 
     from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
@@ -298,11 +298,9 @@
 
   obtain j where jdef: "j = (2::nat)^n" by simp
   have "\<forall>m\<ge>j. 0 < ?f m" by simp
-  with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" unfolding atLeast0LessThan by (rule series_pos_less)
-  then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"
-    apply -
-    apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])
-    by simp
+  with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule setsum_less_suminf)
+  then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
+    unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
   with jdef have
     "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
   then have