src/HOL/NSA/HTranscendental.thy
author huffman
Thu Jul 03 17:47:22 2008 +0200 (2008-07-03)
changeset 27468 0783dd1dc13d
child 30273 ecd6f0ca62ea
permissions -rw-r--r--
move nonstandard analysis theories to NSA directory
     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 HSeries HDeriv
    12 begin
    13 
    14 definition
    15   exphr :: "real => hypreal" where
    16     --{*define exponential function using standard part *}
    17   "exphr x =  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
    18 
    19 definition
    20   sinhr :: "real => hypreal" where
    21   "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else
    22              ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
    23   
    24 definition
    25   coshr :: "real => hypreal" where
    26   "coshr x = st(sumhr (0, whn, %n. (if even(n) then
    27             ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
    28 
    29 
    30 subsection{*Nonstandard Extension of Square Root Function*}
    31 
    32 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
    33 by (simp add: starfun star_n_zero_num)
    34 
    35 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    36 by (simp add: starfun star_n_one_num)
    37 
    38 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
    39 apply (cases x)
    40 apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
    41             simp del: hpowr_Suc realpow_Suc)
    42 done
    43 
    44 lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    45 by (transfer, simp)
    46 
    47 lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
    48 by (frule hypreal_sqrt_gt_zero_pow2, auto)
    49 
    50 lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
    51 apply (frule hypreal_sqrt_pow2_gt_zero)
    52 apply (auto simp add: numeral_2_eq_2)
    53 done
    54 
    55 lemma hypreal_inverse_sqrt_pow2:
    56      "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    57 apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
    58 apply (auto dest: hypreal_sqrt_gt_zero_pow2)
    59 done
    60 
    61 lemma hypreal_sqrt_mult_distrib: 
    62     "!!x y. [|0 < x; 0 <y |] ==>
    63       ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    64 apply transfer
    65 apply (auto intro: real_sqrt_mult_distrib) 
    66 done
    67 
    68 lemma hypreal_sqrt_mult_distrib2:
    69      "[|0\<le>x; 0\<le>y |] ==>  
    70      ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    71 by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
    72 
    73 lemma hypreal_sqrt_approx_zero [simp]:
    74      "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    75 apply (auto simp add: mem_infmal_iff [symmetric])
    76 apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    77 apply (auto intro: Infinitesimal_mult 
    78             dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
    79             simp add: numeral_2_eq_2)
    80 done
    81 
    82 lemma hypreal_sqrt_approx_zero2 [simp]:
    83      "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    84 by (auto simp add: order_le_less)
    85 
    86 lemma hypreal_sqrt_sum_squares [simp]:
    87      "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
    88 apply (rule hypreal_sqrt_approx_zero2)
    89 apply (rule add_nonneg_nonneg)+
    90 apply (auto)
    91 done
    92 
    93 lemma hypreal_sqrt_sum_squares2 [simp]:
    94      "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
    95 apply (rule hypreal_sqrt_approx_zero2)
    96 apply (rule add_nonneg_nonneg)
    97 apply (auto)
    98 done
    99 
   100 lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
   101 apply transfer
   102 apply (auto intro: real_sqrt_gt_zero)
   103 done
   104 
   105 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
   106 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   107 
   108 lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)"
   109 by (transfer, simp)
   110 
   111 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
   112 by (transfer, simp)
   113 
   114 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   115      "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
   116 by (transfer, simp)
   117 
   118 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
   119 apply (rule HFinite_square_iff [THEN iffD1])
   120 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
   121 done
   122 
   123 lemma st_hypreal_sqrt:
   124      "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   125 apply (rule power_inject_base [where n=1])
   126 apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
   127 apply (rule st_mult [THEN subst])
   128 apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
   129 apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
   130 apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
   131 done
   132 
   133 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
   134 by transfer (rule real_sqrt_sum_squares_ge1)
   135 
   136 lemma HFinite_hypreal_sqrt:
   137      "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
   138 apply (auto simp add: order_le_less)
   139 apply (rule HFinite_square_iff [THEN iffD1])
   140 apply (drule hypreal_sqrt_gt_zero_pow2)
   141 apply (simp add: numeral_2_eq_2)
   142 done
   143 
   144 lemma HFinite_hypreal_sqrt_imp_HFinite:
   145      "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
   146 apply (auto simp add: order_le_less)
   147 apply (drule HFinite_square_iff [THEN iffD2])
   148 apply (drule hypreal_sqrt_gt_zero_pow2)
   149 apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
   150 done
   151 
   152 lemma HFinite_hypreal_sqrt_iff [simp]:
   153      "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   154 by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
   155 
   156 lemma HFinite_sqrt_sum_squares [simp]:
   157      "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
   158 apply (rule HFinite_hypreal_sqrt_iff)
   159 apply (rule add_nonneg_nonneg)
   160 apply (auto)
   161 done
   162 
   163 lemma Infinitesimal_hypreal_sqrt:
   164      "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
   165 apply (auto simp add: order_le_less)
   166 apply (rule Infinitesimal_square_iff [THEN iffD2])
   167 apply (drule hypreal_sqrt_gt_zero_pow2)
   168 apply (simp add: numeral_2_eq_2)
   169 done
   170 
   171 lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
   172      "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
   173 apply (auto simp add: order_le_less)
   174 apply (drule Infinitesimal_square_iff [THEN iffD1])
   175 apply (drule hypreal_sqrt_gt_zero_pow2)
   176 apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
   177 done
   178 
   179 lemma Infinitesimal_hypreal_sqrt_iff [simp]:
   180      "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   181 by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
   182 
   183 lemma Infinitesimal_sqrt_sum_squares [simp]:
   184      "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
   185 apply (rule Infinitesimal_hypreal_sqrt_iff)
   186 apply (rule add_nonneg_nonneg)
   187 apply (auto)
   188 done
   189 
   190 lemma HInfinite_hypreal_sqrt:
   191      "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
   192 apply (auto simp add: order_le_less)
   193 apply (rule HInfinite_square_iff [THEN iffD1])
   194 apply (drule hypreal_sqrt_gt_zero_pow2)
   195 apply (simp add: numeral_2_eq_2)
   196 done
   197 
   198 lemma HInfinite_hypreal_sqrt_imp_HInfinite:
   199      "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
   200 apply (auto simp add: order_le_less)
   201 apply (drule HInfinite_square_iff [THEN iffD2])
   202 apply (drule hypreal_sqrt_gt_zero_pow2)
   203 apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
   204 done
   205 
   206 lemma HInfinite_hypreal_sqrt_iff [simp]:
   207      "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   208 by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
   209 
   210 lemma HInfinite_sqrt_sum_squares [simp]:
   211      "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
   212 apply (rule HInfinite_hypreal_sqrt_iff)
   213 apply (rule add_nonneg_nonneg)
   214 apply (auto)
   215 done
   216 
   217 lemma HFinite_exp [simp]:
   218      "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
   219 unfolding sumhr_app
   220 apply (simp only: star_zero_def starfun2_star_of)
   221 apply (rule NSBseqD2)
   222 apply (rule NSconvergent_NSBseq)
   223 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   224 apply (rule summable_convergent_sumr_iff [THEN iffD1])
   225 apply (rule summable_exp)
   226 done
   227 
   228 lemma exphr_zero [simp]: "exphr 0 = 1"
   229 apply (simp add: exphr_def sumhr_split_add
   230                    [OF hypnat_one_less_hypnat_omega, symmetric])
   231 apply (rule st_unique, simp)
   232 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   233 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   234 apply (rule_tac x="whn" in spec)
   235 apply (unfold sumhr_app, transfer, simp)
   236 done
   237 
   238 lemma coshr_zero [simp]: "coshr 0 = 1"
   239 apply (simp add: coshr_def sumhr_split_add
   240                    [OF hypnat_one_less_hypnat_omega, symmetric]) 
   241 apply (rule st_unique, simp)
   242 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   243 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   244 apply (rule_tac x="whn" in spec)
   245 apply (unfold sumhr_app, transfer, simp)
   246 done
   247 
   248 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
   249 apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
   250 apply (transfer, simp)
   251 done
   252 
   253 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1"
   254 apply (case_tac "x = 0")
   255 apply (cut_tac [2] x = 0 in DERIV_exp)
   256 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   257 apply (drule_tac x = x in bspec, auto)
   258 apply (drule_tac c = x in approx_mult1)
   259 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   260             simp add: mult_assoc)
   261 apply (rule approx_add_right_cancel [where d="-1"])
   262 apply (rule approx_sym [THEN [2] approx_trans2])
   263 apply (auto simp add: diff_def mem_infmal_iff)
   264 done
   265 
   266 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   267 by (auto intro: STAR_exp_Infinitesimal)
   268 
   269 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   270 by transfer (rule exp_add)
   271 
   272 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
   273 apply (simp add: exphr_def)
   274 apply (rule st_unique, simp)
   275 apply (subst starfunNat_sumr [symmetric])
   276 apply (rule NSLIMSEQ_D [THEN approx_sym])
   277 apply (rule LIMSEQ_NSLIMSEQ)
   278 apply (subst sums_def [symmetric])
   279 apply (cut_tac exp_converges [where x=x], simp)
   280 apply (rule HNatInfinite_whn)
   281 done
   282 
   283 lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   284 by transfer (rule exp_ge_add_one_self_aux)
   285 
   286 (* exp (oo) is infinite *)
   287 lemma starfun_exp_HInfinite:
   288      "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
   289 apply (frule starfun_exp_ge_add_one_self)
   290 apply (rule HInfinite_ge_HInfinite, assumption)
   291 apply (rule order_trans [of _ "1+x"], auto) 
   292 done
   293 
   294 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)"
   295 by transfer (rule exp_minus)
   296 
   297 (* exp (-oo) is infinitesimal *)
   298 lemma starfun_exp_Infinitesimal:
   299      "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   300 apply (subgoal_tac "\<exists>y. x = - y")
   301 apply (rule_tac [2] x = "- x" in exI)
   302 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
   303             simp add: starfun_exp_minus HInfinite_minus_iff)
   304 done
   305 
   306 lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
   307 by transfer (rule exp_gt_one)
   308 
   309 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
   310 by transfer (rule ln_exp)
   311 
   312 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
   313 by transfer (rule exp_ln_iff)
   314 
   315 lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
   316 by transfer (rule exp_ln_eq)
   317 
   318 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
   319 by transfer (rule ln_less_self)
   320 
   321 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
   322 by transfer (rule ln_ge_zero)
   323 
   324 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
   325 by transfer (rule ln_gt_zero)
   326 
   327 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
   328 by transfer simp
   329 
   330 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
   331 apply (rule HFinite_bounded)
   332 apply assumption 
   333 apply (simp_all add: starfun_ln_less_self order_less_imp_le)
   334 done
   335 
   336 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
   337 by transfer (rule ln_inverse)
   338 
   339 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
   340 by transfer (rule abs_exp_cancel)
   341 
   342 lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
   343 by transfer (rule exp_less_mono)
   344 
   345 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
   346 apply (auto simp add: HFinite_def, rename_tac u)
   347 apply (rule_tac x="( *f* exp) u" in rev_bexI)
   348 apply (simp add: Reals_eq_Standard)
   349 apply (simp add: starfun_abs_exp_cancel)
   350 apply (simp add: starfun_exp_less_mono)
   351 done
   352 
   353 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   354      "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z"
   355 apply (simp add: STAR_exp_add)
   356 apply (frule STAR_exp_Infinitesimal)
   357 apply (drule approx_mult2)
   358 apply (auto intro: starfun_exp_HFinite)
   359 done
   360 
   361 (* using previous result to get to result *)
   362 lemma starfun_ln_HInfinite:
   363      "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   364 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   365 apply (drule starfun_exp_HFinite)
   366 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   367 done
   368 
   369 lemma starfun_exp_HInfinite_Infinitesimal_disj:
   370  "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   371 apply (insert linorder_linear [of x 0]) 
   372 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   373 done
   374 
   375 (* check out this proof!!! *)
   376 lemma starfun_ln_HFinite_not_Infinitesimal:
   377      "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
   378 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   379 apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   380 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   381             del: starfun_exp_ln_iff)
   382 done
   383 
   384 (* we do proof by considering ln of 1/x *)
   385 lemma starfun_ln_Infinitesimal_HInfinite:
   386      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   387 apply (drule Infinitesimal_inverse_HInfinite)
   388 apply (frule positive_imp_inverse_positive)
   389 apply (drule_tac [2] starfun_ln_HInfinite)
   390 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   391 done
   392 
   393 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
   394 by transfer (rule ln_less_zero)
   395 
   396 lemma starfun_ln_Infinitesimal_less_zero:
   397      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
   398 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   399 
   400 lemma starfun_ln_HInfinite_gt_zero:
   401      "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
   402 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   403 
   404 
   405 (*
   406 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
   407 *)
   408 
   409 lemma HFinite_sin [simp]:
   410      "sumhr (0, whn, %n. (if even(n) then 0 else  
   411               (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
   412               \<in> HFinite"
   413 unfolding sumhr_app
   414 apply (simp only: star_zero_def starfun2_star_of)
   415 apply (rule NSBseqD2)
   416 apply (rule NSconvergent_NSBseq)
   417 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   418 apply (rule summable_convergent_sumr_iff [THEN iffD1])
   419 apply (simp only: One_nat_def summable_sin)
   420 done
   421 
   422 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   423 by transfer (rule sin_zero)
   424 
   425 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
   426 apply (case_tac "x = 0")
   427 apply (cut_tac [2] x = 0 in DERIV_sin)
   428 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   429 apply (drule bspec [where x = x], auto)
   430 apply (drule approx_mult1 [where c = x])
   431 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   432            simp add: mult_assoc)
   433 done
   434 
   435 lemma HFinite_cos [simp]:
   436      "sumhr (0, whn, %n. (if even(n) then  
   437             (-1 ^ (n div 2))/(real (fact n)) else  
   438             0) * x ^ n) \<in> HFinite"
   439 unfolding sumhr_app
   440 apply (simp only: star_zero_def starfun2_star_of)
   441 apply (rule NSBseqD2)
   442 apply (rule NSconvergent_NSBseq)
   443 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   444 apply (rule summable_convergent_sumr_iff [THEN iffD1])
   445 apply (rule summable_cos)
   446 done
   447 
   448 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   449 by transfer (rule cos_zero)
   450 
   451 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
   452 apply (case_tac "x = 0")
   453 apply (cut_tac [2] x = 0 in DERIV_cos)
   454 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   455 apply (drule bspec [where x = x])
   456 apply auto
   457 apply (drule approx_mult1 [where c = x])
   458 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   459             simp add: mult_assoc)
   460 apply (rule approx_add_right_cancel [where d = "-1"])
   461 apply (simp add: diff_def)
   462 done
   463 
   464 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   465 by transfer (rule tan_zero)
   466 
   467 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
   468 apply (case_tac "x = 0")
   469 apply (cut_tac [2] x = 0 in DERIV_tan)
   470 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   471 apply (drule bspec [where x = x], auto)
   472 apply (drule approx_mult1 [where c = x])
   473 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   474              simp add: mult_assoc)
   475 done
   476 
   477 lemma STAR_sin_cos_Infinitesimal_mult:
   478      "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
   479 apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) 
   480 apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   481 done
   482 
   483 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   484 by simp
   485 
   486 (* lemmas *)
   487 
   488 lemma lemma_split_hypreal_of_real:
   489      "N \<in> HNatInfinite  
   490       ==> hypreal_of_real a =  
   491           hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   492 by (simp add: mult_assoc [symmetric] zero_less_HNatInfinite)
   493 
   494 lemma STAR_sin_Infinitesimal_divide:
   495      "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
   496 apply (cut_tac x = 0 in DERIV_sin)
   497 apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   498 done
   499 
   500 (*------------------------------------------------------------------------*) 
   501 (* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
   502 (*------------------------------------------------------------------------*)
   503 
   504 lemma lemma_sin_pi:
   505      "n \<in> HNatInfinite  
   506       ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
   507 apply (rule STAR_sin_Infinitesimal_divide)
   508 apply (auto simp add: zero_less_HNatInfinite)
   509 done
   510 
   511 lemma STAR_sin_inverse_HNatInfinite:
   512      "n \<in> HNatInfinite  
   513       ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
   514 apply (frule lemma_sin_pi)
   515 apply (simp add: divide_inverse)
   516 done
   517 
   518 lemma Infinitesimal_pi_divide_HNatInfinite: 
   519      "N \<in> HNatInfinite  
   520       ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   521 apply (simp add: divide_inverse)
   522 apply (auto intro: Infinitesimal_HFinite_mult2)
   523 done
   524 
   525 lemma pi_divide_HNatInfinite_not_zero [simp]:
   526      "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   527 by (simp add: zero_less_HNatInfinite)
   528 
   529 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   530      "n \<in> HNatInfinite  
   531       ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   532           @= hypreal_of_real pi"
   533 apply (frule STAR_sin_Infinitesimal_divide
   534                [OF Infinitesimal_pi_divide_HNatInfinite 
   535                    pi_divide_HNatInfinite_not_zero])
   536 apply (auto)
   537 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   538 apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac)
   539 done
   540 
   541 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   542      "n \<in> HNatInfinite  
   543       ==> hypreal_of_hypnat n *  
   544           ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   545           @= hypreal_of_real pi"
   546 apply (rule mult_commute [THEN subst])
   547 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   548 done
   549 
   550 lemma starfunNat_pi_divide_n_Infinitesimal: 
   551      "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
   552 by (auto intro!: Infinitesimal_HFinite_mult2 
   553          simp add: starfun_mult [symmetric] divide_inverse
   554                    starfun_inverse [symmetric] starfunNat_real_of_nat)
   555 
   556 lemma STAR_sin_pi_divide_n_approx:
   557      "N \<in> HNatInfinite ==>  
   558       ( *f* sin) (( *f* (%x. pi / real x)) N) @=  
   559       hypreal_of_real pi/(hypreal_of_hypnat N)"
   560 apply (simp add: starfunNat_real_of_nat [symmetric])
   561 apply (rule STAR_sin_Infinitesimal)
   562 apply (simp add: divide_inverse)
   563 apply (rule Infinitesimal_HFinite_mult2)
   564 apply (subst starfun_inverse)
   565 apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
   566 apply simp
   567 done
   568 
   569 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
   570 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
   571 apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
   572 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
   573 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   574 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   575             simp add: starfunNat_real_of_nat mult_commute divide_inverse)
   576 done
   577 
   578 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
   579 apply (simp add: NSLIMSEQ_def, auto)
   580 apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
   581 apply (rule STAR_cos_Infinitesimal)
   582 apply (auto intro!: Infinitesimal_HFinite_mult2 
   583             simp add: starfun_mult [symmetric] divide_inverse
   584                       starfun_inverse [symmetric] starfunNat_real_of_nat)
   585 done
   586 
   587 lemma NSLIMSEQ_sin_cos_pi:
   588      "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
   589 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   590 
   591 
   592 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
   593 
   594 lemma STAR_cos_Infinitesimal_approx:
   595      "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
   596 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   597 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   598             diff_minus add_assoc [symmetric] numeral_2_eq_2)
   599 done
   600 
   601 lemma STAR_cos_Infinitesimal_approx2:
   602      "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
   603 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   604 apply (auto intro: Infinitesimal_SReal_divide 
   605             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   606 done
   607 
   608 end