# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1608740752 0
# Node ID 4fc3dc37f4069963db1bd7fd142190537f14d6f9
# Parent  e734cd65c92650ca6e24bfdf2947561a9e77d32a
default simprule for geometric series

diff -r e734cd65c926 -r 4fc3dc37f406 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Series.thy	Wed Dec 23 16:25:52 2020 +0000
@@ -614,7 +614,7 @@
 lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
   by (rule sums_unique[symmetric]) (rule geometric_sums)
 
-lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
+lemma summable_geometric_iff [simp]: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
 proof
   assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
   then have "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"
diff -r e734cd65c926 -r 4fc3dc37f406 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Transcendental.thy	Wed Dec 23 16:25:52 2020 +0000
@@ -1886,10 +1886,8 @@
     next
       fix x :: real
       assume "x \<in> {- 1<..<1}"
-      then have "norm (-x) < 1" by auto
-      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
-        unfolding One_nat_def
-        by (auto simp: power_mult_distrib[symmetric] summable_geometric[OF \<open>norm (-x) < 1\<close>])
+      then show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
+        by (simp add: abs_if flip: power_mult_distrib)
     qed
     then have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
       unfolding One_nat_def by auto