# Theory HTranscendental

Up to index of Isabelle/HOL/HOL-Complex

theory HTranscendental
imports Transcendental Integration
begin

    (*  Title       : HTranscendental.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 2001 University of Edinburgh

    Converted to Isar and polished by lcp
    *)

    header{*Nonstandard Extensions of Transcendental Functions*}

    theory HTranscendental
    imports Transcendental Integration
    begin

    text{*really belongs in Transcendental*}
    lemma sqrt_divide_self_eq:
      assumes nneg: "0 ≤ x"
      shows "sqrt x / x = inverse (sqrt x)"
    proof cases
      assume "x=0" thus ?thesis by simp
    next
      assume nz: "x≠0"
      hence pos: "0<x" using nneg by arith
      show ?thesis
      proof (rule right_inverse_eq [THEN iffD1, THEN sym])
        show "sqrt x / x ≠ 0" by (simp add: divide_inverse nneg nz)
        show "inverse (sqrt x) / (sqrt x / x) = 1"
          by (simp add: divide_inverse mult_assoc [symmetric]
                      power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
      qed
    qed

    constdefs

      exphr :: "real => hypreal"
        --{*define exponential function using standard part *}
        "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"

      sinhr :: "real => hypreal"
        "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
                 ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"

      coshr :: "real => hypreal"
        "coshr x == st(sumhr (0, whn, %n. (if even(n) then
                ((-1) ^ (n div 2))/(real (fact n)) else 0) * 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)

    lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    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 realpow_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)
    apply (auto simp add: numeral_2_eq_2)
    done

    lemma hypreal_inverse_sqrt_pow2:
         "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    apply (cut_tac n1 = 2 and a1 = "( *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]
                simp add: numeral_2_eq_2)
    done

    lemma hypreal_sqrt_approx_zero2 [simp]:
         "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 simp add: zero_le_square)
    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 (rule add_nonneg_nonneg)
    apply (auto simp add: zero_le_square)
    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) = abs(x)"
    by (transfer, simp)

    lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
    by (transfer, simp)

    lemma hypreal_sqrt_hyperpow_hrabs [simp]:
         "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(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, simp)

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

    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 simp add: zero_le_square)
    done

    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

    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

    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 (rule add_nonneg_nonneg)
    apply (auto simp add: zero_le_square)
    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

    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

    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 (rule add_nonneg_nonneg)
    apply (auto simp add: zero_le_square)
    done

    lemma HFinite_exp [simp]:
         "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) ∈ HFinite"
    by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
             simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
                       convergent_NSconvergent_iff [symmetric]
                       summable_convergent_sumr_iff [symmetric] 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 (simp add: sumhr star_n_zero_num starfun star_n_one_num star_n_add
                     hypnat_omega_def
                del: OrderedGroup.add_0)
    apply (simp add: star_n_one_num [symmetric])
    done

    lemma coshr_zero [simp]: "coshr 0 = 1"
    apply (simp add: coshr_def sumhr_split_add
                       [OF hypnat_one_less_hypnat_omega, symmetric])
    apply (simp add: sumhr star_n_zero_num star_n_one_num hypnat_omega_def)
    apply (simp add: star_n_one_num [symmetric] star_n_zero_num [symmetric])
    done

    lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
    by (simp add: star_n_zero_num star_n_one_num starfun)

    lemma STAR_exp_Infinitesimal: "x ∈ Infinitesimal ==> ( *f* exp) x @= 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_epsilon [simp]: "( *f* exp) epsilon @= 1"
    by (auto intro: STAR_exp_Infinitesimal)

    lemma STAR_exp_add: "!!x 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_hypreal_of_real [THEN subst])
    apply (rule approx_st_eq, auto)
    apply (rule approx_minus_iff [THEN iffD2])
    apply (simp only: mem_infmal_iff [symmetric])
    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)
    apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
    apply (insert exp_converges [of x])
    apply (simp add: sums_def)
    apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
    apply (simp add: LIMSEQ_NSLIMSEQ_iff)
    done

    lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 ≤ x ==> (1 + x) ≤ ( *f* exp) x"
    by (transfer, rule exp_ge_add_one_self_aux)

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

    lemma starfun_exp_minus: "!!x. ( *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 ∈ 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

    lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x"
    by (transfer, simp)

    (* needs derivative of inverse function
       TRY a NS one today!!!

    Goal "x @= 1 ==> ( *f* ln) x @= 1"
    by (res_inst_tac [("z","x")] eq_Abs_star 1);
    by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));

    Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";

    *)

    lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
    by (transfer, simp)

    lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
    by (transfer, simp)

    lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
    by auto

    lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
    by (transfer, simp)

    lemma starfun_ln_ge_zero [simp]: "!!x. 1 ≤ x ==> 0 ≤ ( *f* ln) x"
    by (transfer, simp)

    lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
    by (transfer, simp)

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

    lemma starfun_ln_HFinite: "[| x ∈ HFinite; 1 ≤ x |] ==> ( *f* 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_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
    by (transfer, rule ln_inverse)

    lemma starfun_exp_HFinite: "x ∈ HFinite ==> ( *f* exp) x ∈ HFinite"
    apply (cases x)
    apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n], auto)
    apply (rule_tac x = "exp u" in exI)
    apply (ultra, arith)
    done

    lemma starfun_exp_add_HFinite_Infinitesimal_approx:
         "[|x ∈ Infinitesimal; z ∈ HFinite |] ==> ( *f* exp) (z + x) @= ( *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

    (* using previous result to get to result *)
    lemma starfun_ln_HInfinite:
         "[| x ∈ HInfinite; 0 < x |] ==> ( *f* 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 ∈ 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* 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* 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* ln) x < 0"
    by (transfer, simp)

    lemma starfun_ln_Infinitesimal_less_zero:
         "[| x ∈ Infinitesimal; 0 < x |] ==> ( *f* 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* ln) x"
    by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)

    (*
    Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
    *)

    lemma HFinite_sin [simp]:
         "sumhr (0, whn, %n. (if even(n) then 0 else
                  ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
                  ∈ HFinite"
    apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
                simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
                          convergent_NSconvergent_iff [symmetric]
                          summable_convergent_sumr_iff [symmetric])
    apply (simp only: One_nat_def summable_sin)
    done

    lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
    by (transfer, simp)

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

    lemma HFinite_cos [simp]:
         "sumhr (0, whn, %n. (if even(n) then
                ((- 1) ^ (n div 2))/(real (fact n)) else
                0) * x ^ n) ∈ HFinite"
    by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
             simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
                       convergent_NSconvergent_iff [symmetric]
                       summable_convergent_sumr_iff [symmetric] summable_cos)

    lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
    by (simp add: starfun star_n_zero_num star_n_one_num)

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

    lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
    by (simp add: starfun star_n_zero_num)

    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_sin_cos_Infinitesimal_mult:
         "x ∈ Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
    apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1])
    apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
    done

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

    lemma STAR_sin_Infinitesimal_divide:
         "[|x ∈ Infinitesimal; x ≠ 0 |] ==> ( *f* sin) x/x @= 1"
    apply (cut_tac x = 0 in DERIV_sin)
    apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
    done

    (*------------------------------------------------------------------------*)
    (* 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)
    apply (auto simp add: HNatInfinite_not_eq_zero)
    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)
    apply (simp add: divide_inverse)
    done

    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

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

    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: SReal_inverse simp add: divide_inverse mult_ac)
    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
             simp add: starfun_mult [symmetric] divide_inverse
                       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 (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

    lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> 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_cos_one: "(%n. cos (pi / real n))----NS> 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_sin_cos_pi:
         "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> 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:
         "x ∈ Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
    apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
    apply (auto simp add: Infinitesimal_approx_minus [symmetric]
                diff_minus add_assoc [symmetric] numeral_2_eq_2)
    done

    lemma STAR_cos_Infinitesimal_approx2:
         "x ∈ Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
    apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
    apply (auto intro: Infinitesimal_SReal_divide
                simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
    done

    ML
    {*
    val STAR_sqrt_zero = thm "STAR_sqrt_zero";
    val STAR_sqrt_one = thm "STAR_sqrt_one";
    val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
    val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
    val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
    val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
    val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
    val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
    val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
    val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
    val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
    val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
    val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
    val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
    val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
    val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
    val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
    val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
    val star_sqrt_HFinite = thm "star_sqrt_HFinite";
    val st_hypreal_sqrt = thm "st_hypreal_sqrt";
    val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
    val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
    val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
    val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
    val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
    val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
    val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
    val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
    val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
    val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
    val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
    val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
    val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
    val HFinite_exp = thm "HFinite_exp";
    val exphr_zero = thm "exphr_zero";
    val coshr_zero = thm "coshr_zero";
    val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
    val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
    val STAR_exp_epsilon = thm "STAR_exp_epsilon";
    val STAR_exp_add = thm "STAR_exp_add";
    val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
    val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
    val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
    val starfun_exp_minus = thm "starfun_exp_minus";
    val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
    val starfun_exp_gt_one = thm "starfun_exp_gt_one";
    val starfun_ln_exp = thm "starfun_ln_exp";
    val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
    val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
    val starfun_ln_less_self = thm "starfun_ln_less_self";
    val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
    val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
    val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
    val starfun_ln_HFinite = thm "starfun_ln_HFinite";
    val starfun_ln_inverse = thm "starfun_ln_inverse";
    val starfun_exp_HFinite = thm "starfun_exp_HFinite";
    val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
    val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
    val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
    val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
    val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
    val starfun_ln_less_zero = thm "starfun_ln_less_zero";
    val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
    val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
    val HFinite_sin = thm "HFinite_sin";
    val STAR_sin_zero = thm "STAR_sin_zero";
    val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
    val HFinite_cos = thm "HFinite_cos";
    val STAR_cos_zero = thm "STAR_cos_zero";
    val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
    val STAR_tan_zero = thm "STAR_tan_zero";
    val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
    val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
    val HFinite_pi = thm "HFinite_pi";
    val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
    val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
    val lemma_sin_pi = thm "lemma_sin_pi";
    val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
    val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
    val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
    val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
    val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
    val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
    val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
    val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
    val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
    val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
    val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
    val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
    *}

    end

lemma sqrt_divide_self_eq:

      0 ≤ x ==> sqrt x / x = inverse (sqrt x)

### Nonstandard Extension of Square Root Function

lemma STAR_sqrt_zero:

      (*f* sqrt) 0 = 0

lemma STAR_sqrt_one:

      (*f* sqrt) 1 = 1

lemma hypreal_sqrt_pow2_iff:

      (((*f* sqrt) x)² = x) = (0 ≤ x)

lemma hypreal_sqrt_gt_zero_pow2:

      0 < x ==> ((*f* sqrt) x)² = x

lemma hypreal_sqrt_pow2_gt_zero:

      0 < x ==> 0 < ((*f* sqrt) x)²

lemma hypreal_sqrt_not_zero:

      0 < x ==> (*f* sqrt) x ≠ 0

lemma hypreal_inverse_sqrt_pow2:

      0 < x ==> (inverse ((*f* sqrt) x))² = inverse x

lemma hypreal_sqrt_mult_distrib:

      [| 0 < x; 0 < y |] ==> (*f* sqrt) (x * y) = (*f* sqrt) x * (*f* sqrt) y

lemma hypreal_sqrt_mult_distrib2:

      [| 0 ≤ x; 0 ≤ y |] ==> (*f* sqrt) (x * y) = (*f* sqrt) x * (*f* sqrt) y

lemma hypreal_sqrt_approx_zero:

      0 < x ==> ((*f* sqrt) x ≈ 0) = (x ≈ 0)

lemma hypreal_sqrt_approx_zero2:

      0 ≤ x ==> ((*f* sqrt) x ≈ 0) = (x ≈ 0)

lemma hypreal_sqrt_sum_squares:

      ((*f* sqrt) (x * x + y * y + z * z) ≈ 0) = (x * x + y * y + z * z ≈ 0)

lemma hypreal_sqrt_sum_squares2:

      ((*f* sqrt) (x * x + y * y) ≈ 0) = (x * x + y * y ≈ 0)

lemma hypreal_sqrt_gt_zero:

      0 < x ==> 0 < (*f* sqrt) x

lemma hypreal_sqrt_ge_zero:

      0 ≤ x ==> 0 ≤ (*f* sqrt) x

lemma hypreal_sqrt_hrabs:

      (*f* sqrt) (x²) = ¦x¦

lemma hypreal_sqrt_hrabs2:

      (*f* sqrt) (x * x) = ¦x¦

lemma hypreal_sqrt_hyperpow_hrabs:

      (*f* sqrt) (x pow star_of 2) = ¦x¦

lemma star_sqrt_HFinite:

      [| x ∈ HFinite; 0 ≤ x |] ==> (*f* sqrt) x ∈ HFinite

lemma st_hypreal_sqrt:

      [| x ∈ HFinite; 0 ≤ x |] ==> st ((*f* sqrt) x) = (*f* sqrt) (st x)

lemma hypreal_sqrt_sum_squares_ge1:

      x ≤ (*f* sqrt) (x² + y²)

lemma HFinite_hypreal_sqrt:

      [| 0 ≤ x; x ∈ HFinite |] ==> (*f* sqrt) x ∈ HFinite

lemma HFinite_hypreal_sqrt_imp_HFinite:

      [| 0 ≤ x; (*f* sqrt) x ∈ HFinite |] ==> x ∈ HFinite

lemma HFinite_hypreal_sqrt_iff:

      0 ≤ x ==> ((*f* sqrt) x ∈ HFinite) = (x ∈ HFinite)

lemma HFinite_sqrt_sum_squares:

      ((*f* sqrt) (x * x + y * y) ∈ HFinite) = (x * x + y * y ∈ HFinite)

lemma Infinitesimal_hypreal_sqrt:

      [| 0 ≤ x; x ∈ Infinitesimal |] ==> (*f* sqrt) x ∈ Infinitesimal

lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:

      [| 0 ≤ x; (*f* sqrt) x ∈ Infinitesimal |] ==> x ∈ Infinitesimal

lemma Infinitesimal_hypreal_sqrt_iff:

      0 ≤ x ==> ((*f* sqrt) x ∈ Infinitesimal) = (x ∈ Infinitesimal)

lemma Infinitesimal_sqrt_sum_squares:

      ((*f* sqrt) (x * x + y * y) ∈ Infinitesimal) = (x * x + y * y ∈ Infinitesimal)

lemma HInfinite_hypreal_sqrt:

      [| 0 ≤ x; x ∈ HInfinite |] ==> (*f* sqrt) x ∈ HInfinite

lemma HInfinite_hypreal_sqrt_imp_HInfinite:

      [| 0 ≤ x; (*f* sqrt) x ∈ HInfinite |] ==> x ∈ HInfinite

lemma HInfinite_hypreal_sqrt_iff:

      0 ≤ x ==> ((*f* sqrt) x ∈ HInfinite) = (x ∈ HInfinite)

lemma HInfinite_sqrt_sum_squares:

      ((*f* sqrt) (x * x + y * y) ∈ HInfinite) = (x * x + y * y ∈ HInfinite)

lemma HFinite_exp:

      sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) ∈ HFinite

lemma exphr_zero:

      exphr 0 = 1

lemma coshr_zero:

      coshr 0 = 1

lemma STAR_exp_zero_approx_one:

      (*f* exp) 0 ≈ 1

lemma STAR_exp_Infinitesimal:

      x ∈ Infinitesimal ==> (*f* exp) x ≈ 1

lemma STAR_exp_epsilon:

      (*f* exp) ε ≈ 1

lemma STAR_exp_add:

      (*f* exp) (x + y) = (*f* exp) x * (*f* exp) y

lemma exphr_hypreal_of_real_exp_eq:

      exphr x = star_of (exp x)

lemma starfun_exp_ge_add_one_self:

      0 ≤ x ==> 1 + x ≤ (*f* exp) x

lemma starfun_exp_HInfinite:

      [| x ∈ HInfinite; 0 ≤ x |] ==> (*f* exp) x ∈ HInfinite

lemma starfun_exp_minus:

      (*f* exp) (- x) = inverse ((*f* exp) x)

lemma starfun_exp_Infinitesimal:

      [| x ∈ HInfinite; x ≤ 0 |] ==> (*f* exp) x ∈ Infinitesimal

lemma starfun_exp_gt_one:

      0 < x ==> 1 < (*f* exp) x

lemma starfun_ln_exp:

      (*f* ln) ((*f* exp) x) = x

lemma starfun_exp_ln_iff:

      ((*f* exp) ((*f* ln) x) = x) = (0 < x)

lemma starfun_exp_ln_eq:

      (*f* exp) u = x ==> (*f* ln) x = u

lemma starfun_ln_less_self:

      0 < x ==> (*f* ln) x < x

lemma starfun_ln_ge_zero:

      1 ≤ x ==> 0 ≤ (*f* ln) x

lemma starfun_ln_gt_zero:

      1 < x ==> 0 < (*f* ln) x

lemma starfun_ln_not_eq_zero:

      [| 0 < x; x ≠ 1 |] ==> (*f* ln) x ≠ 0

lemma starfun_ln_HFinite:

      [| x ∈ HFinite; 1 ≤ x |] ==> (*f* ln) x ∈ HFinite

lemma starfun_ln_inverse:

      0 < x ==> (*f* ln) (inverse x) = - (*f* ln) x

lemma starfun_exp_HFinite:

      x ∈ HFinite ==> (*f* exp) x ∈ HFinite

lemma starfun_exp_add_HFinite_Infinitesimal_approx:

      [| x ∈ Infinitesimal; z ∈ HFinite |] ==> (*f* exp) (z + x) ≈ (*f* exp) z

lemma starfun_ln_HInfinite:

      [| x ∈ HInfinite; 0 < x |] ==> (*f* ln) x ∈ HInfinite

lemma starfun_exp_HInfinite_Infinitesimal_disj:

      x ∈ HInfinite ==> (*f* exp) x ∈ HInfinite ∨ (*f* exp) x ∈ Infinitesimal

lemma starfun_ln_HFinite_not_Infinitesimal:

      [| x ∈ HFinite - Infinitesimal; 0 < x |] ==> (*f* ln) x ∈ HFinite

lemma starfun_ln_Infinitesimal_HInfinite:

      [| x ∈ Infinitesimal; 0 < x |] ==> (*f* ln) x ∈ HInfinite

lemma starfun_ln_less_zero:

      [| 0 < x; x < 1 |] ==> (*f* ln) x < 0

lemma starfun_ln_Infinitesimal_less_zero:

      [| x ∈ Infinitesimal; 0 < x |] ==> (*f* ln) x < 0

lemma starfun_ln_HInfinite_gt_zero:

      [| x ∈ HInfinite; 0 < x |] ==> 0 < (*f* ln) x

lemma HFinite_sin:

      sumhr
       (0, whn,
        %n. (if even n then 0 else (- 1) ^ ((n - 1) div 2) / real (fact n)) * x ^ n)
      ∈ HFinite

lemma STAR_sin_zero:

      (*f* sin) 0 = 0

lemma STAR_sin_Infinitesimal:

      x ∈ Infinitesimal ==> (*f* sin) x ≈ x

lemma HFinite_cos:

      sumhr
       (0, whn, %n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) * x ^ n)
      ∈ HFinite

lemma STAR_cos_zero:

      (*f* cos) 0 = 1

lemma STAR_cos_Infinitesimal:

      x ∈ Infinitesimal ==> (*f* cos) x ≈ 1

lemma STAR_tan_zero:

      (*f* tan) 0 = 0

lemma STAR_tan_Infinitesimal:

      x ∈ Infinitesimal ==> (*f* tan) x ≈ x

lemma STAR_sin_cos_Infinitesimal_mult:

      x ∈ Infinitesimal ==> (*f* sin) x * (*f* cos) x ≈ x

lemma HFinite_pi:

      star_of pi ∈ HFinite

lemma lemma_split_hypreal_of_real:

      N ∈ HNatInfinite
      ==> star_of a =
          hypreal_of_hypnat N * (inverse (hypreal_of_hypnat N) * star_of a)

lemma STAR_sin_Infinitesimal_divide:

      [| x ∈ Infinitesimal; x ≠ 0 |] ==> (*f* sin) x / x ≈ 1

lemma lemma_sin_pi:

      n ∈ HNatInfinite
      ==> (*f* sin) (inverse (hypreal_of_hypnat n)) / inverse (hypreal_of_hypnat n) ≈
          1

lemma STAR_sin_inverse_HNatInfinite:

      n ∈ HNatInfinite
      ==> (*f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n ≈ 1

lemma Infinitesimal_pi_divide_HNatInfinite:

      N ∈ HNatInfinite ==> star_of pi / hypreal_of_hypnat N ∈ Infinitesimal

lemma pi_divide_HNatInfinite_not_zero:

      N ∈ HNatInfinite ==> star_of pi / hypreal_of_hypnat N ≠ 0

lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:

      n ∈ HNatInfinite
      ==> (*f* sin) (star_of pi / hypreal_of_hypnat n) * hypreal_of_hypnat n ≈
          star_of pi

lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:

      n ∈ HNatInfinite
      ==> hypreal_of_hypnat n * (*f* sin) (star_of pi / hypreal_of_hypnat n) ≈
          star_of pi

lemma starfunNat_pi_divide_n_Infinitesimal:

      N ∈ HNatInfinite ==> (*f* (%x. pi / real x)) N ∈ Infinitesimal

lemma STAR_sin_pi_divide_n_approx:

      N ∈ HNatInfinite
      ==> (*f* sin) ((*f* (%x. pi / real x)) N) ≈ star_of pi / hypreal_of_hypnat N

lemma NSLIMSEQ_sin_pi:

      (%n. real n * sin (pi / real n)) ----NS> pi

lemma NSLIMSEQ_cos_one:

      (%n. cos (pi / real n)) ----NS> 1

lemma NSLIMSEQ_sin_cos_pi:

      (%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi

lemma STAR_cos_Infinitesimal_approx:

      x ∈ Infinitesimal ==> (*f* cos) x ≈ 1 - x²

lemma STAR_cos_Infinitesimal_approx2:

      x ∈ Infinitesimal ==> (*f* cos) x ≈ 1 - x² / 2