src/HOL/Series.thy
changeset 63365 5340fb6633d0
parent 63145 703edebd1d92
child 63550 3a0f40a6fa42
     1.1 --- a/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
     1.2 +++ b/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
     1.3 @@ -283,9 +283,6 @@
     1.4  
     1.5  subsection \<open>Infinite summability on topological monoids\<close>
     1.6  
     1.7 -lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
     1.8 -  by auto
     1.9 -
    1.10  context
    1.11    fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
    1.12  begin
    1.13 @@ -296,7 +293,8 @@
    1.14    have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
    1.15      using assms by (auto intro!: tendsto_add simp: sums_def)
    1.16    moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
    1.17 -    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
    1.18 +    unfolding lessThan_Suc_eq_insert_0
    1.19 +      by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
    1.20    ultimately show ?thesis
    1.21      by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
    1.22  qed
    1.23 @@ -338,7 +336,7 @@
    1.24    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
    1.25      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
    1.26    also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
    1.27 -    by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0)
    1.28 +    by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan setsum_atLeast1_atMost_eq)
    1.29    also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
    1.30    proof
    1.31      assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"