src/HOL/Hyperreal/Transcendental.thy
author paulson
Wed, 28 Jul 2004 16:25:40 +0200
changeset 15081 32402f5624d1
parent 15079 2ef899e4526d
child 15085 5693a977a767
permissions -rw-r--r--
abs notation
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    10
theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    11
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    12
(*????FOR RING_AND_FIELD*)
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    13
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    14
constdefs
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    15
    root :: "[nat,real] => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    16
    "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    17
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    18
    sqrt :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    19
    "sqrt x == root 2 x"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    20
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    21
    exp :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    22
    "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    23
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    24
    sin :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    25
    "sin x == suminf(%n. (if even(n) then 0 else
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    26
             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    27
 
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    28
    diffs :: "(nat => real) => nat => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    29
    "diffs c == (%n. real (Suc n) * c(Suc n))"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    30
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    31
    cos :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    32
    "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    33
                          else 0) * x ^ n)"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    34
  
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    35
    ln :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    36
    "ln x == (@u. exp u = x)"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    37
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    38
    pi :: "real"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    39
    "pi == 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    40
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    41
    tan :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    42
    "tan x == (sin x)/(cos x)"
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    43
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    44
    arcsin :: "real => real"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    45
    "arcsin y == (@x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    46
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    47
    arcos :: "real => real"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    48
    "arcos y == (@x. 0 \<le> x & x \<le> pi & cos x = y)"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    49
     
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 13958
diff changeset
    50
    arctan :: "real => real"
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    51
    "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    52
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    53
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    54
lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    55
apply (unfold root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    56
apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    57
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    58
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    59
lemma real_root_pow_pos: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    60
     "0 < x ==> (root(Suc n) x) ^ (Suc n) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    61
apply (unfold root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    62
apply (drule_tac n = n in realpow_pos_nth2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    63
apply (auto intro: someI2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    64
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    65
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    66
lemma real_root_pow_pos2: "0 \<le> x ==> (root(Suc n) x) ^ (Suc n) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    67
by (auto dest!: real_le_imp_less_or_eq dest: real_root_pow_pos)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    68
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    69
lemma real_root_pos: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    70
     "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    71
apply (unfold root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    72
apply (rule some_equality)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    73
apply (frule_tac [2] n = n in zero_less_power)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    74
apply (auto simp add: zero_less_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    75
apply (rule_tac x = u and y = x in linorder_cases)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    76
apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    77
apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    78
apply (auto simp add: order_less_irrefl)
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 real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    82
by (auto dest!: real_le_imp_less_or_eq real_root_pos)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    83
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    84
lemma real_root_pos_pos: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    85
     "0 < x ==> 0 \<le> root(Suc n) x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    86
apply (unfold root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    87
apply (drule_tac n = n in realpow_pos_nth2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    88
apply (safe, rule someI2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    89
apply (auto intro!: order_less_imp_le dest: zero_less_power simp add: zero_less_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    90
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    91
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    92
lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    93
by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    94
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    95
lemma real_root_one [simp]: "root (Suc n) 1 = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    96
apply (unfold root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    97
apply (rule some_equality, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    98
apply (rule ccontr)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    99
apply (rule_tac x = u and y = 1 in linorder_cases)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   100
apply (drule_tac n = n in realpow_Suc_less_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   101
apply (drule_tac [4] n = n in power_gt1_lemma)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   102
apply (auto simp add: order_less_irrefl)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   103
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   104
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   105
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   106
subsection{*Square Root*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   107
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   108
(*lcp: needed now because 2 is a binary numeral!*)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   109
lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   110
apply (simp (no_asm) del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 add: nat_numeral_0_eq_0 [symmetric])
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 real_sqrt_zero [simp]: "sqrt 0 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   114
by (unfold sqrt_def, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   115
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   116
lemma real_sqrt_one [simp]: "sqrt 1 = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   117
by (unfold sqrt_def, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   118
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   119
lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   120
apply (unfold sqrt_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   121
apply (rule iffI) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   122
 apply (cut_tac r = "root 2 x" in realpow_two_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   123
 apply (simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   124
apply (subst numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   125
apply (erule real_root_pow_pos2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   126
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   127
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   128
lemma [simp]: "(sqrt(u2\<twosuperior> + v2\<twosuperior>))\<twosuperior> = u2\<twosuperior> + v2\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   129
by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   130
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   131
lemma real_sqrt_pow2 [simp]: "0 \<le> x ==> (sqrt x)\<twosuperior> = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   132
by (simp add: real_sqrt_pow2_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   133
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   134
lemma real_sqrt_abs_abs [simp]: "sqrt\<bar>x\<bar> ^ 2 = \<bar>x\<bar>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   135
by (rule real_sqrt_pow2_iff [THEN iffD2], arith)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   136
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   137
lemma real_pow_sqrt_eq_sqrt_pow: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   138
      "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   139
apply (unfold sqrt_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   140
apply (subst numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   141
apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp 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
lemma real_pow_sqrt_eq_sqrt_abs_pow2:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   145
     "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(\<bar>x\<bar> ^ 2)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   146
by (simp add: real_pow_sqrt_eq_sqrt_pow [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   147
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   148
lemma real_sqrt_pow_abs: "0 \<le> x ==> (sqrt x)\<twosuperior> = \<bar>x\<bar>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   149
apply (rule real_sqrt_abs_abs [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   150
apply (rule_tac x1 = x in real_pow_sqrt_eq_sqrt_abs_pow2 [THEN ssubst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   151
apply (rule_tac [2] real_pow_sqrt_eq_sqrt_pow [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   152
apply (assumption, arith)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   153
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   154
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   155
lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   156
apply auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   157
apply (cut_tac x = x and y = 0 in linorder_less_linear)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   158
apply (simp add: zero_less_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   159
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   160
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   161
lemma real_mult_self_eq_zero_iff [simp]: "(r * r = 0) = (r = (0::real))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   162
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   163
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   164
lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   165
apply (unfold sqrt_def root_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   166
apply (subst numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   167
apply (drule realpow_pos_nth2 [where n=1], safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   168
apply (rule someI2, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   169
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   170
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   171
lemma real_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> sqrt(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   172
by (auto intro: real_sqrt_gt_zero simp add: order_le_less)
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   175
(*we need to prove something like this:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   176
lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   177
apply (case_tac n, simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   178
apply (unfold root_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   179
apply (rule someI2 [of _ r], safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   180
apply (auto simp del: realpow_Suc dest: power_inject_base)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   181
*)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   182
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   183
lemma sqrt_eqI: "[|r\<twosuperior> = a; 0 \<le> r|] ==> sqrt a = r"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   184
apply (unfold sqrt_def root_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   185
apply (rule someI2 [of _ r], auto) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   186
apply (auto simp add: numeral_2_eq_2 simp del: realpow_Suc 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   187
            dest: power_inject_base) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   188
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   189
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   190
lemma real_sqrt_mult_distrib: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   191
     "[| 0 \<le> x; 0 \<le> y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   192
apply (rule sqrt_eqI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   193
apply (simp add: power_mult_distrib)  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   194
apply (simp add: zero_le_mult_iff real_sqrt_ge_zero) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   195
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   196
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   197
lemma real_sqrt_mult_distrib2: "[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) =  sqrt(x) * sqrt(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   198
by (auto intro: real_sqrt_mult_distrib simp add: order_le_less)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   199
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   200
lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   201
by (auto intro!: real_sqrt_ge_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   202
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   203
lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   204
by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   205
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   206
lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   207
     "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   208
by (auto simp add: real_sqrt_pow2_iff zero_le_mult_iff simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   209
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   210
lemma real_sqrt_abs [simp]: "sqrt(x\<twosuperior>) = \<bar>x\<bar>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   211
apply (rule abs_realpow_two [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   212
apply (rule real_sqrt_abs_abs [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   213
apply (subst real_pow_sqrt_eq_sqrt_pow)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   214
apply (auto simp add: numeral_2_eq_2 abs_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   215
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   216
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   217
lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   218
apply (rule realpow_two [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   219
apply (subst numeral_2_eq_2 [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   220
apply (rule real_sqrt_abs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   221
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   222
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   223
lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   224
by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   225
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   226
lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   227
apply (frule real_sqrt_pow2_gt_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   228
apply (auto simp add: numeral_2_eq_2 order_less_irrefl)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   229
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   230
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   231
lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   232
by (cut_tac n1 = 2 and a1 = "sqrt x" in power_inverse [symmetric], auto)
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
lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   235
apply (drule real_le_imp_less_or_eq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   236
apply (auto dest: real_sqrt_not_eq_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   237
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   238
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   239
lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x = 0))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   240
by (auto simp add: real_sqrt_eq_zero_cancel)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   241
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   242
lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   243
apply (subgoal_tac "x \<le> 0 | 0 \<le> x", safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   244
apply (rule real_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   245
apply (auto simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   246
apply (rule_tac n = 1 in realpow_increasing)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   247
apply (auto simp add: numeral_2_eq_2 [symmetric] simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   248
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   249
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   250
lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(z\<twosuperior> + y\<twosuperior>)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   251
apply (simp (no_asm) add: real_add_commute del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   252
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   253
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   254
lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   255
apply (rule_tac n = 1 in realpow_increasing)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   256
apply (auto simp add: numeral_2_eq_2 [symmetric] real_sqrt_ge_zero simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   257
            del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   258
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   259
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   260
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   261
subsection{*Exponential Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   262
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   263
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   264
apply (cut_tac 'a = real in zero_less_one [THEN dense], safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   265
apply (cut_tac x = r in reals_Archimedean3, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   266
apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   267
apply (rule_tac N = n and c = r in ratio_test)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   268
apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   269
apply (rule mult_right_mono)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   270
apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   271
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   272
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   273
apply (auto simp add: abs_mult inverse_mult_distrib)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   274
apply (auto simp add: mult_assoc [symmetric] abs_eqI2 positive_imp_inverse_positive)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   275
apply (rule order_less_imp_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   276
apply (rule_tac z1 = "real (Suc na) " in real_mult_less_iff1 [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   277
apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   278
apply (erule order_less_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   279
apply (auto simp add: mult_less_cancel_left mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   280
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   281
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   282
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   283
lemma summable_sin: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   284
     "summable (%n.  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   285
           (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   286
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   287
                x ^ n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   288
apply (unfold real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   289
apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   290
apply (rule_tac [2] summable_exp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   291
apply (rule_tac x = 0 in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   292
apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   293
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   294
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   295
lemma summable_cos: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   296
      "summable (%n.  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   297
           (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   298
           (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   299
apply (unfold real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   300
apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   301
apply (rule_tac [2] summable_exp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   302
apply (rule_tac x = 0 in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   303
apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   304
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   305
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   306
lemma lemma_STAR_sin [simp]: "(if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   307
       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   308
apply (induct_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   309
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   310
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   311
lemma lemma_STAR_cos [simp]: "0 < n -->  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   312
      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   313
apply (induct_tac "n", auto)
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   316
lemma lemma_STAR_cos1 [simp]: "0 < n -->  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   317
      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   318
apply (induct_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   319
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   320
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   321
lemma lemma_STAR_cos2 [simp]: "sumr 1 n (%n. if even n  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   322
                    then (- 1) ^ (n div 2)/(real (fact n)) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   323
                          0 ^ n  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   324
                    else 0) = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   325
apply (induct_tac "n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   326
apply (case_tac [2] "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   327
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   328
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   329
lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   330
apply (unfold exp_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   331
apply (rule summable_exp [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   332
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   333
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   334
lemma sin_converges: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   335
      "(%n. (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   336
            else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   337
                 x ^ n) sums sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   338
apply (unfold sin_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   339
apply (rule summable_sin [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   340
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   341
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   342
lemma cos_converges: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   343
      "(%n. (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   344
           (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   345
           else 0) * x ^ n) sums cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   346
apply (unfold cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   347
apply (rule summable_cos [THEN summable_sums])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   348
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   349
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   350
lemma lemma_realpow_diff [rule_format (no_asm)]: "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   351
apply (induct_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   352
apply (subgoal_tac "p = Suc n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   353
apply (simp (no_asm_simp), auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   354
apply (drule sym)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   355
apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   356
       del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   357
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   358
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   359
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   360
subsection{*Properties of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   361
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   362
lemma lemma_realpow_diff_sumr:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   363
     "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   364
      y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   365
apply (auto simp add: sumr_mult simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   366
apply (rule sumr_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   367
apply (intro strip)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   368
apply (subst lemma_realpow_diff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   369
apply (auto simp add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   370
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   371
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   372
lemma lemma_realpow_diff_sumr2: "x ^ (Suc n) - y ^ (Suc n) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   373
      (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   374
apply (induct_tac "n", simp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   375
apply (auto simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   376
apply (subst sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   377
apply (drule sym)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   378
apply (auto simp add: lemma_realpow_diff_sumr right_distrib real_diff_def mult_ac simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   379
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   380
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   381
lemma lemma_realpow_rev_sumr: "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   382
      sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   383
apply (case_tac "x = y")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   384
apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   385
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
   386
apply (rule_tac [2] minus_minus [THEN subst], simp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   387
apply (subst minus_mult_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   388
apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   389
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   390
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   391
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
   392
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
   393
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   394
lemma powser_insidea:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   395
     "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   396
      ==> summable (%n. \<bar>f(n)\<bar> * (z ^ n))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   397
apply (drule summable_LIMSEQ_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   398
apply (drule convergentI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   399
apply (simp add: Cauchy_convergent_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   400
apply (drule Cauchy_Bseq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   401
apply (simp add: Bseq_def, safe)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   402
apply (rule_tac g = "%n. K * \<bar>z ^ n\<bar> * inverse (\<bar>x ^ n\<bar>)" in summable_comparison_test)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   403
apply (rule_tac x = 0 in exI, safe)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   404
apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   405
apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   406
apply (auto simp add: mult_assoc power_abs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   407
 prefer 2
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   408
 apply (drule_tac x = 0 in spec, force)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   409
apply (auto simp add: abs_mult power_abs mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   410
apply (rule_tac a2 = "z ^ n" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   411
       in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   412
apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   413
apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>))) " in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   414
apply (auto intro!: sums_mult simp add: mult_assoc)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   415
apply (subgoal_tac "\<bar>z ^ n\<bar> * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   416
apply (auto simp add: power_abs [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   417
apply (subgoal_tac "x \<noteq> 0")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   418
apply (subgoal_tac [3] "x \<noteq> 0")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   419
apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   420
apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   421
apply (rule_tac c="\<bar>x\<bar>" in mult_right_less_imp_less) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   422
apply (auto simp add: abs_mult [symmetric] mult_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   423
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   424
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   425
lemma powser_inside: "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   426
      ==> summable (%n. f(n) * (z ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   427
apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   428
apply (auto intro: summable_rabs_cancel simp add: power_abs [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   429
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   430
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   431
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   432
subsection{*Differentiation of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   433
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   434
text{*Lemma about distributing negation over it*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   435
lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   436
by (simp add: diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   437
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   438
text{*Show that we can shift the terms down one*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   439
lemma lemma_diffs:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   440
     "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   441
      sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   442
      (real n * c(n) * x ^ (n - Suc 0))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   443
apply (induct_tac "n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   444
apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   445
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   446
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   447
lemma lemma_diffs2: "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   448
      sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   449
      (real n * c(n) * x ^ (n - Suc 0))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   450
by (auto simp add: lemma_diffs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   451
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   452
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   453
lemma diffs_equiv: "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   454
      (%n. real n * c(n) * (x ^ (n - Suc 0))) sums  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   455
         (suminf(%n. (diffs c)(n) * (x ^ n)))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   456
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
   457
apply (rule_tac [2] LIMSEQ_imp_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   458
apply (drule summable_sums) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   459
apply (auto simp add: sums_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   460
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
   461
apply (auto simp add: lemma_diffs2 [symmetric] diffs_def [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   462
apply (simp add: diffs_def summable_LIMSEQ_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   463
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   464
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   465
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   466
subsection{*Term-by-Term Differentiability of Power Series*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   467
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   468
lemma lemma_termdiff1:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   469
     "sumr 0 m (%p. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   470
        sumr 0 m (%p. (z ^ p) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   471
        (((z + h) ^ (m - p)) - (z ^ (m - p))))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   472
apply (rule sumr_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   473
apply (auto simp add: right_distrib real_diff_def power_add [symmetric] mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   474
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   475
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   476
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
   477
by (simp add: less_iff_Suc_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   478
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   479
lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   480
by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   481
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   482
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   483
lemma lemma_termdiff2: " h \<noteq> 0 ==>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   484
        (((z + h) ^ n) - (z ^ n)) * inverse h -  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   485
            real n * (z ^ (n - Suc 0)) =  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   486
         h * sumr 0 (n - Suc 0) (%p. (z ^ p) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   487
               sumr 0 ((n - Suc 0) - p)  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   488
                 (%q. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   489
apply (rule real_mult_left_cancel [THEN iffD1], simp (no_asm_simp))
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   490
apply (simp add: right_diff_distrib mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   491
apply (simp add: mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   492
apply (case_tac "n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   493
apply (auto simp add: lemma_realpow_diff_sumr2 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   494
                      right_diff_distrib [symmetric] mult_assoc
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   495
            simp del: realpow_Suc sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   496
apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   497
apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   498
                sumdiff lemma_termdiff1 sumr_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   499
apply (auto intro!: sumr_subst simp add: real_diff_def real_add_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   500
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   501
apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   502
                 del: sumr_Suc realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   503
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   504
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   505
lemma lemma_termdiff3: "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   506
      ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   507
          \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   508
apply (subst lemma_termdiff2, assumption)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   509
apply (simp add: abs_mult mult_commute) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   510
apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   511
apply (rule sumr_rabs [THEN real_le_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   512
apply (simp add: mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   513
apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   514
apply (auto intro!: sumr_bound2 simp add: abs_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   515
apply (case_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   516
apply (drule less_add_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   517
(*CLAIM_SIMP " (a * b * c = a * (c * (b::real))" mult_ac]*)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   518
apply clarify 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   519
apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   520
                    K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   521
apply (simp (no_asm_simp) add: power_add del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   522
apply (auto intro!: mult_mono simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   523
apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   524
apply (rule_tac j = "real (Suc d) * (K ^ d) " in real_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   525
apply (subgoal_tac [2] "0 \<le> K")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   526
apply (drule_tac [2] n = d in zero_le_power)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   527
apply (auto simp del: sumr_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   528
apply (rule sumr_rabs [THEN real_le_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   529
apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   530
apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   531
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   532
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   533
lemma lemma_termdiff4: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   534
  "[| 0 < k;  
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   535
      (\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>) |]  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   536
   ==> f -- 0 --> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   537
apply (unfold LIM_def, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   538
apply (subgoal_tac "0 \<le> K")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   539
apply (drule_tac [2] x = "k/2" in spec)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   540
apply (frule_tac [2] real_less_half_sum)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   541
apply (drule_tac [2] real_gt_half_sum)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   542
apply (auto simp add: abs_eqI2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   543
apply (rule_tac [2] c = "k/2" in mult_right_le_imp_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   544
apply (auto intro: abs_ge_zero [THEN real_le_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   545
apply (drule real_le_imp_less_or_eq, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   546
apply (subgoal_tac "0 < (r * inverse K) * inverse 2")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   547
apply (rule_tac [2] real_mult_order)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   548
apply (drule_tac ?d1.0 = "r * inverse K * inverse 2" and ?d2.0 = k in real_lbound_gt_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   549
apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   550
apply (rule_tac [2] y="\<bar>f (k / 2)\<bar> * 2" in order_trans, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   551
apply (rule_tac x = e in exI, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   552
apply (rule_tac y = "K * \<bar>x\<bar>" in order_le_less_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   553
apply (rule_tac [2] y = "K * e" in order_less_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   554
apply (rule_tac [3] c = "inverse K" in mult_right_less_imp_less, force)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   555
apply (simp add: mult_less_cancel_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   556
apply (auto simp add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   557
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   558
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   559
lemma lemma_termdiff5: "[| 0 < k;  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   560
            summable f;  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   561
            \<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k -->  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   562
                    (\<forall>n. abs(g(h) (n::nat)) \<le> (f(n) * \<bar>h\<bar>)) |]  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   563
         ==> (%h. suminf(g h)) -- 0 --> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   564
apply (drule summable_sums)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   565
apply (subgoal_tac "\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>suminf (g h)\<bar> \<le> suminf f * \<bar>h\<bar>")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   566
apply (auto intro!: lemma_termdiff4 simp add: sums_summable [THEN suminf_mult, symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   567
apply (subgoal_tac "summable (%n. f n * \<bar>h\<bar>) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   568
 prefer 2
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   569
 apply (simp add: summable_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   570
 apply (rule_tac x = "suminf f * \<bar>h\<bar>" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   571
 apply (drule_tac c = "\<bar>h\<bar>" in sums_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   572
 apply (simp add: mult_ac) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   573
apply (subgoal_tac "summable (%n. abs (g (h::real) (n::nat))) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   574
 apply (rule_tac [2] g = "%n. f n * \<bar>h\<bar>" in summable_comparison_test)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   575
  apply (rule_tac [2] x = 0 in exI, auto)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   576
apply (rule_tac j = "suminf (%n. \<bar>g h n\<bar>)" in real_le_trans)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   577
apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   578
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   579
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   580
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   581
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   582
text{* FIXME: Long proofs*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   583
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   584
lemma termdiffs_aux:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   585
     "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   586
    ==> (\<lambda>h. suminf
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   587
             (\<lambda>n. c n *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   588
                  (((x + h) ^ n - x ^ n) * inverse h -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   589
                   real n * x ^ (n - Suc 0))))
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   590
       -- 0 --> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   591
apply (drule dense, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   592
apply (frule real_less_sum_gt_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   593
apply (drule_tac
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   594
         f = "%n. \<bar>c n\<bar> * real n * real (n - Suc 0) * (r ^ (n - 2))" 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   595
     and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   596
                             - (real n * (x ^ (n - Suc 0))))" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   597
       in lemma_termdiff5)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   598
apply (auto simp add: add_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   599
apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   600
apply (rule_tac [2] x = K in powser_insidea, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   601
apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   602
apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eqI1], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   603
apply (simp add: diffs_def mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   604
apply (subgoal_tac
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   605
        "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   606
              = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   607
apply auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   608
apply (drule diffs_equiv)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   609
apply (drule sums_summable)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   610
apply (simp_all add: diffs_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   611
apply (simp add: diffs_def mult_ac)
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   612
apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   613
apply auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   614
  prefer 2
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   615
  apply (rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   616
  apply (simp add: diffs_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   617
  apply (case_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   618
txt{*23*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   619
   apply (drule abs_ge_zero [THEN order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   620
   apply (simp add: mult_ac) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   621
  apply (drule abs_ge_zero [THEN order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   622
  apply (simp add: mult_ac) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   623
 apply (drule diffs_equiv)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   624
 apply (drule sums_summable)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   625
apply (subgoal_tac
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   626
          "summable
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   627
            (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   628
                 r ^ (n - Suc 0)) =
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   629
           summable
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   630
            (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   631
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   632
apply (rule_tac f = summable in arg_cong, rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   633
txt{*33*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   634
apply (case_tac "n", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   635
apply (case_tac "nat", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   636
apply (drule abs_ge_zero [THEN order_le_less_trans], auto) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   637
apply (drule abs_ge_zero [THEN order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   638
apply (simp add: mult_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   639
apply (rule mult_left_mono)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   640
apply (rule add_commute [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   641
apply (simp (no_asm) add: mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   642
apply (rule lemma_termdiff3)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   643
apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   644
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   645
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   646
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   647
lemma termdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   648
    "[| summable(%n. c(n) * (K ^ n));  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   649
        summable(%n. (diffs c)(n) * (K ^ n));  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   650
        summable(%n. (diffs(diffs c))(n) * (K ^ n));  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   651
        \<bar>x\<bar> < \<bar>K\<bar> |]  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   652
     ==> DERIV (%x. suminf (%n. c(n) * (x ^ n)))  x :>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   653
             suminf (%n. (diffs c)(n) * (x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   654
apply (unfold deriv_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   655
apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h) " in LIM_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   656
apply (simp add: LIM_def, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   657
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   658
apply (auto simp add: less_diff_eq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   659
apply (drule abs_triangle_ineq [THEN order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   660
apply (rule_tac y = 0 in order_le_less_trans, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   661
apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (suminf (%n. (c n) * (x ^ n))) & (%n. (c n) * ((x + xa) ^ n)) sums (suminf (%n. (c n) * ( (x + xa) ^ n))) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   662
apply (auto intro!: summable_sums)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   663
apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   664
apply (auto simp add: add_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   665
apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   666
apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   667
apply (rule sums_unique [symmetric])
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 15077
diff changeset
   668
apply (simp add: diff_def divide_inverse add_ac mult_ac)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   669
apply (rule LIM_zero_cancel)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   670
apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   671
 prefer 2 apply (blast intro: termdiffs_aux) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   672
apply (simp add: LIM_def, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   673
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   674
apply (auto simp add: less_diff_eq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   675
apply (drule abs_triangle_ineq [THEN order_le_less_trans])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   676
apply (rule_tac y = 0 in order_le_less_trans, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   677
apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   678
apply (rule_tac [2] powser_inside, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   679
apply (drule_tac c = c and x = x in diffs_equiv)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   680
apply (frule sums_unique, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   681
apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (suminf (%n. (c n) * (x ^ n))) & (%n. (c n) * ((x + xa) ^ n)) sums (suminf (%n. (c n) * ( (x + xa) ^ n))) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   682
apply safe
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   683
apply (auto intro!: summable_sums)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   684
apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   685
apply (auto simp add: add_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   686
apply (frule_tac x = " (%n. c n * (xa + x) ^ n) " and y = " (%n. c n * x ^ n) " in sums_diff, assumption)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   687
apply (simp add: suminf_diff [OF sums_summable sums_summable] 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   688
               right_diff_distrib [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   689
apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   690
apply (simp add: sums_summable [THEN suminf_mult2])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   691
apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   692
apply assumption
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   693
apply (subst minus_equation_iff, simp (no_asm))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   694
apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   695
apply (rule_tac f = suminf in arg_cong)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   696
apply (rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   697
apply (simp add: diff_def right_distrib add_ac mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   698
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   699
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   700
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   701
subsection{*Formal Derivatives of Exp, Sin, and Cos Series*} 
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_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   704
      "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   705
apply (unfold diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   706
apply (rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   707
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   708
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   709
apply (subst inverse_mult_distrib)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   710
apply (auto simp add: mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   711
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   712
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   713
lemma sin_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   714
      "diffs(%n. if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   715
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n)))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   716
       = (%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   717
                 (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   718
              else 0)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   719
apply (unfold diffs_def real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   720
apply (rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   721
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   722
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   723
apply (subst even_nat_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   724
apply (subst inverse_mult_distrib, auto)
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
lemma sin_fdiffs2: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   728
       "diffs(%n. if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   729
           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   730
       = (if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   731
                 (- 1) ^ (n div 2)/(real (fact n))  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   732
              else 0)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   733
apply (unfold diffs_def real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   734
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   735
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   736
apply (subst even_nat_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   737
apply (subst inverse_mult_distrib, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   738
done
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 cos_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   741
      "diffs(%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   742
                 (- 1) ^ (n div 2)/(real (fact n)) else 0)  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   743
       = (%n. - (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   744
           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   745
apply (unfold diffs_def real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   746
apply (rule ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   747
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   748
apply (subst real_of_nat_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   749
apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   750
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   751
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   752
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   753
lemma cos_fdiffs2: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   754
      "diffs(%n. if even n then  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   755
                 (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   756
       = - (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   757
           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   758
apply (unfold diffs_def real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   759
apply (subst fact_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   760
apply (subst real_of_nat_mult) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   761
apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   762
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   763
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   764
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
   765
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   766
lemma lemma_sin_minus:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   767
     "- sin x =
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   768
         suminf(%n. - ((if even n then 0 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   769
                  else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   770
by (auto intro!: sums_unique sums_minus sin_converges)
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
lemma lemma_exp_ext: "exp = (%x. suminf (%n. inverse (real (fact n)) * x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   773
by (auto intro!: ext simp add: exp_def)
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 DERIV_exp [simp]: "DERIV exp x :> exp(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   776
apply (unfold exp_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   777
apply (subst lemma_exp_ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   778
apply (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n) ")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   779
apply (rule_tac [2] K = "1 + \<bar>x\<bar> " in termdiffs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   780
apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
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 lemma_sin_ext:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   784
     "sin = (%x. suminf(%n. 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   785
                   (if even n then 0  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   786
                       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   787
                   x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   788
by (auto intro!: ext simp add: sin_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   789
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   790
lemma lemma_cos_ext:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   791
     "cos = (%x. suminf(%n. 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   792
                   (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) *
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   793
                   x ^ n))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   794
by (auto intro!: ext simp add: cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   795
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   796
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   797
apply (unfold cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   798
apply (subst lemma_sin_ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   799
apply (auto simp add: sin_fdiffs2 [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   800
apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   801
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   802
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   803
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   804
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   805
apply (subst lemma_cos_ext)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   806
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   807
apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   808
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   809
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   810
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   811
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   812
subsection{*Properties of the Exponential Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   813
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   814
lemma exp_zero [simp]: "exp 0 = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   815
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   816
  have "(\<Sum>n = 0..<1. inverse (real (fact n)) * 0 ^ n) =
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   817
        suminf (\<lambda>n. inverse (real (fact n)) * 0 ^ n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   818
    by (rule series_zero [rule_format, THEN sums_unique],
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   819
        case_tac "m", auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   820
  thus ?thesis by (simp add:  exp_def) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   821
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   822
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   823
lemma exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> exp(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   824
apply (drule real_le_imp_less_or_eq, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   825
apply (unfold exp_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   826
apply (rule real_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   827
apply (rule_tac [2] n = 2 and f = " (%n. inverse (real (fact n)) * x ^ n) " in series_pos_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   828
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
   829
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   830
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   831
lemma exp_gt_one [simp]: "0 < x ==> 1 < exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   832
apply (rule order_less_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   833
apply (rule_tac [2] exp_ge_add_one_self, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   834
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   835
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   836
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
   837
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   838
  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
   839
    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
   840
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   841
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   842
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   843
lemma DERIV_exp_minus [simp]: "DERIV (%x. exp (-x)) x :> - exp(-x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   844
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   845
  have "DERIV (exp \<circ> uminus) x :> exp (- x) * - 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   846
    by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_Id) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   847
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   848
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   849
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   850
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
   851
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   852
  have "DERIV (\<lambda>x. exp (x + y) * exp (- x)) x
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   853
       :> exp (x + y) * exp (- x) + - exp (- x) * exp (x + y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   854
    by (fast intro: DERIV_exp_add_const DERIV_exp_minus DERIV_mult) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   855
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   856
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   857
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   858
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
   859
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   860
  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
   861
  hence "exp (x + y) * exp (- x) = exp (0 + y) * exp (- 0)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   862
    by (rule DERIV_isconst_all) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   863
  thus ?thesis by simp
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 exp_mult_minus [simp]: "exp x * exp(-x) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   867
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   868
  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
   869
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   870
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   871
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   872
lemma exp_mult_minus2 [simp]: "exp(-x)*exp(x) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   873
by (simp add: mult_commute)
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   876
lemma exp_minus: "exp(-x) = inverse(exp(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   877
by (auto intro: inverse_unique [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   878
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   879
lemma exp_add: "exp(x + y) = exp(x) * exp(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   880
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   881
  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
   882
  thus ?thesis by (simp (no_asm_simp) add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   883
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   884
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   885
text{*Proof: because every exponential can be seen as a square.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   886
lemma exp_ge_zero [simp]: "0 \<le> exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   887
apply (rule_tac t = x in real_sum_of_halves [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   888
apply (subst exp_add, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   889
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   890
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   891
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   892
apply (cut_tac x = x in exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   893
apply (auto simp del: exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   894
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   895
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   896
lemma exp_gt_zero [simp]: "0 < exp x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   897
by (simp add: order_less_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   898
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   899
lemma inv_exp_gt_zero [simp]: "0 < inverse(exp x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   900
by (auto intro: positive_imp_inverse_positive)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   901
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
   902
lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   903
by (auto simp add: abs_eqI2)
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 exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   906
apply (induct_tac "n")
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   907
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
   908
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   909
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   910
lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   911
apply (unfold real_diff_def real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   912
apply (simp (no_asm) add: exp_add exp_minus)
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   916
lemma exp_less_mono:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   917
  assumes xy: "x < y" shows "exp x < exp y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   918
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   919
  have "1 < exp (y + - x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   920
    by (rule real_less_sum_gt_zero [THEN exp_gt_one])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   921
  hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   922
    by (auto simp add: exp_add exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   923
  thus ?thesis
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   924
    by (simp add: divide_inverse [symmetric] pos_less_divide_eq)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   925
qed
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 exp_less_cancel: "exp x < exp y ==> x < y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   928
apply (rule ccontr) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   929
apply (simp add: linorder_not_less order_le_less) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   930
apply (auto dest: exp_less_mono)
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 exp_less_cancel_iff [iff]: "(exp(x) < exp(y)) = (x < y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   934
by (auto intro: exp_less_mono exp_less_cancel)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   935
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   936
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
   937
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   938
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   939
lemma exp_inj_iff [iff]: "(exp x = exp y) = (x = y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   940
by (simp add: order_eq_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   941
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   942
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
   943
apply (rule IVT)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   944
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
   945
apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)") 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   946
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   947
apply (rule exp_ge_add_one_self, simp)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   948
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   949
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   950
lemma exp_total: "0 < y ==> \<exists>x. exp x = y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   951
apply (rule_tac x = 1 and y = y in linorder_cases)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   952
apply (drule order_less_imp_le [THEN lemma_exp_total])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   953
apply (rule_tac [2] x = 0 in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   954
apply (frule_tac [3] real_inverse_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   955
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
   956
apply (rule_tac x = "-x" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   957
apply (simp add: exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   958
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   959
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   960
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   961
subsection{*Properties of the Logarithmic Function*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   962
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   963
lemma ln_exp[simp]: "ln(exp x) = x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   964
by (simp add: ln_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   965
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   966
lemma exp_ln_iff[simp]: "(exp(ln x) = x) = (0 < x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   967
apply (auto dest: exp_total)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   968
apply (erule subst, simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   969
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   970
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   971
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
   972
apply (rule exp_inj_iff [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   973
apply (frule real_mult_order)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   974
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
   975
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   976
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   977
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
   978
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   979
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   980
apply simp 
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 ln_one[simp]: "ln 1 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   984
by (rule exp_inj_iff [THEN iffD1], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   985
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   986
lemma ln_inverse: "0 < x ==> ln(inverse x) = - ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   987
apply (rule_tac a1 = "ln x" in add_left_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   988
apply (auto simp add: positive_imp_inverse_positive ln_mult [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   989
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   990
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   991
lemma ln_div: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   992
    "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   993
apply (unfold real_divide_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   994
apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   995
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   996
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   997
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
   998
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   999
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1000
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1001
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1002
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1003
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
  1004
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1005
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1006
lemma ln_realpow: "0 < x ==> ln(x ^ n) = real n * ln(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1007
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
  1008
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1009
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
  1010
apply (rule ln_exp [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1011
apply (rule ln_le_cancel_iff [THEN iffD2], auto)
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
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1014
lemma ln_less_self [simp]: "0 < x ==> ln x < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1015
apply (rule order_less_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1016
apply (rule_tac [2] ln_add_one_self_le_self)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1017
apply (rule ln_less_cancel_iff [THEN iffD2], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1018
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1019
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1020
lemma ln_ge_zero:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1021
  assumes x: "1 \<le> x" shows "0 \<le> ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1022
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1023
  have "0 < x" using x by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1024
  hence "exp 0 \<le> exp (ln x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1025
    by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1026
  thus ?thesis by (simp only: exp_le_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1027
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1028
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1029
lemma ln_ge_zero_imp_ge_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1030
  assumes ln: "0 \<le> ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1031
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1032
  shows "1 \<le> x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1033
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1034
  from ln have "ln 1 \<le> ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1035
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1036
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1037
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1038
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
  1039
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1040
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1041
lemma ln_gt_zero:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1042
  assumes x: "1 < x" shows "0 < ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1043
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1044
  have "0 < x" using x by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1045
  hence "exp 0 < exp (ln x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1046
    by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1047
  thus ?thesis  by (simp only: exp_less_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1048
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1049
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1050
lemma ln_gt_zero_imp_gt_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1051
  assumes ln: "0 < ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1052
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1053
  shows "1 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1054
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1055
  from ln have "ln 1 < ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1056
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1057
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1058
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1059
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
  1060
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1061
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1062
lemma ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ln x \<noteq> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1063
apply safe
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1064
apply (drule exp_inj_iff [THEN iffD2])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1065
apply (drule exp_ln_iff [THEN iffD2], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1066
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1067
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1068
lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1069
apply (rule exp_less_cancel_iff [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1070
apply (auto simp add: exp_ln_iff [symmetric] simp del: exp_ln_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1071
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1072
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1073
lemma exp_ln_eq: "exp u = x ==> ln x = u"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1074
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1075
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
subsection{*Basic Properties of the Trigonometric Functions*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1078
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1079
lemma sin_zero [simp]: "sin 0 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1080
by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1081
         simp add: sin_def sums_def simp del: power_0_left)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1082
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1083
lemma lemma_series_zero2: "(\<forall>m. n \<le> m --> f m = 0) --> f sums sumr 0 n f"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1084
by (auto intro: series_zero)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1085
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1086
lemma cos_zero [simp]: "cos 0 = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1087
apply (unfold cos_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1088
apply (rule sums_unique [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1089
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)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1090
apply auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1091
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1092
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1093
lemma DERIV_sin_sin_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1094
     "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
  1095
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1096
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1097
lemma DERIV_sin_sin_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1098
     "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1099
apply (cut_tac x = x in DERIV_sin_sin_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1100
apply (auto simp add: mult_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1101
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1102
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1103
lemma DERIV_sin_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1104
     "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
  1105
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1106
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1107
lemma DERIV_sin_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1108
     "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1109
by (auto simp add: numeral_2_eq_2)
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 DERIV_cos_cos_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1112
     "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
  1113
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1114
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1115
lemma DERIV_cos_cos_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1116
     "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1117
apply (cut_tac x = x in DERIV_cos_cos_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1118
apply (auto simp add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1119
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1120
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1121
lemma DERIV_cos_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1122
     "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
  1123
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1124
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1125
lemma DERIV_cos_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1126
     "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1127
by (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1128
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1129
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
  1130
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1131
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1132
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
  1133
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1134
apply (rule DERIV_cos_realpow2a, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1135
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1136
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1137
(* most useful *)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1138
lemma DERIV_cos_cos_mult3 [simp]: "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1139
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1140
apply (rule DERIV_cos_cos_mult2, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1141
done
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 DERIV_sin_circle_all: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1144
     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1145
             (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1146
apply (unfold real_diff_def, safe)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1147
apply (rule DERIV_add)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1148
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1149
done
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
lemma DERIV_sin_circle_all_zero [simp]: "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1152
by (cut_tac DERIV_sin_circle_all, auto)
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_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1155
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
  1156
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1157
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1158
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1159
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
  1160
apply (subst real_add_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1161
apply (simp (no_asm) del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1162
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1163
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1164
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
  1165
apply (cut_tac x = x in sin_cos_squared_add2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1166
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1167
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1168
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1169
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1170
apply (rule_tac a1 = "(cos x)\<twosuperior> " in add_right_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1171
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1172
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1173
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1174
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1175
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
  1176
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1177
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1178
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1179
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
  1180
by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1181
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
  1182
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
  1183
apply (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1184
apply (drule_tac n = "Suc 0" in power_gt1)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1185
apply (auto simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1186
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
  1187
apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1188
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1189
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1190
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1191
apply (insert abs_sin_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1192
apply (simp add: abs_le_interval_iff del: abs_sin_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1193
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1194
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1195
lemma sin_le_one [simp]: "sin x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1196
apply (insert abs_sin_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1197
apply (simp add: abs_le_interval_iff del: abs_sin_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1198
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1199
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
  1200
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
  1201
apply (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1202
apply (drule_tac n = "Suc 0" in power_gt1)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1203
apply (auto simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1204
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
  1205
apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1206
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1207
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1208
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1209
apply (insert abs_cos_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1210
apply (simp add: abs_le_interval_iff del: abs_cos_le_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1211
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1212
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1213
lemma cos_le_one [simp]: "cos x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1214
apply (insert abs_cos_le_one [of x]) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1215
apply (simp add: abs_le_interval_iff del: abs_cos_le_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1216
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1217
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1218
lemma DERIV_fun_pow: "DERIV g x :> m ==>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1219
      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
  1220
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1221
apply (rule_tac f = " (%x. x ^ n) " in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1222
apply (rule DERIV_pow, auto)
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 DERIV_fun_exp: "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1226
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1227
apply (rule_tac f = exp in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1228
apply (rule DERIV_exp, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1229
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1230
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1231
lemma DERIV_fun_sin: "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1232
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1233
apply (rule_tac f = sin in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1234
apply (rule DERIV_sin, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1235
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1236
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1237
lemma DERIV_fun_cos: "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1238
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1239
apply (rule_tac f = cos in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1240
apply (rule DERIV_cos, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1241
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1242
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1243
lemmas DERIV_intros = DERIV_Id DERIV_const DERIV_cos DERIV_cmult 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1244
                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1245
                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1246
                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1247
                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1248
                    DERIV_Id DERIV_const DERIV_cos
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1249
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1250
(* lemma *)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1251
lemma lemma_DERIV_sin_cos_add: "\<forall>x.  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1252
         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
  1253
               (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
  1254
apply (safe, rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1255
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1256
  --{*replaces the old @{text DERIV_tac}*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1257
apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1258
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1259
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1260
lemma sin_cos_add [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1261
     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1262
      (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
89840837108e converting Hyperreal/Transc