author haftmann Fri Sep 13 07:59:50 2013 +0200 (2013-09-13) changeset 53602 0ae3db699a3e parent 53601 f2025867320a child 53615 f557a4645f61
tuned proofs
 src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Limits.thy	Thu Sep 12 18:09:56 2013 -0700
1.2 +++ b/src/HOL/Limits.thy	Fri Sep 13 07:59:50 2013 +0200
1.3 @@ -185,17 +185,19 @@
1.4  done
1.5
1.6  text{*alternative formulation for boundedness*}
1.7 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
1.8 -apply safe
1.9 -apply (simp add: Bseq_def, safe)
1.10 -apply (rule_tac x = "K + norm (X N)" in exI)
1.11 -apply auto
1.12 -apply (erule order_less_le_trans, simp)
1.13 -apply (rule_tac x = N in exI, safe)
1.14 -apply (drule_tac x = n in spec)
1.15 -apply (rule order_trans [OF norm_triangle_ineq], simp)
1.16 -apply (auto simp add: Bseq_iff2)
1.17 -done
1.18 +lemma Bseq_iff3:
1.19 +  "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)" (is "?P \<longleftrightarrow> ?Q")
1.20 +proof
1.21 +  assume ?P
1.22 +  then obtain K
1.23 +    where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" by (auto simp add: Bseq_def)
1.24 +  from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
1.25 +  moreover from ** have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
1.26 +    by (auto intro: order_trans norm_triangle_ineq)
1.27 +  ultimately show ?Q by blast
1.28 +next
1.29 +  assume ?Q then show ?P by (auto simp add: Bseq_iff2)
1.30 +qed
1.31
1.32  lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
```
```     2.1 --- a/src/HOL/Series.thy	Thu Sep 12 18:09:56 2013 -0700
2.2 +++ b/src/HOL/Series.thy	Fri Sep 13 07:59:50 2013 +0200
2.3 @@ -446,7 +446,7 @@
2.4  lemma sumr_pos_lt_pair:
2.5    fixes f :: "nat \<Rightarrow> real"
2.6    shows "\<lbrakk>summable f;
2.7 -        \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
2.8 +        \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
2.9        \<Longrightarrow> setsum f {0..<k} < suminf f"
2.10  unfolding One_nat_def
2.11  apply (subst suminf_split_initial_segment [where k="k"])
```
```     3.1 --- a/src/HOL/Transcendental.thy	Thu Sep 12 18:09:56 2013 -0700
3.2 +++ b/src/HOL/Transcendental.thy	Fri Sep 13 07:59:50 2013 +0200
3.3 @@ -2495,35 +2495,47 @@
3.4       "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
3.5    by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
3.6
3.7 -lemma realpow_num_eq_if:
3.8 -  fixes m :: "'a::power"
3.9 -  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
3.10 -  by (cases n) auto
3.11 -
3.12 -lemma cos_two_less_zero [simp]: "cos (2) < 0"
3.13 -  apply (cut_tac x = 2 in cos_paired)
3.14 -  apply (drule sums_minus)
3.15 -  apply (rule neg_less_iff_less [THEN iffD1])
3.16 -  apply (frule sums_unique, auto)
3.17 -  apply (rule_tac y =
3.18 -   "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
3.19 -         in order_less_trans)
3.20 -  apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
3.21 -  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
3.22 -  apply (rule sumr_pos_lt_pair)
3.23 -  apply (erule sums_summable, safe)
3.24 -  unfolding One_nat_def
3.26 -              del: fact_Suc)
3.27 -  apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
3.28 -  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
3.29 -  apply (simp only: real_of_nat_mult)
3.30 -  apply (rule mult_strict_mono, force)
3.31 -    apply (rule_tac [3] real_of_nat_ge_zero)
3.32 -   prefer 2 apply force
3.33 -  apply (rule real_of_nat_less_iff [THEN iffD2])
3.34 -  apply (rule fact_less_mono_nat, auto)
3.35 -  done
3.36 +lemmas realpow_num_eq_if = power_eq_if
3.37 +
3.38 +lemma cos_two_less_zero [simp]:
3.39 +  "cos 2 < 0"
3.40 +proof -
3.41 +  note fact_Suc [simp del]
3.42 +  from cos_paired
3.43 +  have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
3.44 +    by (rule sums_minus)
3.45 +  then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
3.46 +    by simp
3.47 +  then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
3.48 +    by (rule sums_summable)
3.49 +  have "0 < (\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
3.50 +    by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
3.51 +  moreover have "(\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
3.52 +    < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
3.53 +  proof -
3.54 +    { fix d
3.55 +      have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
3.56 +       < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
3.57 +           fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
3.58 +        by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
3.59 +      then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
3.60 +        < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
3.61 +        by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
3.62 +      then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
3.63 +        < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
3.64 +        by (simp add: inverse_eq_divide less_divide_eq)
3.65 +    }
3.66 +    note *** = this
3.67 +    from ** show ?thesis by (rule sumr_pos_lt_pair)