--- a/src/HOL/Set_Interval.thy Tue Mar 18 14:32:23 2014 +0100
+++ b/src/HOL/Set_Interval.thy Tue Mar 18 15:53:48 2014 +0100
@@ -1472,10 +1472,10 @@
lemma geometric_sum:
assumes "x \<noteq> 1"
- shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
+ shows "(\<Sum>i<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
proof -
from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
- moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
+ moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
proof (induct n)
case 0 then show ?case by simp
next
@@ -1490,8 +1490,7 @@
subsection {* The formula for arithmetic sums *}
lemma gauss_sum:
- "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) =
- of_nat n*((of_nat n)+1)"
+ "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"
proof (induct n)
case 0
show ?case by simp
@@ -1575,8 +1574,8 @@
lemma nat_diff_setsum_reindex:
fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "(\<Sum>i=0..<n. f (n - Suc i)) = (\<Sum>i=0..<n. f i)"
-apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{0..< n}"])
+ shows "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
+apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{..< n}"])
apply (auto simp: inj_on_def)
apply (rule_tac x="n - Suc x" in image_eqI, auto)
done