# HG changeset patch # User nipkow # Date 1220289424 -7200 # Node ID ba4de3022862dd19d82c92ac99efea963899b70f # Parent f6b2d19951710840d2fc8747c4550b5b5dd78e7b moved lemma into SetInterval where it belongs diff -r f6b2d1995171 -r ba4de3022862 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Mon Sep 01 19:16:40 2008 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Mon Sep 01 19:17:04 2008 +0200 @@ -669,13 +669,9 @@ lemma exp_zero [simp]: "exp 0 = 1" unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) -lemma setsum_head2: - "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}" -by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) - lemma setsum_cl_ivl_Suc2: "(\i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\i=m..n. f (Suc i)))" -by (simp add: setsum_head2 setsum_shift_bounds_cl_Suc_ivl +by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl del: setsum_cl_ivl_Suc) lemma exp_series_add: