src/HOL/NSA/HTranscendental.thy
 author paulson Sat Apr 11 11:56:40 2015 +0100 (2015-04-11) changeset 60017 b785d6d06430 parent 59730 b7c394c7a619 child 61945 1135b8de26c3 permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
```     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 section{*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 (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\<^sup>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\<^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) @= 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) @= 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 @= 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) @= ( *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) -- 0 --NS> 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 @= 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 @= 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 @= 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 @= 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 @= 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) @= 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)) @= 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 @= 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           @= 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           @= 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) @=
```
```   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)) ----NS> 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))----NS> 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)) ----NS> pi"
```
```   592 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
```
```   593
```
```   594
```
```   595 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
```
```   596
```
```   597 lemma STAR_cos_Infinitesimal_approx:
```
```   598   fixes x :: "'a::{real_normed_field,banach} star"
```
```   599   shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 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  --{*perhaps could be generalised, like many other hypreal results*}
```
```   607   shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 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
```