sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
authorhaftmann
Fri Apr 23 15:18:00 2010 +0200 (2010-04-23)
changeset 363071732232f9b27
parent 36306 18c088e1c4ef
child 36308 bbcfeddeafbb
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
src/HOL/SetInterval.thy
     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.5  
     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.14  
    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.34  
    1.35  subsection {* The formula for arithmetic sums *}
    1.36