# HG changeset patch
# User haftmann
# Date 1379051990 -7200
# Node ID 0ae3db699a3e11e7683152f455a30b7a362bd738
# Parent  f2025867320a903ba1cad67c4de5d2fd51a06eff
tuned proofs

diff -r f2025867320a -r 0ae3db699a3e src/HOL/Limits.thy
--- 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)
diff -r f2025867320a -r 0ae3db699a3e src/HOL/Series.thy
--- 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"])
diff -r f2025867320a -r 0ae3db699a3e src/HOL/Transcendental.thy
--- 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]