# HG changeset patch
# User huffman
# Date 1315154985 25200
# Node ID 9caf6883f1f479fbce58af2a849bb8fa8b9de369
# Parent  79f10d9e63c1361c1614939b42aaaef0aa048dc2
remove redundant lemmas about LIMSEQ

diff -r 79f10d9e63c1 -r 9caf6883f1f4 NEWS
--- a/NEWS	Sun Sep 04 07:15:13 2011 -0700
+++ b/NEWS	Sun Sep 04 09:49:45 2011 -0700
@@ -296,6 +296,9 @@
   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
   LIMSEQ_imp_rabs ~> tendsto_rabs
+  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
+  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
+  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
   LIM_ident ~> tendsto_ident_at
   LIM_const ~> tendsto_const
   LIM_add ~> tendsto_add
diff -r 79f10d9e63c1 -r 9caf6883f1f4 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sun Sep 04 07:15:13 2011 -0700
+++ b/src/HOL/SEQ.thy	Sun Sep 04 09:49:45 2011 -0700
@@ -380,22 +380,6 @@
   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
 unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
 
-lemma LIMSEQ_add_const: (* FIXME: delete *)
-  fixes a :: "'a::real_normed_vector"
-  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
-by (intro tendsto_intros)
-
-(* FIXME: delete *)
-lemma LIMSEQ_add_minus:
-  fixes a b :: "'a::real_normed_vector"
-  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
-by (intro tendsto_intros)
-
-lemma LIMSEQ_diff_const: (* FIXME: delete *)
-  fixes a b :: "'a::real_normed_vector"
-  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
-by (intro tendsto_intros)
-
 lemma LIMSEQ_diff_approach_zero:
   fixes L :: "'a::real_normed_vector"
   shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
@@ -438,7 +422,8 @@
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus:
      "(%n. r + -inverse(real(Suc n))) ----> r"
-  using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
+  using tendsto_add [OF tendsto_const
+    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
diff -r 79f10d9e63c1 -r 9caf6883f1f4 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Sun Sep 04 07:15:13 2011 -0700
+++ b/src/HOL/Series.thy	Sun Sep 04 09:49:45 2011 -0700
@@ -122,7 +122,7 @@
   shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   apply (unfold sums_def)
   apply (simp add: sumr_offset)
-  apply (rule LIMSEQ_diff_const)
+  apply (rule tendsto_diff [OF _ tendsto_const])
   apply (rule LIMSEQ_ignore_initial_segment)
   apply assumption
 done
@@ -166,7 +166,7 @@
 proof -
   from sumSuc[unfolded sums_def]
   have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
-  from LIMSEQ_add_const[OF this, where b="f 0"]
+  from tendsto_add[OF this tendsto_const, where b="f 0"]
   have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
   thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
 qed
@@ -625,7 +625,7 @@
  apply (simp add:diff_Suc split:nat.splits)
  apply (blast intro: norm_ratiotest_lemma)
 apply (rule_tac x = "Suc N" in exI, clarify)
-apply(simp cong:setsum_ivl_cong)
+apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
 done
 
 lemma ratio_test:
diff -r 79f10d9e63c1 -r 9caf6883f1f4 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Sep 04 07:15:13 2011 -0700
+++ b/src/HOL/Transcendental.thy	Sun Sep 04 09:49:45 2011 -0700
@@ -1999,7 +1999,7 @@
 apply (drule tan_total_pos)
 apply (cut_tac [2] y="-y" in tan_total_pos, safe)
 apply (rule_tac [3] x = "-x" in exI)
-apply (auto intro!: exI)
+apply (auto del: exI intro!: exI)
 done
 
 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
@@ -2009,7 +2009,7 @@
 apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
 apply (rule_tac [4] Rolle)
 apply (rule_tac [2] Rolle)
-apply (auto intro!: DERIV_tan DERIV_isCont exI
+apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
             simp add: differentiable_def)
 txt{*Now, simulate TRYALL*}
 apply (rule_tac [!] DERIV_tan asm_rl)
@@ -2785,7 +2785,7 @@
         have "norm (?diff 1 n - 0) < r" by auto }
       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
     qed
-    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
+    from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)