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