src/HOL/Nonstandard_Analysis/HTranscendental.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (20 months ago)
changeset 67006 b1278ed3cd46
parent 66453 cc19f7ca2ed6
child 67091 1393c2340eec
permissions -rw-r--r--
prefer main entry points of HOL;
     1 (*  Title:      HOL/Nonstandard_Analysis/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 section\<open>Nonstandard Extensions of Transcendental Functions\<close>
     9 
    10 theory HTranscendental
    11 imports Complex_Main HSeries HDeriv
    12 begin
    13 
    14 definition
    15   exphr :: "real => hypreal" where
    16     \<comment>\<open>define exponential function using standard part\<close>
    17   "exphr x =  st(sumhr (0, whn, %n. inverse (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\<open>Nonstandard Extension of Square Root Function\<close>
    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) \<approx> 0) = (x \<approx> 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) \<approx> 0) = (x \<approx> 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) \<approx> 0) = (x*x + y*y + z*z \<approx> 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) \<approx> 0) = (x*x + y*y \<approx> 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\<^sup>2) = \<bar>x\<bar>"
   107 by (transfer, simp)
   108 
   109 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
   110 by (transfer, simp)
   111 
   112 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   113      "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
   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\<^sup>2 + y\<^sup>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 (fact n) * x ^ n) \<in> HFinite"
   217 unfolding sumhr_app
   218 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   219 apply (rule NSBseqD2)
   220 apply (rule NSconvergent_NSBseq)
   221 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   222 apply (rule summable_iff_convergent [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 [OF hypnat_one_less_hypnat_omega, symmetric])
   228 apply (rule st_unique, simp)
   229 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   230 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   231 apply (rule_tac x="whn" in spec)
   232 apply (unfold sumhr_app, transfer, simp add: power_0_left)
   233 done
   234 
   235 lemma coshr_zero [simp]: "coshr 0 = 1"
   236 apply (simp add: coshr_def sumhr_split_add
   237                    [OF hypnat_one_less_hypnat_omega, symmetric]) 
   238 apply (rule st_unique, simp)
   239 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   240 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   241 apply (rule_tac x="whn" in spec)
   242 apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
   243 done
   244 
   245 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
   246 apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
   247 apply (transfer, simp)
   248 done
   249 
   250 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
   251 apply (case_tac "x = 0")
   252 apply (cut_tac [2] x = 0 in DERIV_exp)
   253 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   254 apply (drule_tac x = x in bspec, auto)
   255 apply (drule_tac c = x in approx_mult1)
   256 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   257             simp add: mult.assoc)
   258 apply (rule approx_add_right_cancel [where d="-1"])
   259 apply (rule approx_sym [THEN [2] approx_trans2])
   260 apply (auto simp add: mem_infmal_iff)
   261 done
   262 
   263 lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
   264 by (auto intro: STAR_exp_Infinitesimal)
   265 
   266 lemma STAR_exp_add:
   267   "!!(x::'a:: {banach,real_normed_field} star) 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 unfolding atLeast0LessThan
   275 apply (rule NSLIMSEQ_D [THEN approx_sym])
   276 apply (rule LIMSEQ_NSLIMSEQ)
   277 apply (subst sums_def [symmetric])
   278 apply (cut_tac exp_converges [where x=x], simp)
   279 apply (rule HNatInfinite_whn)
   280 done
   281 
   282 lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   283 by transfer (rule exp_ge_add_one_self_aux)
   284 
   285 (* exp (oo) is infinite *)
   286 lemma starfun_exp_HInfinite:
   287      "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
   288 apply (frule starfun_exp_ge_add_one_self)
   289 apply (rule HInfinite_ge_HInfinite, assumption)
   290 apply (rule order_trans [of _ "1+x"], auto) 
   291 done
   292 
   293 lemma starfun_exp_minus:
   294   "!!x::'a:: {banach,real_normed_field} star. ( *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 abbreviation real_ln :: "real \<Rightarrow> real" where 
   310   "real_ln \<equiv> ln"
   311 
   312 lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
   313 by transfer (rule ln_exp)
   314 
   315 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
   316 by transfer (rule exp_ln_iff)
   317 
   318 lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
   319 by transfer (rule ln_unique)
   320 
   321 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
   322 by transfer (rule ln_less_self)
   323 
   324 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
   325 by transfer (rule ln_ge_zero)
   326 
   327 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
   328 by transfer (rule ln_gt_zero)
   329 
   330 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
   331 by transfer simp
   332 
   333 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
   334 apply (rule HFinite_bounded)
   335 apply assumption 
   336 apply (simp_all add: starfun_ln_less_self order_less_imp_le)
   337 done
   338 
   339 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
   340 by transfer (rule ln_inverse)
   341 
   342 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
   343 by transfer (rule abs_exp_cancel)
   344 
   345 lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
   346 by transfer (rule exp_less_mono)
   347 
   348 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
   349 apply (auto simp add: HFinite_def, rename_tac u)
   350 apply (rule_tac x="( *f* exp) u" in rev_bexI)
   351 apply (simp add: Reals_eq_Standard)
   352 apply (simp add: starfun_abs_exp_cancel)
   353 apply (simp add: starfun_exp_less_mono)
   354 done
   355 
   356 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   357      "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
   358 apply (simp add: STAR_exp_add)
   359 apply (frule STAR_exp_Infinitesimal)
   360 apply (drule approx_mult2)
   361 apply (auto intro: starfun_exp_HFinite)
   362 done
   363 
   364 (* using previous result to get to result *)
   365 lemma starfun_ln_HInfinite:
   366      "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   367 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   368 apply (drule starfun_exp_HFinite)
   369 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   370 done
   371 
   372 lemma starfun_exp_HInfinite_Infinitesimal_disj:
   373  "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   374 apply (insert linorder_linear [of x 0]) 
   375 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   376 done
   377 
   378 (* check out this proof!!! *)
   379 lemma starfun_ln_HFinite_not_Infinitesimal:
   380      "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
   381 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   382 apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   383 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   384             del: starfun_exp_ln_iff)
   385 done
   386 
   387 (* we do proof by considering ln of 1/x *)
   388 lemma starfun_ln_Infinitesimal_HInfinite:
   389      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   390 apply (drule Infinitesimal_inverse_HInfinite)
   391 apply (frule positive_imp_inverse_positive)
   392 apply (drule_tac [2] starfun_ln_HInfinite)
   393 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   394 done
   395 
   396 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
   397 by transfer (rule ln_less_zero)
   398 
   399 lemma starfun_ln_Infinitesimal_less_zero:
   400      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
   401 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   402 
   403 lemma starfun_ln_HInfinite_gt_zero:
   404      "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
   405 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   406 
   407 
   408 (*
   409 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
   410 *)
   411 
   412 lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
   413 unfolding sumhr_app
   414 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   415 apply (rule NSBseqD2)
   416 apply (rule NSconvergent_NSBseq)
   417 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   418 apply (rule summable_iff_convergent [THEN iffD1])
   419 using summable_norm_sin [of x]
   420 apply (simp add: summable_rabs_cancel)
   421 done
   422 
   423 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   424 by transfer (rule sin_zero)
   425 
   426 lemma STAR_sin_Infinitesimal [simp]:
   427   fixes x :: "'a::{real_normed_field,banach} star"
   428   shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
   429 apply (case_tac "x = 0")
   430 apply (cut_tac [2] x = 0 in DERIV_sin)
   431 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   432 apply (drule bspec [where x = x], auto)
   433 apply (drule approx_mult1 [where c = x])
   434 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   435            simp add: mult.assoc)
   436 done
   437 
   438 lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
   439 unfolding sumhr_app
   440 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   441 apply (rule NSBseqD2)
   442 apply (rule NSconvergent_NSBseq)
   443 apply (rule convergent_NSconvergent_iff [THEN iffD1])
   444 apply (rule summable_iff_convergent [THEN iffD1])
   445 using summable_norm_cos [of x]
   446 apply (simp add: summable_rabs_cancel)
   447 done
   448 
   449 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   450 by transfer (rule cos_zero)
   451 
   452 lemma STAR_cos_Infinitesimal [simp]:
   453   fixes x :: "'a::{real_normed_field,banach} star"
   454   shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
   455 apply (case_tac "x = 0")
   456 apply (cut_tac [2] x = 0 in DERIV_cos)
   457 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   458 apply (drule bspec [where x = x])
   459 apply auto
   460 apply (drule approx_mult1 [where c = x])
   461 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   462             simp add: mult.assoc)
   463 apply (rule approx_add_right_cancel [where d = "-1"])
   464 apply simp
   465 done
   466 
   467 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   468 by transfer (rule tan_zero)
   469 
   470 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
   471 apply (case_tac "x = 0")
   472 apply (cut_tac [2] x = 0 in DERIV_tan)
   473 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   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 STAR_sin_cos_Infinitesimal_mult:
   481   fixes x :: "'a::{real_normed_field,banach} star"
   482   shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
   483 using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
   484 by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   485 
   486 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   487 by simp
   488 
   489 (* lemmas *)
   490 
   491 lemma lemma_split_hypreal_of_real:
   492      "N \<in> HNatInfinite  
   493       ==> hypreal_of_real a =  
   494           hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   495 by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
   496 
   497 lemma STAR_sin_Infinitesimal_divide:
   498   fixes x :: "'a::{real_normed_field,banach} star"
   499   shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
   500 using DERIV_sin [of "0::'a"]
   501 by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   502 
   503 (*------------------------------------------------------------------------*) 
   504 (* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
   505 (*------------------------------------------------------------------------*)
   506 
   507 lemma lemma_sin_pi:
   508      "n \<in> HNatInfinite  
   509       ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
   510 apply (rule STAR_sin_Infinitesimal_divide)
   511 apply (auto simp add: zero_less_HNatInfinite)
   512 done
   513 
   514 lemma STAR_sin_inverse_HNatInfinite:
   515      "n \<in> HNatInfinite  
   516       ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
   517 apply (frule lemma_sin_pi)
   518 apply (simp add: divide_inverse)
   519 done
   520 
   521 lemma Infinitesimal_pi_divide_HNatInfinite: 
   522      "N \<in> HNatInfinite  
   523       ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   524 apply (simp add: divide_inverse)
   525 apply (auto intro: Infinitesimal_HFinite_mult2)
   526 done
   527 
   528 lemma pi_divide_HNatInfinite_not_zero [simp]:
   529      "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   530 by (simp add: zero_less_HNatInfinite)
   531 
   532 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   533      "n \<in> HNatInfinite  
   534       ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   535           \<approx> hypreal_of_real pi"
   536 apply (frule STAR_sin_Infinitesimal_divide
   537                [OF Infinitesimal_pi_divide_HNatInfinite 
   538                    pi_divide_HNatInfinite_not_zero])
   539 apply (auto)
   540 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   541 apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
   542 done
   543 
   544 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   545      "n \<in> HNatInfinite  
   546       ==> hypreal_of_hypnat n *  
   547           ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   548           \<approx> hypreal_of_real pi"
   549 apply (rule mult.commute [THEN subst])
   550 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   551 done
   552 
   553 lemma starfunNat_pi_divide_n_Infinitesimal: 
   554      "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
   555 by (auto intro!: Infinitesimal_HFinite_mult2 
   556          simp add: starfun_mult [symmetric] divide_inverse
   557                    starfun_inverse [symmetric] starfunNat_real_of_nat)
   558 
   559 lemma STAR_sin_pi_divide_n_approx:
   560      "N \<in> HNatInfinite ==>  
   561       ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>  
   562       hypreal_of_real pi/(hypreal_of_hypnat N)"
   563 apply (simp add: starfunNat_real_of_nat [symmetric])
   564 apply (rule STAR_sin_Infinitesimal)
   565 apply (simp add: divide_inverse)
   566 apply (rule Infinitesimal_HFinite_mult2)
   567 apply (subst starfun_inverse)
   568 apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
   569 apply simp
   570 done
   571 
   572 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   573 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
   574 apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
   575 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
   576 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   577 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   578             simp add: starfunNat_real_of_nat mult.commute divide_inverse)
   579 done
   580 
   581 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
   582 apply (simp add: NSLIMSEQ_def, auto)
   583 apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
   584 apply (rule STAR_cos_Infinitesimal)
   585 apply (auto intro!: Infinitesimal_HFinite_mult2 
   586             simp add: starfun_mult [symmetric] divide_inverse
   587                       starfun_inverse [symmetric] starfunNat_real_of_nat)
   588 done
   589 
   590 lemma NSLIMSEQ_sin_cos_pi:
   591      "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   592 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   593 
   594 
   595 text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
   596 
   597 lemma STAR_cos_Infinitesimal_approx:
   598   fixes x :: "'a::{real_normed_field,banach} star"
   599   shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
   600 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   601 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   602             add.assoc [symmetric] numeral_2_eq_2)
   603 done
   604 
   605 lemma STAR_cos_Infinitesimal_approx2:
   606   fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
   607   shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
   608 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   609 apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
   610             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   611 done
   612 
   613 end