author berghofe Fri, 01 Jul 2005 14:06:57 +0200 changeset 16641 fce796ad9c2b parent 16640 03bdf544a552 child 16642 849ec3962b55
Simplified some proofs (thanks to strong_setsum_cong).
```--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Jul 01 14:05:41 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Jul 01 14:06:57 2005 +0200
@@ -360,11 +360,8 @@
lemma lemma_realpow_diff_sumr:
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =
y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
-apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc)
-apply (rule setsum_cong[OF refl])
-apply (subst lemma_realpow_diff)
-done
+by (auto simp add: setsum_mult lemma_realpow_diff mult_ac
+  simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)

lemma lemma_realpow_diff_sumr2:
"x ^ (Suc n) - y ^ (Suc n) =
@@ -468,9 +465,8 @@
lemma lemma_termdiff1:
"(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
(\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
-apply (rule setsum_cong[OF refl])
-done
+  cong: strong_setsum_cong)

lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"