tuned proofs
authorhaftmann
Fri Sep 13 07:59:50 2013 +0200 (2013-09-13)
changeset 536020ae3db699a3e
parent 53601 f2025867320a
child 53615 f557a4645f61
tuned proofs
src/HOL/Limits.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     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"
    1.33  apply (simp add: Bseq_def)
     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.25 -  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
    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)
    3.68 +      (simp add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] ***)
    3.69 +  qed
    3.70 +  ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
    3.71 +    by (rule order_less_trans)
    3.72 +  moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
    3.73 +    by (rule sums_unique)
    3.74 +  ultimately have "0 < - cos 2" by simp
    3.75 +  then show ?thesis by simp
    3.76 +qed
    3.77  
    3.78  lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
    3.79  lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]