src/HOL/Series.thy
 changeset 57129 7edb7550663e parent 57025 e7fd64f82876 child 57275 0ddb5b755cdc
```     1.1 --- a/src/HOL/Series.thy	Fri May 30 12:54:42 2014 +0200
1.2 +++ b/src/HOL/Series.thy	Fri May 30 14:55:10 2014 +0200
1.3 @@ -560,19 +560,10 @@
1.4  lemma setsum_triangle_reindex:
1.5    fixes n :: nat
1.6    shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
1.7 -proof -
1.8 -  have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
1.9 -    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
1.10 -  proof (rule setsum_reindex_cong)
1.11 -    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
1.12 -      by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
1.13 -    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
1.14 -      by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
1.15 -    show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
1.16 -      by clarify
1.17 -  qed
1.18 -  thus ?thesis by (simp add: setsum_Sigma)
1.19 -qed
1.20 +  apply (simp add: setsum_Sigma)
1.21 +  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
1.22 +  apply auto
1.23 +  done
1.24
1.25  lemma Cauchy_product_sums:
1.26    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
```