author haftmann Fri, 23 Apr 2010 15:18:00 +0200 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 | comparison | revisions
```--- 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::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 *}
```