src/HOL/Series.thy
changeset 57418 6ab1c7cb0b8d
parent 57275 0ddb5b755cdc
child 58729 e8ecc79aee43
     1.1 --- a/src/HOL/Series.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Series.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4      next
     1.5        assume [simp]: "N \<noteq> {}"
     1.6        show ?thesis
     1.7 -      proof (safe intro!: setsum_mono_zero_right f)
     1.8 +      proof (safe intro!: setsum.mono_neutral_right f)
     1.9          fix i assume "i \<in> N"
    1.10          then have "i \<le> Max N" by simp
    1.11          then show "i < n + Suc (Max N)" by simp
    1.12 @@ -225,7 +225,7 @@
    1.13    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) ----> s + f 0"
    1.14      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
    1.15    also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) ----> s + f 0"
    1.16 -    by (simp add: ac_simps setsum_reindex image_iff lessThan_Suc_eq_insert_0)
    1.17 +    by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0)
    1.18    also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
    1.19    proof
    1.20      assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) ----> s + f 0"
    1.21 @@ -241,7 +241,7 @@
    1.22  begin
    1.23  
    1.24  lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
    1.25 -  unfolding sums_def by (simp add: setsum_addf tendsto_add)
    1.26 +  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
    1.27  
    1.28  lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
    1.29    unfolding summable_def by (auto intro: sums_add)
    1.30 @@ -568,7 +568,7 @@
    1.31  lemma setsum_triangle_reindex:
    1.32    fixes n :: nat
    1.33    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.34 -  apply (simp add: setsum_Sigma)
    1.35 +  apply (simp add: setsum.Sigma)
    1.36    apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    1.37    apply auto
    1.38    done
    1.39 @@ -597,12 +597,12 @@
    1.40    have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    1.41      by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b])
    1.42    hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    1.43 -    by (simp only: setsum_product setsum_Sigma [rule_format] finite_lessThan)
    1.44 +    by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
    1.45  
    1.46    have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
    1.47      using a b by (intro tendsto_mult summable_LIMSEQ)
    1.48    hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
    1.49 -    by (simp only: setsum_product setsum_Sigma [rule_format] finite_lessThan)
    1.50 +    by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
    1.51    hence "convergent (\<lambda>n. setsum ?f (?S1 n))"
    1.52      by (rule convergentI)
    1.53    hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"