--- 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
--- 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"
--- 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:
--- 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)