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}"