author haftmann Fri Apr 23 15:18:00 2010 +0200 (2010-04-23) changeset 36307 1732232f9b27 parent 36306 18c088e1c4ef child 36308 bbcfeddeafbb
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
 src/HOL/SetInterval.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/SetInterval.thy	Fri Apr 23 15:18:00 2010 +0200
1.2 +++ b/src/HOL/SetInterval.thy	Fri Apr 23 15:18:00 2010 +0200
1.3 @@ -1012,7 +1012,7 @@
1.4  qed
1.6  lemma setsum_le_included:
1.7 -  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
1.8 +  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
1.9    assumes "finite s" "finite t"
1.10    and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
1.11    shows "setsum f s \<le> setsum g t"
1.12 @@ -1085,9 +1085,21 @@
1.13  subsection {* The formula for geometric sums *}
1.15  lemma geometric_sum:
1.16 -  "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
1.17 -  (x ^ n - 1) / (x - 1::'a::{field})"
1.18 -by (induct "n") (simp_all add: field_simps)
1.19 +  assumes "x \<noteq> 1"
1.20 +  shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
1.21 +proof -
1.22 +  from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
1.23 +  moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
1.24 +  proof (induct n)
1.25 +    case 0 then show ?case by simp
1.26 +  next
1.27 +    case (Suc n)
1.28 +    moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
1.29 +    ultimately show ?case by (simp add: field_eq_simps divide_inverse)
1.30 +  qed
1.31 +  ultimately show ?thesis by simp
1.32 +qed
1.33 +
1.35  subsection {* The formula for arithmetic sums *}