src/HOL/Hyperreal/Transcendental.thy
author berghofe
Fri, 13 Oct 2006 18:15:18 +0200
changeset 21020 9af9ceb16d58
parent 20860 1a8efd618190
child 21165 8fb49f668511
permissions -rw-r--r--
Adapted to changes in FixedPoint theory.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     1
(*  Title       : Transcendental.thy
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     3
    Copyright   : 1998,1999 University of Cambridge
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents: 12196
diff changeset
     4
                  1999,2001 University of Edinburgh
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     6
*)
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     7
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     8
header{*Power Series, Transcendental Functions etc.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    10
theory Transcendental
20690
136b206327a4 remove extra dependencies
huffman
parents: 20687
diff changeset
    11
imports NthRoot Fact Series EvenOdd Lim
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    12
begin
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    13
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    14
definition
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    15
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    16
  exp :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    17
  "exp x = (\<Sum>n. inverse(real (fact n)) * (x ^ n))"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    18
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    19
  sin :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    20
  "sin x = (\<Sum>n. (if even(n) then 0 else
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    21
             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    22
 
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    23
  diffs :: "(nat => real) => nat => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    24
  "diffs c = (%n. real (Suc n) * c(Suc n))"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    25
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    26
  cos :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    27
  "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    28
                            else 0) * x ^ n)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    29
  
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    30
  ln :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    31
  "ln x = (SOME u. exp u = x)"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    32
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    33
  pi :: "real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    34
  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    35
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    36
  tan :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    37
  "tan x = (sin x)/(cos x)"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    38
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    39
  arcsin :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    40
  "arcsin y = (SOME x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    41
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    42
  arcos :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    43
  "arcos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    44
     
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    45
  arctan :: "real => real"
dfe940911617 misc cleanup;
wenzelm
parents: 19279
diff changeset
    46
  "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    47
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    48
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    49
subsection{*Exponential Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    50
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    51
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    52
apply (cut_tac 'a = real in zero_less_one [THEN dense], safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    53
apply (cut_tac x = r in reals_Archimedean3, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    54
apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    55
apply (rule_tac N = n and c = r in ratio_test)
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    56
apply (safe, simp add: abs_mult mult_assoc [symmetric] del: fact_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    57
apply (rule mult_right_mono)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    58
apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    59
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    60
apply (subst real_of_nat_mult)
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
    61
apply (auto)
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    62
apply (simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    63
apply (rule order_less_imp_le)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    64
apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
    65
apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    66
apply (erule order_less_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    67
apply (auto simp add: mult_less_cancel_left mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    68
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    69
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    70
lemma summable_sin: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    71
     "summable (%n.  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    72
           (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    73
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    74
                x ^ n)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    75
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    76
apply (rule_tac [2] summable_exp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    77
apply (rule_tac x = 0 in exI)
16924
04246269386e removed the dependence on abs_mult
paulson
parents: 16819
diff changeset
    78
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    79
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    80
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    81
lemma summable_cos: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    82
      "summable (%n.  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    83
           (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    84
           (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    85
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    86
apply (rule_tac [2] summable_exp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    87
apply (rule_tac x = 0 in exI)
16924
04246269386e removed the dependence on abs_mult
paulson
parents: 16819
diff changeset
    88
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    89
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    90
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    91
lemma lemma_STAR_sin [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    92
     "(if even n then 0  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    93
       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
    94
by (induct "n", auto)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    95
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    96
lemma lemma_STAR_cos [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    97
     "0 < n -->  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    98
      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
    99
by (induct "n", auto)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   100
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   101
lemma lemma_STAR_cos1 [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   102
     "0 < n -->  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   103
      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   104
by (induct "n", auto)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   105
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   106
lemma lemma_STAR_cos2 [simp]:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   107
  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   108
                         else 0) = 0"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   109
apply (induct "n")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   110
apply (case_tac [2] "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   111
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   112
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   113
lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   114
apply (simp add: exp_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   115
apply (rule summable_exp [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   116
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   117
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   118
lemma sin_converges: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   119
      "(%n. (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   120
            else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   121
                 x ^ n) sums sin(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   122
apply (simp add: sin_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   123
apply (rule summable_sin [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   124
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   125
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   126
lemma cos_converges: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   127
      "(%n. (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   128
           (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   129
           else 0) * x ^ n) sums cos(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   130
apply (simp add: cos_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   131
apply (rule summable_cos [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   132
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   133
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   134
lemma lemma_realpow_diff [rule_format (no_asm)]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   135
     "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   136
apply (induct "n", auto)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   137
apply (subgoal_tac "p = Suc n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   138
apply (simp (no_asm_simp), auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   139
apply (drule sym)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   140
apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   141
       del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   142
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   143
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   144
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   145
subsection{*Properties of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   146
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   147
lemma lemma_realpow_diff_sumr:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   148
     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   149
      y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
19279
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18585
diff changeset
   150
by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac
16641
fce796ad9c2b Simplified some proofs (thanks to strong_setsum_cong).
berghofe
parents: 15561
diff changeset
   151
  simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   152
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   153
lemma lemma_realpow_diff_sumr2:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   154
     "x ^ (Suc n) - y ^ (Suc n) =  
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   155
      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   156
apply (induct "n", simp)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
   157
apply (auto simp del: setsum_op_ivl_Suc)
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
   158
apply (subst setsum_op_ivl_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   159
apply (drule sym)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
   160
apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   161
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   162
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   163
lemma lemma_realpow_rev_sumr:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   164
     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   165
      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   166
apply (case_tac "x = y")
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
   167
apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   168
apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   169
apply (rule_tac [2] minus_minus [THEN subst], simp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   170
apply (subst minus_mult_left)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
   171
apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   172
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   173
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   174
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   175
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   176
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   177
lemma powser_insidea:
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   178
  fixes x z :: real
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   179
  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   180
  assumes 2: "\<bar>z\<bar> < \<bar>x\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   181
  shows "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   182
proof -
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   183
  from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   184
  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   185
    by (rule summable_LIMSEQ_zero)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   186
  hence "convergent (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   187
    by (rule convergentI)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   188
  hence "Cauchy (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   189
    by (simp add: Cauchy_convergent_iff)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   190
  hence "Bseq (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   191
    by (rule Cauchy_Bseq)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   192
  then obtain K where 3: "0 < K" and 4: "\<forall>n. \<bar>f n * x ^ n\<bar> \<le> K"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   193
    by (simp add: Bseq_def, safe)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   194
  have "\<exists>N. \<forall>n\<ge>N. norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   195
  proof (intro exI allI impI)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   196
    fix n::nat assume "0 \<le> n"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   197
    have "norm (\<bar>f n\<bar> * z ^ n) * \<bar>x ^ n\<bar> = \<bar>f n * x ^ n\<bar> * \<bar>z ^ n\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   198
      by (simp add: abs_mult)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   199
    also have "\<dots> \<le> K * \<bar>z ^ n\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   200
      by (simp only: mult_right_mono 4 abs_ge_zero)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   201
    also have "\<dots> = K * \<bar>z ^ n\<bar> * (inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   202
      by (simp add: x_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   203
    also have "\<dots> = K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   204
      by (simp only: mult_assoc)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   205
    finally show "norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   206
      by (simp add: mult_le_cancel_right x_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   207
  qed
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   208
  moreover have "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   209
  proof -
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   210
    from 2 have "norm \<bar>z * inverse x\<bar> < 1"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   211
      by (simp add: abs_mult divide_inverse [symmetric])
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   212
    hence "summable (\<lambda>n. \<bar>z * inverse x\<bar> ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   213
      by (rule summable_geometric)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   214
    hence "summable (\<lambda>n. K * \<bar>z * inverse x\<bar> ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   215
      by (rule summable_mult)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   216
    thus "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   217
      by (simp add: abs_mult power_mult_distrib power_abs
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   218
                    power_inverse mult_assoc)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   219
  qed
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   220
  ultimately show "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   221
    by (rule summable_comparison_test)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   222
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   223
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   224
lemma powser_inside:
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   225
  fixes f :: "nat \<Rightarrow> real" shows
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   226
     "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   227
      ==> summable (%n. f(n) * (z ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   228
apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea, simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   229
apply (rule summable_rabs_cancel)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   230
apply (simp add: abs_mult power_abs [symmetric])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   231
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   232
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   233
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   234
subsection{*Differentiation of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   235
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   236
text{*Lemma about distributing negation over it*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   237
lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   238
by (simp add: diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   239
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   240
text{*Show that we can shift the terms down one*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   241
lemma lemma_diffs:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   242
     "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   243
      (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) +  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   244
      (real n * c(n) * x ^ (n - Suc 0))"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   245
apply (induct "n")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   246
apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   247
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   248
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   249
lemma lemma_diffs2:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   250
     "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) =  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   251
      (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   252
      (real n * c(n) * x ^ (n - Suc 0))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   253
by (auto simp add: lemma_diffs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   254
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   255
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   256
lemma diffs_equiv:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   257
     "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   258
      (%n. real n * c(n) * (x ^ (n - Suc 0))) sums  
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   259
         (\<Sum>n. (diffs c)(n) * (x ^ n))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   260
apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   261
apply (rule_tac [2] LIMSEQ_imp_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   262
apply (drule summable_sums) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   263
apply (auto simp add: sums_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   264
apply (drule_tac X="(\<lambda>n. \<Sum>n = 0..<n. diffs c n * x ^ n)" in LIMSEQ_diff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   265
apply (auto simp add: lemma_diffs2 [symmetric] diffs_def [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   266
apply (simp add: diffs_def summable_LIMSEQ_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   267
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   268
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   269
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   270
subsection{*Term-by-Term Differentiability of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   271
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   272
lemma lemma_termdiff1:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   273
  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   274
   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
16641
fce796ad9c2b Simplified some proofs (thanks to strong_setsum_cong).
berghofe
parents: 15561
diff changeset
   275
by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
fce796ad9c2b Simplified some proofs (thanks to strong_setsum_cong).
berghofe
parents: 15561
diff changeset
   276
  cong: strong_setsum_cong)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   277
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   278
lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   279
by (simp add: less_iff_Suc_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   280
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   281
lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   282
by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   283
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   284
lemma lemma_termdiff2:
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   285
  assumes h: "h \<noteq> 0" shows
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   286
  "((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0) =
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   287
   h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   288
        (z + h) ^ q * z ^ (n - 2 - q))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   289
apply (rule real_mult_left_cancel [OF h, THEN iffD1])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   290
apply (simp add: right_diff_distrib diff_divide_distrib h)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   291
apply (simp add: mult_assoc [symmetric])
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   292
apply (cases "n", simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   293
apply (simp add: lemma_realpow_diff_sumr2 h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   294
                 right_diff_distrib [symmetric] mult_assoc
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   295
            del: realpow_Suc setsum_op_ivl_Suc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   296
apply (subst lemma_realpow_rev_sumr)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   297
apply (subst sumr_diff_mult_const)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   298
apply simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   299
apply (simp only: lemma_termdiff1 setsum_right_distrib)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   300
apply (rule setsum_cong [OF refl])
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   301
apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   302
apply (clarify)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   303
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   304
            del: setsum_op_ivl_Suc realpow_Suc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   305
apply (subst mult_assoc [symmetric], subst power_add [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   306
apply (simp add: mult_ac)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   307
done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   308
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   309
lemma real_setsum_nat_ivl_bounded2:
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   310
  "\<lbrakk>\<And>p::nat. p < n \<Longrightarrow> f p \<le> K; 0 \<le> K\<rbrakk>
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   311
   \<Longrightarrow> setsum f {0..<n-k} \<le> real n * K"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   312
apply (rule order_trans [OF real_setsum_nat_ivl_bounded mult_right_mono])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   313
apply simp_all
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   314
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   315
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   316
lemma lemma_termdiff3:
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   317
  assumes 1: "h \<noteq> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   318
  assumes 2: "\<bar>z\<bar> \<le> K"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   319
  assumes 3: "\<bar>z + h\<bar> \<le> K"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   320
  shows "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar>
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   321
          \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   322
proof -
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   323
  have "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar> =
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   324
        \<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   325
          (z + h) ^ q * z ^ (n - 2 - q)\<bar> * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   326
    apply (subst lemma_termdiff2 [OF 1])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   327
    apply (subst abs_mult)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   328
    apply (rule mult_commute)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   329
    done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   330
  also have "\<dots> \<le> real n * (real (n - Suc 0) * K ^ (n - 2)) * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   331
  proof (rule mult_right_mono [OF _ abs_ge_zero])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   332
    from abs_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   333
    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> \<bar>(z + h) ^ i * z ^ j\<bar> \<le> K ^ n"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   334
      apply (erule subst)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   335
      apply (simp only: abs_mult power_abs power_add)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   336
      apply (intro mult_mono power_mono 2 3 abs_ge_zero zero_le_power K)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   337
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   338
    show "\<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   339
              (z + h) ^ q * z ^ (n - 2 - q)\<bar>
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   340
          \<le> real n * (real (n - Suc 0) * K ^ (n - 2))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   341
      apply (intro
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   342
         order_trans [OF setsum_abs]
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   343
         real_setsum_nat_ivl_bounded2
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   344
         mult_nonneg_nonneg
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   345
         real_of_nat_ge_zero
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   346
         zero_le_power K)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   347
      apply (rule le_Kn, simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   348
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   349
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   350
  also have "\<dots> = real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   351
    by (simp only: mult_assoc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   352
  finally show ?thesis .
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   353
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   354
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   355
lemma lemma_termdiff4:
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   356
  assumes k: "0 < (k::real)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   357
  assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   358
  shows "f -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   359
proof (simp add: LIM_def, safe)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   360
  fix r::real assume r: "0 < r"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   361
  have zero_le_K: "0 \<le> K"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   362
    apply (cut_tac k)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   363
    apply (cut_tac h="k/2" in le, simp, simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   364
    apply (subgoal_tac "0 \<le> K*k", simp add: zero_le_mult_iff) 
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   365
    apply (force intro: order_trans [of _ "\<bar>f (k / 2)\<bar> * 2"]) 
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   366
    done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   367
  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   368
  proof (cases)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   369
    assume "K = 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   370
    with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < k \<longrightarrow> \<bar>f x\<bar> < r)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   371
      by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   372
    thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)" ..
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   373
  next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   374
    assume K_neq_zero: "K \<noteq> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   375
    with zero_le_K have K: "0 < K" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   376
    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   377
    proof (rule exI, safe)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   378
      from k r K show "0 < min k (r * inverse K / 2)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   379
        by (simp add: mult_pos_pos positive_imp_inverse_positive)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   380
    next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   381
      fix x::real
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   382
      assume x1: "x \<noteq> 0" and x2: "\<bar>x\<bar> < min k (r * inverse K / 2)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   383
      from x2 have x3: "\<bar>x\<bar> < k" and x4: "\<bar>x\<bar> < r * inverse K / 2"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   384
        by simp_all
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   385
      from x1 x3 le have "\<bar>f x\<bar> \<le> K * \<bar>x\<bar>" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   386
      also from x4 K have "K * \<bar>x\<bar> < K * (r * inverse K / 2)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   387
        by (rule mult_strict_left_mono)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   388
      also have "\<dots> = r / 2"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   389
        using K_neq_zero by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   390
      also have "r / 2 < r"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   391
        using r by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   392
      finally show "\<bar>f x\<bar> < r" .
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   393
    qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   394
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   395
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   396
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   397
lemma lemma_termdiff5:
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   398
  assumes k: "0 < (k::real)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   399
  assumes f: "summable f"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   400
  assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   401
  shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   402
proof (rule lemma_termdiff4 [OF k])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   403
  fix h assume "h \<noteq> 0" and "\<bar>h\<bar> < k"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   404
  hence A: "\<forall>n. \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   405
    by (simp add: le)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   406
  hence "\<exists>N. \<forall>n\<ge>N. norm \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   407
    by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   408
  moreover from f have B: "summable (\<lambda>n. f n * \<bar>h\<bar>)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   409
    by (rule summable_mult2)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   410
  ultimately have C: "summable (\<lambda>n. \<bar>g h n\<bar>)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   411
    by (rule summable_comparison_test)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   412
  hence "\<bar>suminf (g h)\<bar> \<le> (\<Sum>n. \<bar>g h n\<bar>)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   413
    by (rule summable_rabs)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   414
  also from A C B have "(\<Sum>n. \<bar>g h n\<bar>) \<le> (\<Sum>n. f n * \<bar>h\<bar>)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   415
    by (rule summable_le)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   416
  also from f have "(\<Sum>n. f n * \<bar>h\<bar>) = suminf f * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   417
    by (rule suminf_mult2 [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   418
  finally show "\<bar>suminf (g h)\<bar> \<le> suminf f * \<bar>h\<bar>" .
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   419
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   420
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   421
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   422
text{* FIXME: Long proofs*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   423
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   424
lemma termdiffs_aux:
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   425
  assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   426
  assumes 2: "\<bar>x\<bar> < \<bar>K\<bar>"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   427
  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   428
             - real n * x ^ (n - Suc 0))) -- 0 --> 0"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   429
proof -
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   430
  from dense [OF 2]
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   431
  obtain r where r1: "\<bar>x\<bar> < r" and r2: "r < \<bar>K\<bar>" by fast
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   432
  from abs_ge_zero r1 have r: "0 < r"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   433
    by (rule order_le_less_trans)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   434
  hence r_neq_0: "r \<noteq> 0" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   435
  show ?thesis
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   436
  proof (rule lemma_termdiff5)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   437
    show "0 < r - \<bar>x\<bar>" using r1 by simp
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   438
  next
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   439
    from r r2 have "\<bar>r\<bar> < \<bar>K\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   440
      by (simp only: abs_of_nonneg order_less_imp_le)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   441
    with 1 have "summable (\<lambda>n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   442
      by (rule powser_insidea)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   443
    hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. \<bar>c n\<bar>)) n * r ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   444
      by (simp only: diffs_def abs_mult abs_real_of_nat_cancel)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   445
    hence "summable (\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   446
      by (rule diffs_equiv [THEN sums_summable])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   447
    also have "(\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0))
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   448
      = (\<lambda>n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   449
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   450
      apply (simp add: diffs_def)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   451
      apply (case_tac n, simp_all add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   452
      done
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   453
    finally have "summable 
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   454
      (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * r ^ (n - Suc 0))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   455
      by (rule diffs_equiv [THEN sums_summable])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   456
    also have
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   457
      "(\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   458
           r ^ (n - Suc 0)) =
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   459
       (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   460
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   461
      apply (case_tac "n", simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   462
      apply (case_tac "nat", simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   463
      apply (simp add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   464
      done
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   465
    finally show
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   466
      "summable (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))" .
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   467
  next
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   468
    fix h::real and n::nat
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   469
    assume h: "h \<noteq> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   470
    assume "\<bar>h\<bar> < r - \<bar>x\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   471
    hence "\<bar>x\<bar> + \<bar>h\<bar> < r" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   472
    with abs_triangle_ineq have xh: "\<bar>x + h\<bar> < r"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   473
      by (rule order_le_less_trans)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   474
    show "\<bar>c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0))\<bar>
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   475
          \<le> \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2) * \<bar>h\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   476
      apply (simp only: abs_mult mult_assoc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   477
      apply (rule mult_left_mono [OF _ abs_ge_zero])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   478
      apply (simp (no_asm) add: mult_assoc [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   479
      apply (rule lemma_termdiff3)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   480
      apply (rule h)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   481
      apply (rule r1 [THEN order_less_imp_le])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   482
      apply (rule xh [THEN order_less_imp_le])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   483
      done
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   484
  qed
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   485
qed
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   486
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   487
lemma termdiffs:
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   488
  assumes 1: "summable (\<lambda>n. c n * K ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   489
  assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   490
  assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   491
  assumes 4: "\<bar>x\<bar> < \<bar>K\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   492
  shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   493
proof (simp add: deriv_def, rule LIM_zero_cancel)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   494
  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   495
            - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   496
  proof (rule LIM_equal2)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   497
    show "0 < \<bar>K\<bar> - \<bar>x\<bar>" by (simp add: less_diff_eq 4)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   498
  next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   499
    fix h :: real
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   500
    assume "h \<noteq> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   501
    assume "norm (h - 0) < \<bar>K\<bar> - \<bar>x\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   502
    hence "\<bar>x\<bar> + \<bar>h\<bar> < \<bar>K\<bar>" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   503
    hence 5: "\<bar>x + h\<bar> < \<bar>K\<bar>"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   504
      by (rule abs_triangle_ineq [THEN order_le_less_trans])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   505
    have A: "summable (\<lambda>n. c n * x ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   506
      by (rule powser_inside [OF 1 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   507
    have B: "summable (\<lambda>n. c n * (x + h) ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   508
      by (rule powser_inside [OF 1 5])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   509
    have C: "summable (\<lambda>n. diffs c n * x ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   510
      by (rule powser_inside [OF 2 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   511
    show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   512
             - (\<Sum>n. diffs c n * x ^ n) = 
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   513
          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0)))"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   514
      apply (subst sums_unique [OF diffs_equiv [OF C]])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   515
      apply (subst suminf_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   516
      apply (subst suminf_divide [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   517
      apply (rule summable_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   518
      apply (subst suminf_diff)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   519
      apply (rule summable_divide)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   520
      apply (rule summable_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   521
      apply (rule sums_summable [OF diffs_equiv [OF C]])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   522
      apply (rule_tac f="suminf" in arg_cong)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   523
      apply (rule ext)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   524
      apply (simp add: ring_eq_simps)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   525
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   526
  next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   527
    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   528
               real n * x ^ (n - Suc 0))) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   529
        by (rule termdiffs_aux [OF 3 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   530
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   531
qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   532
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   533
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   534
subsection{*Formal Derivatives of Exp, Sin, and Cos Series*} 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   535
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   536
lemma exp_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   537
      "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   538
by (simp add: diffs_def mult_assoc [symmetric] del: mult_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   539
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   540
lemma sin_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   541
      "diffs(%n. if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   542
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n)))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   543
       = (%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   544
                 (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   545
              else 0)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   546
by (auto intro!: ext 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   547
         simp add: diffs_def divide_inverse simp del: mult_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   548
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   549
lemma sin_fdiffs2: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   550
       "diffs(%n. if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   551
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   552
       = (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   553
                 (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   554
              else 0)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   555
by (auto intro!: ext 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   556
         simp add: diffs_def divide_inverse simp del: mult_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   557
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   558
lemma cos_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   559
      "diffs(%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   560
                 (- 1) ^ (n div 2)/(real (fact n)) else 0)  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   561
       = (%n. - (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   562
           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   563
by (auto intro!: ext 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   564
         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   565
         simp del: mult_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   566
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   567
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   568
lemma cos_fdiffs2: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   569
      "diffs(%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   570
                 (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   571
       = - (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   572
           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   573
by (auto intro!: ext 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   574
         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   575
         simp del: mult_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   576
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   577
text{*Now at last we can get the derivatives of exp, sin and cos*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   578
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   579
lemma lemma_sin_minus:
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   580
     "- sin x = (\<Sum>n. - ((if even n then 0 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   581
                  else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   582
by (auto intro!: sums_unique sums_minus sin_converges)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   583
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   584
lemma lemma_exp_ext: "exp = (%x. \<Sum>n. inverse (real (fact n)) * x ^ n)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   585
by (auto intro!: ext simp add: exp_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   586
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   587
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   588
apply (simp add: exp_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   589
apply (subst lemma_exp_ext)
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   590
apply (subgoal_tac "DERIV (%u. \<Sum>n. inverse (real (fact n)) * u ^ n) x :> (\<Sum>n. diffs (%n. inverse (real (fact n))) n * x ^ n)")
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   591
apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   592
apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   593
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   594
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   595
lemma lemma_sin_ext:
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   596
     "sin = (%x. \<Sum>n. 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   597
                   (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   598
                       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   599
                   x ^ n)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   600
by (auto intro!: ext simp add: sin_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   601
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   602
lemma lemma_cos_ext:
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   603
     "cos = (%x. \<Sum>n. 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   604
                   (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) *
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   605
                   x ^ n)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   606
by (auto intro!: ext simp add: cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   607
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   608
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   609
apply (simp add: cos_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   610
apply (subst lemma_sin_ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   611
apply (auto simp add: sin_fdiffs2 [symmetric])
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   612
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   613
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   614
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   615
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   616
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   617
apply (subst lemma_cos_ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   618
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   619
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   620
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   621
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   622
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   623
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   624
subsection{*Properties of the Exponential Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   625
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   626
lemma exp_zero [simp]: "exp 0 = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   627
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   628
  have "(\<Sum>n = 0..<1. inverse (real (fact n)) * 0 ^ n) =
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   629
        (\<Sum>n. inverse (real (fact n)) * 0 ^ n)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   630
    by (rule series_zero [rule_format, THEN sums_unique],
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   631
        case_tac "m", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   632
  thus ?thesis by (simp add:  exp_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   633
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   634
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   635
lemma exp_ge_add_one_self_aux: "0 \<le> x ==> (1 + x) \<le> exp(x)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   636
apply (drule real_le_imp_less_or_eq, auto)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   637
apply (simp add: exp_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   638
apply (rule real_le_trans)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   639
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   640
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   641
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   642
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   643
lemma exp_gt_one [simp]: "0 < x ==> 1 < exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   644
apply (rule order_less_le_trans)
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   645
apply (rule_tac [2] exp_ge_add_one_self_aux, auto)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   646
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   647
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   648
lemma DERIV_exp_add_const: "DERIV (%x. exp (x + y)) x :> exp(x + y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   649
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   650
  have "DERIV (exp \<circ> (\<lambda>x. x + y)) x :> exp (x + y) * (1+0)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   651
    by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_Id DERIV_const) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   652
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   653
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   654
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   655
lemma DERIV_exp_minus [simp]: "DERIV (%x. exp (-x)) x :> - exp(-x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   656
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   657
  have "DERIV (exp \<circ> uminus) x :> exp (- x) * - 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   658
    by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_Id) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   659
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   660
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   661
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   662
lemma DERIV_exp_exp_zero [simp]: "DERIV (%x. exp (x + y) * exp (- x)) x :> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   663
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   664
  have "DERIV (\<lambda>x. exp (x + y) * exp (- x)) x
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   665
       :> exp (x + y) * exp (- x) + - exp (- x) * exp (x + y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   666
    by (fast intro: DERIV_exp_add_const DERIV_exp_minus DERIV_mult) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   667
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   668
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   669
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   670
lemma exp_add_mult_minus [simp]: "exp(x + y)*exp(-x) = exp(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   671
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   672
  have "\<forall>x. DERIV (%x. exp (x + y) * exp (- x)) x :> 0" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   673
  hence "exp (x + y) * exp (- x) = exp (0 + y) * exp (- 0)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   674
    by (rule DERIV_isconst_all) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   675
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   676
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   677
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   678
lemma exp_mult_minus [simp]: "exp x * exp(-x) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   679
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   680
  have "exp (x + 0) * exp (- x) = exp 0" by (rule exp_add_mult_minus) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   681
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   682
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   683
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   684
lemma exp_mult_minus2 [simp]: "exp(-x)*exp(x) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   685
by (simp add: mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   686
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   687
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   688
lemma exp_minus: "exp(-x) = inverse(exp(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   689
by (auto intro: inverse_unique [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   690
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   691
lemma exp_add: "exp(x + y) = exp(x) * exp(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   692
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   693
  have "exp x * exp y = exp x * (exp (x + y) * exp (- x))" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   694
  thus ?thesis by (simp (no_asm_simp) add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   695
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   696
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   697
text{*Proof: because every exponential can be seen as a square.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   698
lemma exp_ge_zero [simp]: "0 \<le> exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   699
apply (rule_tac t = x in real_sum_of_halves [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   700
apply (subst exp_add, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   701
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   702
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   703
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   704
apply (cut_tac x = x in exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   705
apply (auto simp del: exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   706
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   707
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   708
lemma exp_gt_zero [simp]: "0 < exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   709
by (simp add: order_less_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   710
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   711
lemma inv_exp_gt_zero [simp]: "0 < inverse(exp x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   712
by (auto intro: positive_imp_inverse_positive)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   713
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   714
lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   715
by auto
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   716
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   717
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   718
apply (induct "n")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   719
apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   720
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   721
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   722
lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   723
apply (simp add: diff_minus divide_inverse)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   724
apply (simp (no_asm) add: exp_add exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   725
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   726
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   727
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   728
lemma exp_less_mono:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   729
  assumes xy: "x < y" shows "exp x < exp y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   730
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   731
  have "1 < exp (y + - x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   732
    by (rule real_less_sum_gt_zero [THEN exp_gt_one])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   733
  hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   734
    by (auto simp add: exp_add exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   735
  thus ?thesis
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   736
    by (simp add: divide_inverse [symmetric] pos_less_divide_eq
15228
4d332d10fa3d revised simprules for division
paulson
parents: 15140
diff changeset
   737
             del: divide_self_if)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   738
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   739
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   740
lemma exp_less_cancel: "exp x < exp y ==> x < y"
15228
4d332d10fa3d revised simprules for division
paulson
parents: 15140
diff changeset
   741
apply (simp add: linorder_not_le [symmetric]) 
4d332d10fa3d revised simprules for division
paulson
parents: 15140
diff changeset
   742
apply (auto simp add: order_le_less exp_less_mono) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   743
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   744
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   745
lemma exp_less_cancel_iff [iff]: "(exp(x) < exp(y)) = (x < y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   746
by (auto intro: exp_less_mono exp_less_cancel)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   747
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   748
lemma exp_le_cancel_iff [iff]: "(exp(x) \<le> exp(y)) = (x \<le> y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   749
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   750
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   751
lemma exp_inj_iff [iff]: "(exp x = exp y) = (x = y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   752
by (simp add: order_eq_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   753
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   754
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x) = y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   755
apply (rule IVT)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   756
apply (auto intro: DERIV_exp [THEN DERIV_isCont] simp add: le_diff_eq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   757
apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)") 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   758
apply simp 
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   759
apply (rule exp_ge_add_one_self_aux, simp)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   760
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   761
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   762
lemma exp_total: "0 < y ==> \<exists>x. exp x = y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   763
apply (rule_tac x = 1 and y = y in linorder_cases)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   764
apply (drule order_less_imp_le [THEN lemma_exp_total])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   765
apply (rule_tac [2] x = 0 in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   766
apply (frule_tac [3] real_inverse_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   767
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   768
apply (rule_tac x = "-x" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   769
apply (simp add: exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   770
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   771
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   772
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   773
subsection{*Properties of the Logarithmic Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   774
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   775
lemma ln_exp[simp]: "ln(exp x) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   776
by (simp add: ln_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   777
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   778
lemma exp_ln_iff[simp]: "(exp(ln x) = x) = (0 < x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   779
apply (auto dest: exp_total)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   780
apply (erule subst, simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   781
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   782
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   783
lemma ln_mult: "[| 0 < x; 0 < y |] ==> ln(x * y) = ln(x) + ln(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   784
apply (rule exp_inj_iff [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   785
apply (frule real_mult_order)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   786
apply (auto simp add: exp_add exp_ln_iff [symmetric] simp del: exp_inj_iff exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   787
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   788
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   789
lemma ln_inj_iff[simp]: "[| 0 < x; 0 < y |] ==> (ln x = ln y) = (x = y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   790
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   791
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   792
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   793
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   794
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   795
lemma ln_one[simp]: "ln 1 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   796
by (rule exp_inj_iff [THEN iffD1], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   797
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   798
lemma ln_inverse: "0 < x ==> ln(inverse x) = - ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   799
apply (rule_tac a1 = "ln x" in add_left_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   800
apply (auto simp add: positive_imp_inverse_positive ln_mult [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   801
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   802
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   803
lemma ln_div: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   804
    "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   805
apply (simp add: divide_inverse)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   806
apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   807
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   808
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   809
lemma ln_less_cancel_iff[simp]: "[| 0 < x; 0 < y|] ==> (ln x < ln y) = (x < y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   810
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   811
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   812
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   813
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   814
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   815
lemma ln_le_cancel_iff[simp]: "[| 0 < x; 0 < y|] ==> (ln x \<le> ln y) = (x \<le> y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   816
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   817
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   818
lemma ln_realpow: "0 < x ==> ln(x ^ n) = real n * ln(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   819
by (auto dest!: exp_total simp add: exp_real_of_nat_mult [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   820
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   821
lemma ln_add_one_self_le_self [simp]: "0 \<le> x ==> ln(1 + x) \<le> x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   822
apply (rule ln_exp [THEN subst])
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   823
apply (rule ln_le_cancel_iff [THEN iffD2]) 
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   824
apply (auto simp add: exp_ge_add_one_self_aux)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   825
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   826
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   827
lemma ln_less_self [simp]: "0 < x ==> ln x < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   828
apply (rule order_less_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   829
apply (rule_tac [2] ln_add_one_self_le_self)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   830
apply (rule ln_less_cancel_iff [THEN iffD2], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   831
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   832
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   833
lemma ln_ge_zero [simp]:
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   834
  assumes x: "1 \<le> x" shows "0 \<le> ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   835
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   836
  have "0 < x" using x by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   837
  hence "exp 0 \<le> exp (ln x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   838
    by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   839
  thus ?thesis by (simp only: exp_le_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   840
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   841
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   842
lemma ln_ge_zero_imp_ge_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   843
  assumes ln: "0 \<le> ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   844
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   845
  shows "1 \<le> x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   846
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   847
  from ln have "ln 1 \<le> ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   848
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   849
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   850
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   851
lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   852
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   853
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   854
lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   855
by (insert ln_ge_zero_iff [of x], arith)
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   856
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   857
lemma ln_gt_zero:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   858
  assumes x: "1 < x" shows "0 < ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   859
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   860
  have "0 < x" using x by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   861
  hence "exp 0 < exp (ln x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   862
    by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   863
  thus ?thesis  by (simp only: exp_less_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   864
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   865
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   866
lemma ln_gt_zero_imp_gt_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   867
  assumes ln: "0 < ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   868
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   869
  shows "1 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   870
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   871
  from ln have "ln 1 < ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   872
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   873
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   874
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   875
lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   876
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   877
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   878
lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   879
by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   880
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   881
lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   882
by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   883
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   884
lemma exp_ln_eq: "exp u = x ==> ln x = u"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   885
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   886
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   887
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   888
subsection{*Basic Properties of the Trigonometric Functions*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   889
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   890
lemma sin_zero [simp]: "sin 0 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   891
by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   892
         simp add: sin_def sums_def simp del: power_0_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   893
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   894
lemma lemma_series_zero2:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   895
 "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   896
by (auto intro: series_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   897
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   898
lemma cos_zero [simp]: "cos 0 = 1"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   899
apply (simp add: cos_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   900
apply (rule sums_unique [symmetric])
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   901
apply (cut_tac n = 1 and f = "(%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   902
apply auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   903
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   904
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   905
lemma DERIV_sin_sin_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   906
     "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   907
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   908
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   909
lemma DERIV_sin_sin_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   910
     "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   911
apply (cut_tac x = x in DERIV_sin_sin_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   912
apply (auto simp add: mult_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   913
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   914
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   915
lemma DERIV_sin_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   916
     "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   917
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   918
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   919
lemma DERIV_sin_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   920
     "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   921
by (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   922
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   923
lemma DERIV_cos_cos_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   924
     "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   925
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   926
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   927
lemma DERIV_cos_cos_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   928
     "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   929
apply (cut_tac x = x in DERIV_cos_cos_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   930
apply (auto simp add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   931
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   932
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   933
lemma DERIV_cos_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   934
     "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   935
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   936
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   937
lemma DERIV_cos_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   938
     "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   939
by (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   940
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   941
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   942
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   943
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   944
lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   945
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   946
apply (rule DERIV_cos_realpow2a, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   947
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   948
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   949
(* most useful *)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   950
lemma DERIV_cos_cos_mult3 [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   951
     "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   952
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   953
apply (rule DERIV_cos_cos_mult2, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   954
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   955
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   956
lemma DERIV_sin_circle_all: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   957
     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   958
             (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   959
apply (simp only: diff_minus, safe)
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   960
apply (rule DERIV_add) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   961
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   962
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   963
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   964
lemma DERIV_sin_circle_all_zero [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   965
     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   966
by (cut_tac DERIV_sin_circle_all, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   967
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   968
lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   969
apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   970
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   971
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   972
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   973
lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   974
apply (subst real_add_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   975
apply (simp (no_asm) del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   976
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   977
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   978
lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   979
apply (cut_tac x = x in sin_cos_squared_add2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   980
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   981
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   982
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   983
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   984
apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   985
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   986
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   987
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   988
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   989
apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   990
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   991
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   992
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   993
lemma real_gt_one_ge_zero_add_less: "[| 1 < x; 0 \<le> y |] ==> 1 < x + (y::real)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   994
by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   995
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   996
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   997
apply (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   998
apply (drule_tac n = "Suc 0" in power_gt1)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   999
apply (auto simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1000
apply (drule_tac r1 = "cos x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1001
apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1002
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1003
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1004
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1005
apply (insert abs_sin_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1006
apply (simp add: abs_le_interval_iff del: abs_sin_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1007
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1008
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1009
lemma sin_le_one [simp]: "sin x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1010
apply (insert abs_sin_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1011
apply (simp add: abs_le_interval_iff del: abs_sin_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1012
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1013
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
  1014
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1015
apply (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1016
apply (drule_tac n = "Suc 0" in power_gt1)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1017
apply (auto simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1018
apply (drule_tac r1 = "sin x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1019
apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1020
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1021
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1022
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1023
apply (insert abs_cos_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1024
apply (simp add: abs_le_interval_iff del: abs_cos_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1025
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1026
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1027
lemma cos_le_one [simp]: "cos x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1028
apply (insert abs_cos_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1029
apply (simp add: abs_le_interval_iff del: abs_cos_le_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1030
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1031
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1032
lemma DERIV_fun_pow: "DERIV g x :> m ==>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1033
      DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1034
apply (rule lemma_DERIV_subst)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1035
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1036
apply (rule DERIV_pow, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1037
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1038
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1039
lemma DERIV_fun_exp:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1040
     "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1041
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1042
apply (rule_tac f = exp in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1043
apply (rule DERIV_exp, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1044
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1045
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1046
lemma DERIV_fun_sin:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1047
     "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1048
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1049
apply (rule_tac f = sin in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1050
apply (rule DERIV_sin, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1051
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1052
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1053
lemma DERIV_fun_cos:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1054
     "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1055
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1056
apply (rule_tac f = cos in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1057
apply (rule DERIV_cos, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1058
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1059
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1060
lemmas DERIV_intros = DERIV_Id DERIV_const DERIV_cos DERIV_cmult 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1061
                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1062
                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1063
                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1064
                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1065
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1066
(* lemma *)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1067
lemma lemma_DERIV_sin_cos_add:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1068
     "\<forall>x.  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1069
         DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1070
               (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1071
apply (safe, rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1072
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1073
  --{*replaces the old @{text DERIV_tac}*}
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1074
apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1075
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1076
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1077
lemma sin_cos_add [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1078
     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1079
      (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1080
apply (cut_tac y = 0 and x = x and y7 = y 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1081
       in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1082
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1083
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1084
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1085
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1086
apply (cut_tac x = x and y = y in sin_cos_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1087
apply (auto dest!: real_sum_squares_cancel_a 
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1088
            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1089
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1090
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1091
lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1092
apply (cut_tac x = x and y = y in sin_cos_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1093
apply (auto dest!: real_sum_squares_cancel_a
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1094
            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1095
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1096
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1097
lemma lemma_DERIV_sin_cos_minus:
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1098
    "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1099
apply (safe, rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1100
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1101
apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1102
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1103
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1104
lemma sin_cos_minus [simp]: 
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1105
    "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1106
apply (cut_tac y = 0 and x = x 
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1107
       in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1108
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1109
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1110
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1111
lemma sin_minus [simp]: "sin (-x) = -sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1112
apply (cut_tac x = x in sin_cos_minus)
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1113
apply (auto dest!: real_sum_squares_cancel_a 
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1114
       simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1115
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1116
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1117
lemma cos_minus [simp]: "cos (-x) = cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1118
apply (cut_tac x = x in sin_cos_minus)
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1119
apply (auto dest!: real_sum_squares_cancel_a 
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1120
                   simp add: numeral_2_eq_2 simp del: sin_cos_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1121
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1122
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1123
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1124
apply (simp add: diff_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1125
apply (simp (no_asm) add: sin_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1126
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1127
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1128
lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1129
by (simp add: sin_diff mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1130
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1131
lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1132
apply (simp add: diff_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1133
apply (simp (no_asm) add: cos_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1134
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1135
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1136
lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1137
by (simp add: cos_diff mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1138
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1139
lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1140
by (cut_tac x = x and y = x in sin_add, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1141
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1142
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1143
lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1144
apply (cut_tac x = x and y = x in cos_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1145
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1146
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1147
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1148
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1149
subsection{*The Constant Pi*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1150
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1151
text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1152
   hence define pi.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1153
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1154
lemma sin_paired:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1155
     "(%n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1156
      sums  sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1157
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1158
  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1159
            (if even k then 0
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1160
             else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1161
            x ^ k) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1162
	sums
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
  1163
	(\<Sum>n. (if even n then 0
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1164
		     else (- 1) ^ ((n - Suc 0) div 2) / real (fact n)) *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1165
	            x ^ n)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1166
    by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1167
  thus ?thesis by (simp add: mult_ac sin_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1168
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1169
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1170
lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1171
apply (subgoal_tac 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1172
       "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1173
              (- 1) ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
  1174
     sums (\<Sum>n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1175
 prefer 2
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1176
 apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1177
apply (rotate_tac 2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1178
apply (drule sin_paired [THEN sums_unique, THEN ssubst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1179
apply (auto simp del: fact_Suc realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1180
apply (frule sums_unique)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1181
apply (auto simp del: fact_Suc realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1182
apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1183
apply (auto simp del: fact_Suc realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1184
apply (erule sums_summable)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1185
apply (case_tac "m=0")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1186
apply (simp (no_asm_simp))
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
  1187
apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x") 
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
  1188
apply (simp only: mult_less_cancel_left, simp)  
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
  1189
apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1190
apply (subgoal_tac "x*x < 2*3", simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1191
apply (rule mult_strict_mono)
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1192
apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1193
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1194
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1195
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1196
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1197
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1198
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1199
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1200
apply (subst real_of_nat_mult)
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
  1201
apply (simp (no_asm) add: divide_inverse del: fact_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1202
apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1203
apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1204
apply (auto simp add: mult_assoc simp del: fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1205
apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1206
apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1207
apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1208
apply (erule ssubst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1209
apply (auto simp del: fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1210
apply (subgoal_tac "0 < x ^ (4 * m) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1211
 prefer 2 apply (simp only: zero_less_power) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1212
apply (simp (no_asm_simp) add: mult_less_cancel_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1213
apply (rule mult_strict_mono)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1214
apply (simp_all (no_asm_simp))
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1215
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1216
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1217
lemma sin_gt_zero1: "[|0 < x; x < 2 |] ==> 0 < sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1218
by (auto intro: sin_gt_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1219
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1220
lemma cos_double_less_one: "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1221
apply (cut_tac x = x in sin_gt_zero1)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1222
apply (auto simp add: cos_squared_eq cos_double)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1223
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1224
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1225
lemma cos_paired:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1226
     "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1227
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1228
  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1229
            (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1230
            x ^ k) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1231
        sums
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
  1232
	(\<Sum>n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) *
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1233
	      x ^ n)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1234
    by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1235
  thus ?thesis by (simp add: mult_ac cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1236
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset