# Theory HTranscendental

theory HTranscendental
imports HSeries HDeriv
```(*  Title       : HTranscendental.thy
Author      : Jacques D. Fleuriot
Copyright   : 2001 University of Edinburgh

Converted to Isar and polished by lcp
*)

section‹Nonstandard Extensions of Transcendental Functions›

theory HTranscendental
imports Transcendental HSeries HDeriv
begin

definition
exphr :: "real => hypreal" where
―‹define exponential function using standard part›
"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))"

definition
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"

lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"

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)

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"
apply (frule hypreal_sqrt_pow2_gt_zero)
done

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

lemma hypreal_sqrt_mult_distrib:
"!!x y. [|0 < x; 0 <y |] ==>
( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
apply transfer
apply (auto intro: real_sqrt_mult_distrib)
done

lemma hypreal_sqrt_mult_distrib2:
"[|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]
done

lemma hypreal_sqrt_approx_zero2 [simp]:
"0 ≤ x ==> (( *f* sqrt)(x) ≈ 0) = (x ≈ 0)"

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 (auto)
done

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 (auto)
done

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_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⇧2) = ¦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)

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

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

lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x ≤ ( *f* sqrt)(x⇧2 + y⇧2)"
by transfer (rule real_sqrt_sum_squares_ge1)

lemma HFinite_hypreal_sqrt:
"[| 0 ≤ x; x ∈ HFinite |] ==> ( *f* sqrt) x ∈ HFinite"
apply (rule HFinite_square_iff [THEN iffD1])
apply (drule hypreal_sqrt_gt_zero_pow2)
done

lemma HFinite_hypreal_sqrt_imp_HFinite:
"[| 0 ≤ x; ( *f* sqrt) x ∈ HFinite |] ==> x ∈ HFinite"
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

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 (auto)
done

lemma Infinitesimal_hypreal_sqrt:
"[| 0 ≤ x; x ∈ Infinitesimal |] ==> ( *f* sqrt) x ∈ Infinitesimal"
apply (rule Infinitesimal_square_iff [THEN iffD2])
apply (drule hypreal_sqrt_gt_zero_pow2)
done

lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
"[| 0 ≤ x; ( *f* sqrt) x ∈ Infinitesimal |] ==> x ∈ Infinitesimal"
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

lemma Infinitesimal_hypreal_sqrt_iff [simp]:
"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 (auto)
done

lemma HInfinite_hypreal_sqrt:
"[| 0 ≤ x; x ∈ HInfinite |] ==> ( *f* sqrt) x ∈ HInfinite"
apply (rule HInfinite_square_iff [THEN iffD1])
apply (drule hypreal_sqrt_gt_zero_pow2)
done

lemma HInfinite_hypreal_sqrt_imp_HInfinite:
"[| 0 ≤ x; ( *f* sqrt) x ∈ HInfinite |] ==> x ∈ HInfinite"
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

lemma HInfinite_hypreal_sqrt_iff [simp]:
"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 (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

lemma exphr_zero [simp]: "exphr 0 = 1"
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

lemma coshr_zero [simp]: "coshr 0 = 1"
[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

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

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]
apply (rule approx_sym [THEN [2] approx_trans2])
done

lemma STAR_exp_epsilon [simp]: "( *f* exp) ε ≈ 1"
by (auto intro: STAR_exp_Infinitesimal)

"!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"

lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
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

lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 ≤ x ==> (1 + x) ≤ ( *f* exp) x"

(* exp (oo) is infinite *)
lemma starfun_exp_HInfinite:
"[| x ∈ HInfinite; 0 ≤ x |] ==> ( *f* exp) (x::hypreal) ∈ HInfinite"
apply (rule HInfinite_ge_HInfinite, assumption)
apply (rule order_trans [of _ "1+x"], auto)
done

lemma starfun_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 *)
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
done

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_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_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_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
by transfer (rule ln_gt_zero)

lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x ≠ 1 |] ==> ( *f* real_ln) x ≠ 0"
by transfer simp

lemma starfun_ln_HFinite: "[| x ∈ HFinite; 1 ≤ x |] ==> ( *f* real_ln) x ∈ HFinite"
apply (rule HFinite_bounded)
apply assumption
done

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)

lemma starfun_exp_less_mono: "⋀x y::hypreal. x < y ⟹ ( *f* exp) x < ( *f* exp) y"
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)
done

"[|x ∈ Infinitesimal; z ∈ HFinite |] ==> ( *f* exp) (z + x::hypreal) ≈ ( *f* exp) z"
apply (frule STAR_exp_Infinitesimal)
apply (drule approx_mult2)
apply (auto intro: starfun_exp_HFinite)
done

(* 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

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

(* 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

(* 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

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)

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)

(*
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) ─0→⇩N⇩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]
done

lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
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]
done

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]
done

lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
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]
apply (rule approx_add_right_cancel [where d = "-1"])
apply simp
done

lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
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]
done

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])

lemma HFinite_pi: "hypreal_of_real pi ∈ HFinite"
by simp

(* lemmas *)

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)

(*------------------------------------------------------------------------*)
(* sin* (1/n) * 1/(1/n) ≈ 1 for n = oo                                   *)
(*------------------------------------------------------------------------*)

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)
done

lemma STAR_sin_inverse_HNatInfinite:
"n ∈ HNatInfinite
==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n ≈ 1"
apply (frule lemma_sin_pi)
done

lemma Infinitesimal_pi_divide_HNatInfinite:
"N ∈ HNatInfinite
==> hypreal_of_real pi/(hypreal_of_hypnat N) ∈ Infinitesimal"
apply (auto intro: Infinitesimal_HFinite_mult2)
done

lemma pi_divide_HNatInfinite_not_zero [simp]:
"N ∈ HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) ≠ 0"

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

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

lemma starfunNat_pi_divide_n_Infinitesimal:
"N ∈ HNatInfinite ==> ( *f* (%x. pi / real x)) N ∈ Infinitesimal"
by (auto intro!: Infinitesimal_HFinite_mult2
starfun_inverse [symmetric] 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 (rule STAR_sin_Infinitesimal)
apply (rule Infinitesimal_HFinite_mult2)
apply (subst starfun_inverse)
apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
apply simp
done

lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ⇢⇩N⇩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
done

lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))⇢⇩N⇩S 1"
apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
apply (rule STAR_cos_Infinitesimal)
apply (auto intro!: Infinitesimal_HFinite_mult2
starfun_inverse [symmetric] starfunNat_real_of_nat)
done

lemma NSLIMSEQ_sin_cos_pi:
"(%n. real n * sin (pi / real n) * cos (pi / real n)) ⇢⇩N⇩S pi"
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)

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⇧2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto simp add: Infinitesimal_approx_minus [symmetric]