# HG changeset patch
# User haftmann
# Date 1272028680 -7200
# Node ID 1732232f9b27c41b173f5fd321eac6fd96268419
# Parent  18c088e1c4efcd7f94b04c92d86a2f0236ac570b
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit

diff -r 18c088e1c4ef -r 1732232f9b27 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Apr 23 15:18:00 2010 +0200
+++ b/src/HOL/SetInterval.thy	Fri Apr 23 15:18:00 2010 +0200
@@ -1012,7 +1012,7 @@
 qed
 
 lemma setsum_le_included:
-  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
+  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   assumes "finite s" "finite t"
   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)"
   shows "setsum f s \<le> setsum g t"
@@ -1085,9 +1085,21 @@
 subsection {* The formula for geometric sums *}
 
 lemma geometric_sum:
-  "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
-  (x ^ n - 1) / (x - 1::'a::{field})"
-by (induct "n") (simp_all add: field_simps)
+  assumes "x \<noteq> 1"
+  shows "(\<Sum>i=0..<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"
+  proof (induct n)
+    case 0 then show ?case by simp
+  next
+    case (Suc n)
+    moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
+    ultimately show ?case by (simp add: field_eq_simps divide_inverse)
+  qed
+  ultimately show ?thesis by simp
+qed
+
 
 subsection {* The formula for arithmetic sums *}