240 convergent_NSconvergent_iff [symmetric] |
240 convergent_NSconvergent_iff [symmetric] |
241 summable_convergent_sumr_iff [symmetric] summable_exp) |
241 summable_convergent_sumr_iff [symmetric] summable_exp) |
242 |
242 |
243 lemma exphr_zero [simp]: "exphr 0 = 1" |
243 lemma exphr_zero [simp]: "exphr 0 = 1" |
244 apply (simp add: exphr_def sumhr_split_add |
244 apply (simp add: exphr_def sumhr_split_add |
245 [OF hypnat_one_less_hypnat_omega, symmetric]) |
245 [OF hypnat_one_less_hypnat_omega, symmetric]) |
246 apply (simp add: sumhr star_n_zero_num starfun star_n_one_num star_n_add |
246 apply (rule st_unique, simp) |
247 hypnat_omega_def |
247 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl]) |
248 del: OrderedGroup.add_0) |
248 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) |
249 apply (simp add: star_n_one_num [symmetric]) |
249 apply (rule_tac x="whn" in spec) |
|
250 apply (unfold sumhr_app, transfer, simp) |
250 done |
251 done |
251 |
252 |
252 lemma coshr_zero [simp]: "coshr 0 = 1" |
253 lemma coshr_zero [simp]: "coshr 0 = 1" |
253 apply (simp add: coshr_def sumhr_split_add |
254 apply (simp add: coshr_def sumhr_split_add |
254 [OF hypnat_one_less_hypnat_omega, symmetric]) |
255 [OF hypnat_one_less_hypnat_omega, symmetric]) |
255 apply (simp add: sumhr star_n_zero_num star_n_one_num hypnat_omega_def) |
256 apply (rule st_unique, simp) |
256 apply (simp add: star_n_one_num [symmetric] star_n_zero_num [symmetric]) |
257 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl]) |
|
258 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) |
|
259 apply (rule_tac x="whn" in spec) |
|
260 apply (unfold sumhr_app, transfer, simp) |
257 done |
261 done |
258 |
262 |
259 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1" |
263 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1" |
260 by (simp add: star_n_zero_num star_n_one_num starfun) |
264 apply (subgoal_tac "( *f* exp) 0 = 1", simp) |
|
265 apply (transfer, simp) |
|
266 done |
261 |
267 |
262 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1" |
268 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1" |
263 apply (case_tac "x = 0") |
269 apply (case_tac "x = 0") |
264 apply (cut_tac [2] x = 0 in DERIV_exp) |
270 apply (cut_tac [2] x = 0 in DERIV_exp) |
265 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
271 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
274 |
280 |
275 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1" |
281 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1" |
276 by (auto intro: STAR_exp_Infinitesimal) |
282 by (auto intro: STAR_exp_Infinitesimal) |
277 |
283 |
278 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" |
284 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" |
279 by (transfer, rule exp_add) |
285 by transfer (rule exp_add) |
280 |
286 |
281 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" |
287 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" |
282 apply (simp add: exphr_def) |
288 apply (simp add: exphr_def) |
283 apply (rule st_hypreal_of_real [THEN subst]) |
289 apply (rule st_unique, simp) |
284 apply (rule approx_st_eq, auto) |
290 apply (subst starfunNat_sumr [symmetric]) |
285 apply (rule approx_minus_iff [THEN iffD2]) |
291 apply (rule NSLIMSEQ_D [THEN approx_sym]) |
286 apply (simp only: mem_infmal_iff [symmetric]) |
292 apply (rule LIMSEQ_NSLIMSEQ) |
287 apply (auto simp add: mem_infmal_iff [symmetric] star_of_def star_n_zero_num hypnat_omega_def sumhr star_n_diff) |
293 apply (subst sums_def [symmetric]) |
288 apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal) |
294 apply (rule exp_converges) |
289 apply (insert exp_converges [of x]) |
295 apply (rule HNatInfinite_whn) |
290 apply (simp add: sums_def) |
|
291 apply (drule LIMSEQ_const [THEN [2] LIMSEQ_diff, where b = "exp x"]) |
|
292 apply (simp add: LIMSEQ_NSLIMSEQ_iff) |
|
293 done |
296 done |
294 |
297 |
295 lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x" |
298 lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x" |
296 by (transfer, rule exp_ge_add_one_self_aux) |
299 by transfer (rule exp_ge_add_one_self_aux) |
297 |
300 |
298 (* exp (oo) is infinite *) |
301 (* exp (oo) is infinite *) |
299 lemma starfun_exp_HInfinite: |
302 lemma starfun_exp_HInfinite: |
300 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite" |
303 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite" |
301 apply (frule starfun_exp_ge_add_one_self) |
304 apply (frule starfun_exp_ge_add_one_self) |
302 apply (rule HInfinite_ge_HInfinite, assumption) |
305 apply (rule HInfinite_ge_HInfinite, assumption) |
303 apply (rule order_trans [of _ "1+x"], auto) |
306 apply (rule order_trans [of _ "1+x"], auto) |
304 done |
307 done |
305 |
308 |
306 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)" |
309 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)" |
307 by (transfer, rule exp_minus) |
310 by transfer (rule exp_minus) |
308 |
311 |
309 (* exp (-oo) is infinitesimal *) |
312 (* exp (-oo) is infinitesimal *) |
310 lemma starfun_exp_Infinitesimal: |
313 lemma starfun_exp_Infinitesimal: |
311 "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal" |
314 "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal" |
312 apply (subgoal_tac "\<exists>y. x = - y") |
315 apply (subgoal_tac "\<exists>y. x = - y") |
314 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite |
317 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite |
315 simp add: starfun_exp_minus HInfinite_minus_iff) |
318 simp add: starfun_exp_minus HInfinite_minus_iff) |
316 done |
319 done |
317 |
320 |
318 lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x" |
321 lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x" |
319 by (transfer, simp) |
322 by transfer (rule exp_gt_one) |
320 |
323 |
321 (* needs derivative of inverse function |
324 (* needs derivative of inverse function |
322 TRY a NS one today!!! |
325 TRY a NS one today!!! |
323 |
326 |
324 Goal "x @= 1 ==> ( *f* ln) x @= 1" |
327 Goal "x @= 1 ==> ( *f* ln) x @= 1" |
330 |
333 |
331 *) |
334 *) |
332 |
335 |
333 |
336 |
334 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x" |
337 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x" |
335 by (transfer, simp) |
338 by transfer (rule ln_exp) |
336 |
339 |
337 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)" |
340 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)" |
338 by (transfer, simp) |
341 by transfer (rule exp_ln_iff) |
339 |
342 |
340 lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u" |
343 lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u" |
341 by auto |
344 by transfer (rule exp_ln_eq) |
342 |
345 |
343 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x" |
346 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x" |
344 by (transfer, simp) |
347 by transfer (rule ln_less_self) |
345 |
348 |
346 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x" |
349 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x" |
347 by (transfer, simp) |
350 by transfer (rule ln_ge_zero) |
348 |
351 |
349 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x" |
352 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x" |
350 by (transfer, simp) |
353 by transfer (rule ln_gt_zero) |
351 |
354 |
352 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0" |
355 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0" |
353 by (transfer, simp) |
356 by transfer simp |
354 |
357 |
355 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite" |
358 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite" |
356 apply (rule HFinite_bounded) |
359 apply (rule HFinite_bounded) |
357 apply assumption |
360 apply assumption |
358 apply (simp_all add: starfun_ln_less_self order_less_imp_le) |
361 apply (simp_all add: starfun_ln_less_self order_less_imp_le) |
359 done |
362 done |
360 |
363 |
361 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x" |
364 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x" |
362 by (transfer, rule ln_inverse) |
365 by transfer (rule ln_inverse) |
363 |
366 |
364 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) x\<bar> = ( *f* exp) x" |
367 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) x\<bar> = ( *f* exp) x" |
365 by transfer (rule abs_exp_cancel) |
368 by transfer (rule abs_exp_cancel) |
366 |
369 |
367 lemma starfun_exp_less_mono: "\<And>x y. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y" |
370 lemma starfun_exp_less_mono: "\<And>x y. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y" |
414 apply (drule_tac [2] starfun_ln_HInfinite) |
417 apply (drule_tac [2] starfun_ln_HInfinite) |
415 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) |
418 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) |
416 done |
419 done |
417 |
420 |
418 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0" |
421 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0" |
419 by (transfer, simp) |
422 by transfer (rule ln_less_zero) |
420 |
423 |
421 lemma starfun_ln_Infinitesimal_less_zero: |
424 lemma starfun_ln_Infinitesimal_less_zero: |
422 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0" |
425 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0" |
423 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) |
426 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) |
424 |
427 |
441 summable_convergent_sumr_iff [symmetric]) |
444 summable_convergent_sumr_iff [symmetric]) |
442 apply (simp only: One_nat_def summable_sin) |
445 apply (simp only: One_nat_def summable_sin) |
443 done |
446 done |
444 |
447 |
445 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" |
448 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" |
446 by (transfer, simp) |
449 by transfer (rule sin_zero) |
447 |
450 |
448 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x" |
451 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x" |
449 apply (case_tac "x = 0") |
452 apply (case_tac "x = 0") |
450 apply (cut_tac [2] x = 0 in DERIV_sin) |
453 apply (cut_tac [2] x = 0 in DERIV_sin) |
451 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
454 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
463 simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def |
466 simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def |
464 convergent_NSconvergent_iff [symmetric] |
467 convergent_NSconvergent_iff [symmetric] |
465 summable_convergent_sumr_iff [symmetric] summable_cos) |
468 summable_convergent_sumr_iff [symmetric] summable_cos) |
466 |
469 |
467 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" |
470 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" |
468 by (simp add: starfun star_n_zero_num star_n_one_num) |
471 by transfer (rule cos_zero) |
469 |
472 |
470 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1" |
473 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1" |
471 apply (case_tac "x = 0") |
474 apply (case_tac "x = 0") |
472 apply (cut_tac [2] x = 0 in DERIV_cos) |
475 apply (cut_tac [2] x = 0 in DERIV_cos) |
473 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
476 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
479 apply (rule approx_add_right_cancel [where d = "-1"]) |
482 apply (rule approx_add_right_cancel [where d = "-1"]) |
480 apply (simp add: diff_def) |
483 apply (simp add: diff_def) |
481 done |
484 done |
482 |
485 |
483 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" |
486 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" |
484 by (simp add: starfun star_n_zero_num) |
487 by transfer (rule tan_zero) |
485 |
488 |
486 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x" |
489 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x" |
487 apply (case_tac "x = 0") |
490 apply (case_tac "x = 0") |
488 apply (cut_tac [2] x = 0 in DERIV_tan) |
491 apply (cut_tac [2] x = 0 in DERIV_tan) |
489 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
492 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |