src/HOL/Hyperreal/HTranscendental.thy
changeset 14420 4e72cd222e0b
parent 13958 c1c67582c9b5
child 14430 5cb24165a2e1
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 01 05:39:32 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 01 11:52:59 2004 +0100
     1.3 @@ -1,23 +1,740 @@
     1.4  (*  Title       : HTranscendental.thy
     1.5      Author      : Jacques D. Fleuriot
     1.6      Copyright   : 2001 University of Edinburgh
     1.7 -    Description : Nonstandard extensions of transcendental functions
     1.8 +
     1.9 +Converted to Isar and polished by lcp
    1.10  *)
    1.11  
    1.12 -HTranscendental = Transcendental + IntFloor + 
    1.13 +header{*Nonstandard Extensions of Transcendental Functions*}
    1.14 +
    1.15 +theory HTranscendental = Transcendental + IntFloor:
    1.16  
    1.17  constdefs
    1.18  
    1.19 -
    1.20 -    (* define exponential function using standard part *)
    1.21 -    exphr :: real => hypreal
    1.22 +  exphr :: "real => hypreal"
    1.23 +    --{*define exponential function using standard part *}
    1.24      "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
    1.25  
    1.26 -    sinhr :: real => hypreal
    1.27 +  sinhr :: "real => hypreal"
    1.28      "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
    1.29               ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
    1.30    
    1.31 -    coshr :: real => hypreal
    1.32 +  coshr :: "real => hypreal"
    1.33      "coshr x == st(sumhr (0, whn, %n. (if even(n) then
    1.34              ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
    1.35 -end
    1.36 \ No newline at end of file
    1.37 +
    1.38 +
    1.39 +subsection{*Nonstandard Extension of Square Root Function*}
    1.40 +
    1.41 +lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
    1.42 +by (simp add: starfun hypreal_zero_num)
    1.43 +
    1.44 +lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    1.45 +by (simp add: starfun hypreal_one_num)
    1.46 +
    1.47 +lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
    1.48 +apply (rule eq_Abs_hypreal [of x])
    1.49 +apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
    1.50 +                      real_sqrt_pow2_iff 
    1.51 +            simp del: hpowr_Suc realpow_Suc)
    1.52 +done
    1.53 +
    1.54 +lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    1.55 +apply (rule eq_Abs_hypreal [of x])
    1.56 +apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
    1.57 +            simp add: hypreal_less starfun hrealpow hypreal_zero_num 
    1.58 +            simp del: hpowr_Suc realpow_Suc)
    1.59 +done
    1.60 +
    1.61 +lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
    1.62 +by (frule hypreal_sqrt_gt_zero_pow2, auto)
    1.63 +
    1.64 +lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
    1.65 +apply (frule hypreal_sqrt_pow2_gt_zero)
    1.66 +apply (auto simp add: numeral_2_eq_2)
    1.67 +done
    1.68 +
    1.69 +lemma hypreal_inverse_sqrt_pow2:
    1.70 +     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    1.71 +apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
    1.72 +apply (auto dest: hypreal_sqrt_gt_zero_pow2)
    1.73 +done
    1.74 +
    1.75 +lemma hypreal_sqrt_mult_distrib: 
    1.76 +    "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.77 +apply (rule eq_Abs_hypreal [of x])
    1.78 +apply (rule eq_Abs_hypreal [of y])
    1.79 +apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
    1.80 +apply (auto intro: real_sqrt_mult_distrib) 
    1.81 +done
    1.82 +
    1.83 +lemma hypreal_sqrt_mult_distrib2:
    1.84 +     "[|0\<le>x; 0\<le>y |] ==>  
    1.85 +     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.86 +by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
    1.87 +
    1.88 +lemma hypreal_sqrt_approx_zero [simp]:
    1.89 +     "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    1.90 +apply (auto simp add: mem_infmal_iff [symmetric])
    1.91 +apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    1.92 +apply (auto intro: Infinitesimal_mult 
    1.93 +            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
    1.94 +            simp add: numeral_2_eq_2)
    1.95 +done
    1.96 +
    1.97 +lemma hypreal_sqrt_approx_zero2 [simp]:
    1.98 +     "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    1.99 +by (auto simp add: order_le_less)
   1.100 +
   1.101 +lemma hypreal_sqrt_sum_squares [simp]:
   1.102 +     "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
   1.103 +apply (rule hypreal_sqrt_approx_zero2)
   1.104 +apply (rule hypreal_le_add_order)+
   1.105 +apply (auto simp add: zero_le_square)
   1.106 +done
   1.107 +
   1.108 +lemma hypreal_sqrt_sum_squares2 [simp]:
   1.109 +     "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
   1.110 +apply (rule hypreal_sqrt_approx_zero2)
   1.111 +apply (rule hypreal_le_add_order)
   1.112 +apply (auto simp add: zero_le_square)
   1.113 +done
   1.114 +
   1.115 +lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
   1.116 +apply (rule eq_Abs_hypreal [of x])
   1.117 +apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
   1.118 +apply (auto intro: real_sqrt_gt_zero)
   1.119 +done
   1.120 +
   1.121 +lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
   1.122 +by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   1.123 +
   1.124 +lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
   1.125 +apply (rule eq_Abs_hypreal [of x])
   1.126 +apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
   1.127 +done
   1.128 +
   1.129 +lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
   1.130 +apply (rule hrealpow_two [THEN subst])
   1.131 +apply (rule numeral_2_eq_2 [THEN subst])
   1.132 +apply (rule hypreal_sqrt_hrabs)
   1.133 +done
   1.134 +
   1.135 +lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   1.136 +     "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
   1.137 +apply (rule eq_Abs_hypreal [of x])
   1.138 +apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
   1.139 +done
   1.140 +
   1.141 +lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
   1.142 +apply (rule HFinite_square_iff [THEN iffD1])
   1.143 +apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
   1.144 +done
   1.145 +
   1.146 +lemma st_hypreal_sqrt:
   1.147 +     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   1.148 +apply (rule power_inject_base [where n=1])
   1.149 +apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
   1.150 +apply (rule st_mult [THEN subst])
   1.151 +apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.152 +apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.153 +apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
   1.154 +done
   1.155 +
   1.156 +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
   1.157 +apply (rule eq_Abs_hypreal [of x])
   1.158 +apply (rule eq_Abs_hypreal [of y])
   1.159 +apply (simp add: starfun hypreal_add hrealpow hypreal_le 
   1.160 +            del: hpowr_Suc realpow_Suc)
   1.161 +done
   1.162 +
   1.163 +lemma HFinite_hypreal_sqrt:
   1.164 +     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
   1.165 +apply (auto simp add: order_le_less)
   1.166 +apply (rule HFinite_square_iff [THEN iffD1])
   1.167 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.168 +apply (simp add: numeral_2_eq_2)
   1.169 +done
   1.170 +
   1.171 +lemma HFinite_hypreal_sqrt_imp_HFinite:
   1.172 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
   1.173 +apply (auto simp add: order_le_less)
   1.174 +apply (drule HFinite_square_iff [THEN iffD2])
   1.175 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.176 +apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
   1.177 +done
   1.178 +
   1.179 +lemma HFinite_hypreal_sqrt_iff [simp]:
   1.180 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   1.181 +by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
   1.182 +
   1.183 +lemma HFinite_sqrt_sum_squares [simp]:
   1.184 +     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
   1.185 +apply (rule HFinite_hypreal_sqrt_iff)
   1.186 +apply (rule hypreal_le_add_order)
   1.187 +apply (auto simp add: zero_le_square)
   1.188 +done
   1.189 +
   1.190 +lemma Infinitesimal_hypreal_sqrt:
   1.191 +     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
   1.192 +apply (auto simp add: order_le_less)
   1.193 +apply (rule Infinitesimal_square_iff [THEN iffD2])
   1.194 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.195 +apply (simp add: numeral_2_eq_2)
   1.196 +done
   1.197 +
   1.198 +lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
   1.199 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
   1.200 +apply (auto simp add: order_le_less)
   1.201 +apply (drule Infinitesimal_square_iff [THEN iffD1])
   1.202 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.203 +apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
   1.204 +done
   1.205 +
   1.206 +lemma Infinitesimal_hypreal_sqrt_iff [simp]:
   1.207 +     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   1.208 +by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
   1.209 +
   1.210 +lemma Infinitesimal_sqrt_sum_squares [simp]:
   1.211 +     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
   1.212 +apply (rule Infinitesimal_hypreal_sqrt_iff)
   1.213 +apply (rule hypreal_le_add_order)
   1.214 +apply (auto simp add: zero_le_square)
   1.215 +done
   1.216 +
   1.217 +lemma HInfinite_hypreal_sqrt:
   1.218 +     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
   1.219 +apply (auto simp add: order_le_less)
   1.220 +apply (rule HInfinite_square_iff [THEN iffD1])
   1.221 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.222 +apply (simp add: numeral_2_eq_2)
   1.223 +done
   1.224 +
   1.225 +lemma HInfinite_hypreal_sqrt_imp_HInfinite:
   1.226 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
   1.227 +apply (auto simp add: order_le_less)
   1.228 +apply (drule HInfinite_square_iff [THEN iffD2])
   1.229 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.230 +apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
   1.231 +done
   1.232 +
   1.233 +lemma HInfinite_hypreal_sqrt_iff [simp]:
   1.234 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   1.235 +by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
   1.236 +
   1.237 +lemma HInfinite_sqrt_sum_squares [simp]:
   1.238 +     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
   1.239 +apply (rule HInfinite_hypreal_sqrt_iff)
   1.240 +apply (rule hypreal_le_add_order)
   1.241 +apply (auto simp add: zero_le_square)
   1.242 +done
   1.243 +
   1.244 +lemma HFinite_exp [simp]:
   1.245 +     "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
   1.246 +by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   1.247 +         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   1.248 +                   convergent_NSconvergent_iff [symmetric] 
   1.249 +                   summable_convergent_sumr_iff [symmetric] summable_exp)
   1.250 +
   1.251 +lemma exphr_zero [simp]: "exphr 0 = 1"
   1.252 +apply (simp add: exphr_def sumhr_split_add
   1.253 +                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   1.254 +apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
   1.255 +                 hypnat_omega_def hypreal_add 
   1.256 +            del: hypnat_add_zero_left)
   1.257 +apply (simp add: hypreal_one_num [symmetric])
   1.258 +done
   1.259 +
   1.260 +lemma coshr_zero [simp]: "coshr 0 = 1"
   1.261 +apply (simp add: coshr_def sumhr_split_add
   1.262 +                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   1.263 +apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def 
   1.264 +         hypnat_add hypnat_omega_def st_add [symmetric] 
   1.265 +         hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
   1.266 +       del: hypnat_add_zero_left)
   1.267 +done
   1.268 +
   1.269 +lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
   1.270 +by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
   1.271 +
   1.272 +lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
   1.273 +apply (case_tac "x = 0")
   1.274 +apply (cut_tac [2] x = 0 in DERIV_exp)
   1.275 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.276 +apply (drule_tac x = x in bspec, auto)
   1.277 +apply (drule_tac c = x in approx_mult1)
   1.278 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   1.279 +            simp add: mult_assoc)
   1.280 +apply (rule approx_add_right_cancel [where d="-1"])
   1.281 +apply (rule approx_sym [THEN [2] approx_trans2])
   1.282 +apply (auto simp add: mem_infmal_iff)
   1.283 +done
   1.284 +
   1.285 +lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   1.286 +by (auto intro: STAR_exp_Infinitesimal)
   1.287 +
   1.288 +lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   1.289 +apply (rule eq_Abs_hypreal [of x])
   1.290 +apply (rule eq_Abs_hypreal [of y])
   1.291 +apply (simp add: starfun hypreal_add hypreal_mult exp_add)
   1.292 +done
   1.293 +
   1.294 +lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
   1.295 +apply (simp add: exphr_def)
   1.296 +apply (rule st_hypreal_of_real [THEN subst])
   1.297 +apply (rule approx_st_eq, auto)
   1.298 +apply (rule approx_minus_iff [THEN iffD2])
   1.299 +apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
   1.300 +apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
   1.301 +apply (insert exp_converges [of x]) 
   1.302 +apply (simp add: sums_def) 
   1.303 +apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
   1.304 +apply (simp add: LIMSEQ_NSLIMSEQ_iff)
   1.305 +done
   1.306 +
   1.307 +lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   1.308 +apply (rule eq_Abs_hypreal [of x])
   1.309 +apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
   1.310 +done
   1.311 +
   1.312 +(* exp (oo) is infinite *)
   1.313 +lemma starfun_exp_HInfinite:
   1.314 +     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
   1.315 +apply (frule starfun_exp_ge_add_one_self)
   1.316 +apply (rule HInfinite_ge_HInfinite, assumption)
   1.317 +apply (rule order_trans [of _ "1+x"], auto) 
   1.318 +done
   1.319 +
   1.320 +lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
   1.321 +apply (rule eq_Abs_hypreal [of x])
   1.322 +apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
   1.323 +done
   1.324 +
   1.325 +(* exp (-oo) is infinitesimal *)
   1.326 +lemma starfun_exp_Infinitesimal:
   1.327 +     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
   1.328 +apply (subgoal_tac "\<exists>y. x = - y")
   1.329 +apply (rule_tac [2] x = "- x" in exI)
   1.330 +apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
   1.331 +            simp add: starfun_exp_minus HInfinite_minus_iff)
   1.332 +done
   1.333 +
   1.334 +lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
   1.335 +apply (rule eq_Abs_hypreal [of x])
   1.336 +apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
   1.337 +done
   1.338 +
   1.339 +(* needs derivative of inverse function
   1.340 +   TRY a NS one today!!!
   1.341 +
   1.342 +Goal "x @= 1 ==> ( *f* ln) x @= 1"
   1.343 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.344 +by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
   1.345 +
   1.346 +
   1.347 +Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
   1.348 +
   1.349 +*)
   1.350 +
   1.351 +
   1.352 +lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
   1.353 +apply (rule eq_Abs_hypreal [of x])
   1.354 +apply (simp add: starfun)
   1.355 +done
   1.356 +
   1.357 +lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
   1.358 +apply (rule eq_Abs_hypreal [of x])
   1.359 +apply (simp add: starfun hypreal_zero_num hypreal_less)
   1.360 +done
   1.361 +
   1.362 +lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
   1.363 +by (auto simp add: starfun)
   1.364 +
   1.365 +lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
   1.366 +apply (rule eq_Abs_hypreal [of x])
   1.367 +apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
   1.368 +done
   1.369 +
   1.370 +lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
   1.371 +apply (rule eq_Abs_hypreal [of x])
   1.372 +apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
   1.373 +done
   1.374 +
   1.375 +lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
   1.376 +apply (rule eq_Abs_hypreal [of x])
   1.377 +apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   1.378 +done
   1.379 +
   1.380 +lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
   1.381 +apply (rule eq_Abs_hypreal [of x])
   1.382 +apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   1.383 +apply (auto dest: ln_not_eq_zero) 
   1.384 +done
   1.385 +
   1.386 +lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
   1.387 +apply (rule HFinite_bounded)
   1.388 +apply (rule_tac [2] order_less_imp_le)
   1.389 +apply (rule_tac [2] starfun_ln_less_self)
   1.390 +apply (rule_tac [2] order_less_le_trans, auto)
   1.391 +done
   1.392 +
   1.393 +lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
   1.394 +apply (rule eq_Abs_hypreal [of x])
   1.395 +apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
   1.396 +apply (simp add: ln_inverse)
   1.397 +done
   1.398 +
   1.399 +lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
   1.400 +apply (rule eq_Abs_hypreal [of x])
   1.401 +apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
   1.402 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   1.403 +apply (rule_tac x = "exp u" in exI)
   1.404 +apply (ultra, arith)
   1.405 +done
   1.406 +
   1.407 +lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   1.408 +     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
   1.409 +apply (simp add: STAR_exp_add)
   1.410 +apply (frule STAR_exp_Infinitesimal)
   1.411 +apply (drule approx_mult2)
   1.412 +apply (auto intro: starfun_exp_HFinite)
   1.413 +done
   1.414 +
   1.415 +(* using previous result to get to result *)
   1.416 +lemma starfun_ln_HInfinite:
   1.417 +     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   1.418 +apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   1.419 +apply (drule starfun_exp_HFinite)
   1.420 +apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   1.421 +done
   1.422 +
   1.423 +lemma starfun_exp_HInfinite_Infinitesimal_disj:
   1.424 + "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
   1.425 +apply (insert linorder_linear [of x 0]) 
   1.426 +apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   1.427 +done
   1.428 +
   1.429 +(* check out this proof!!! *)
   1.430 +lemma starfun_ln_HFinite_not_Infinitesimal:
   1.431 +     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
   1.432 +apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   1.433 +apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   1.434 +apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   1.435 +            del: starfun_exp_ln_iff)
   1.436 +done
   1.437 +
   1.438 +(* we do proof by considering ln of 1/x *)
   1.439 +lemma starfun_ln_Infinitesimal_HInfinite:
   1.440 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   1.441 +apply (drule Infinitesimal_inverse_HInfinite)
   1.442 +apply (frule positive_imp_inverse_positive)
   1.443 +apply (drule_tac [2] starfun_ln_HInfinite)
   1.444 +apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   1.445 +done
   1.446 +
   1.447 +lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
   1.448 +apply (rule eq_Abs_hypreal [of x])
   1.449 +apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
   1.450 +apply (auto intro: ln_less_zero) 
   1.451 +done
   1.452 +
   1.453 +lemma starfun_ln_Infinitesimal_less_zero:
   1.454 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
   1.455 +apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   1.456 +apply (drule bspec [where x = 1])
   1.457 +apply (auto simp add: abs_if)
   1.458 +done
   1.459 +
   1.460 +lemma starfun_ln_HInfinite_gt_zero:
   1.461 +     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
   1.462 +apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   1.463 +apply (drule bspec [where x = 1])
   1.464 +apply (auto simp add: abs_if)
   1.465 +done
   1.466 +
   1.467 +(*
   1.468 +Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
   1.469 +*)
   1.470 +
   1.471 +lemma HFinite_sin [simp]:
   1.472 +     "sumhr (0, whn, %n. (if even(n) then 0 else  
   1.473 +              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
   1.474 +              \<in> HFinite"
   1.475 +apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   1.476 +            simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   1.477 +                      convergent_NSconvergent_iff [symmetric] 
   1.478 +                      summable_convergent_sumr_iff [symmetric])
   1.479 +apply (simp only: One_nat_def summable_sin)
   1.480 +done
   1.481 +
   1.482 +lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   1.483 +by (simp add: starfun hypreal_zero_num)
   1.484 +
   1.485 +lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
   1.486 +apply (case_tac "x = 0")
   1.487 +apply (cut_tac [2] x = 0 in DERIV_sin)
   1.488 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   1.489 +apply (drule bspec [where x = x], auto)
   1.490 +apply (drule approx_mult1 [where c = x])
   1.491 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.492 +           simp add: mult_assoc)
   1.493 +done
   1.494 +
   1.495 +lemma HFinite_cos [simp]:
   1.496 +     "sumhr (0, whn, %n. (if even(n) then  
   1.497 +            ((- 1) ^ (n div 2))/(real (fact n)) else  
   1.498 +            0) * x ^ n) \<in> HFinite"
   1.499 +by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   1.500 +         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   1.501 +                   convergent_NSconvergent_iff [symmetric] 
   1.502 +                   summable_convergent_sumr_iff [symmetric] summable_cos)
   1.503 +
   1.504 +lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   1.505 +by (simp add: starfun hypreal_zero_num hypreal_one_num)
   1.506 +
   1.507 +lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
   1.508 +apply (case_tac "x = 0")
   1.509 +apply (cut_tac [2] x = 0 in DERIV_cos)
   1.510 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   1.511 +apply (drule bspec [where x = x])
   1.512 +apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
   1.513 +apply (drule approx_mult1 [where c = x])
   1.514 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.515 +            simp add: mult_assoc hypreal_of_real_one)
   1.516 +apply (rule approx_add_right_cancel [where d = "-1"], auto)
   1.517 +done
   1.518 +
   1.519 +lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   1.520 +by (simp add: starfun hypreal_zero_num)
   1.521 +
   1.522 +lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
   1.523 +apply (case_tac "x = 0")
   1.524 +apply (cut_tac [2] x = 0 in DERIV_tan)
   1.525 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   1.526 +apply (drule bspec [where x = x], auto)
   1.527 +apply (drule approx_mult1 [where c = x])
   1.528 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.529 +             simp add: mult_assoc)
   1.530 +done
   1.531 +
   1.532 +lemma STAR_sin_cos_Infinitesimal_mult:
   1.533 +     "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
   1.534 +apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) 
   1.535 +apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   1.536 +done
   1.537 +
   1.538 +lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   1.539 +by simp
   1.540 +
   1.541 +(* lemmas *)
   1.542 +
   1.543 +lemma lemma_split_hypreal_of_real:
   1.544 +     "N \<in> HNatInfinite  
   1.545 +      ==> hypreal_of_real a =  
   1.546 +          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   1.547 +by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
   1.548 +
   1.549 +lemma STAR_sin_Infinitesimal_divide:
   1.550 +     "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
   1.551 +apply (cut_tac x = 0 in DERIV_sin)
   1.552 +apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
   1.553 +done
   1.554 +
   1.555 +(*------------------------------------------------------------------------*) 
   1.556 +(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
   1.557 +(*------------------------------------------------------------------------*)
   1.558 +
   1.559 +lemma lemma_sin_pi:
   1.560 +     "n \<in> HNatInfinite  
   1.561 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
   1.562 +apply (rule STAR_sin_Infinitesimal_divide)
   1.563 +apply (auto simp add: HNatInfinite_not_eq_zero)
   1.564 +done
   1.565 +
   1.566 +lemma STAR_sin_inverse_HNatInfinite:
   1.567 +     "n \<in> HNatInfinite  
   1.568 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
   1.569 +apply (frule lemma_sin_pi)
   1.570 +apply (simp add: divide_inverse_zero)
   1.571 +done
   1.572 +
   1.573 +lemma Infinitesimal_pi_divide_HNatInfinite: 
   1.574 +     "N \<in> HNatInfinite  
   1.575 +      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   1.576 +apply (simp add: divide_inverse_zero)
   1.577 +apply (auto intro: Infinitesimal_HFinite_mult2)
   1.578 +done
   1.579 +
   1.580 +lemma pi_divide_HNatInfinite_not_zero [simp]:
   1.581 +     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   1.582 +by (simp add: HNatInfinite_not_eq_zero)
   1.583 +
   1.584 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   1.585 +     "n \<in> HNatInfinite  
   1.586 +      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   1.587 +          @= hypreal_of_real pi"
   1.588 +apply (frule STAR_sin_Infinitesimal_divide
   1.589 +               [OF Infinitesimal_pi_divide_HNatInfinite 
   1.590 +                   pi_divide_HNatInfinite_not_zero])
   1.591 +apply (auto simp add: hypreal_inverse_distrib)
   1.592 +apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   1.593 +apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
   1.594 +done
   1.595 +
   1.596 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   1.597 +     "n \<in> HNatInfinite  
   1.598 +      ==> hypreal_of_hypnat n *  
   1.599 +          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   1.600 +          @= hypreal_of_real pi"
   1.601 +apply (rule mult_commute [THEN subst])
   1.602 +apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   1.603 +done
   1.604 +
   1.605 +lemma starfunNat_pi_divide_n_Infinitesimal: 
   1.606 +     "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
   1.607 +by (auto intro!: Infinitesimal_HFinite_mult2 
   1.608 +         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   1.609 +                   starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   1.610 +
   1.611 +lemma STAR_sin_pi_divide_n_approx:
   1.612 +     "N \<in> HNatInfinite ==>  
   1.613 +      ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
   1.614 +      hypreal_of_real pi/(hypreal_of_hypnat N)"
   1.615 +by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
   1.616 +         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   1.617 +                   starfunNat_inverse_real_of_nat_eq)
   1.618 +
   1.619 +lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
   1.620 +apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
   1.621 +apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
   1.622 +apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
   1.623 +apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
   1.624 +apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   1.625 +            simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
   1.626 +done
   1.627 +
   1.628 +lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
   1.629 +apply (simp add: NSLIMSEQ_def, auto)
   1.630 +apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
   1.631 +apply (rule STAR_cos_Infinitesimal)
   1.632 +apply (auto intro!: Infinitesimal_HFinite_mult2 
   1.633 +            simp add: starfunNat_mult [symmetric] divide_inverse_zero
   1.634 +                      starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   1.635 +done
   1.636 +
   1.637 +lemma NSLIMSEQ_sin_cos_pi:
   1.638 +     "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
   1.639 +by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   1.640 +
   1.641 +
   1.642 +text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
   1.643 +
   1.644 +lemma STAR_cos_Infinitesimal_approx:
   1.645 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
   1.646 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.647 +apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   1.648 +            diff_minus add_assoc [symmetric] numeral_2_eq_2)
   1.649 +done
   1.650 +
   1.651 +lemma STAR_cos_Infinitesimal_approx2:
   1.652 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
   1.653 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.654 +apply (auto intro: Infinitesimal_SReal_divide 
   1.655 +            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   1.656 +done
   1.657 +
   1.658 +ML
   1.659 +{*
   1.660 +val STAR_sqrt_zero = thm "STAR_sqrt_zero";
   1.661 +val STAR_sqrt_one = thm "STAR_sqrt_one";
   1.662 +val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
   1.663 +val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
   1.664 +val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
   1.665 +val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
   1.666 +val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
   1.667 +val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
   1.668 +val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
   1.669 +val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
   1.670 +val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
   1.671 +val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
   1.672 +val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
   1.673 +val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
   1.674 +val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
   1.675 +val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
   1.676 +val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
   1.677 +val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
   1.678 +val star_sqrt_HFinite = thm "star_sqrt_HFinite";
   1.679 +val st_hypreal_sqrt = thm "st_hypreal_sqrt";
   1.680 +val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
   1.681 +val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
   1.682 +val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
   1.683 +val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
   1.684 +val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
   1.685 +val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
   1.686 +val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
   1.687 +val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
   1.688 +val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
   1.689 +val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
   1.690 +val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
   1.691 +val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
   1.692 +val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
   1.693 +val HFinite_exp = thm "HFinite_exp";
   1.694 +val exphr_zero = thm "exphr_zero";
   1.695 +val coshr_zero = thm "coshr_zero";
   1.696 +val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
   1.697 +val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
   1.698 +val STAR_exp_epsilon = thm "STAR_exp_epsilon";
   1.699 +val STAR_exp_add = thm "STAR_exp_add";
   1.700 +val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
   1.701 +val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
   1.702 +val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
   1.703 +val starfun_exp_minus = thm "starfun_exp_minus";
   1.704 +val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
   1.705 +val starfun_exp_gt_one = thm "starfun_exp_gt_one";
   1.706 +val starfun_ln_exp = thm "starfun_ln_exp";
   1.707 +val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
   1.708 +val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
   1.709 +val starfun_ln_less_self = thm "starfun_ln_less_self";
   1.710 +val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
   1.711 +val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
   1.712 +val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
   1.713 +val starfun_ln_HFinite = thm "starfun_ln_HFinite";
   1.714 +val starfun_ln_inverse = thm "starfun_ln_inverse";
   1.715 +val starfun_exp_HFinite = thm "starfun_exp_HFinite";
   1.716 +val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
   1.717 +val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
   1.718 +val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
   1.719 +val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
   1.720 +val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
   1.721 +val starfun_ln_less_zero = thm "starfun_ln_less_zero";
   1.722 +val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
   1.723 +val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
   1.724 +val HFinite_sin = thm "HFinite_sin";
   1.725 +val STAR_sin_zero = thm "STAR_sin_zero";
   1.726 +val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
   1.727 +val HFinite_cos = thm "HFinite_cos";
   1.728 +val STAR_cos_zero = thm "STAR_cos_zero";
   1.729 +val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
   1.730 +val STAR_tan_zero = thm "STAR_tan_zero";
   1.731 +val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
   1.732 +val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
   1.733 +val HFinite_pi = thm "HFinite_pi";
   1.734 +val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
   1.735 +val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
   1.736 +val lemma_sin_pi = thm "lemma_sin_pi";
   1.737 +val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
   1.738 +val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
   1.739 +val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
   1.740 +val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
   1.741 +val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
   1.742 +val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
   1.743 +val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
   1.744 +val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
   1.745 +val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
   1.746 +val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
   1.747 +val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
   1.748 +val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
   1.749 +*}
   1.750 +
   1.751 +
   1.752 +end