src/HOL/Hyperreal/HTranscendental.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 15229 1eb23f805c06 permissions -rw-r--r--
import -> imports
```     1 (*  Title       : HTranscendental.thy
```
```     2     Author      : Jacques D. Fleuriot
```
```     3     Copyright   : 2001 University of Edinburgh
```
```     4
```
```     5 Converted to Isar and polished by lcp
```
```     6 *)
```
```     7
```
```     8 header{*Nonstandard Extensions of Transcendental Functions*}
```
```     9
```
```    10 theory HTranscendental
```
```    11 imports Transcendental Integration
```
```    12 begin
```
```    13
```
```    14 text{*really belongs in Transcendental*}
```
```    15 lemma sqrt_divide_self_eq:
```
```    16   assumes nneg: "0 \<le> x"
```
```    17   shows "sqrt x / x = inverse (sqrt x)"
```
```    18 proof cases
```
```    19   assume "x=0" thus ?thesis by simp
```
```    20 next
```
```    21   assume nz: "x\<noteq>0"
```
```    22   hence pos: "0<x" using nneg by arith
```
```    23   show ?thesis
```
```    24   proof (rule right_inverse_eq [THEN iffD1, THEN sym])
```
```    25     show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz)
```
```    26     show "inverse (sqrt x) / (sqrt x / x) = 1"
```
```    27       by (simp add: divide_inverse mult_assoc [symmetric]
```
```    28                   power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
```
```    29   qed
```
```    30 qed
```
```    31
```
```    32
```
```    33 constdefs
```
```    34
```
```    35   exphr :: "real => hypreal"
```
```    36     --{*define exponential function using standard part *}
```
```    37     "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
```
```    38
```
```    39   sinhr :: "real => hypreal"
```
```    40     "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
```
```    41              ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
```
```    42
```
```    43   coshr :: "real => hypreal"
```
```    44     "coshr x == st(sumhr (0, whn, %n. (if even(n) then
```
```    45             ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
```
```    46
```
```    47
```
```    48 subsection{*Nonstandard Extension of Square Root Function*}
```
```    49
```
```    50 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
```
```    51 by (simp add: starfun hypreal_zero_num)
```
```    52
```
```    53 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
```
```    54 by (simp add: starfun hypreal_one_num)
```
```    55
```
```    56 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
```
```    57 apply (cases x)
```
```    58 apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow
```
```    59                       real_sqrt_pow2_iff
```
```    60             simp del: hpowr_Suc realpow_Suc)
```
```    61 done
```
```    62
```
```    63 lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
```
```    64 apply (cases x)
```
```    65 apply (auto intro: FreeUltrafilterNat_subset
```
```    66             simp add: hypreal_less starfun hrealpow hypreal_zero_num
```
```    67             simp del: hpowr_Suc realpow_Suc)
```
```    68 done
```
```    69
```
```    70 lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
```
```    71 by (frule hypreal_sqrt_gt_zero_pow2, auto)
```
```    72
```
```    73 lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
```
```    74 apply (frule hypreal_sqrt_pow2_gt_zero)
```
```    75 apply (auto simp add: numeral_2_eq_2)
```
```    76 done
```
```    77
```
```    78 lemma hypreal_inverse_sqrt_pow2:
```
```    79      "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
```
```    80 apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
```
```    81 apply (auto dest: hypreal_sqrt_gt_zero_pow2)
```
```    82 done
```
```    83
```
```    84 lemma hypreal_sqrt_mult_distrib:
```
```    85     "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
```
```    86 apply (cases x, cases y)
```
```    87 apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
```
```    88 apply (auto intro: real_sqrt_mult_distrib)
```
```    89 done
```
```    90
```
```    91 lemma hypreal_sqrt_mult_distrib2:
```
```    92      "[|0\<le>x; 0\<le>y |] ==>
```
```    93      ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
```
```    94 by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
```
```    95
```
```    96 lemma hypreal_sqrt_approx_zero [simp]:
```
```    97      "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
```
```    98 apply (auto simp add: mem_infmal_iff [symmetric])
```
```    99 apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
```
```   100 apply (auto intro: Infinitesimal_mult
```
```   101             dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst]
```
```   102             simp add: numeral_2_eq_2)
```
```   103 done
```
```   104
```
```   105 lemma hypreal_sqrt_approx_zero2 [simp]:
```
```   106      "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
```
```   107 by (auto simp add: order_le_less)
```
```   108
```
```   109 lemma hypreal_sqrt_sum_squares [simp]:
```
```   110      "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
```
```   111 apply (rule hypreal_sqrt_approx_zero2)
```
```   112 apply (rule hypreal_le_add_order)+
```
```   113 apply (auto simp add: zero_le_square)
```
```   114 done
```
```   115
```
```   116 lemma hypreal_sqrt_sum_squares2 [simp]:
```
```   117      "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
```
```   118 apply (rule hypreal_sqrt_approx_zero2)
```
```   119 apply (rule hypreal_le_add_order)
```
```   120 apply (auto simp add: zero_le_square)
```
```   121 done
```
```   122
```
```   123 lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
```
```   124 apply (cases x)
```
```   125 apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
```
```   126 apply (auto intro: real_sqrt_gt_zero)
```
```   127 done
```
```   128
```
```   129 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
```
```   130 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
```
```   131
```
```   132 lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
```
```   133 apply (cases x)
```
```   134 apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
```
```   135 done
```
```   136
```
```   137 lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
```
```   138 apply (rule hrealpow_two [THEN subst])
```
```   139 apply (rule numeral_2_eq_2 [THEN subst])
```
```   140 apply (rule hypreal_sqrt_hrabs)
```
```   141 done
```
```   142
```
```   143 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
```
```   144      "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
```
```   145 apply (cases x)
```
```   146 apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
```
```   147 done
```
```   148
```
```   149 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
```
```   150 apply (rule HFinite_square_iff [THEN iffD1])
```
```   151 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp)
```
```   152 done
```
```   153
```
```   154 lemma st_hypreal_sqrt:
```
```   155      "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
```
```   156 apply (rule power_inject_base [where n=1])
```
```   157 apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
```
```   158 apply (rule st_mult [THEN subst])
```
```   159 apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
```
```   160 apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
```
```   161 apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
```
```   162 done
```
```   163
```
```   164 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
```
```   165 apply (cases x, cases y)
```
```   166 apply (simp add: starfun hypreal_add hrealpow hypreal_le
```
```   167             del: hpowr_Suc realpow_Suc)
```
```   168 done
```
```   169
```
```   170 lemma HFinite_hypreal_sqrt:
```
```   171      "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
```
```   172 apply (auto simp add: order_le_less)
```
```   173 apply (rule HFinite_square_iff [THEN iffD1])
```
```   174 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   175 apply (simp add: numeral_2_eq_2)
```
```   176 done
```
```   177
```
```   178 lemma HFinite_hypreal_sqrt_imp_HFinite:
```
```   179      "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
```
```   180 apply (auto simp add: order_le_less)
```
```   181 apply (drule HFinite_square_iff [THEN iffD2])
```
```   182 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   183 apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
```
```   184 done
```
```   185
```
```   186 lemma HFinite_hypreal_sqrt_iff [simp]:
```
```   187      "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
```
```   188 by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
```
```   189
```
```   190 lemma HFinite_sqrt_sum_squares [simp]:
```
```   191      "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
```
```   192 apply (rule HFinite_hypreal_sqrt_iff)
```
```   193 apply (rule hypreal_le_add_order)
```
```   194 apply (auto simp add: zero_le_square)
```
```   195 done
```
```   196
```
```   197 lemma Infinitesimal_hypreal_sqrt:
```
```   198      "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
```
```   199 apply (auto simp add: order_le_less)
```
```   200 apply (rule Infinitesimal_square_iff [THEN iffD2])
```
```   201 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   202 apply (simp add: numeral_2_eq_2)
```
```   203 done
```
```   204
```
```   205 lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
```
```   206      "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
```
```   207 apply (auto simp add: order_le_less)
```
```   208 apply (drule Infinitesimal_square_iff [THEN iffD1])
```
```   209 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   210 apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
```
```   211 done
```
```   212
```
```   213 lemma Infinitesimal_hypreal_sqrt_iff [simp]:
```
```   214      "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
```
```   215 by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
```
```   216
```
```   217 lemma Infinitesimal_sqrt_sum_squares [simp]:
```
```   218      "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
```
```   219 apply (rule Infinitesimal_hypreal_sqrt_iff)
```
```   220 apply (rule hypreal_le_add_order)
```
```   221 apply (auto simp add: zero_le_square)
```
```   222 done
```
```   223
```
```   224 lemma HInfinite_hypreal_sqrt:
```
```   225      "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
```
```   226 apply (auto simp add: order_le_less)
```
```   227 apply (rule HInfinite_square_iff [THEN iffD1])
```
```   228 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   229 apply (simp add: numeral_2_eq_2)
```
```   230 done
```
```   231
```
```   232 lemma HInfinite_hypreal_sqrt_imp_HInfinite:
```
```   233      "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
```
```   234 apply (auto simp add: order_le_less)
```
```   235 apply (drule HInfinite_square_iff [THEN iffD2])
```
```   236 apply (drule hypreal_sqrt_gt_zero_pow2)
```
```   237 apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
```
```   238 done
```
```   239
```
```   240 lemma HInfinite_hypreal_sqrt_iff [simp]:
```
```   241      "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
```
```   242 by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
```
```   243
```
```   244 lemma HInfinite_sqrt_sum_squares [simp]:
```
```   245      "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
```
```   246 apply (rule HInfinite_hypreal_sqrt_iff)
```
```   247 apply (rule hypreal_le_add_order)
```
```   248 apply (auto simp add: zero_le_square)
```
```   249 done
```
```   250
```
```   251 lemma HFinite_exp [simp]:
```
```   252      "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
```
```   253 by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
```
```   254          simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
```
```   255                    convergent_NSconvergent_iff [symmetric]
```
```   256                    summable_convergent_sumr_iff [symmetric] summable_exp)
```
```   257
```
```   258 lemma exphr_zero [simp]: "exphr 0 = 1"
```
```   259 apply (simp add: exphr_def sumhr_split_add
```
```   260                    [OF hypnat_one_less_hypnat_omega, symmetric])
```
```   261 apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
```
```   262                  hypnat_omega_def hypreal_add
```
```   263             del: hypnat_add_zero_left)
```
```   264 apply (simp add: hypreal_one_num [symmetric])
```
```   265 done
```
```   266
```
```   267 lemma coshr_zero [simp]: "coshr 0 = 1"
```
```   268 apply (simp add: coshr_def sumhr_split_add
```
```   269                    [OF hypnat_one_less_hypnat_omega, symmetric])
```
```   270 apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def
```
```   271          hypnat_add hypnat_omega_def st_add [symmetric]
```
```   272          hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
```
```   273        del: hypnat_add_zero_left)
```
```   274 done
```
```   275
```
```   276 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
```
```   277 by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
```
```   278
```
```   279 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
```
```   280 apply (case_tac "x = 0")
```
```   281 apply (cut_tac [2] x = 0 in DERIV_exp)
```
```   282 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
```
```   283 apply (drule_tac x = x in bspec, auto)
```
```   284 apply (drule_tac c = x in approx_mult1)
```
```   285 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
```
```   286             simp add: mult_assoc)
```
```   287 apply (rule approx_add_right_cancel [where d="-1"])
```
```   288 apply (rule approx_sym [THEN [2] approx_trans2])
```
```   289 apply (auto simp add: mem_infmal_iff)
```
```   290 done
```
```   291
```
```   292 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
```
```   293 by (auto intro: STAR_exp_Infinitesimal)
```
```   294
```
```   295 lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
```
```   296 apply (cases x, cases y)
```
```   297 apply (simp add: starfun hypreal_add hypreal_mult exp_add)
```
```   298 done
```
```   299
```
```   300 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
```
```   301 apply (simp add: exphr_def)
```
```   302 apply (rule st_hypreal_of_real [THEN subst])
```
```   303 apply (rule approx_st_eq, auto)
```
```   304 apply (rule approx_minus_iff [THEN iffD2])
```
```   305 apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
```
```   306 apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
```
```   307 apply (insert exp_converges [of x])
```
```   308 apply (simp add: sums_def)
```
```   309 apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
```
```   310 apply (simp add: LIMSEQ_NSLIMSEQ_iff)
```
```   311 done
```
```   312
```
```   313 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
```
```   314 apply (cases x)
```
```   315 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
```
```   316 done
```
```   317
```
```   318 (* exp (oo) is infinite *)
```
```   319 lemma starfun_exp_HInfinite:
```
```   320      "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
```
```   321 apply (frule starfun_exp_ge_add_one_self)
```
```   322 apply (rule HInfinite_ge_HInfinite, assumption)
```
```   323 apply (rule order_trans [of _ "1+x"], auto)
```
```   324 done
```
```   325
```
```   326 lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
```
```   327 apply (cases x)
```
```   328 apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
```
```   329 done
```
```   330
```
```   331 (* exp (-oo) is infinitesimal *)
```
```   332 lemma starfun_exp_Infinitesimal:
```
```   333      "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
```
```   334 apply (subgoal_tac "\<exists>y. x = - y")
```
```   335 apply (rule_tac [2] x = "- x" in exI)
```
```   336 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
```
```   337             simp add: starfun_exp_minus HInfinite_minus_iff)
```
```   338 done
```
```   339
```
```   340 lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
```
```   341 apply (cases x)
```
```   342 apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
```
```   343 done
```
```   344
```
```   345 (* needs derivative of inverse function
```
```   346    TRY a NS one today!!!
```
```   347
```
```   348 Goal "x @= 1 ==> ( *f* ln) x @= 1"
```
```   349 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
```
```   350 by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
```
```   351
```
```   352
```
```   353 Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
```
```   354
```
```   355 *)
```
```   356
```
```   357
```
```   358 lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
```
```   359 apply (cases x)
```
```   360 apply (simp add: starfun)
```
```   361 done
```
```   362
```
```   363 lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
```
```   364 apply (cases x)
```
```   365 apply (simp add: starfun hypreal_zero_num hypreal_less)
```
```   366 done
```
```   367
```
```   368 lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
```
```   369 by (auto simp add: starfun)
```
```   370
```
```   371 lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
```
```   372 apply (cases x)
```
```   373 apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
```
```   374 done
```
```   375
```
```   376 lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
```
```   377 apply (cases x)
```
```   378 apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
```
```   379 done
```
```   380
```
```   381 lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
```
```   382 apply (cases x)
```
```   383 apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
```
```   384 done
```
```   385
```
```   386 lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
```
```   387 apply (cases x)
```
```   388 apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
```
```   389 apply (auto dest: ln_not_eq_zero)
```
```   390 done
```
```   391
```
```   392 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
```
```   393 apply (rule HFinite_bounded)
```
```   394 apply (rule_tac [2] order_less_imp_le)
```
```   395 apply (rule_tac [2] starfun_ln_less_self)
```
```   396 apply (rule_tac [2] order_less_le_trans, auto)
```
```   397 done
```
```   398
```
```   399 lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
```
```   400 apply (cases x)
```
```   401 apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
```
```   402 apply (simp add: ln_inverse)
```
```   403 done
```
```   404
```
```   405 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
```
```   406 apply (cases x)
```
```   407 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
```
```   408 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
```
```   409 apply (rule_tac x = "exp u" in exI)
```
```   410 apply (ultra, arith)
```
```   411 done
```
```   412
```
```   413 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
```
```   414      "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
```
```   415 apply (simp add: STAR_exp_add)
```
```   416 apply (frule STAR_exp_Infinitesimal)
```
```   417 apply (drule approx_mult2)
```
```   418 apply (auto intro: starfun_exp_HFinite)
```
```   419 done
```
```   420
```
```   421 (* using previous result to get to result *)
```
```   422 lemma starfun_ln_HInfinite:
```
```   423      "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
```
```   424 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
```
```   425 apply (drule starfun_exp_HFinite)
```
```   426 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
```
```   427 done
```
```   428
```
```   429 lemma starfun_exp_HInfinite_Infinitesimal_disj:
```
```   430  "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
```
```   431 apply (insert linorder_linear [of x 0])
```
```   432 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
```
```   433 done
```
```   434
```
```   435 (* check out this proof!!! *)
```
```   436 lemma starfun_ln_HFinite_not_Infinitesimal:
```
```   437      "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
```
```   438 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
```
```   439 apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
```
```   440 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
```
```   441             del: starfun_exp_ln_iff)
```
```   442 done
```
```   443
```
```   444 (* we do proof by considering ln of 1/x *)
```
```   445 lemma starfun_ln_Infinitesimal_HInfinite:
```
```   446      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
```
```   447 apply (drule Infinitesimal_inverse_HInfinite)
```
```   448 apply (frule positive_imp_inverse_positive)
```
```   449 apply (drule_tac [2] starfun_ln_HInfinite)
```
```   450 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
```
```   451 done
```
```   452
```
```   453 lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
```
```   454 apply (cases x)
```
```   455 apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
```
```   456 apply (auto intro: ln_less_zero)
```
```   457 done
```
```   458
```
```   459 lemma starfun_ln_Infinitesimal_less_zero:
```
```   460      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
```
```   461 apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
```
```   462 apply (drule bspec [where x = 1])
```
```   463 apply (auto simp add: abs_if)
```
```   464 done
```
```   465
```
```   466 lemma starfun_ln_HInfinite_gt_zero:
```
```   467      "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
```
```   468 apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
```
```   469 apply (drule bspec [where x = 1])
```
```   470 apply (auto simp add: abs_if)
```
```   471 done
```
```   472
```
```   473 (*
```
```   474 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
```
```   475 *)
```
```   476
```
```   477 lemma HFinite_sin [simp]:
```
```   478      "sumhr (0, whn, %n. (if even(n) then 0 else
```
```   479               ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
```
```   480               \<in> HFinite"
```
```   481 apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
```
```   482             simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
```
```   483                       convergent_NSconvergent_iff [symmetric]
```
```   484                       summable_convergent_sumr_iff [symmetric])
```
```   485 apply (simp only: One_nat_def summable_sin)
```
```   486 done
```
```   487
```
```   488 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
```
```   489 by (simp add: starfun hypreal_zero_num)
```
```   490
```
```   491 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
```
```   492 apply (case_tac "x = 0")
```
```   493 apply (cut_tac [2] x = 0 in DERIV_sin)
```
```   494 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
```
```   495 apply (drule bspec [where x = x], auto)
```
```   496 apply (drule approx_mult1 [where c = x])
```
```   497 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
```
```   498            simp add: mult_assoc)
```
```   499 done
```
```   500
```
```   501 lemma HFinite_cos [simp]:
```
```   502      "sumhr (0, whn, %n. (if even(n) then
```
```   503             ((- 1) ^ (n div 2))/(real (fact n)) else
```
```   504             0) * x ^ n) \<in> HFinite"
```
```   505 by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
```
```   506          simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
```
```   507                    convergent_NSconvergent_iff [symmetric]
```
```   508                    summable_convergent_sumr_iff [symmetric] summable_cos)
```
```   509
```
```   510 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
```
```   511 by (simp add: starfun hypreal_zero_num hypreal_one_num)
```
```   512
```
```   513 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
```
```   514 apply (case_tac "x = 0")
```
```   515 apply (cut_tac [2] x = 0 in DERIV_cos)
```
```   516 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
```
```   517 apply (drule bspec [where x = x])
```
```   518 apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
```
```   519 apply (drule approx_mult1 [where c = x])
```
```   520 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
```
```   521             simp add: mult_assoc hypreal_of_real_one)
```
```   522 apply (rule approx_add_right_cancel [where d = "-1"], auto)
```
```   523 done
```
```   524
```
```   525 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
```
```   526 by (simp add: starfun hypreal_zero_num)
```
```   527
```
```   528 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
```
```   529 apply (case_tac "x = 0")
```
```   530 apply (cut_tac [2] x = 0 in DERIV_tan)
```
```   531 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
```
```   532 apply (drule bspec [where x = x], auto)
```
```   533 apply (drule approx_mult1 [where c = x])
```
```   534 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
```
```   535              simp add: mult_assoc)
```
```   536 done
```
```   537
```
```   538 lemma STAR_sin_cos_Infinitesimal_mult:
```
```   539      "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
```
```   540 apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1])
```
```   541 apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
```
```   542 done
```
```   543
```
```   544 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
```
```   545 by simp
```
```   546
```
```   547 (* lemmas *)
```
```   548
```
```   549 lemma lemma_split_hypreal_of_real:
```
```   550      "N \<in> HNatInfinite
```
```   551       ==> hypreal_of_real a =
```
```   552           hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
```
```   553 by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
```
```   554
```
```   555 lemma STAR_sin_Infinitesimal_divide:
```
```   556      "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
```
```   557 apply (cut_tac x = 0 in DERIV_sin)
```
```   558 apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
```
```   559 done
```
```   560
```
```   561 (*------------------------------------------------------------------------*)
```
```   562 (* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
```
```   563 (*------------------------------------------------------------------------*)
```
```   564
```
```   565 lemma lemma_sin_pi:
```
```   566      "n \<in> HNatInfinite
```
```   567       ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
```
```   568 apply (rule STAR_sin_Infinitesimal_divide)
```
```   569 apply (auto simp add: HNatInfinite_not_eq_zero)
```
```   570 done
```
```   571
```
```   572 lemma STAR_sin_inverse_HNatInfinite:
```
```   573      "n \<in> HNatInfinite
```
```   574       ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
```
```   575 apply (frule lemma_sin_pi)
```
```   576 apply (simp add: divide_inverse)
```
```   577 done
```
```   578
```
```   579 lemma Infinitesimal_pi_divide_HNatInfinite:
```
```   580      "N \<in> HNatInfinite
```
```   581       ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
```
```   582 apply (simp add: divide_inverse)
```
```   583 apply (auto intro: Infinitesimal_HFinite_mult2)
```
```   584 done
```
```   585
```
```   586 lemma pi_divide_HNatInfinite_not_zero [simp]:
```
```   587      "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
```
```   588 by (simp add: HNatInfinite_not_eq_zero)
```
```   589
```
```   590 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
```
```   591      "n \<in> HNatInfinite
```
```   592       ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n
```
```   593           @= hypreal_of_real pi"
```
```   594 apply (frule STAR_sin_Infinitesimal_divide
```
```   595                [OF Infinitesimal_pi_divide_HNatInfinite
```
```   596                    pi_divide_HNatInfinite_not_zero])
```
```   597 apply (auto simp add: inverse_mult_distrib)
```
```   598 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
```
```   599 apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
```
```   600 done
```
```   601
```
```   602 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
```
```   603      "n \<in> HNatInfinite
```
```   604       ==> hypreal_of_hypnat n *
```
```   605           ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))
```
```   606           @= hypreal_of_real pi"
```
```   607 apply (rule mult_commute [THEN subst])
```
```   608 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
```
```   609 done
```
```   610
```
```   611 lemma starfunNat_pi_divide_n_Infinitesimal:
```
```   612      "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
```
```   613 by (auto intro!: Infinitesimal_HFinite_mult2
```
```   614          simp add: starfunNat_mult [symmetric] divide_inverse
```
```   615                    starfunNat_inverse [symmetric] starfunNat_real_of_nat)
```
```   616
```
```   617 lemma STAR_sin_pi_divide_n_approx:
```
```   618      "N \<in> HNatInfinite ==>
```
```   619       ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=
```
```   620       hypreal_of_real pi/(hypreal_of_hypnat N)"
```
```   621 by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2
```
```   622          simp add: starfunNat_mult [symmetric] divide_inverse
```
```   623                    starfunNat_inverse_real_of_nat_eq)
```
```   624
```
```   625 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
```
```   626 apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
```
```   627 apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
```
```   628 apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
```
```   629 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
```
```   630 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi
```
```   631             simp add: starfunNat_real_of_nat mult_commute divide_inverse)
```
```   632 done
```
```   633
```
```   634 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
```
```   635 apply (simp add: NSLIMSEQ_def, auto)
```
```   636 apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
```
```   637 apply (rule STAR_cos_Infinitesimal)
```
```   638 apply (auto intro!: Infinitesimal_HFinite_mult2
```
```   639             simp add: starfunNat_mult [symmetric] divide_inverse
```
```   640                       starfunNat_inverse [symmetric] starfunNat_real_of_nat)
```
```   641 done
```
```   642
```
```   643 lemma NSLIMSEQ_sin_cos_pi:
```
```   644      "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
```
```   645 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
```
```   646
```
```   647
```
```   648 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
```
```   649
```
```   650 lemma STAR_cos_Infinitesimal_approx:
```
```   651      "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
```
```   652 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
```
```   653 apply (auto simp add: Infinitesimal_approx_minus [symmetric]
```
```   654             diff_minus add_assoc [symmetric] numeral_2_eq_2)
```
```   655 done
```
```   656
```
```   657 lemma STAR_cos_Infinitesimal_approx2:
```
```   658      "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
```
```   659 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
```
```   660 apply (auto intro: Infinitesimal_SReal_divide
```
```   661             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
```
```   662 done
```
```   663
```
```   664 ML
```
```   665 {*
```
```   666 val STAR_sqrt_zero = thm "STAR_sqrt_zero";
```
```   667 val STAR_sqrt_one = thm "STAR_sqrt_one";
```
```   668 val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
```
```   669 val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
```
```   670 val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
```
```   671 val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
```
```   672 val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
```
```   673 val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
```
```   674 val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
```
```   675 val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
```
```   676 val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
```
```   677 val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
```
```   678 val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
```
```   679 val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
```
```   680 val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
```
```   681 val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
```
```   682 val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
```
```   683 val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
```
```   684 val star_sqrt_HFinite = thm "star_sqrt_HFinite";
```
```   685 val st_hypreal_sqrt = thm "st_hypreal_sqrt";
```
```   686 val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
```
```   687 val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
```
```   688 val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
```
```   689 val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
```
```   690 val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
```
```   691 val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
```
```   692 val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
```
```   693 val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
```
```   694 val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
```
```   695 val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
```
```   696 val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
```
```   697 val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
```
```   698 val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
```
```   699 val HFinite_exp = thm "HFinite_exp";
```
```   700 val exphr_zero = thm "exphr_zero";
```
```   701 val coshr_zero = thm "coshr_zero";
```
```   702 val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
```
```   703 val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
```
```   704 val STAR_exp_epsilon = thm "STAR_exp_epsilon";
```
```   705 val STAR_exp_add = thm "STAR_exp_add";
```
```   706 val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
```
```   707 val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
```
```   708 val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
```
```   709 val starfun_exp_minus = thm "starfun_exp_minus";
```
```   710 val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
```
```   711 val starfun_exp_gt_one = thm "starfun_exp_gt_one";
```
```   712 val starfun_ln_exp = thm "starfun_ln_exp";
```
```   713 val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
```
```   714 val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
```
```   715 val starfun_ln_less_self = thm "starfun_ln_less_self";
```
```   716 val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
```
```   717 val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
```
```   718 val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
```
```   719 val starfun_ln_HFinite = thm "starfun_ln_HFinite";
```
```   720 val starfun_ln_inverse = thm "starfun_ln_inverse";
```
```   721 val starfun_exp_HFinite = thm "starfun_exp_HFinite";
```
```   722 val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
```
```   723 val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
```
```   724 val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
```
```   725 val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
```
```   726 val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
```
```   727 val starfun_ln_less_zero = thm "starfun_ln_less_zero";
```
```   728 val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
```
```   729 val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
```
```   730 val HFinite_sin = thm "HFinite_sin";
```
```   731 val STAR_sin_zero = thm "STAR_sin_zero";
```
```   732 val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
```
```   733 val HFinite_cos = thm "HFinite_cos";
```
```   734 val STAR_cos_zero = thm "STAR_cos_zero";
```
```   735 val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
```
```   736 val STAR_tan_zero = thm "STAR_tan_zero";
```
```   737 val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
```
```   738 val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
```
```   739 val HFinite_pi = thm "HFinite_pi";
```
```   740 val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
```
```   741 val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
```
```   742 val lemma_sin_pi = thm "lemma_sin_pi";
```
```   743 val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
```
```   744 val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
```
```   745 val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
```
```   746 val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
```
```   747 val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
```
```   748 val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
```
```   749 val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
```
```   750 val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
```
```   751 val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
```
```   752 val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
```
```   753 val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
```
```   754 val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
```
```   755 *}
```
```   756
```
```   757
```
```   758 end
```