src/HOL/Transcendental.thy
 changeset 54575 0b9ca2c865cb parent 54573 07864001495d child 54576 e877eec2b698
```--- a/src/HOL/Transcendental.thy	Sun Nov 24 13:07:47 2013 +0000
+++ b/src/HOL/Transcendental.thy	Sun Nov 24 18:37:25 2013 +0000
@@ -641,11 +641,8 @@
\<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
apply (simp only: norm_mult mult_assoc)
apply (rule mult_left_mono [OF _ norm_ge_zero])
-      apply (simp (no_asm) add: mult_assoc [symmetric])
-      apply (rule lemma_termdiff3)
-      apply (rule h)
-      apply (rule r1 [THEN order_less_imp_le])
-      apply (rule xh [THEN order_less_imp_le])
+      apply (simp add: mult_assoc [symmetric])
+      apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
done
qed
qed
@@ -653,9 +650,9 @@
lemma termdiffs:
fixes K x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (\<lambda>n. c n * K ^ n)"
-    and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
-    and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
-    and 4: "norm x < norm K"
+      and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
+      and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
+      and 4: "norm x < norm K"
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
unfolding deriv_def
proof (rule LIM_zero_cancel)
@@ -676,20 +673,23 @@
by (rule powser_inside [OF 1 5])
have C: "summable (\<lambda>n. diffs c n * x ^ n)"
by (rule powser_inside [OF 2 4])
-    show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
-             - (\<Sum>n. diffs c n * x ^ n) =
-          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
-      apply (subst sums_unique [OF diffs_equiv [OF C]])
-      apply (subst suminf_diff [OF B A])
-      apply (subst suminf_divide [symmetric])
-      apply (rule summable_diff [OF B A])
+    let ?dp = "(\<Sum>n. of_nat n * c n * x ^ (n - Suc 0))"
+    have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
+          ((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - ?dp"
+      by (metis sums_unique [OF diffs_equiv [OF C]])
+    also have "... = (\<Sum>n. c n * (x + h) ^ n - c n * x ^ n) / h - ?dp"
+      by (metis suminf_diff [OF B A])
+    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h)  - ?dp"
+      by (metis suminf_divide [OF summable_diff [OF B A]] )
+    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
apply (subst suminf_diff)
-      apply (rule summable_divide)
-      apply (rule summable_diff [OF B A])
-      apply (rule sums_summable [OF diffs_equiv [OF C]])
-      apply (rule arg_cong [where f="suminf"], rule ext)
+      apply (auto intro: summable_divide summable_diff [OF B A] sums_summable [OF diffs_equiv [OF C]])
done
+    also have "... = (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
+    finally show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
+                   - (\<Sum>n. diffs c n * x ^ n) =
+                  (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))" .
next
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
by (rule termdiffs_aux [OF 3 4])
@@ -1159,13 +1159,25 @@

text {* Strict monotonicity of exponential. *}

-lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) \<Longrightarrow> (1 + x) \<le> exp(x)"
-  apply (drule order_le_imp_less_or_eq, auto)
-  apply (rule order_trans)
-  apply (rule_tac [2] n = 2 and f = "(\<lambda>n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
-  apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
-  done
+  assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
+using order_le_imp_less_or_eq [OF assms]
+proof
+  assume "0 < x"
+  have "1+x \<le> (\<Sum>n = 0..<2. inverse (real (fact n)) * x ^ n)"
+    by (auto simp add: numeral_2_eq_2)
+  also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
+    apply (rule series_pos_le [OF summable_exp])
+    using `0 < x`
+    apply (auto  simp add:  zero_le_mult_iff)
+    done
+  finally show "1+x \<le> exp x"
+next
+  assume "0 = x"
+  then show "1 + x \<le> exp x"
+    by auto
+qed

lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
proof -
@@ -1188,9 +1200,8 @@
qed

lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
-  apply (simp add: linorder_not_le [symmetric])
-  apply (auto simp add: order_le_less exp_less_mono)
-  done
+  unfolding linorder_not_le [symmetric]
+  by (auto simp add: order_le_less exp_less_mono)

lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
by (auto intro: exp_less_mono exp_less_cancel)
@@ -2090,55 +2101,32 @@
lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
apply (case_tac "a = 0", simp)
apply (case_tac "x = y", simp)
-  apply (rule order_less_imp_le)
-  apply (rule powr_less_mono2, auto)
+  apply (metis less_eq_real_def powr_less_mono2)
done

lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
unfolding powr_def exp_inj_iff by simp

lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
-  apply (rule mult_imp_le_div_pos)
-  apply (assumption)
-  apply (subst mult_commute)
-  apply (subst ln_powr [THEN sym])
-  apply auto
-  apply (rule ln_bound)
-  apply (erule ge_one_powr_ge_zero)
-  apply (erule order_less_imp_le)
-  done
+  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult_commute
+            order.strict_trans2 powr_gt_zero zero_less_one)

lemma ln_powr_bound2:
assumes "1 < x" and "0 < a"
shows "(ln x) powr a <= (a powr a) * x"
proof -
from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
-    apply (intro ln_powr_bound)
-    apply (erule order_less_imp_le)
-    apply (rule divide_pos_pos)
-    apply simp_all
-    done
+    by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
also have "... = a * (x powr (1 / a))"
by simp
finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
-    apply (intro powr_mono2)
-    apply (rule order_less_imp_le, rule assms)
-    apply (rule ln_gt_zero)
-    apply (rule assms)
-    apply assumption
-    done
+    by (metis assms less_imp_le ln_gt_zero powr_mono2)
also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
-    apply (rule powr_mult)
-    apply (rule assms)
-    apply (rule powr_gt_zero)
-    done
+    by (metis assms(2) powr_mult powr_gt_zero)
also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
by (rule powr_powr)
-  also have "... = x"
-    apply simp
-    apply (subgoal_tac "a ~= 0")
-    using assms apply auto
-    done
+  also have "... = x" using assms
+    by auto
finally show ?thesis .
qed

@@ -2488,12 +2476,7 @@
lemma real_mult_inverse_cancel:
"[|(0::real) < x; 0 < x1; x1 * y < x * u |]
==> inverse x * y < inverse x1 * u"
-  apply (rule_tac c=x in mult_less_imp_less_left)
-  apply (auto simp add: mult_assoc [symmetric])
-  apply (simp (no_asm) add: mult_ac)
-  apply (rule_tac c=x1 in mult_less_imp_less_right)
-  apply (auto simp add: mult_ac)
-  done
+  by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)

lemma real_mult_inverse_cancel2:
"[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
@@ -2574,7 +2557,7 @@
lemma pi_half_gt_zero [simp]: "0 < pi / 2"
apply (rule order_le_neq_trans)
apply (simp add: pi_half cos_is_zero [THEN theI'])
-  apply (rule notI, drule arg_cong [where f=cos], simp)
+  apply (metis cos_pi_half cos_zero zero_neq_one)
done

lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
@@ -2583,7 +2566,7 @@
lemma pi_half_less_two [simp]: "pi / 2 < 2"
apply (rule order_le_neq_trans)
apply (simp add: pi_half cos_is_zero [THEN theI'])
-  apply (rule notI, drule arg_cong [where f=cos], simp)
+  apply (metis cos_pi_half cos_two_neq_zero)
done

lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
@@ -2646,11 +2629,7 @@
by (induct n) (auto simp add: real_of_nat_Suc distrib_right)

lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
-proof -
-  have "cos (pi * real n) = cos (real n * pi)" by (simp only: mult_commute)
-  also have "... = -1 ^ n" by (rule cos_npi)
-  finally show ?thesis .
-qed
+  by (metis cos_npi mult_commute)

lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
@@ -2665,10 +2644,7 @@
by simp

lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
-  apply (rule sin_gt_zero, assumption)
-  apply (rule order_less_trans, assumption)
-  apply (rule pi_half_less_two)
-  done
+  by (metis sin_gt_zero order_less_trans pi_half_less_two)

lemma sin_less_zero:
assumes "- pi/2 < x" and "x < 0"
@@ -2692,8 +2668,7 @@

lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
apply (rule_tac x = x and y = 0 in linorder_cases)
-  apply (rule cos_minus [THEN subst])
-  apply (rule cos_gt_zero)
+  apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
apply (auto intro: cos_gt_zero)
done
```