src/HOL/Transcendental.thy
changeset 54573 07864001495d
parent 54489 03ff4d1e6784
child 54575 0b9ca2c865cb
     1.1 --- a/src/HOL/Transcendental.thy	Sun Nov 24 00:31:50 2013 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Nov 24 13:06:22 2013 +0000
     1.3 @@ -33,24 +33,31 @@
     1.4    shows
     1.5      "x ^ (Suc n) - y ^ (Suc n) =
     1.6        (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
     1.7 -  apply (induct n)
     1.8 -  apply simp
     1.9 -  apply (simp del: setsum_op_ivl_Suc)
    1.10 -  apply (subst setsum_op_ivl_Suc)
    1.11 -  apply (subst lemma_realpow_diff_sumr)
    1.12 -  apply (simp add: distrib_left del: setsum_op_ivl_Suc)
    1.13 -  apply (subst mult_left_commute [of "x - y"])
    1.14 -  apply (erule subst)
    1.15 -  apply (simp add: algebra_simps)
    1.16 -  done
    1.17 +proof (induct n)
    1.18 +  case 0 show ?case
    1.19 +    by simp
    1.20 +next
    1.21 +  case (Suc n)
    1.22 +  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    1.23 +    by simp
    1.24 +  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    1.25 +    by (simp add: algebra_simps)
    1.26 +  also have "... = y * ((x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.27 +    by (simp only: Suc)
    1.28 +  also have "... = (x - y) * (y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.29 +    by (simp only: mult_left_commute)
    1.30 +  also have "... = (x - y) * (\<Sum>p = 0..<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    1.31 +    by (simp add: setsum_op_ivl_Suc [where n = "Suc n"] distrib_left lemma_realpow_diff_sumr
    1.32 +             del: setsum_op_ivl_Suc)
    1.33 +  finally show ?case .
    1.34 +qed
    1.35  
    1.36  lemma lemma_realpow_rev_sumr:
    1.37 -  "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
    1.38 +   "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
    1.39      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
    1.40    apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
    1.41 -  apply (rule inj_onI, simp)
    1.42 -  apply auto
    1.43 -  apply (rule_tac x="n - x" in image_eqI, simp, simp)
    1.44 +  apply (rule inj_onI, auto)
    1.45 +  apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
    1.46    done
    1.47  
    1.48  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    1.49 @@ -388,12 +395,9 @@
    1.50        by auto
    1.51      ultimately show ?thesis by auto
    1.52    qed
    1.53 -  from this[THEN conjunct1]
    1.54 -    this[THEN conjunct2, THEN conjunct1]
    1.55 -    this[THEN conjunct2, THEN conjunct2, THEN conjunct1]
    1.56 -    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
    1.57 -    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2]
    1.58 -  show ?summable and ?pos and ?neg and ?f and ?g .
    1.59 +  then
    1.60 +  show ?summable and ?pos and ?neg and ?f and ?g 
    1.61 +    by safe
    1.62  qed
    1.63  
    1.64  subsection {* Term-by-Term Differentiability of Power Series *}
    1.65 @@ -420,9 +424,7 @@
    1.66        (\<lambda>n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
    1.67           (\<Sum>n. (diffs c)(n) * (x ^ n))"
    1.68    unfolding diffs_def
    1.69 -  apply (drule summable_sums)
    1.70 -  apply (rule sums_Suc_imp, simp_all)
    1.71 -  done
    1.72 +  by (simp add: summable_sums sums_Suc_imp)
    1.73  
    1.74  lemma lemma_termdiff1:
    1.75    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
    1.76 @@ -482,10 +484,7 @@
    1.77    have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
    1.78          norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
    1.79            (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
    1.80 -    apply (subst lemma_termdiff2 [OF 1])
    1.81 -    apply (subst norm_mult)
    1.82 -    apply (rule mult_commute)
    1.83 -    done
    1.84 +    by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult_commute norm_mult)
    1.85    also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
    1.86    proof (rule mult_right_mono [OF _ norm_ge_zero])
    1.87      from norm_ge_zero 2 have K: "0 \<le> K"
    1.88 @@ -3705,8 +3704,8 @@
    1.89    assumes "\<bar>x\<bar> < 1"
    1.90    shows "x\<^sup>2 < 1"
    1.91  proof -
    1.92 -  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
    1.93 -  have "\<bar>x\<^sup>2\<bar> < 1" using `\<bar>x\<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
    1.94 +  have "\<bar>x\<^sup>2\<bar> < 1"
    1.95 +    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
    1.96    thus ?thesis using zero_le_power2 by auto
    1.97  qed
    1.98  
    1.99 @@ -3867,7 +3866,7 @@
   1.100          moreover
   1.101          have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
   1.102            by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
   1.103 -            (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
   1.104 +             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
   1.105          ultimately
   1.106          show ?thesis using suminf_arctan_zero by auto
   1.107        qed
   1.108 @@ -4085,28 +4084,28 @@
   1.109  
   1.110  lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
   1.111  
   1.112 -lemma polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
   1.113 -  apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
   1.114 -  apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
   1.115 -  apply (simp add: cos_arccos_lemma1)
   1.116 -  apply (simp add: sin_arccos_lemma1)
   1.117 -  apply (simp add: power_divide)
   1.118 -  apply (simp add: real_sqrt_mult [symmetric])
   1.119 -  apply (simp add: right_diff_distrib)
   1.120 -  done
   1.121 -
   1.122 -lemma polar_ex2: "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
   1.123 -  using polar_ex1 [where x=x and y="-y"]
   1.124 -  apply simp
   1.125 -  apply clarify
   1.126 -  apply (metis cos_minus minus_minus minus_mult_right sin_minus)
   1.127 -  done
   1.128 -
   1.129  lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
   1.130 -  apply (rule_tac x=0 and y=y in linorder_cases)
   1.131 -  apply (erule polar_ex1)
   1.132 -  apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
   1.133 -  apply (erule polar_ex2)
   1.134 -  done
   1.135 +proof -
   1.136 +  have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
   1.137 +    apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
   1.138 +    apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
   1.139 +    apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
   1.140 +                     real_sqrt_mult [symmetric] right_diff_distrib)
   1.141 +    done
   1.142 +  show ?thesis
   1.143 +  proof (cases "0::real" y rule: linorder_cases)
   1.144 +    case less 
   1.145 +      then show ?thesis by (rule polar_ex1)
   1.146 +  next
   1.147 +    case equal
   1.148 +      then show ?thesis
   1.149 +        by (force simp add: intro!: cos_zero sin_zero)
   1.150 +  next
   1.151 +    case greater
   1.152 +      then show ?thesis 
   1.153 +     using polar_ex1 [where y="-y"]
   1.154 +    by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
   1.155 +  qed
   1.156 +qed
   1.157  
   1.158  end