# 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 "\X ----> a; a \ 0\ \ Bseq (\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 ==> (\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 "(\i. \n = Suc 0.. 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 "(\i. \n = 0.. 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 "\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 "\ N. \ n \ 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 = (\ i. ?c 1 i)" by (rule sums_unique)