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