1 (* Title : HTranscendental.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2001 University of Edinburgh |
|
4 |
|
5 Converted to Isar and polished by lcp |
|
6 *) |
|
7 |
|
8 header{*Nonstandard Extensions of Transcendental Functions*} |
|
9 |
|
10 theory HTranscendental |
|
11 imports Transcendental HSeries HDeriv |
|
12 begin |
|
13 |
|
14 definition |
|
15 exphr :: "real => hypreal" where |
|
16 --{*define exponential function using standard part *} |
|
17 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" |
|
18 |
|
19 definition |
|
20 sinhr :: "real => hypreal" where |
|
21 "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else |
|
22 ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))" |
|
23 |
|
24 definition |
|
25 coshr :: "real => hypreal" where |
|
26 "coshr x = st(sumhr (0, whn, %n. (if even(n) then |
|
27 ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))" |
|
28 |
|
29 |
|
30 subsection{*Nonstandard Extension of Square Root Function*} |
|
31 |
|
32 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0" |
|
33 by (simp add: starfun star_n_zero_num) |
|
34 |
|
35 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1" |
|
36 by (simp add: starfun star_n_one_num) |
|
37 |
|
38 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)" |
|
39 apply (cases x) |
|
40 apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff |
|
41 simp del: hpowr_Suc realpow_Suc) |
|
42 done |
|
43 |
|
44 lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x" |
|
45 by (transfer, simp) |
|
46 |
|
47 lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2" |
|
48 by (frule hypreal_sqrt_gt_zero_pow2, auto) |
|
49 |
|
50 lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0" |
|
51 apply (frule hypreal_sqrt_pow2_gt_zero) |
|
52 apply (auto simp add: numeral_2_eq_2) |
|
53 done |
|
54 |
|
55 lemma hypreal_inverse_sqrt_pow2: |
|
56 "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x" |
|
57 apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric]) |
|
58 apply (auto dest: hypreal_sqrt_gt_zero_pow2) |
|
59 done |
|
60 |
|
61 lemma hypreal_sqrt_mult_distrib: |
|
62 "!!x y. [|0 < x; 0 <y |] ==> |
|
63 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |
|
64 apply transfer |
|
65 apply (auto intro: real_sqrt_mult_distrib) |
|
66 done |
|
67 |
|
68 lemma hypreal_sqrt_mult_distrib2: |
|
69 "[|0\<le>x; 0\<le>y |] ==> |
|
70 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |
|
71 by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less) |
|
72 |
|
73 lemma hypreal_sqrt_approx_zero [simp]: |
|
74 "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)" |
|
75 apply (auto simp add: mem_infmal_iff [symmetric]) |
|
76 apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst]) |
|
77 apply (auto intro: Infinitesimal_mult |
|
78 dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] |
|
79 simp add: numeral_2_eq_2) |
|
80 done |
|
81 |
|
82 lemma hypreal_sqrt_approx_zero2 [simp]: |
|
83 "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)" |
|
84 by (auto simp add: order_le_less) |
|
85 |
|
86 lemma hypreal_sqrt_sum_squares [simp]: |
|
87 "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)" |
|
88 apply (rule hypreal_sqrt_approx_zero2) |
|
89 apply (rule add_nonneg_nonneg)+ |
|
90 apply (auto) |
|
91 done |
|
92 |
|
93 lemma hypreal_sqrt_sum_squares2 [simp]: |
|
94 "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)" |
|
95 apply (rule hypreal_sqrt_approx_zero2) |
|
96 apply (rule add_nonneg_nonneg) |
|
97 apply (auto) |
|
98 done |
|
99 |
|
100 lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)" |
|
101 apply transfer |
|
102 apply (auto intro: real_sqrt_gt_zero) |
|
103 done |
|
104 |
|
105 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)" |
|
106 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) |
|
107 |
|
108 lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)" |
|
109 by (transfer, simp) |
|
110 |
|
111 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)" |
|
112 by (transfer, simp) |
|
113 |
|
114 lemma hypreal_sqrt_hyperpow_hrabs [simp]: |
|
115 "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)" |
|
116 by (transfer, simp) |
|
117 |
|
118 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite" |
|
119 apply (rule HFinite_square_iff [THEN iffD1]) |
|
120 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) |
|
121 done |
|
122 |
|
123 lemma st_hypreal_sqrt: |
|
124 "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)" |
|
125 apply (rule power_inject_base [where n=1]) |
|
126 apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero) |
|
127 apply (rule st_mult [THEN subst]) |
|
128 apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst]) |
|
129 apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst]) |
|
130 apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite) |
|
131 done |
|
132 |
|
133 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)" |
|
134 by transfer (rule real_sqrt_sum_squares_ge1) |
|
135 |
|
136 lemma HFinite_hypreal_sqrt: |
|
137 "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite" |
|
138 apply (auto simp add: order_le_less) |
|
139 apply (rule HFinite_square_iff [THEN iffD1]) |
|
140 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
141 apply (simp add: numeral_2_eq_2) |
|
142 done |
|
143 |
|
144 lemma HFinite_hypreal_sqrt_imp_HFinite: |
|
145 "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite" |
|
146 apply (auto simp add: order_le_less) |
|
147 apply (drule HFinite_square_iff [THEN iffD2]) |
|
148 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
149 apply (simp add: numeral_2_eq_2 del: HFinite_square_iff) |
|
150 done |
|
151 |
|
152 lemma HFinite_hypreal_sqrt_iff [simp]: |
|
153 "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)" |
|
154 by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite) |
|
155 |
|
156 lemma HFinite_sqrt_sum_squares [simp]: |
|
157 "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)" |
|
158 apply (rule HFinite_hypreal_sqrt_iff) |
|
159 apply (rule add_nonneg_nonneg) |
|
160 apply (auto) |
|
161 done |
|
162 |
|
163 lemma Infinitesimal_hypreal_sqrt: |
|
164 "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal" |
|
165 apply (auto simp add: order_le_less) |
|
166 apply (rule Infinitesimal_square_iff [THEN iffD2]) |
|
167 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
168 apply (simp add: numeral_2_eq_2) |
|
169 done |
|
170 |
|
171 lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal: |
|
172 "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal" |
|
173 apply (auto simp add: order_le_less) |
|
174 apply (drule Infinitesimal_square_iff [THEN iffD1]) |
|
175 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
176 apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric]) |
|
177 done |
|
178 |
|
179 lemma Infinitesimal_hypreal_sqrt_iff [simp]: |
|
180 "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)" |
|
181 by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt) |
|
182 |
|
183 lemma Infinitesimal_sqrt_sum_squares [simp]: |
|
184 "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)" |
|
185 apply (rule Infinitesimal_hypreal_sqrt_iff) |
|
186 apply (rule add_nonneg_nonneg) |
|
187 apply (auto) |
|
188 done |
|
189 |
|
190 lemma HInfinite_hypreal_sqrt: |
|
191 "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite" |
|
192 apply (auto simp add: order_le_less) |
|
193 apply (rule HInfinite_square_iff [THEN iffD1]) |
|
194 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
195 apply (simp add: numeral_2_eq_2) |
|
196 done |
|
197 |
|
198 lemma HInfinite_hypreal_sqrt_imp_HInfinite: |
|
199 "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite" |
|
200 apply (auto simp add: order_le_less) |
|
201 apply (drule HInfinite_square_iff [THEN iffD2]) |
|
202 apply (drule hypreal_sqrt_gt_zero_pow2) |
|
203 apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff) |
|
204 done |
|
205 |
|
206 lemma HInfinite_hypreal_sqrt_iff [simp]: |
|
207 "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)" |
|
208 by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite) |
|
209 |
|
210 lemma HInfinite_sqrt_sum_squares [simp]: |
|
211 "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)" |
|
212 apply (rule HInfinite_hypreal_sqrt_iff) |
|
213 apply (rule add_nonneg_nonneg) |
|
214 apply (auto) |
|
215 done |
|
216 |
|
217 lemma HFinite_exp [simp]: |
|
218 "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite" |
|
219 unfolding sumhr_app |
|
220 apply (simp only: star_zero_def starfun2_star_of) |
|
221 apply (rule NSBseqD2) |
|
222 apply (rule NSconvergent_NSBseq) |
|
223 apply (rule convergent_NSconvergent_iff [THEN iffD1]) |
|
224 apply (rule summable_convergent_sumr_iff [THEN iffD1]) |
|
225 apply (rule summable_exp) |
|
226 done |
|
227 |
|
228 lemma exphr_zero [simp]: "exphr 0 = 1" |
|
229 apply (simp add: exphr_def sumhr_split_add |
|
230 [OF hypnat_one_less_hypnat_omega, symmetric]) |
|
231 apply (rule st_unique, simp) |
|
232 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl]) |
|
233 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) |
|
234 apply (rule_tac x="whn" in spec) |
|
235 apply (unfold sumhr_app, transfer, simp) |
|
236 done |
|
237 |
|
238 lemma coshr_zero [simp]: "coshr 0 = 1" |
|
239 apply (simp add: coshr_def sumhr_split_add |
|
240 [OF hypnat_one_less_hypnat_omega, symmetric]) |
|
241 apply (rule st_unique, simp) |
|
242 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl]) |
|
243 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) |
|
244 apply (rule_tac x="whn" in spec) |
|
245 apply (unfold sumhr_app, transfer, simp) |
|
246 done |
|
247 |
|
248 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1" |
|
249 apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp) |
|
250 apply (transfer, simp) |
|
251 done |
|
252 |
|
253 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1" |
|
254 apply (case_tac "x = 0") |
|
255 apply (cut_tac [2] x = 0 in DERIV_exp) |
|
256 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
|
257 apply (drule_tac x = x in bspec, auto) |
|
258 apply (drule_tac c = x in approx_mult1) |
|
259 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
260 simp add: mult_assoc) |
|
261 apply (rule approx_add_right_cancel [where d="-1"]) |
|
262 apply (rule approx_sym [THEN [2] approx_trans2]) |
|
263 apply (auto simp add: diff_def mem_infmal_iff) |
|
264 done |
|
265 |
|
266 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1" |
|
267 by (auto intro: STAR_exp_Infinitesimal) |
|
268 |
|
269 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" |
|
270 by transfer (rule exp_add) |
|
271 |
|
272 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" |
|
273 apply (simp add: exphr_def) |
|
274 apply (rule st_unique, simp) |
|
275 apply (subst starfunNat_sumr [symmetric]) |
|
276 apply (rule NSLIMSEQ_D [THEN approx_sym]) |
|
277 apply (rule LIMSEQ_NSLIMSEQ) |
|
278 apply (subst sums_def [symmetric]) |
|
279 apply (cut_tac exp_converges [where x=x], simp) |
|
280 apply (rule HNatInfinite_whn) |
|
281 done |
|
282 |
|
283 lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x" |
|
284 by transfer (rule exp_ge_add_one_self_aux) |
|
285 |
|
286 (* exp (oo) is infinite *) |
|
287 lemma starfun_exp_HInfinite: |
|
288 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite" |
|
289 apply (frule starfun_exp_ge_add_one_self) |
|
290 apply (rule HInfinite_ge_HInfinite, assumption) |
|
291 apply (rule order_trans [of _ "1+x"], auto) |
|
292 done |
|
293 |
|
294 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)" |
|
295 by transfer (rule exp_minus) |
|
296 |
|
297 (* exp (-oo) is infinitesimal *) |
|
298 lemma starfun_exp_Infinitesimal: |
|
299 "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal" |
|
300 apply (subgoal_tac "\<exists>y. x = - y") |
|
301 apply (rule_tac [2] x = "- x" in exI) |
|
302 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite |
|
303 simp add: starfun_exp_minus HInfinite_minus_iff) |
|
304 done |
|
305 |
|
306 lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x" |
|
307 by transfer (rule exp_gt_one) |
|
308 |
|
309 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x" |
|
310 by transfer (rule ln_exp) |
|
311 |
|
312 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)" |
|
313 by transfer (rule exp_ln_iff) |
|
314 |
|
315 lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u" |
|
316 by transfer (rule exp_ln_eq) |
|
317 |
|
318 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x" |
|
319 by transfer (rule ln_less_self) |
|
320 |
|
321 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x" |
|
322 by transfer (rule ln_ge_zero) |
|
323 |
|
324 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x" |
|
325 by transfer (rule ln_gt_zero) |
|
326 |
|
327 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0" |
|
328 by transfer simp |
|
329 |
|
330 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite" |
|
331 apply (rule HFinite_bounded) |
|
332 apply assumption |
|
333 apply (simp_all add: starfun_ln_less_self order_less_imp_le) |
|
334 done |
|
335 |
|
336 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x" |
|
337 by transfer (rule ln_inverse) |
|
338 |
|
339 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x" |
|
340 by transfer (rule abs_exp_cancel) |
|
341 |
|
342 lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y" |
|
343 by transfer (rule exp_less_mono) |
|
344 |
|
345 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite" |
|
346 apply (auto simp add: HFinite_def, rename_tac u) |
|
347 apply (rule_tac x="( *f* exp) u" in rev_bexI) |
|
348 apply (simp add: Reals_eq_Standard) |
|
349 apply (simp add: starfun_abs_exp_cancel) |
|
350 apply (simp add: starfun_exp_less_mono) |
|
351 done |
|
352 |
|
353 lemma starfun_exp_add_HFinite_Infinitesimal_approx: |
|
354 "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z" |
|
355 apply (simp add: STAR_exp_add) |
|
356 apply (frule STAR_exp_Infinitesimal) |
|
357 apply (drule approx_mult2) |
|
358 apply (auto intro: starfun_exp_HFinite) |
|
359 done |
|
360 |
|
361 (* using previous result to get to result *) |
|
362 lemma starfun_ln_HInfinite: |
|
363 "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite" |
|
364 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
|
365 apply (drule starfun_exp_HFinite) |
|
366 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff) |
|
367 done |
|
368 |
|
369 lemma starfun_exp_HInfinite_Infinitesimal_disj: |
|
370 "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) (x::hypreal) \<in> Infinitesimal" |
|
371 apply (insert linorder_linear [of x 0]) |
|
372 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal) |
|
373 done |
|
374 |
|
375 (* check out this proof!!! *) |
|
376 lemma starfun_ln_HFinite_not_Infinitesimal: |
|
377 "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite" |
|
378 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2]) |
|
379 apply (drule starfun_exp_HInfinite_Infinitesimal_disj) |
|
380 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff |
|
381 del: starfun_exp_ln_iff) |
|
382 done |
|
383 |
|
384 (* we do proof by considering ln of 1/x *) |
|
385 lemma starfun_ln_Infinitesimal_HInfinite: |
|
386 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite" |
|
387 apply (drule Infinitesimal_inverse_HInfinite) |
|
388 apply (frule positive_imp_inverse_positive) |
|
389 apply (drule_tac [2] starfun_ln_HInfinite) |
|
390 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) |
|
391 done |
|
392 |
|
393 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0" |
|
394 by transfer (rule ln_less_zero) |
|
395 |
|
396 lemma starfun_ln_Infinitesimal_less_zero: |
|
397 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0" |
|
398 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) |
|
399 |
|
400 lemma starfun_ln_HInfinite_gt_zero: |
|
401 "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x" |
|
402 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) |
|
403 |
|
404 |
|
405 (* |
|
406 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x" |
|
407 *) |
|
408 |
|
409 lemma HFinite_sin [simp]: |
|
410 "sumhr (0, whn, %n. (if even(n) then 0 else |
|
411 (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n) |
|
412 \<in> HFinite" |
|
413 unfolding sumhr_app |
|
414 apply (simp only: star_zero_def starfun2_star_of) |
|
415 apply (rule NSBseqD2) |
|
416 apply (rule NSconvergent_NSBseq) |
|
417 apply (rule convergent_NSconvergent_iff [THEN iffD1]) |
|
418 apply (rule summable_convergent_sumr_iff [THEN iffD1]) |
|
419 apply (simp only: One_nat_def summable_sin) |
|
420 done |
|
421 |
|
422 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" |
|
423 by transfer (rule sin_zero) |
|
424 |
|
425 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x" |
|
426 apply (case_tac "x = 0") |
|
427 apply (cut_tac [2] x = 0 in DERIV_sin) |
|
428 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
|
429 apply (drule bspec [where x = x], auto) |
|
430 apply (drule approx_mult1 [where c = x]) |
|
431 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
432 simp add: mult_assoc) |
|
433 done |
|
434 |
|
435 lemma HFinite_cos [simp]: |
|
436 "sumhr (0, whn, %n. (if even(n) then |
|
437 (-1 ^ (n div 2))/(real (fact n)) else |
|
438 0) * x ^ n) \<in> HFinite" |
|
439 unfolding sumhr_app |
|
440 apply (simp only: star_zero_def starfun2_star_of) |
|
441 apply (rule NSBseqD2) |
|
442 apply (rule NSconvergent_NSBseq) |
|
443 apply (rule convergent_NSconvergent_iff [THEN iffD1]) |
|
444 apply (rule summable_convergent_sumr_iff [THEN iffD1]) |
|
445 apply (rule summable_cos) |
|
446 done |
|
447 |
|
448 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" |
|
449 by transfer (rule cos_zero) |
|
450 |
|
451 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1" |
|
452 apply (case_tac "x = 0") |
|
453 apply (cut_tac [2] x = 0 in DERIV_cos) |
|
454 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
|
455 apply (drule bspec [where x = x]) |
|
456 apply auto |
|
457 apply (drule approx_mult1 [where c = x]) |
|
458 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
459 simp add: mult_assoc) |
|
460 apply (rule approx_add_right_cancel [where d = "-1"]) |
|
461 apply (simp add: diff_def) |
|
462 done |
|
463 |
|
464 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" |
|
465 by transfer (rule tan_zero) |
|
466 |
|
467 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x" |
|
468 apply (case_tac "x = 0") |
|
469 apply (cut_tac [2] x = 0 in DERIV_tan) |
|
470 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
|
471 apply (drule bspec [where x = x], auto) |
|
472 apply (drule approx_mult1 [where c = x]) |
|
473 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
474 simp add: mult_assoc) |
|
475 done |
|
476 |
|
477 lemma STAR_sin_cos_Infinitesimal_mult: |
|
478 "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x" |
|
479 apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) |
|
480 apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) |
|
481 done |
|
482 |
|
483 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite" |
|
484 by simp |
|
485 |
|
486 (* lemmas *) |
|
487 |
|
488 lemma lemma_split_hypreal_of_real: |
|
489 "N \<in> HNatInfinite |
|
490 ==> hypreal_of_real a = |
|
491 hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)" |
|
492 by (simp add: mult_assoc [symmetric] zero_less_HNatInfinite) |
|
493 |
|
494 lemma STAR_sin_Infinitesimal_divide: |
|
495 "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1" |
|
496 apply (cut_tac x = 0 in DERIV_sin) |
|
497 apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
|
498 done |
|
499 |
|
500 (*------------------------------------------------------------------------*) |
|
501 (* sin* (1/n) * 1/(1/n) @= 1 for n = oo *) |
|
502 (*------------------------------------------------------------------------*) |
|
503 |
|
504 lemma lemma_sin_pi: |
|
505 "n \<in> HNatInfinite |
|
506 ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1" |
|
507 apply (rule STAR_sin_Infinitesimal_divide) |
|
508 apply (auto simp add: zero_less_HNatInfinite) |
|
509 done |
|
510 |
|
511 lemma STAR_sin_inverse_HNatInfinite: |
|
512 "n \<in> HNatInfinite |
|
513 ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1" |
|
514 apply (frule lemma_sin_pi) |
|
515 apply (simp add: divide_inverse) |
|
516 done |
|
517 |
|
518 lemma Infinitesimal_pi_divide_HNatInfinite: |
|
519 "N \<in> HNatInfinite |
|
520 ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal" |
|
521 apply (simp add: divide_inverse) |
|
522 apply (auto intro: Infinitesimal_HFinite_mult2) |
|
523 done |
|
524 |
|
525 lemma pi_divide_HNatInfinite_not_zero [simp]: |
|
526 "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0" |
|
527 by (simp add: zero_less_HNatInfinite) |
|
528 |
|
529 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi: |
|
530 "n \<in> HNatInfinite |
|
531 ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n |
|
532 @= hypreal_of_real pi" |
|
533 apply (frule STAR_sin_Infinitesimal_divide |
|
534 [OF Infinitesimal_pi_divide_HNatInfinite |
|
535 pi_divide_HNatInfinite_not_zero]) |
|
536 apply (auto) |
|
537 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) |
|
538 apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac) |
|
539 done |
|
540 |
|
541 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: |
|
542 "n \<in> HNatInfinite |
|
543 ==> hypreal_of_hypnat n * |
|
544 ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) |
|
545 @= hypreal_of_real pi" |
|
546 apply (rule mult_commute [THEN subst]) |
|
547 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi) |
|
548 done |
|
549 |
|
550 lemma starfunNat_pi_divide_n_Infinitesimal: |
|
551 "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal" |
|
552 by (auto intro!: Infinitesimal_HFinite_mult2 |
|
553 simp add: starfun_mult [symmetric] divide_inverse |
|
554 starfun_inverse [symmetric] starfunNat_real_of_nat) |
|
555 |
|
556 lemma STAR_sin_pi_divide_n_approx: |
|
557 "N \<in> HNatInfinite ==> |
|
558 ( *f* sin) (( *f* (%x. pi / real x)) N) @= |
|
559 hypreal_of_real pi/(hypreal_of_hypnat N)" |
|
560 apply (simp add: starfunNat_real_of_nat [symmetric]) |
|
561 apply (rule STAR_sin_Infinitesimal) |
|
562 apply (simp add: divide_inverse) |
|
563 apply (rule Infinitesimal_HFinite_mult2) |
|
564 apply (subst starfun_inverse) |
|
565 apply (erule starfunNat_inverse_real_of_nat_Infinitesimal) |
|
566 apply simp |
|
567 done |
|
568 |
|
569 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi" |
|
570 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat) |
|
571 apply (rule_tac f1 = sin in starfun_o2 [THEN subst]) |
|
572 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse) |
|
573 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |
|
574 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi |
|
575 simp add: starfunNat_real_of_nat mult_commute divide_inverse) |
|
576 done |
|
577 |
|
578 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1" |
|
579 apply (simp add: NSLIMSEQ_def, auto) |
|
580 apply (rule_tac f1 = cos in starfun_o2 [THEN subst]) |
|
581 apply (rule STAR_cos_Infinitesimal) |
|
582 apply (auto intro!: Infinitesimal_HFinite_mult2 |
|
583 simp add: starfun_mult [symmetric] divide_inverse |
|
584 starfun_inverse [symmetric] starfunNat_real_of_nat) |
|
585 done |
|
586 |
|
587 lemma NSLIMSEQ_sin_cos_pi: |
|
588 "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi" |
|
589 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp) |
|
590 |
|
591 |
|
592 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*} |
|
593 |
|
594 lemma STAR_cos_Infinitesimal_approx: |
|
595 "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2" |
|
596 apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) |
|
597 apply (auto simp add: Infinitesimal_approx_minus [symmetric] |
|
598 diff_minus add_assoc [symmetric] numeral_2_eq_2) |
|
599 done |
|
600 |
|
601 lemma STAR_cos_Infinitesimal_approx2: |
|
602 "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2" |
|
603 apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) |
|
604 apply (auto intro: Infinitesimal_SReal_divide |
|
605 simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) |
|
606 done |
|
607 |
|
608 end |
|