linear arithmetic splits certain operators (e.g. min, max, abs)
1 (* Title : HTranscendental.thy
2 Author : Jacques D. Fleuriot
3 Copyright : 2001 University of Edinburgh
5 Converted to Isar and polished by lcp
8 header{*Nonstandard Extensions of Transcendental Functions*}
10 theory HTranscendental
11 imports Transcendental Integration
14 text{*really belongs in Transcendental*}
15 lemma sqrt_divide_self_eq:
16 assumes nneg: "0 \<le> x"
17 shows "sqrt x / x = inverse (sqrt x)"
19 assume "x=0" thus ?thesis by simp
21 assume nz: "x\<noteq>0"
22 hence pos: "0<x" using nneg by arith
24 proof (rule right_inverse_eq [THEN iffD1, THEN sym])
25 show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz)
26 show "inverse (sqrt x) / (sqrt x / x) = 1"
27 by (simp add: divide_inverse mult_assoc [symmetric]
28 power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
34 exphr :: "real => hypreal"
35 --{*define exponential function using standard part *}
36 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
38 sinhr :: "real => hypreal"
39 "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else
40 ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
42 coshr :: "real => hypreal"
43 "coshr x = st(sumhr (0, whn, %n. (if even(n) then
44 ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
47 subsection{*Nonstandard Extension of Square Root Function*}
49 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
50 by (simp add: starfun star_n_zero_num)
52 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
53 by (simp add: starfun star_n_one_num)
55 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
57 apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
58 simp del: hpowr_Suc realpow_Suc)
61 lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
64 lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
65 by (frule hypreal_sqrt_gt_zero_pow2, auto)
67 lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
68 apply (frule hypreal_sqrt_pow2_gt_zero)
69 apply (auto simp add: numeral_2_eq_2)
72 lemma hypreal_inverse_sqrt_pow2:
73 "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
74 apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
75 apply (auto dest: hypreal_sqrt_gt_zero_pow2)
78 lemma hypreal_sqrt_mult_distrib:
79 "!!x y. [|0 < x; 0 <y |] ==>
80 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
82 apply (auto intro: real_sqrt_mult_distrib)
85 lemma hypreal_sqrt_mult_distrib2:
86 "[|0\<le>x; 0\<le>y |] ==>
87 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
88 by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
90 lemma hypreal_sqrt_approx_zero [simp]:
91 "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
92 apply (auto simp add: mem_infmal_iff [symmetric])
93 apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
94 apply (auto intro: Infinitesimal_mult
95 dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst]
96 simp add: numeral_2_eq_2)
99 lemma hypreal_sqrt_approx_zero2 [simp]:
100 "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
101 by (auto simp add: order_le_less)
103 lemma hypreal_sqrt_sum_squares [simp]:
104 "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
105 apply (rule hypreal_sqrt_approx_zero2)
106 apply (rule add_nonneg_nonneg)+
107 apply (auto simp add: zero_le_square)
110 lemma hypreal_sqrt_sum_squares2 [simp]:
111 "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
112 apply (rule hypreal_sqrt_approx_zero2)
113 apply (rule add_nonneg_nonneg)
114 apply (auto simp add: zero_le_square)
117 lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
119 apply (auto intro: real_sqrt_gt_zero)
122 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
123 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
125 lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)"
128 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
131 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
132 "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
135 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
136 apply (rule HFinite_square_iff [THEN iffD1])
137 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp)
140 lemma st_hypreal_sqrt:
141 "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
142 apply (rule power_inject_base [where n=1])
143 apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
144 apply (rule st_mult [THEN subst])
145 apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
146 apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
147 apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
150 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
153 lemma HFinite_hypreal_sqrt:
154 "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
155 apply (auto simp add: order_le_less)
156 apply (rule HFinite_square_iff [THEN iffD1])
157 apply (drule hypreal_sqrt_gt_zero_pow2)
158 apply (simp add: numeral_2_eq_2)
161 lemma HFinite_hypreal_sqrt_imp_HFinite:
162 "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
163 apply (auto simp add: order_le_less)
164 apply (drule HFinite_square_iff [THEN iffD2])
165 apply (drule hypreal_sqrt_gt_zero_pow2)
166 apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
169 lemma HFinite_hypreal_sqrt_iff [simp]:
170 "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
171 by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
173 lemma HFinite_sqrt_sum_squares [simp]:
174 "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
175 apply (rule HFinite_hypreal_sqrt_iff)
176 apply (rule add_nonneg_nonneg)
177 apply (auto simp add: zero_le_square)
180 lemma Infinitesimal_hypreal_sqrt:
181 "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
182 apply (auto simp add: order_le_less)
183 apply (rule Infinitesimal_square_iff [THEN iffD2])
184 apply (drule hypreal_sqrt_gt_zero_pow2)
185 apply (simp add: numeral_2_eq_2)
188 lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
189 "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
190 apply (auto simp add: order_le_less)
191 apply (drule Infinitesimal_square_iff [THEN iffD1])
192 apply (drule hypreal_sqrt_gt_zero_pow2)
193 apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
196 lemma Infinitesimal_hypreal_sqrt_iff [simp]:
197 "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
198 by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
200 lemma Infinitesimal_sqrt_sum_squares [simp]:
201 "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
202 apply (rule Infinitesimal_hypreal_sqrt_iff)
203 apply (rule add_nonneg_nonneg)
204 apply (auto simp add: zero_le_square)
207 lemma HInfinite_hypreal_sqrt:
208 "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
209 apply (auto simp add: order_le_less)
210 apply (rule HInfinite_square_iff [THEN iffD1])
211 apply (drule hypreal_sqrt_gt_zero_pow2)
212 apply (simp add: numeral_2_eq_2)
215 lemma HInfinite_hypreal_sqrt_imp_HInfinite:
216 "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
217 apply (auto simp add: order_le_less)
218 apply (drule HInfinite_square_iff [THEN iffD2])
219 apply (drule hypreal_sqrt_gt_zero_pow2)
220 apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
223 lemma HInfinite_hypreal_sqrt_iff [simp]:
224 "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
225 by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
227 lemma HInfinite_sqrt_sum_squares [simp]:
228 "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
229 apply (rule HInfinite_hypreal_sqrt_iff)
230 apply (rule add_nonneg_nonneg)
231 apply (auto simp add: zero_le_square)
234 lemma HFinite_exp [simp]:
235 "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
236 by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
237 simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
238 convergent_NSconvergent_iff [symmetric]
239 summable_convergent_sumr_iff [symmetric] summable_exp)
241 lemma exphr_zero [simp]: "exphr 0 = 1"
242 apply (simp add: exphr_def sumhr_split_add
243 [OF hypnat_one_less_hypnat_omega, symmetric])
244 apply (simp add: sumhr star_n_zero_num starfun star_n_one_num star_n_add
246 del: OrderedGroup.add_0)
247 apply (simp add: star_n_one_num [symmetric])
250 lemma coshr_zero [simp]: "coshr 0 = 1"
251 apply (simp add: coshr_def sumhr_split_add
252 [OF hypnat_one_less_hypnat_omega, symmetric])
253 apply (simp add: sumhr star_n_zero_num star_n_one_num hypnat_omega_def)
254 apply (simp add: star_n_one_num [symmetric] star_n_zero_num [symmetric])
257 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
258 by (simp add: star_n_zero_num star_n_one_num starfun)
260 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
261 apply (case_tac "x = 0")
262 apply (cut_tac [2] x = 0 in DERIV_exp)
263 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
264 apply (drule_tac x = x in bspec, auto)
265 apply (drule_tac c = x in approx_mult1)
266 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
267 simp add: mult_assoc)
268 apply (rule approx_add_right_cancel [where d="-1"])
269 apply (rule approx_sym [THEN [2] approx_trans2])
270 apply (auto simp add: mem_infmal_iff)
273 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
274 by (auto intro: STAR_exp_Infinitesimal)
276 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
277 by (transfer, rule exp_add)
279 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
280 apply (simp add: exphr_def)
281 apply (rule st_hypreal_of_real [THEN subst])
282 apply (rule approx_st_eq, auto)
283 apply (rule approx_minus_iff [THEN iffD2])
284 apply (simp only: mem_infmal_iff [symmetric])
285 apply (auto simp add: mem_infmal_iff [symmetric] star_of_def star_n_zero_num hypnat_omega_def sumhr star_n_minus star_n_add)
286 apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
287 apply (insert exp_converges [of x])
288 apply (simp add: sums_def)
289 apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
290 apply (simp add: LIMSEQ_NSLIMSEQ_iff)
293 lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
294 by (transfer, rule exp_ge_add_one_self_aux)
296 (* exp (oo) is infinite *)
297 lemma starfun_exp_HInfinite:
298 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
299 apply (frule starfun_exp_ge_add_one_self)
300 apply (rule HInfinite_ge_HInfinite, assumption)
301 apply (rule order_trans [of _ "1+x"], auto)
304 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)"
305 by (transfer, rule exp_minus)
307 (* exp (-oo) is infinitesimal *)
308 lemma starfun_exp_Infinitesimal:
309 "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
310 apply (subgoal_tac "\<exists>y. x = - y")
311 apply (rule_tac [2] x = "- x" in exI)
312 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
313 simp add: starfun_exp_minus HInfinite_minus_iff)
316 lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x"
319 (* needs derivative of inverse function
320 TRY a NS one today!!!
322 Goal "x @= 1 ==> ( *f* ln) x @= 1"
323 by (res_inst_tac [("z","x")] eq_Abs_star 1);
324 by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
327 Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
332 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
335 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
338 lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
341 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
344 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
347 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
350 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
353 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
354 apply (rule HFinite_bounded)
356 apply (simp_all add: starfun_ln_less_self order_less_imp_le)
359 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
360 by (transfer, rule ln_inverse)
362 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
364 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
365 apply (rule bexI [OF _ Rep_star_star_n], auto)
366 apply (rule_tac x = "exp u" in exI)
370 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
371 "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
372 apply (simp add: STAR_exp_add)
373 apply (frule STAR_exp_Infinitesimal)
374 apply (drule approx_mult2)
375 apply (auto intro: starfun_exp_HFinite)
378 (* using previous result to get to result *)
379 lemma starfun_ln_HInfinite:
380 "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
381 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
382 apply (drule starfun_exp_HFinite)
383 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
386 lemma starfun_exp_HInfinite_Infinitesimal_disj:
387 "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
388 apply (insert linorder_linear [of x 0])
389 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
392 (* check out this proof!!! *)
393 lemma starfun_ln_HFinite_not_Infinitesimal:
394 "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
395 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
396 apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
397 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
398 del: starfun_exp_ln_iff)
401 (* we do proof by considering ln of 1/x *)
402 lemma starfun_ln_Infinitesimal_HInfinite:
403 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
404 apply (drule Infinitesimal_inverse_HInfinite)
405 apply (frule positive_imp_inverse_positive)
406 apply (drule_tac [2] starfun_ln_HInfinite)
407 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
410 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
413 lemma starfun_ln_Infinitesimal_less_zero:
414 "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
415 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
417 lemma starfun_ln_HInfinite_gt_zero:
418 "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
419 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
423 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
426 lemma HFinite_sin [simp]:
427 "sumhr (0, whn, %n. (if even(n) then 0 else
428 ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
430 apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
431 simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
432 convergent_NSconvergent_iff [symmetric]
433 summable_convergent_sumr_iff [symmetric])
434 apply (simp only: One_nat_def summable_sin)
437 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
440 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
441 apply (case_tac "x = 0")
442 apply (cut_tac [2] x = 0 in DERIV_sin)
443 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
444 apply (drule bspec [where x = x], auto)
445 apply (drule approx_mult1 [where c = x])
446 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
447 simp add: mult_assoc)
450 lemma HFinite_cos [simp]:
451 "sumhr (0, whn, %n. (if even(n) then
452 ((- 1) ^ (n div 2))/(real (fact n)) else
453 0) * x ^ n) \<in> HFinite"
454 by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
455 simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
456 convergent_NSconvergent_iff [symmetric]
457 summable_convergent_sumr_iff [symmetric] summable_cos)
459 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
460 by (simp add: starfun star_n_zero_num star_n_one_num)
462 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
463 apply (case_tac "x = 0")
464 apply (cut_tac [2] x = 0 in DERIV_cos)
465 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
466 apply (drule bspec [where x = x])
468 apply (drule approx_mult1 [where c = x])
469 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
470 simp add: mult_assoc)
471 apply (rule approx_add_right_cancel [where d = "-1"], auto)
474 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
475 by (simp add: starfun star_n_zero_num)
477 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
478 apply (case_tac "x = 0")
479 apply (cut_tac [2] x = 0 in DERIV_tan)
480 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
481 apply (drule bspec [where x = x], auto)
482 apply (drule approx_mult1 [where c = x])
483 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
484 simp add: mult_assoc)
487 lemma STAR_sin_cos_Infinitesimal_mult:
488 "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
489 apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1])
490 apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
493 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
498 lemma lemma_split_hypreal_of_real:
499 "N \<in> HNatInfinite
500 ==> hypreal_of_real a =
501 hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
502 by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
504 lemma STAR_sin_Infinitesimal_divide:
505 "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
506 apply (cut_tac x = 0 in DERIV_sin)
507 apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
510 (*------------------------------------------------------------------------*)
511 (* sin* (1/n) * 1/(1/n) @= 1 for n = oo *)
512 (*------------------------------------------------------------------------*)
515 "n \<in> HNatInfinite
516 ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
517 apply (rule STAR_sin_Infinitesimal_divide)
518 apply (auto simp add: HNatInfinite_not_eq_zero)
521 lemma STAR_sin_inverse_HNatInfinite:
522 "n \<in> HNatInfinite
523 ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
524 apply (frule lemma_sin_pi)
525 apply (simp add: divide_inverse)
528 lemma Infinitesimal_pi_divide_HNatInfinite:
529 "N \<in> HNatInfinite
530 ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
531 apply (simp add: divide_inverse)
532 apply (auto intro: Infinitesimal_HFinite_mult2)
535 lemma pi_divide_HNatInfinite_not_zero [simp]:
536 "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
537 by (simp add: HNatInfinite_not_eq_zero)
539 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
540 "n \<in> HNatInfinite
541 ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n
542 @= hypreal_of_real pi"
543 apply (frule STAR_sin_Infinitesimal_divide
544 [OF Infinitesimal_pi_divide_HNatInfinite
545 pi_divide_HNatInfinite_not_zero])
547 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
548 apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
551 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
552 "n \<in> HNatInfinite
553 ==> hypreal_of_hypnat n *
554 ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))
555 @= hypreal_of_real pi"
556 apply (rule mult_commute [THEN subst])
557 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
560 lemma starfunNat_pi_divide_n_Infinitesimal:
561 "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
562 by (auto intro!: Infinitesimal_HFinite_mult2
563 simp add: starfun_mult [symmetric] divide_inverse
564 starfun_inverse [symmetric] starfunNat_real_of_nat)
566 lemma STAR_sin_pi_divide_n_approx:
567 "N \<in> HNatInfinite ==>
568 ( *f* sin) (( *f* (%x. pi / real x)) N) @=
569 hypreal_of_real pi/(hypreal_of_hypnat N)"
570 apply (simp add: starfunNat_real_of_nat [symmetric])
571 apply (rule STAR_sin_Infinitesimal)
572 apply (simp add: divide_inverse)
573 apply (rule Infinitesimal_HFinite_mult2)
574 apply (subst starfun_inverse)
575 apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
579 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
580 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
581 apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
582 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
583 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
584 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi
585 simp add: starfunNat_real_of_nat mult_commute divide_inverse)
588 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
589 apply (simp add: NSLIMSEQ_def, auto)
590 apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
591 apply (rule STAR_cos_Infinitesimal)
592 apply (auto intro!: Infinitesimal_HFinite_mult2
593 simp add: starfun_mult [symmetric] divide_inverse
594 starfun_inverse [symmetric] starfunNat_real_of_nat)
597 lemma NSLIMSEQ_sin_cos_pi:
598 "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
599 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
602 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
604 lemma STAR_cos_Infinitesimal_approx:
605 "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
606 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
607 apply (auto simp add: Infinitesimal_approx_minus [symmetric]
608 diff_minus add_assoc [symmetric] numeral_2_eq_2)
611 lemma STAR_cos_Infinitesimal_approx2:
612 "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
613 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
614 apply (auto intro: Infinitesimal_SReal_divide
615 simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)