--- a/src/HOL/Limits.thy Thu Sep 12 18:09:56 2013 -0700
+++ b/src/HOL/Limits.thy Fri Sep 13 07:59:50 2013 +0200
@@ -185,17 +185,19 @@
done
text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
-apply safe
-apply (simp add: Bseq_def, safe)
-apply (rule_tac x = "K + norm (X N)" in exI)
-apply auto
-apply (erule order_less_le_trans, simp)
-apply (rule_tac x = N in exI, safe)
-apply (drule_tac x = n in spec)
-apply (rule order_trans [OF norm_triangle_ineq], simp)
-apply (auto simp add: Bseq_iff2)
-done
+lemma Bseq_iff3:
+ "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ then obtain K
+ where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" by (auto simp add: Bseq_def)
+ from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
+ moreover from ** have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
+ by (auto intro: order_trans norm_triangle_ineq)
+ ultimately show ?Q by blast
+next
+ assume ?Q then show ?P by (auto simp add: Bseq_iff2)
+qed
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
apply (simp add: Bseq_def)
--- a/src/HOL/Series.thy Thu Sep 12 18:09:56 2013 -0700
+++ b/src/HOL/Series.thy Fri Sep 13 07:59:50 2013 +0200
@@ -446,7 +446,7 @@
lemma sumr_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>summable f;
- \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
+ \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
\<Longrightarrow> setsum f {0..<k} < suminf f"
unfolding One_nat_def
apply (subst suminf_split_initial_segment [where k="k"])
--- a/src/HOL/Transcendental.thy Thu Sep 12 18:09:56 2013 -0700
+++ b/src/HOL/Transcendental.thy Fri Sep 13 07:59:50 2013 +0200
@@ -2495,35 +2495,47 @@
"[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
-lemma realpow_num_eq_if:
- fixes m :: "'a::power"
- shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
- by (cases n) auto
-
-lemma cos_two_less_zero [simp]: "cos (2) < 0"
- apply (cut_tac x = 2 in cos_paired)
- apply (drule sums_minus)
- apply (rule neg_less_iff_less [THEN iffD1])
- apply (frule sums_unique, auto)
- apply (rule_tac y =
- "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
- in order_less_trans)
- apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
- apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
- apply (rule sumr_pos_lt_pair)
- apply (erule sums_summable, safe)
- unfolding One_nat_def
- apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
- del: fact_Suc)
- apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
- apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
- apply (simp only: real_of_nat_mult)
- apply (rule mult_strict_mono, force)
- apply (rule_tac [3] real_of_nat_ge_zero)
- prefer 2 apply force
- apply (rule real_of_nat_less_iff [THEN iffD2])
- apply (rule fact_less_mono_nat, auto)
- done
+lemmas realpow_num_eq_if = power_eq_if
+
+lemma cos_two_less_zero [simp]:
+ "cos 2 < 0"
+proof -
+ note fact_Suc [simp del]
+ from cos_paired
+ have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
+ by (rule sums_minus)
+ then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
+ by simp
+ then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ by (rule sums_summable)
+ have "0 < (\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
+ moreover have "(\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))
+ < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ proof -
+ { fix d
+ have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
+ < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
+ fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+ by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
+ then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
+ < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
+ by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+ then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
+ < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+ by (simp add: inverse_eq_divide less_divide_eq)
+ }
+ note *** = this
+ from ** show ?thesis by (rule sumr_pos_lt_pair)
+ (simp add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] ***)
+ qed
+ ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ by (rule order_less_trans)
+ moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ by (rule sums_unique)
+ ultimately have "0 < - cos 2" by simp
+ then show ?thesis by simp
+qed
lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]