# HG changeset patch # User paulson # Date 1556494614 -3600 # Node ID 2388e0d2827b44d5753fefb161485e480f369dcc # Parent 511352b4d5d32345fe88626830e090dfe23ce19c# Parent 1ececb77b27a5588a151bd0a9eff0809ae2bcf10 merged diff -r 511352b4d5d3 -r 2388e0d2827b src/HOL/Nonstandard_Analysis/HTranscendental.thy --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sun Apr 28 22:22:29 2019 +0200 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Mon Apr 29 00:36:54 2019 +0100 @@ -12,602 +12,524 @@ begin definition - exphr :: "real => hypreal" where + exphr :: "real \ hypreal" where \ \define exponential function using standard part\ - "exphr x = st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))" + "exphr x \ st(sumhr (0, whn, \n. inverse (fact n) * (x ^ n)))" definition - sinhr :: "real => hypreal" where - "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))" + sinhr :: "real \ hypreal" where + "sinhr x \ st(sumhr (0, whn, \n. sin_coeff n * x ^ n))" definition - coshr :: "real => hypreal" where - "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))" + coshr :: "real \ hypreal" where + "coshr x \ st(sumhr (0, whn, \n. cos_coeff n * x ^ n))" subsection\Nonstandard Extension of Square Root Function\ lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0" -by (simp add: starfun star_n_zero_num) + by (simp add: starfun star_n_zero_num) lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1" -by (simp add: starfun star_n_one_num) + by (simp add: starfun star_n_one_num) lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \ x)" -apply (cases x) -apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff - simp del: hpowr_Suc power_Suc) -done - -lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x" -by (transfer, simp) +proof (cases x) + case (star_n X) + then show ?thesis + by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc) +qed -lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2" -by (frule hypreal_sqrt_gt_zero_pow2, auto) +lemma hypreal_sqrt_gt_zero_pow2: "\x. 0 < x \ ( *f* sqrt) (x) ^ 2 = x" + by transfer simp -lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \ 0" -apply (frule hypreal_sqrt_pow2_gt_zero) -apply (auto simp add: numeral_2_eq_2) -done +lemma hypreal_sqrt_pow2_gt_zero: "0 < x \ 0 < ( *f* sqrt) (x) ^ 2" + by (frule hypreal_sqrt_gt_zero_pow2, auto) + +lemma hypreal_sqrt_not_zero: "0 < x \ ( *f* sqrt) (x) \ 0" + using hypreal_sqrt_gt_zero_pow2 by fastforce lemma hypreal_inverse_sqrt_pow2: - "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x" -apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric]) -apply (auto dest: hypreal_sqrt_gt_zero_pow2) -done + "0 < x \ inverse (( *f* sqrt)(x)) ^ 2 = inverse x" + by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse) lemma hypreal_sqrt_mult_distrib: - "!!x y. [|0 < x; 0 + "\x y. \0 < x; 0 \ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" -apply transfer -apply (auto intro: real_sqrt_mult) -done + by transfer (auto intro: real_sqrt_mult) lemma hypreal_sqrt_mult_distrib2: - "[|0\x; 0\y |] ==> - ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" + "\0\x; 0\y\ \ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less) lemma hypreal_sqrt_approx_zero [simp]: - "0 < x ==> (( *f* sqrt)(x) \ 0) = (x \ 0)" -apply (auto simp add: mem_infmal_iff [symmetric]) -apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst]) -apply (auto intro: Infinitesimal_mult - dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] - simp add: numeral_2_eq_2) -done + assumes "0 < x" + shows "(( *f* sqrt) x \ 0) \ (x \ 0)" +proof - + have "( *f* sqrt) x \ Infinitesimal \ ((*f* sqrt) x)\<^sup>2 \ Infinitesimal" + by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff) + also have "... \ x \ Infinitesimal" + by (simp add: assms hypreal_sqrt_gt_zero_pow2) + finally show ?thesis + using mem_infmal_iff by blast +qed lemma hypreal_sqrt_approx_zero2 [simp]: - "0 \ x ==> (( *f* sqrt)(x) \ 0) = (x \ 0)" -by (auto simp add: order_le_less) + "0 \ x \ (( *f* sqrt)(x) \ 0) = (x \ 0)" + by (auto simp add: order_le_less) -lemma hypreal_sqrt_sum_squares [simp]: - "(( *f* sqrt)(x*x + y*y + z*z) \ 0) = (x*x + y*y + z*z \ 0)" -apply (rule hypreal_sqrt_approx_zero2) -apply (rule add_nonneg_nonneg)+ -apply (auto) -done +lemma hypreal_sqrt_gt_zero: "\x. 0 < x \ 0 < ( *f* sqrt)(x)" + by transfer (simp add: real_sqrt_gt_zero) -lemma hypreal_sqrt_sum_squares2 [simp]: - "(( *f* sqrt)(x*x + y*y) \ 0) = (x*x + y*y \ 0)" -apply (rule hypreal_sqrt_approx_zero2) -apply (rule add_nonneg_nonneg) -apply (auto) -done +lemma hypreal_sqrt_ge_zero: "0 \ x \ 0 \ ( *f* sqrt)(x)" + by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) -lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)" -apply transfer -apply (auto intro: real_sqrt_gt_zero) -done +lemma hypreal_sqrt_hrabs [simp]: "\x. ( *f* sqrt)(x\<^sup>2) = \x\" + by transfer simp -lemma hypreal_sqrt_ge_zero: "0 \ x ==> 0 \ ( *f* sqrt)(x)" -by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) - -lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \x\" -by (transfer, simp) - -lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \x\" -by (transfer, simp) +lemma hypreal_sqrt_hrabs2 [simp]: "\x. ( *f* sqrt)(x*x) = \x\" + by transfer simp lemma hypreal_sqrt_hyperpow_hrabs [simp]: - "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \x\" -by (transfer, simp) + "\x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \x\" + by transfer simp lemma star_sqrt_HFinite: "\x \ HFinite; 0 \ x\ \ ( *f* sqrt) x \ HFinite" -apply (rule HFinite_square_iff [THEN iffD1]) -apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) -done + by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square) lemma st_hypreal_sqrt: - "[| x \ HFinite; 0 \ x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)" -apply (rule power_inject_base [where n=1]) -apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero) -apply (rule st_mult [THEN subst]) -apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst]) -apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst]) -apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite) -done + assumes "x \ HFinite" "0 \ x" + shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)" +proof (rule power_inject_base) + show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1" + using assms hypreal_sqrt_pow2_iff [of x] + by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult) + show "0 \ st ((*f* sqrt) x)" + by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite) + show "0 \ (*f* sqrt) (st x)" + by (simp add: assms hypreal_sqrt_ge_zero st_zero_le) +qed -lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \ ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)" -by transfer (rule real_sqrt_sum_squares_ge1) - -lemma HFinite_hypreal_sqrt: - "[| 0 \ x; x \ HFinite |] ==> ( *f* sqrt) x \ HFinite" -apply (auto simp add: order_le_less) -apply (rule HFinite_square_iff [THEN iffD1]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2) -done +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\x y. x \ ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)" + by transfer (rule real_sqrt_sum_squares_ge1) lemma HFinite_hypreal_sqrt_imp_HFinite: - "[| 0 \ x; ( *f* sqrt) x \ HFinite |] ==> x \ HFinite" -apply (auto simp add: order_le_less) -apply (drule HFinite_square_iff [THEN iffD2]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2 del: HFinite_square_iff) -done + "\0 \ x; ( *f* sqrt) x \ HFinite\ \ x \ HFinite" + by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2) lemma HFinite_hypreal_sqrt_iff [simp]: - "0 \ x ==> (( *f* sqrt) x \ HFinite) = (x \ HFinite)" -by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite) - -lemma HFinite_sqrt_sum_squares [simp]: - "(( *f* sqrt)(x*x + y*y) \ HFinite) = (x*x + y*y \ HFinite)" -apply (rule HFinite_hypreal_sqrt_iff) -apply (rule add_nonneg_nonneg) -apply (auto) -done + "0 \ x \ (( *f* sqrt) x \ HFinite) = (x \ HFinite)" + by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite) lemma Infinitesimal_hypreal_sqrt: - "[| 0 \ x; x \ Infinitesimal |] ==> ( *f* sqrt) x \ Infinitesimal" -apply (auto simp add: order_le_less) -apply (rule Infinitesimal_square_iff [THEN iffD2]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2) -done + "\0 \ x; x \ Infinitesimal\ \ ( *f* sqrt) x \ Infinitesimal" + by (simp add: mem_infmal_iff) lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal: - "[| 0 \ x; ( *f* sqrt) x \ Infinitesimal |] ==> x \ Infinitesimal" -apply (auto simp add: order_le_less) -apply (drule Infinitesimal_square_iff [THEN iffD1]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric]) -done + "\0 \ x; ( *f* sqrt) x \ Infinitesimal\ \ x \ Infinitesimal" + using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast lemma Infinitesimal_hypreal_sqrt_iff [simp]: - "0 \ x ==> (( *f* sqrt) x \ Infinitesimal) = (x \ Infinitesimal)" + "0 \ x \ (( *f* sqrt) x \ Infinitesimal) = (x \ Infinitesimal)" by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt) -lemma Infinitesimal_sqrt_sum_squares [simp]: - "(( *f* sqrt)(x*x + y*y) \ Infinitesimal) = (x*x + y*y \ Infinitesimal)" -apply (rule Infinitesimal_hypreal_sqrt_iff) -apply (rule add_nonneg_nonneg) -apply (auto) -done - lemma HInfinite_hypreal_sqrt: - "[| 0 \ x; x \ HInfinite |] ==> ( *f* sqrt) x \ HInfinite" -apply (auto simp add: order_le_less) -apply (rule HInfinite_square_iff [THEN iffD1]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2) -done + "\0 \ x; x \ HInfinite\ \ ( *f* sqrt) x \ HInfinite" + by (simp add: HInfinite_HFinite_iff) lemma HInfinite_hypreal_sqrt_imp_HInfinite: - "[| 0 \ x; ( *f* sqrt) x \ HInfinite |] ==> x \ HInfinite" -apply (auto simp add: order_le_less) -apply (drule HInfinite_square_iff [THEN iffD2]) -apply (drule hypreal_sqrt_gt_zero_pow2) -apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff) -done + "\0 \ x; ( *f* sqrt) x \ HInfinite\ \ x \ HInfinite" + using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast lemma HInfinite_hypreal_sqrt_iff [simp]: - "0 \ x ==> (( *f* sqrt) x \ HInfinite) = (x \ HInfinite)" + "0 \ x \ (( *f* sqrt) x \ HInfinite) = (x \ HInfinite)" by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite) -lemma HInfinite_sqrt_sum_squares [simp]: - "(( *f* sqrt)(x*x + y*y) \ HInfinite) = (x*x + y*y \ HInfinite)" -apply (rule HInfinite_hypreal_sqrt_iff) -apply (rule add_nonneg_nonneg) -apply (auto) -done - lemma HFinite_exp [simp]: - "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \ HFinite" -unfolding sumhr_app -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan) -apply (rule NSBseqD2) -apply (rule NSconvergent_NSBseq) -apply (rule convergent_NSconvergent_iff [THEN iffD1]) -apply (rule summable_iff_convergent [THEN iffD1]) -apply (rule summable_exp) -done + "sumhr (0, whn, \n. inverse (fact n) * x ^ n) \ HFinite" + unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan + by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp) lemma exphr_zero [simp]: "exphr 0 = 1" -apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric]) -apply (rule st_unique, simp) -apply (rule subst [where P="\x. 1 \ x", OF _ approx_refl]) -apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) -apply (rule_tac x="whn" in spec) -apply (unfold sumhr_app, transfer, simp add: power_0_left) -done +proof - + have "\x>1. 1 = sumhr (0, 1, \n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \n. inverse (fact n) * 0 ^ n)" + unfolding sumhr_app by transfer (simp add: power_0_left) + then have "sumhr (0, 1, \n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \n. inverse (fact n) * 0 ^ n) \ 1" + by auto + then show ?thesis + unfolding exphr_def + using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto +qed lemma coshr_zero [simp]: "coshr 0 = 1" -apply (simp add: coshr_def sumhr_split_add - [OF hypnat_one_less_hypnat_omega, symmetric]) -apply (rule st_unique, simp) -apply (rule subst [where P="\x. 1 \ x", OF _ approx_refl]) -apply (rule rev_mp [OF hypnat_one_less_hypnat_omega]) -apply (rule_tac x="whn" in spec) -apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left) -done + proof - + have "\x>1. 1 = sumhr (0, 1, \n. cos_coeff n * 0 ^ n) + sumhr (1, x, \n. cos_coeff n * 0 ^ n)" + unfolding sumhr_app by transfer (simp add: power_0_left) + then have "sumhr (0, 1, \n. cos_coeff n * 0 ^ n) + sumhr (1, whn, \n. cos_coeff n * 0 ^ n) \ 1" + by auto + then show ?thesis + unfolding coshr_def + using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto +qed lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \ 1" -apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp) -apply (transfer, simp) -done + proof - + have "(*f* exp) (0::real star) = 1" + by transfer simp + then show ?thesis + by auto +qed -lemma STAR_exp_Infinitesimal: "x \ Infinitesimal ==> ( *f* exp) (x::hypreal) \ 1" -apply (case_tac "x = 0") -apply (cut_tac [2] x = 0 in DERIV_exp) -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) -apply (drule_tac x = x in bspec, auto) -apply (drule_tac c = x in approx_mult1) -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult.assoc) -apply (rule approx_add_right_cancel [where d="-1"]) -apply (rule approx_sym [THEN [2] approx_trans2]) -apply (auto simp add: mem_infmal_iff) -done +lemma STAR_exp_Infinitesimal: + assumes "x \ Infinitesimal" shows "( *f* exp) (x::hypreal) \ 1" +proof (cases "x = 0") + case False + have "NSDERIV exp 0 :> 1" + by (metis DERIV_exp NSDERIV_DERIV_iff exp_zero) + then have "((*f* exp) x - 1) / x \ 1" + using nsderiv_def False NSDERIVD2 assms by fastforce + then have "(*f* exp) x - 1 \ x" + using NSDERIVD4 \NSDERIV exp 0 :> 1\ assms by fastforce + then show ?thesis + by (meson Infinitesimal_approx approx_minus_iff approx_trans2 assms not_Infinitesimal_not_zero) +qed auto lemma STAR_exp_epsilon [simp]: "( *f* exp) \ \ 1" -by (auto intro: STAR_exp_Infinitesimal) + by (auto intro: STAR_exp_Infinitesimal) lemma STAR_exp_add: - "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" -by transfer (rule exp_add) + "\(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" + by transfer (rule exp_add) lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" -apply (simp add: exphr_def) -apply (rule st_unique, simp) -apply (subst starfunNat_sumr [symmetric]) -unfolding atLeast0LessThan -apply (rule NSLIMSEQ_D [THEN approx_sym]) -apply (rule LIMSEQ_NSLIMSEQ) -apply (subst sums_def [symmetric]) -apply (cut_tac exp_converges [where x=x], simp) -apply (rule HNatInfinite_whn) -done +proof - + have "(\n. inverse (fact n) * x ^ n) sums exp x" + using exp_converges [of x] by simp + then have "(\n. \n\<^sub>N\<^sub>S exp x" + using NSsums_def sums_NSsums_iff by blast + then have "hypreal_of_real (exp x) \ sumhr (0, whn, \n. inverse (fact n) * x ^ n)" + unfolding starfunNat_sumr [symmetric] atLeast0LessThan + using HNatInfinite_whn NSLIMSEQ_iff approx_sym by blast + then show ?thesis + unfolding exphr_def using st_eq_approx_iff by auto +qed -lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \ x ==> (1 + x) \ ( *f* exp) x" -by transfer (rule exp_ge_add_one_self_aux) +lemma starfun_exp_ge_add_one_self [simp]: "\x::hypreal. 0 \ x \ (1 + x) \ ( *f* exp) x" + by transfer (rule exp_ge_add_one_self_aux) -(* exp (oo) is infinite *) +text\exp maps infinities to infinities\ lemma starfun_exp_HInfinite: - "[| x \ HInfinite; 0 \ x |] ==> ( *f* exp) (x::hypreal) \ HInfinite" -apply (frule starfun_exp_ge_add_one_self) -apply (rule HInfinite_ge_HInfinite, assumption) -apply (rule order_trans [of _ "1+x"], auto) -done + fixes x :: hypreal + assumes "x \ HInfinite" "0 \ x" + shows "( *f* exp) x \ HInfinite" +proof - + have "x \ 1 + x" + by simp + also have "\ \ (*f* exp) x" + by (simp add: \0 \ x\) + finally show ?thesis + using HInfinite_ge_HInfinite assms by blast +qed lemma starfun_exp_minus: - "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)" -by transfer (rule exp_minus) + "\x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)" + by transfer (rule exp_minus) -(* exp (-oo) is infinitesimal *) +text\exp maps infinitesimals to infinitesimals\ lemma starfun_exp_Infinitesimal: - "[| x \ HInfinite; x \ 0 |] ==> ( *f* exp) (x::hypreal) \ Infinitesimal" -apply (subgoal_tac "\y. x = - y") -apply (rule_tac [2] x = "- x" in exI) -apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite - simp add: starfun_exp_minus HInfinite_minus_iff) -done + fixes x :: hypreal + assumes "x \ HInfinite" "x \ 0" + shows "( *f* exp) x \ Infinitesimal" +proof - + obtain y where "x = -y" "y \ 0" + by (metis abs_of_nonpos assms(2) eq_abs_iff') + then have "( *f* exp) y \ HInfinite" + using HInfinite_minus_iff assms(1) starfun_exp_HInfinite by blast + then show ?thesis + by (simp add: HInfinite_inverse_Infinitesimal \x = - y\ starfun_exp_minus) +qed -lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x" -by transfer (rule exp_gt_one) +lemma starfun_exp_gt_one [simp]: "\x::hypreal. 0 < x \ 1 < ( *f* exp) x" + by transfer (rule exp_gt_one) abbreviation real_ln :: "real \ real" where "real_ln \ ln" -lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x" -by transfer (rule ln_exp) +lemma starfun_ln_exp [simp]: "\x. ( *f* real_ln) (( *f* exp) x) = x" + by transfer (rule ln_exp) -lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)" -by transfer (rule exp_ln_iff) +lemma starfun_exp_ln_iff [simp]: "\x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)" + by transfer (rule exp_ln_iff) -lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u" -by transfer (rule ln_unique) +lemma starfun_exp_ln_eq: "\u x. ( *f* exp) u = x \ ( *f* real_ln) x = u" + by transfer (rule ln_unique) -lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x" -by transfer (rule ln_less_self) - -lemma starfun_ln_ge_zero [simp]: "!!x. 1 \ x ==> 0 \ ( *f* real_ln) x" -by transfer (rule ln_ge_zero) +lemma starfun_ln_less_self [simp]: "\x. 0 < x \ ( *f* real_ln) x < x" + by transfer (rule ln_less_self) -lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x" -by transfer (rule ln_gt_zero) +lemma starfun_ln_ge_zero [simp]: "\x. 1 \ x \ 0 \ ( *f* real_ln) x" + by transfer (rule ln_ge_zero) -lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \ 1 |] ==> ( *f* real_ln) x \ 0" -by transfer simp +lemma starfun_ln_gt_zero [simp]: "\x .1 < x \ 0 < ( *f* real_ln) x" + by transfer (rule ln_gt_zero) -lemma starfun_ln_HFinite: "[| x \ HFinite; 1 \ x |] ==> ( *f* real_ln) x \ HFinite" -apply (rule HFinite_bounded) -apply assumption -apply (simp_all add: starfun_ln_less_self order_less_imp_le) -done +lemma starfun_ln_not_eq_zero [simp]: "\x. \0 < x; x \ 1\ \ ( *f* real_ln) x \ 0" + by transfer simp -lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x" -by transfer (rule ln_inverse) +lemma starfun_ln_HFinite: "\x \ HFinite; 1 \ x\ \ ( *f* real_ln) x \ HFinite" + by (metis HFinite_HInfinite_iff less_le_trans starfun_exp_HInfinite starfun_exp_ln_iff starfun_ln_ge_zero zero_less_one) + +lemma starfun_ln_inverse: "\x. 0 < x \ ( *f* real_ln) (inverse x) = -( *f* ln) x" + by transfer (rule ln_inverse) lemma starfun_abs_exp_cancel: "\x. \( *f* exp) (x::hypreal)\ = ( *f* exp) x" -by transfer (rule abs_exp_cancel) + by transfer (rule abs_exp_cancel) lemma starfun_exp_less_mono: "\x y::hypreal. x < y \ ( *f* exp) x < ( *f* exp) y" -by transfer (rule exp_less_mono) + by transfer (rule exp_less_mono) -lemma starfun_exp_HFinite: "x \ HFinite ==> ( *f* exp) (x::hypreal) \ HFinite" -apply (auto simp add: HFinite_def, rename_tac u) -apply (rule_tac x="( *f* exp) u" in rev_bexI) -apply (simp add: Reals_eq_Standard) -apply (simp add: starfun_abs_exp_cancel) -apply (simp add: starfun_exp_less_mono) -done +lemma starfun_exp_HFinite: + fixes x :: hypreal + assumes "x \ HFinite" + shows "( *f* exp) x \ HFinite" +proof - + obtain u where "u \ \" "\x\ < u" + using HFiniteD assms by force + with assms have "\(*f* exp) x\ < (*f* exp) u" + using starfun_abs_exp_cancel starfun_exp_less_mono by auto + with \u \ \\ show ?thesis + by (force simp: HFinite_def Reals_eq_Standard) +qed lemma starfun_exp_add_HFinite_Infinitesimal_approx: - "[|x \ Infinitesimal; z \ HFinite |] ==> ( *f* exp) (z + x::hypreal) \ ( *f* exp) z" -apply (simp add: STAR_exp_add) -apply (frule STAR_exp_Infinitesimal) -apply (drule approx_mult2) -apply (auto intro: starfun_exp_HFinite) -done + fixes x :: hypreal + shows "\x \ Infinitesimal; z \ HFinite\ \ ( *f* exp) (z + x::hypreal) \ ( *f* exp) z" + using STAR_exp_Infinitesimal approx_mult2 starfun_exp_HFinite by (fastforce simp add: STAR_exp_add) -(* using previous result to get to result *) lemma starfun_ln_HInfinite: - "[| x \ HInfinite; 0 < x |] ==> ( *f* real_ln) x \ HInfinite" -apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) -apply (drule starfun_exp_HFinite) -apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff) -done + "\x \ HInfinite; 0 < x\ \ ( *f* real_ln) x \ HInfinite" + by (metis HInfinite_HFinite_iff starfun_exp_HFinite starfun_exp_ln_iff) lemma starfun_exp_HInfinite_Infinitesimal_disj: - "x \ HInfinite \ ( *f* exp) x \ HInfinite \ ( *f* exp) (x::hypreal) \ Infinitesimal" -apply (insert linorder_linear [of x 0]) -apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal) -done + fixes x :: hypreal + shows "x \ HInfinite \ ( *f* exp) x \ HInfinite \ ( *f* exp) (x::hypreal) \ Infinitesimal" + by (meson linear starfun_exp_HInfinite starfun_exp_Infinitesimal) -(* check out this proof!!! *) lemma starfun_ln_HFinite_not_Infinitesimal: - "[| x \ HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \ HFinite" -apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2]) -apply (drule starfun_exp_HInfinite_Infinitesimal_disj) -apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff - del: starfun_exp_ln_iff) -done + "\x \ HFinite - Infinitesimal; 0 < x\ \ ( *f* real_ln) x \ HFinite" + by (metis DiffD1 DiffD2 HInfinite_HFinite_iff starfun_exp_HInfinite_Infinitesimal_disj starfun_exp_ln_iff) (* we do proof by considering ln of 1/x *) lemma starfun_ln_Infinitesimal_HInfinite: - "[| x \ Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \ HInfinite" -apply (drule Infinitesimal_inverse_HInfinite) -apply (frule positive_imp_inverse_positive) -apply (drule_tac [2] starfun_ln_HInfinite) -apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) -done + assumes "x \ Infinitesimal" "0 < x" + shows "( *f* real_ln) x \ HInfinite" +proof - + have "inverse x \ HInfinite" + using Infinitesimal_inverse_HInfinite assms by blast + then show ?thesis + using HInfinite_minus_iff assms(2) starfun_ln_HInfinite starfun_ln_inverse by fastforce +qed -lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0" -by transfer (rule ln_less_zero) +lemma starfun_ln_less_zero: "\x. \0 < x; x < 1\ \ ( *f* real_ln) x < 0" + by transfer (rule ln_less_zero) lemma starfun_ln_Infinitesimal_less_zero: - "[| x \ Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0" -by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) + "\x \ Infinitesimal; 0 < x\ \ ( *f* real_ln) x < 0" + by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) lemma starfun_ln_HInfinite_gt_zero: - "[| x \ HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x" -by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) + "\x \ HInfinite; 0 < x\ \ 0 < ( *f* real_ln) x" + by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) -(* -Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \0\\<^sub>N\<^sub>S ln x" -*) - -lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \ HFinite" -unfolding sumhr_app -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan) -apply (rule NSBseqD2) -apply (rule NSconvergent_NSBseq) -apply (rule convergent_NSconvergent_iff [THEN iffD1]) -apply (rule summable_iff_convergent [THEN iffD1]) -using summable_norm_sin [of x] -apply (simp add: summable_rabs_cancel) -done +lemma HFinite_sin [simp]: "sumhr (0, whn, \n. sin_coeff n * x ^ n) \ HFinite" +proof - + have "summable (\i. sin_coeff i * x ^ i)" + using summable_norm_sin [of x] by (simp add: summable_rabs_cancel) + then have "(*f* (\n. \n HFinite" + unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff + using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast + then show ?thesis + unfolding sumhr_app + by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) +qed lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" -by transfer (rule sin_zero) + by transfer (rule sin_zero) lemma STAR_sin_Infinitesimal [simp]: fixes x :: "'a::{real_normed_field,banach} star" - shows "x \ Infinitesimal ==> ( *f* sin) x \ x" -apply (case_tac "x = 0") -apply (cut_tac [2] x = 0 in DERIV_sin) -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) -apply (drule bspec [where x = x], auto) -apply (drule approx_mult1 [where c = x]) -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult.assoc) -done + assumes "x \ Infinitesimal" + shows "( *f* sin) x \ x" +proof (cases "x = 0") + case False + have "NSDERIV sin 0 :> 1" + by (metis DERIV_sin NSDERIV_DERIV_iff cos_zero) + then have "(*f* sin) x / x \ 1" + using False NSDERIVD2 assms by fastforce + with assms show ?thesis + unfolding star_one_def + by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) +qed auto -lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \ HFinite" -unfolding sumhr_app -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan) -apply (rule NSBseqD2) -apply (rule NSconvergent_NSBseq) -apply (rule convergent_NSconvergent_iff [THEN iffD1]) -apply (rule summable_iff_convergent [THEN iffD1]) -using summable_norm_cos [of x] -apply (simp add: summable_rabs_cancel) -done +lemma HFinite_cos [simp]: "sumhr (0, whn, \n. cos_coeff n * x ^ n) \ HFinite" +proof - + have "summable (\i. cos_coeff i * x ^ i)" + using summable_norm_cos [of x] by (simp add: summable_rabs_cancel) + then have "(*f* (\n. \n HFinite" + unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff + using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast + then show ?thesis + unfolding sumhr_app + by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) +qed lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" -by transfer (rule cos_zero) + by transfer (rule cos_zero) lemma STAR_cos_Infinitesimal [simp]: fixes x :: "'a::{real_normed_field,banach} star" - shows "x \ Infinitesimal ==> ( *f* cos) x \ 1" -apply (case_tac "x = 0") -apply (cut_tac [2] x = 0 in DERIV_cos) -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) -apply (drule bspec [where x = x]) -apply auto -apply (drule approx_mult1 [where c = x]) -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult.assoc) -apply (rule approx_add_right_cancel [where d = "-1"]) -apply simp -done + assumes "x \ Infinitesimal" + shows "( *f* cos) x \ 1" +proof (cases "x = 0") + case False + have "NSDERIV cos 0 :> 0" + by (metis DERIV_cos NSDERIV_DERIV_iff add.inverse_neutral sin_zero) + then have "(*f* cos) x - 1 \ 0" + using NSDERIV_approx assms by fastforce + with assms show ?thesis + using approx_minus_iff by blast +qed auto lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" -by transfer (rule tan_zero) + by transfer (rule tan_zero) -lemma STAR_tan_Infinitesimal: "x \ Infinitesimal ==> ( *f* tan) x \ x" -apply (case_tac "x = 0") -apply (cut_tac [2] x = 0 in DERIV_tan) -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) -apply (drule bspec [where x = x], auto) -apply (drule approx_mult1 [where c = x]) -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult.assoc) -done +lemma STAR_tan_Infinitesimal [simp]: + assumes "x \ Infinitesimal" + shows "( *f* tan) x \ x" +proof (cases "x = 0") + case False + have "NSDERIV tan 0 :> 1" + using DERIV_tan [of 0] by (simp add: NSDERIV_DERIV_iff) + then have "(*f* tan) x / x \ 1" + using False NSDERIVD2 assms by fastforce + with assms show ?thesis + unfolding star_one_def + by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) +qed auto lemma STAR_sin_cos_Infinitesimal_mult: fixes x :: "'a::{real_normed_field,banach} star" - shows "x \ Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \ x" -using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] -by (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) + shows "x \ Infinitesimal \ ( *f* sin) x * ( *f* cos) x \ x" + using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] + by (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) lemma HFinite_pi: "hypreal_of_real pi \ HFinite" -by simp - -(* lemmas *) + by simp -lemma lemma_split_hypreal_of_real: - "N \ HNatInfinite - ==> hypreal_of_real a = - hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)" -by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite) lemma STAR_sin_Infinitesimal_divide: fixes x :: "'a::{real_normed_field,banach} star" - shows "[|x \ Infinitesimal; x \ 0 |] ==> ( *f* sin) x/x \ 1" -using DERIV_sin [of "0::'a"] -by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) + shows "\x \ Infinitesimal; x \ 0\ \ ( *f* sin) x/x \ 1" + using DERIV_sin [of "0::'a"] + by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) -(*------------------------------------------------------------------------*) -(* sin* (1/n) * 1/(1/n) \ 1 for n = oo *) -(*------------------------------------------------------------------------*) +subsection \Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ \ lemma lemma_sin_pi: - "n \ HNatInfinite - ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \ 1" -apply (rule STAR_sin_Infinitesimal_divide) -apply (auto simp add: zero_less_HNatInfinite) -done + "n \ HNatInfinite + \ ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \ 1" + by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite) lemma STAR_sin_inverse_HNatInfinite: "n \ HNatInfinite - ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \ 1" -apply (frule lemma_sin_pi) -apply (simp add: divide_inverse) -done + \ ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \ 1" + by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi) lemma Infinitesimal_pi_divide_HNatInfinite: "N \ HNatInfinite - ==> hypreal_of_real pi/(hypreal_of_hypnat N) \ Infinitesimal" -apply (simp add: divide_inverse) -apply (auto intro: Infinitesimal_HFinite_mult2) -done + \ hypreal_of_real pi/(hypreal_of_hypnat N) \ Infinitesimal" + by (simp add: Infinitesimal_HFinite_mult2 field_class.field_divide_inverse) lemma pi_divide_HNatInfinite_not_zero [simp]: - "N \ HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \ 0" -by (simp add: zero_less_HNatInfinite) + "N \ HNatInfinite \ hypreal_of_real pi/(hypreal_of_hypnat N) \ 0" + by (simp add: zero_less_HNatInfinite) lemma STAR_sin_pi_divide_HNatInfinite_approx_pi: - "n \ HNatInfinite - ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n - \ hypreal_of_real pi" -apply (frule STAR_sin_Infinitesimal_divide - [OF Infinitesimal_pi_divide_HNatInfinite - pi_divide_HNatInfinite_not_zero]) -apply (auto) -apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) -apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps) -done + assumes "n \ HNatInfinite" + shows "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) * hypreal_of_hypnat n \ + hypreal_of_real pi" +proof - + have "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) / (hypreal_of_real pi / hypreal_of_hypnat n) \ 1" + using Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal_divide assms pi_divide_HNatInfinite_not_zero by blast + then have "hypreal_of_hypnat n * star_of sin \ (hypreal_of_real pi / hypreal_of_hypnat n) / hypreal_of_real pi \ 1" + by (simp add: mult.commute starfun_def) + then show ?thesis + apply (simp add: starfun_def field_simps) + 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) +qed lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: "n \ HNatInfinite - ==> hypreal_of_hypnat n * - ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) - \ hypreal_of_real pi" -apply (rule mult.commute [THEN subst]) -apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi) -done + \ hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \ hypreal_of_real pi" + by (metis STAR_sin_pi_divide_HNatInfinite_approx_pi mult.commute) lemma starfunNat_pi_divide_n_Infinitesimal: - "N \ HNatInfinite ==> ( *f* (%x. pi / real x)) N \ Infinitesimal" -by (auto intro!: Infinitesimal_HFinite_mult2 - simp add: starfun_mult [symmetric] divide_inverse - starfun_inverse [symmetric] starfunNat_real_of_nat) + "N \ HNatInfinite \ ( *f* (\x. pi / real x)) N \ Infinitesimal" + by (simp add: Infinitesimal_HFinite_mult2 divide_inverse starfunNat_real_of_nat) lemma STAR_sin_pi_divide_n_approx: - "N \ HNatInfinite ==> - ( *f* sin) (( *f* (%x. pi / real x)) N) \ - hypreal_of_real pi/(hypreal_of_hypnat N)" -apply (simp add: starfunNat_real_of_nat [symmetric]) -apply (rule STAR_sin_Infinitesimal) -apply (simp add: divide_inverse) -apply (rule Infinitesimal_HFinite_mult2) -apply (subst starfun_inverse) -apply (erule starfunNat_inverse_real_of_nat_Infinitesimal) -apply simp -done + assumes "N \ HNatInfinite" + shows "( *f* sin) (( *f* (\x. pi / real x)) N) \ hypreal_of_real pi/(hypreal_of_hypnat N)" +proof - + have "\s. (*f* sin) ((*f* (\n. pi / real n)) N) \ s \ hypreal_of_real pi / hypreal_of_hypnat N \ s" + by (metis (lifting) Infinitesimal_approx Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal assms starfunNat_pi_divide_n_Infinitesimal) + then show ?thesis + by (meson approx_trans2) +qed -lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \\<^sub>N\<^sub>S pi" -apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat) -apply (rule_tac f1 = sin in starfun_o2 [THEN subst]) -apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse) -apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) -apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi - simp add: starfunNat_real_of_nat mult.commute divide_inverse) -done +lemma NSLIMSEQ_sin_pi: "(\n. real n * sin (pi / real n)) \\<^sub>N\<^sub>S pi" +proof - + have *: "hypreal_of_hypnat N * (*f* sin) ((*f* (\x. pi / real x)) N) \ hypreal_of_real pi" + if "N \ HNatInfinite" + for N :: "nat star" + using that + by simp (metis STAR_sin_pi_divide_HNatInfinite_approx_pi2 starfunNat_real_of_nat) + show ?thesis + by (simp add: NSLIMSEQ_def starfunNat_real_of_nat) (metis * starfun_o2) +qed -lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\\<^sub>N\<^sub>S 1" -apply (simp add: NSLIMSEQ_def, auto) -apply (rule_tac f1 = cos in starfun_o2 [THEN subst]) -apply (rule STAR_cos_Infinitesimal) -apply (auto intro!: Infinitesimal_HFinite_mult2 - simp add: starfun_mult [symmetric] divide_inverse - starfun_inverse [symmetric] starfunNat_real_of_nat) -done +lemma NSLIMSEQ_cos_one: "(\n. cos (pi / real n))\\<^sub>N\<^sub>S 1" +proof - + have "(*f* cos) ((*f* (\x. pi / real x)) N) \ 1" + if "N \ HNatInfinite" for N + using that STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal by blast + then show ?thesis + by (simp add: NSLIMSEQ_def) (metis STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal starfun_o2) +qed lemma NSLIMSEQ_sin_cos_pi: - "(%n. real n * sin (pi / real n) * cos (pi / real n)) \\<^sub>N\<^sub>S pi" -by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp) + "(\n. real n * sin (pi / real n) * cos (pi / real n)) \\<^sub>N\<^sub>S pi" + using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force text\A familiar approximation to \<^term>\cos x\ when \<^term>\x\ is small\ lemma STAR_cos_Infinitesimal_approx: fixes x :: "'a::{real_normed_field,banach} star" - shows "x \ Infinitesimal ==> ( *f* cos) x \ 1 - x\<^sup>2" -apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) -apply (auto simp add: Infinitesimal_approx_minus [symmetric] - add.assoc [symmetric] numeral_2_eq_2) -done + shows "x \ Infinitesimal \ ( *f* cos) x \ 1 - x\<^sup>2" + by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square) lemma STAR_cos_Infinitesimal_approx2: fixes x :: hypreal \ \perhaps could be generalised, like many other hypreal results\ - shows "x \ Infinitesimal ==> ( *f* cos) x \ 1 - (x\<^sup>2)/2" -apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) -apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult - simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) -done + assumes "x \ Infinitesimal" + shows "( *f* cos) x \ 1 - (x\<^sup>2)/2" +proof - + have "1 \ 1 - x\<^sup>2 / 2" + using assms + by (auto intro: Infinitesimal_SReal_divide simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) + then show ?thesis + using STAR_cos_Infinitesimal approx_trans assms by blast +qed end