1(* Title: HOL/Nonstandard_Analysis/HTranscendental.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 2001 University of Edinburgh 4 5Converted to Isar and polished by lcp 6*) 7 8section\<open>Nonstandard Extensions of Transcendental Functions\<close> 9 10theory HTranscendental 11imports Complex_Main HSeries HDeriv 12begin 13 14definition 15 exphr :: "real \<Rightarrow> hypreal" where 16 \<comment> \<open>define exponential function using standard part\<close> 17 "exphr x \<equiv> st(sumhr (0, whn, \<lambda>n. inverse (fact n) * (x ^ n)))" 18 19definition 20 sinhr :: "real \<Rightarrow> hypreal" where 21 "sinhr x \<equiv> st(sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n))" 22 23definition 24 coshr :: "real \<Rightarrow> hypreal" where 25 "coshr x \<equiv> st(sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n))" 26 27 28subsection\<open>Nonstandard Extension of Square Root Function\<close> 29 30lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0" 31 by (simp add: starfun star_n_zero_num) 32 33lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1" 34 by (simp add: starfun star_n_one_num) 35 36lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)" 37proof (cases x) 38 case (star_n X) 39 then show ?thesis 40 by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc) 41qed 42 43lemma hypreal_sqrt_gt_zero_pow2: "\<And>x. 0 < x \<Longrightarrow> ( *f* sqrt) (x) ^ 2 = x" 44 by transfer simp 45 46lemma hypreal_sqrt_pow2_gt_zero: "0 < x \<Longrightarrow> 0 < ( *f* sqrt) (x) ^ 2" 47 by (frule hypreal_sqrt_gt_zero_pow2, auto) 48 49lemma hypreal_sqrt_not_zero: "0 < x \<Longrightarrow> ( *f* sqrt) (x) \<noteq> 0" 50 using hypreal_sqrt_gt_zero_pow2 by fastforce 51 52lemma hypreal_inverse_sqrt_pow2: 53 "0 < x \<Longrightarrow> inverse (( *f* sqrt)(x)) ^ 2 = inverse x" 54 by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse) 55 56lemma hypreal_sqrt_mult_distrib: 57 "\<And>x y. \<lbrakk>0 < x; 0 <y\<rbrakk> \<Longrightarrow> 58 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" 59 by transfer (auto intro: real_sqrt_mult) 60 61lemma hypreal_sqrt_mult_distrib2: 62 "\<lbrakk>0\<le>x; 0\<le>y\<rbrakk> \<Longrightarrow> ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" 63by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less) 64 65lemma hypreal_sqrt_approx_zero [simp]: 66 assumes "0 < x" 67 shows "(( *f* sqrt) x \<approx> 0) \<longleftrightarrow> (x \<approx> 0)" 68proof - 69 have "( *f* sqrt) x \<in> Infinitesimal \<longleftrightarrow> ((*f* sqrt) x)\<^sup>2 \<in> Infinitesimal" 70 by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff) 71 also have "... \<longleftrightarrow> x \<in> Infinitesimal" 72 by (simp add: assms hypreal_sqrt_gt_zero_pow2) 73 finally show ?thesis 74 using mem_infmal_iff by blast 75qed 76 77lemma hypreal_sqrt_approx_zero2 [simp]: 78 "0 \<le> x \<Longrightarrow> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)" 79 by (auto simp add: order_le_less) 80 81lemma hypreal_sqrt_gt_zero: "\<And>x. 0 < x \<Longrightarrow> 0 < ( *f* sqrt)(x)" 82 by transfer (simp add: real_sqrt_gt_zero) 83 84lemma hypreal_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt)(x)" 85 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) 86 87lemma hypreal_sqrt_lessI: 88 "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u" 89proof transfer 90 show "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> sqrt x < u" 91 by (metis less_le real_sqrt_less_iff real_sqrt_pow2 real_sqrt_power) 92qed 93 94lemma hypreal_sqrt_hrabs [simp]: "\<And>x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>" 95 by transfer simp 96 97lemma hypreal_sqrt_hrabs2 [simp]: "\<And>x. ( *f* sqrt)(x*x) = \<bar>x\<bar>" 98 by transfer simp 99 100lemma hypreal_sqrt_hyperpow_hrabs [simp]: 101 "\<And>x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>" 102 by transfer simp 103 104lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite" 105 by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square) 106 107lemma st_hypreal_sqrt: 108 assumes "x \<in> HFinite" "0 \<le> x" 109 shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)" 110proof (rule power_inject_base) 111 show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1" 112 using assms hypreal_sqrt_pow2_iff [of x] 113 by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult) 114 show "0 \<le> st ((*f* sqrt) x)" 115 by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite) 116 show "0 \<le> (*f* sqrt) (st x)" 117 by (simp add: assms hypreal_sqrt_ge_zero st_zero_le) 118qed 119 120lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\<And>x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)" 121 by transfer (rule real_sqrt_sum_squares_ge1) 122 123lemma HFinite_hypreal_sqrt_imp_HFinite: 124 "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HFinite\<rbrakk> \<Longrightarrow> x \<in> HFinite" 125 by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2) 126 127lemma HFinite_hypreal_sqrt_iff [simp]: 128 "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)" 129 by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite) 130 131lemma Infinitesimal_hypreal_sqrt: 132 "\<lbrakk>0 \<le> x; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal" 133 by (simp add: mem_infmal_iff) 134 135lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal: 136 "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal" 137 using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast 138 139lemma Infinitesimal_hypreal_sqrt_iff [simp]: 140 "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)" 141by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt) 142 143lemma HInfinite_hypreal_sqrt: 144 "\<lbrakk>0 \<le> x; x \<in> HInfinite\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HInfinite" 145 by (simp add: HInfinite_HFinite_iff) 146 147lemma HInfinite_hypreal_sqrt_imp_HInfinite: 148 "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HInfinite\<rbrakk> \<Longrightarrow> x \<in> HInfinite" 149 using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast 150 151lemma HInfinite_hypreal_sqrt_iff [simp]: 152 "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)" 153by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite) 154 155lemma HFinite_exp [simp]: 156 "sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n) \<in> HFinite" 157 unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan 158 by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp) 159 160lemma exphr_zero [simp]: "exphr 0 = 1" 161proof - 162 have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \<lambda>n. inverse (fact n) * 0 ^ n)" 163 unfolding sumhr_app by transfer (simp add: power_0_left) 164 then have "sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \<lambda>n. inverse (fact n) * 0 ^ n) \<approx> 1" 165 by auto 166 then show ?thesis 167 unfolding exphr_def 168 using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto 169qed 170 171lemma coshr_zero [simp]: "coshr 0 = 1" 172 proof - 173 have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, x, \<lambda>n. cos_coeff n * 0 ^ n)" 174 unfolding sumhr_app by transfer (simp add: power_0_left) 175 then have "sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, whn, \<lambda>n. cos_coeff n * 0 ^ n) \<approx> 1" 176 by auto 177 then show ?thesis 178 unfolding coshr_def 179 using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto 180qed 181 182lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1" 183 proof - 184 have "(*f* exp) (0::real star) = 1" 185 by transfer simp 186 then show ?thesis 187 by auto 188qed 189 190lemma STAR_exp_Infinitesimal: 191 assumes "x \<in> Infinitesimal" shows "( *f* exp) (x::hypreal) \<approx> 1" 192proof (cases "x = 0") 193 case False 194 have "NSDERIV exp 0 :> 1" 195 by (metis DERIV_exp NSDERIV_DERIV_iff exp_zero) 196 then have "((*f* exp) x - 1) / x \<approx> 1" 197 using nsderiv_def False NSDERIVD2 assms by fastforce 198 then have "(*f* exp) x - 1 \<approx> x" 199 using NSDERIVD4 \<open>NSDERIV exp 0 :> 1\<close> assms by fastforce 200 then show ?thesis 201 by (meson Infinitesimal_approx approx_minus_iff approx_trans2 assms not_Infinitesimal_not_zero) 202qed auto 203 204lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1" 205 by (auto intro: STAR_exp_Infinitesimal) 206 207lemma STAR_exp_add: 208 "\<And>(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" 209 by transfer (rule exp_add) 210 211lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" 212proof - 213 have "(\<lambda>n. inverse (fact n) * x ^ n) sums exp x" 214 using exp_converges [of x] by simp 215 then have "(\<lambda>n. \<Sum>n<n. inverse (fact n) * x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S exp x" 216 using NSsums_def sums_NSsums_iff by blast 217 then have "hypreal_of_real (exp x) \<approx> sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n)" 218 unfolding starfunNat_sumr [symmetric] atLeast0LessThan 219 using HNatInfinite_whn NSLIMSEQ_def approx_sym by blast 220 then show ?thesis 221 unfolding exphr_def using st_eq_approx_iff by auto 222qed 223 224lemma starfun_exp_ge_add_one_self [simp]: "\<And>x::hypreal. 0 \<le> x \<Longrightarrow> (1 + x) \<le> ( *f* exp) x" 225 by transfer (rule exp_ge_add_one_self_aux) 226 227text\<open>exp maps infinities to infinities\<close> 228lemma starfun_exp_HInfinite: 229 fixes x :: hypreal 230 assumes "x \<in> HInfinite" "0 \<le> x" 231 shows "( *f* exp) x \<in> HInfinite" 232proof - 233 have "x \<le> 1 + x" 234 by simp 235 also have "\<dots> \<le> (*f* exp) x" 236 by (simp add: \<open>0 \<le> x\<close>) 237 finally show ?thesis 238 using HInfinite_ge_HInfinite assms by blast 239qed 240 241lemma starfun_exp_minus: 242 "\<And>x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)" 243 by transfer (rule exp_minus) 244 245text\<open>exp maps infinitesimals to infinitesimals\<close> 246lemma starfun_exp_Infinitesimal: 247 fixes x :: hypreal 248 assumes "x \<in> HInfinite" "x \<le> 0" 249 shows "( *f* exp) x \<in> Infinitesimal" 250proof - 251 obtain y where "x = -y" "y \<ge> 0" 252 by (metis abs_of_nonpos assms(2) eq_abs_iff') 253 then have "( *f* exp) y \<in> HInfinite" 254 using HInfinite_minus_iff assms(1) starfun_exp_HInfinite by blast 255 then show ?thesis 256 by (simp add: HInfinite_inverse_Infinitesimal \<open>x = - y\<close> starfun_exp_minus) 257qed 258 259lemma starfun_exp_gt_one [simp]: "\<And>x::hypreal. 0 < x \<Longrightarrow> 1 < ( *f* exp) x" 260 by transfer (rule exp_gt_one) 261 262abbreviation real_ln :: "real \<Rightarrow> real" where 263 "real_ln \<equiv> ln" 264 265lemma starfun_ln_exp [simp]: "\<And>x. ( *f* real_ln) (( *f* exp) x) = x" 266 by transfer (rule ln_exp) 267 268lemma starfun_exp_ln_iff [simp]: "\<And>x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)" 269 by transfer (rule exp_ln_iff) 270 271lemma starfun_exp_ln_eq: "\<And>u x. ( *f* exp) u = x \<Longrightarrow> ( *f* real_ln) x = u" 272 by transfer (rule ln_unique) 273 274lemma starfun_ln_less_self [simp]: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) x < x" 275 by transfer (rule ln_less_self) 276 277lemma starfun_ln_ge_zero [simp]: "\<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ( *f* real_ln) x" 278 by transfer (rule ln_ge_zero) 279 280lemma starfun_ln_gt_zero [simp]: "\<And>x .1 < x \<Longrightarrow> 0 < ( *f* real_ln) x" 281 by transfer (rule ln_gt_zero) 282 283lemma starfun_ln_not_eq_zero [simp]: "\<And>x. \<lbrakk>0 < x; x \<noteq> 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<noteq> 0" 284 by transfer simp 285 286lemma starfun_ln_HFinite: "\<lbrakk>x \<in> HFinite; 1 \<le> x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite" 287 by (metis HFinite_HInfinite_iff less_le_trans starfun_exp_HInfinite starfun_exp_ln_iff starfun_ln_ge_zero zero_less_one) 288 289lemma starfun_ln_inverse: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) (inverse x) = -( *f* ln) x" 290 by transfer (rule ln_inverse) 291 292lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x" 293 by transfer (rule abs_exp_cancel) 294 295lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y" 296 by transfer (rule exp_less_mono) 297 298lemma starfun_exp_HFinite: 299 fixes x :: hypreal 300 assumes "x \<in> HFinite" 301 shows "( *f* exp) x \<in> HFinite" 302proof - 303 obtain u where "u \<in> \<real>" "\<bar>x\<bar> < u" 304 using HFiniteD assms by force 305 with assms have "\<bar>(*f* exp) x\<bar> < (*f* exp) u" 306 using starfun_abs_exp_cancel starfun_exp_less_mono by auto 307 with \<open>u \<in> \<real>\<close> show ?thesis 308 by (force simp: HFinite_def Reals_eq_Standard) 309qed 310 311lemma starfun_exp_add_HFinite_Infinitesimal_approx: 312 fixes x :: hypreal 313 shows "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z" 314 using STAR_exp_Infinitesimal approx_mult2 starfun_exp_HFinite by (fastforce simp add: STAR_exp_add) 315 316lemma starfun_ln_HInfinite: 317 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite" 318 by (metis HInfinite_HFinite_iff starfun_exp_HFinite starfun_exp_ln_iff) 319 320lemma starfun_exp_HInfinite_Infinitesimal_disj: 321 fixes x :: hypreal 322 shows "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal" 323 by (meson linear starfun_exp_HInfinite starfun_exp_Infinitesimal) 324 325lemma starfun_ln_HFinite_not_Infinitesimal: 326 "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite" 327 by (metis DiffD1 DiffD2 HInfinite_HFinite_iff starfun_exp_HInfinite_Infinitesimal_disj starfun_exp_ln_iff) 328 329(* we do proof by considering ln of 1/x *) 330lemma starfun_ln_Infinitesimal_HInfinite: 331 assumes "x \<in> Infinitesimal" "0 < x" 332 shows "( *f* real_ln) x \<in> HInfinite" 333proof - 334 have "inverse x \<in> HInfinite" 335 using Infinitesimal_inverse_HInfinite assms by blast 336 then show ?thesis 337 using HInfinite_minus_iff assms(2) starfun_ln_HInfinite starfun_ln_inverse by fastforce 338qed 339 340lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" 341 by transfer (rule ln_less_zero) 342 343lemma starfun_ln_Infinitesimal_less_zero: 344 "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" 345 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) 346 347lemma starfun_ln_HInfinite_gt_zero: 348 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x" 349 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) 350 351 352lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite" 353proof - 354 have "summable (\<lambda>i. sin_coeff i * x ^ i)" 355 using summable_norm_sin [of x] by (simp add: summable_rabs_cancel) 356 then have "(*f* (\<lambda>n. \<Sum>n<n. sin_coeff n * x ^ n)) whn \<in> HFinite" 357 unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def 358 using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast 359 then show ?thesis 360 unfolding sumhr_app 361 by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) 362qed 363 364lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" 365 by transfer (rule sin_zero) 366 367lemma STAR_sin_Infinitesimal [simp]: 368 fixes x :: "'a::{real_normed_field,banach} star" 369 assumes "x \<in> Infinitesimal" 370 shows "( *f* sin) x \<approx> x" 371proof (cases "x = 0") 372 case False 373 have "NSDERIV sin 0 :> 1" 374 by (metis DERIV_sin NSDERIV_DERIV_iff cos_zero) 375 then have "(*f* sin) x / x \<approx> 1" 376 using False NSDERIVD2 assms by fastforce 377 with assms show ?thesis 378 unfolding star_one_def 379 by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) 380qed auto 381 382lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite" 383proof - 384 have "summable (\<lambda>i. cos_coeff i * x ^ i)" 385 using summable_norm_cos [of x] by (simp add: summable_rabs_cancel) 386 then have "(*f* (\<lambda>n. \<Sum>n<n. cos_coeff n * x ^ n)) whn \<in> HFinite" 387 unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def 388 using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast 389 then show ?thesis 390 unfolding sumhr_app 391 by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) 392qed 393 394lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" 395 by transfer (rule cos_zero) 396 397lemma STAR_cos_Infinitesimal [simp]: 398 fixes x :: "'a::{real_normed_field,banach} star" 399 assumes "x \<in> Infinitesimal" 400 shows "( *f* cos) x \<approx> 1" 401proof (cases "x = 0") 402 case False 403 have "NSDERIV cos 0 :> 0" 404 by (metis DERIV_cos NSDERIV_DERIV_iff add.inverse_neutral sin_zero) 405 then have "(*f* cos) x - 1 \<approx> 0" 406 using NSDERIV_approx assms by fastforce 407 with assms show ?thesis 408 using approx_minus_iff by blast 409qed auto 410 411lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" 412 by transfer (rule tan_zero) 413 414lemma STAR_tan_Infinitesimal [simp]: 415 assumes "x \<in> Infinitesimal" 416 shows "( *f* tan) x \<approx> x" 417proof (cases "x = 0") 418 case False 419 have "NSDERIV tan 0 :> 1" 420 using DERIV_tan [of 0] by (simp add: NSDERIV_DERIV_iff) 421 then have "(*f* tan) x / x \<approx> 1" 422 using False NSDERIVD2 assms by fastforce 423 with assms show ?thesis 424 unfolding star_one_def 425 by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) 426qed auto 427 428lemma STAR_sin_cos_Infinitesimal_mult: 429 fixes x :: "'a::{real_normed_field,banach} star" 430 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x" 431 using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 432 by (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) 433 434lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite" 435 by simp 436 437 438lemma STAR_sin_Infinitesimal_divide: 439 fixes x :: "'a::{real_normed_field,banach} star" 440 shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1" 441 using DERIV_sin [of "0::'a"] 442 by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) 443 444subsection \<open>Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ \<close> 445 446lemma lemma_sin_pi: 447 "n \<in> HNatInfinite 448 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1" 449 by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite) 450 451lemma STAR_sin_inverse_HNatInfinite: 452 "n \<in> HNatInfinite 453 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1" 454 by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi) 455 456lemma Infinitesimal_pi_divide_HNatInfinite: 457 "N \<in> HNatInfinite 458 \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal" 459 by (simp add: Infinitesimal_HFinite_mult2 field_class.field_divide_inverse) 460 461lemma pi_divide_HNatInfinite_not_zero [simp]: 462 "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0" 463 by (simp add: zero_less_HNatInfinite) 464 465lemma STAR_sin_pi_divide_HNatInfinite_approx_pi: 466 assumes "n \<in> HNatInfinite" 467 shows "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) * hypreal_of_hypnat n \<approx> 468 hypreal_of_real pi" 469proof - 470 have "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) / (hypreal_of_real pi / hypreal_of_hypnat n) \<approx> 1" 471 using Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal_divide assms pi_divide_HNatInfinite_not_zero by blast 472 then have "hypreal_of_hypnat n * star_of sin \<star> (hypreal_of_real pi / hypreal_of_hypnat n) / hypreal_of_real pi \<approx> 1" 473 by (simp add: mult.commute starfun_def) 474 then show ?thesis 475 apply (simp add: starfun_def field_simps) 476 by (metis (no_types, lifting) approx_mult_subst_star_of approx_refl mult_cancel_right1 nonzero_eq_divide_eq pi_neq_zero star_of_eq_0) 477qed 478 479lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: 480 "n \<in> HNatInfinite 481 \<Longrightarrow> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \<approx> hypreal_of_real pi" 482 by (metis STAR_sin_pi_divide_HNatInfinite_approx_pi mult.commute) 483 484lemma starfunNat_pi_divide_n_Infinitesimal: 485 "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal" 486 by (simp add: Infinitesimal_HFinite_mult2 divide_inverse starfunNat_real_of_nat) 487 488lemma STAR_sin_pi_divide_n_approx: 489 assumes "N \<in> HNatInfinite" 490 shows "( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi/(hypreal_of_hypnat N)" 491proof - 492 have "\<exists>s. (*f* sin) ((*f* (\<lambda>n. pi / real n)) N) \<approx> s \<and> hypreal_of_real pi / hypreal_of_hypnat N \<approx> s" 493 by (metis (lifting) Infinitesimal_approx Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal assms starfunNat_pi_divide_n_Infinitesimal) 494 then show ?thesis 495 by (meson approx_trans2) 496qed 497 498lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" 499proof - 500 have *: "hypreal_of_hypnat N * (*f* sin) ((*f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi" 501 if "N \<in> HNatInfinite" 502 for N :: "nat star" 503 using that 504 by simp (metis STAR_sin_pi_divide_HNatInfinite_approx_pi2 starfunNat_real_of_nat) 505 show ?thesis 506 by (simp add: NSLIMSEQ_def starfunNat_real_of_nat) (metis * starfun_o2) 507qed 508 509lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1" 510proof - 511 have "(*f* cos) ((*f* (\<lambda>x. pi / real x)) N) \<approx> 1" 512 if "N \<in> HNatInfinite" for N 513 using that STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal by blast 514 then show ?thesis 515 by (simp add: NSLIMSEQ_def) (metis STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal starfun_o2) 516qed 517 518lemma NSLIMSEQ_sin_cos_pi: 519 "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" 520 using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force 521 522 523text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close> 524 525lemma STAR_cos_Infinitesimal_approx: 526 fixes x :: "'a::{real_normed_field,banach} star" 527 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2" 528 by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square) 529 530lemma STAR_cos_Infinitesimal_approx2: 531 fixes x :: hypreal 532 assumes "x \<in> Infinitesimal" 533 shows "( *f* cos) x \<approx> 1 - (x\<^sup>2)/2" 534proof - 535 have "1 \<approx> 1 - x\<^sup>2 / 2" 536 using assms 537 by (auto intro: Infinitesimal_SReal_divide simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) 538 then show ?thesis 539 using STAR_cos_Infinitesimal approx_trans assms by blast 540qed 541 542end 543