# HG changeset patch
# User paulson
# Date 1385318245 0
# Node ID 0b9ca2c865cb007e433072c972a4ac6f96a2e254
# Parent  d04e74341d433ee049628d275bbc67b083163947
cleaned up more messy proofs

diff -r d04e74341d43 -r 0b9ca2c865cb src/HOL/Transcendental.thy
--- 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 (simp add: algebra_simps)
+      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)))"
+      by (simp add: algebra_simps)
+    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 (simp add: exp_def)
-  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
+lemma exp_ge_add_one_self_aux: 
+  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" 
+    by (simp add: exp_def)
+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