src/HOL/Nonstandard_Analysis/HTranscendental.thy
changeset 62479 716336f19aa9
parent 61982 3af5a06577c7
child 66453 cc19f7ca2ed6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Mon Feb 29 22:34:36 2016 +0100
     1.3 @@ -0,0 +1,613 @@
     1.4 +(*  Title:      HOL/Nonstandard_Analysis/HTranscendental.thy
     1.5 +    Author:     Jacques D. Fleuriot
     1.6 +    Copyright:  2001 University of Edinburgh
     1.7 +
     1.8 +Converted to Isar and polished by lcp
     1.9 +*)
    1.10 +
    1.11 +section\<open>Nonstandard Extensions of Transcendental Functions\<close>
    1.12 +
    1.13 +theory HTranscendental
    1.14 +imports Transcendental HSeries HDeriv
    1.15 +begin
    1.16 +
    1.17 +definition
    1.18 +  exphr :: "real => hypreal" where
    1.19 +    \<comment>\<open>define exponential function using standard part\<close>
    1.20 +  "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
    1.21 +
    1.22 +definition
    1.23 +  sinhr :: "real => hypreal" where
    1.24 +  "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))"
    1.25 +  
    1.26 +definition
    1.27 +  coshr :: "real => hypreal" where
    1.28 +  "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
    1.29 +
    1.30 +
    1.31 +subsection\<open>Nonstandard Extension of Square Root Function\<close>
    1.32 +
    1.33 +lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
    1.34 +by (simp add: starfun star_n_zero_num)
    1.35 +
    1.36 +lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    1.37 +by (simp add: starfun star_n_one_num)
    1.38 +
    1.39 +lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
    1.40 +apply (cases x)
    1.41 +apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
    1.42 +            simp del: hpowr_Suc power_Suc)
    1.43 +done
    1.44 +
    1.45 +lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    1.46 +by (transfer, simp)
    1.47 +
    1.48 +lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
    1.49 +by (frule hypreal_sqrt_gt_zero_pow2, auto)
    1.50 +
    1.51 +lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
    1.52 +apply (frule hypreal_sqrt_pow2_gt_zero)
    1.53 +apply (auto simp add: numeral_2_eq_2)
    1.54 +done
    1.55 +
    1.56 +lemma hypreal_inverse_sqrt_pow2:
    1.57 +     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    1.58 +apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
    1.59 +apply (auto dest: hypreal_sqrt_gt_zero_pow2)
    1.60 +done
    1.61 +
    1.62 +lemma hypreal_sqrt_mult_distrib: 
    1.63 +    "!!x y. [|0 < x; 0 <y |] ==>
    1.64 +      ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.65 +apply transfer
    1.66 +apply (auto intro: real_sqrt_mult_distrib) 
    1.67 +done
    1.68 +
    1.69 +lemma hypreal_sqrt_mult_distrib2:
    1.70 +     "[|0\<le>x; 0\<le>y |] ==>  
    1.71 +     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.72 +by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
    1.73 +
    1.74 +lemma hypreal_sqrt_approx_zero [simp]:
    1.75 +     "0 < x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
    1.76 +apply (auto simp add: mem_infmal_iff [symmetric])
    1.77 +apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    1.78 +apply (auto intro: Infinitesimal_mult 
    1.79 +            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
    1.80 +            simp add: numeral_2_eq_2)
    1.81 +done
    1.82 +
    1.83 +lemma hypreal_sqrt_approx_zero2 [simp]:
    1.84 +     "0 \<le> x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
    1.85 +by (auto simp add: order_le_less)
    1.86 +
    1.87 +lemma hypreal_sqrt_sum_squares [simp]:
    1.88 +     "(( *f* sqrt)(x*x + y*y + z*z) \<approx> 0) = (x*x + y*y + z*z \<approx> 0)"
    1.89 +apply (rule hypreal_sqrt_approx_zero2)
    1.90 +apply (rule add_nonneg_nonneg)+
    1.91 +apply (auto)
    1.92 +done
    1.93 +
    1.94 +lemma hypreal_sqrt_sum_squares2 [simp]:
    1.95 +     "(( *f* sqrt)(x*x + y*y) \<approx> 0) = (x*x + y*y \<approx> 0)"
    1.96 +apply (rule hypreal_sqrt_approx_zero2)
    1.97 +apply (rule add_nonneg_nonneg)
    1.98 +apply (auto)
    1.99 +done
   1.100 +
   1.101 +lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
   1.102 +apply transfer
   1.103 +apply (auto intro: real_sqrt_gt_zero)
   1.104 +done
   1.105 +
   1.106 +lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
   1.107 +by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   1.108 +
   1.109 +lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
   1.110 +by (transfer, simp)
   1.111 +
   1.112 +lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
   1.113 +by (transfer, simp)
   1.114 +
   1.115 +lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   1.116 +     "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
   1.117 +by (transfer, simp)
   1.118 +
   1.119 +lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
   1.120 +apply (rule HFinite_square_iff [THEN iffD1])
   1.121 +apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
   1.122 +done
   1.123 +
   1.124 +lemma st_hypreal_sqrt:
   1.125 +     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   1.126 +apply (rule power_inject_base [where n=1])
   1.127 +apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
   1.128 +apply (rule st_mult [THEN subst])
   1.129 +apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.130 +apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.131 +apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
   1.132 +done
   1.133 +
   1.134 +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
   1.135 +by transfer (rule real_sqrt_sum_squares_ge1)
   1.136 +
   1.137 +lemma HFinite_hypreal_sqrt:
   1.138 +     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
   1.139 +apply (auto simp add: order_le_less)
   1.140 +apply (rule HFinite_square_iff [THEN iffD1])
   1.141 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.142 +apply (simp add: numeral_2_eq_2)
   1.143 +done
   1.144 +
   1.145 +lemma HFinite_hypreal_sqrt_imp_HFinite:
   1.146 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
   1.147 +apply (auto simp add: order_le_less)
   1.148 +apply (drule HFinite_square_iff [THEN iffD2])
   1.149 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.150 +apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
   1.151 +done
   1.152 +
   1.153 +lemma HFinite_hypreal_sqrt_iff [simp]:
   1.154 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   1.155 +by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
   1.156 +
   1.157 +lemma HFinite_sqrt_sum_squares [simp]:
   1.158 +     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
   1.159 +apply (rule HFinite_hypreal_sqrt_iff)
   1.160 +apply (rule add_nonneg_nonneg)
   1.161 +apply (auto)
   1.162 +done
   1.163 +
   1.164 +lemma Infinitesimal_hypreal_sqrt:
   1.165 +     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
   1.166 +apply (auto simp add: order_le_less)
   1.167 +apply (rule Infinitesimal_square_iff [THEN iffD2])
   1.168 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.169 +apply (simp add: numeral_2_eq_2)
   1.170 +done
   1.171 +
   1.172 +lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
   1.173 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
   1.174 +apply (auto simp add: order_le_less)
   1.175 +apply (drule Infinitesimal_square_iff [THEN iffD1])
   1.176 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.177 +apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
   1.178 +done
   1.179 +
   1.180 +lemma Infinitesimal_hypreal_sqrt_iff [simp]:
   1.181 +     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   1.182 +by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
   1.183 +
   1.184 +lemma Infinitesimal_sqrt_sum_squares [simp]:
   1.185 +     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
   1.186 +apply (rule Infinitesimal_hypreal_sqrt_iff)
   1.187 +apply (rule add_nonneg_nonneg)
   1.188 +apply (auto)
   1.189 +done
   1.190 +
   1.191 +lemma HInfinite_hypreal_sqrt:
   1.192 +     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
   1.193 +apply (auto simp add: order_le_less)
   1.194 +apply (rule HInfinite_square_iff [THEN iffD1])
   1.195 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.196 +apply (simp add: numeral_2_eq_2)
   1.197 +done
   1.198 +
   1.199 +lemma HInfinite_hypreal_sqrt_imp_HInfinite:
   1.200 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
   1.201 +apply (auto simp add: order_le_less)
   1.202 +apply (drule HInfinite_square_iff [THEN iffD2])
   1.203 +apply (drule hypreal_sqrt_gt_zero_pow2)
   1.204 +apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
   1.205 +done
   1.206 +
   1.207 +lemma HInfinite_hypreal_sqrt_iff [simp]:
   1.208 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   1.209 +by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
   1.210 +
   1.211 +lemma HInfinite_sqrt_sum_squares [simp]:
   1.212 +     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
   1.213 +apply (rule HInfinite_hypreal_sqrt_iff)
   1.214 +apply (rule add_nonneg_nonneg)
   1.215 +apply (auto)
   1.216 +done
   1.217 +
   1.218 +lemma HFinite_exp [simp]:
   1.219 +     "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \<in> HFinite"
   1.220 +unfolding sumhr_app
   1.221 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.222 +apply (rule NSBseqD2)
   1.223 +apply (rule NSconvergent_NSBseq)
   1.224 +apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.225 +apply (rule summable_iff_convergent [THEN iffD1])
   1.226 +apply (rule summable_exp)
   1.227 +done
   1.228 +
   1.229 +lemma exphr_zero [simp]: "exphr 0 = 1"
   1.230 +apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
   1.231 +apply (rule st_unique, simp)
   1.232 +apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   1.233 +apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   1.234 +apply (rule_tac x="whn" in spec)
   1.235 +apply (unfold sumhr_app, transfer, simp add: power_0_left)
   1.236 +done
   1.237 +
   1.238 +lemma coshr_zero [simp]: "coshr 0 = 1"
   1.239 +apply (simp add: coshr_def sumhr_split_add
   1.240 +                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   1.241 +apply (rule st_unique, simp)
   1.242 +apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   1.243 +apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   1.244 +apply (rule_tac x="whn" in spec)
   1.245 +apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
   1.246 +done
   1.247 +
   1.248 +lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
   1.249 +apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
   1.250 +apply (transfer, simp)
   1.251 +done
   1.252 +
   1.253 +lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
   1.254 +apply (case_tac "x = 0")
   1.255 +apply (cut_tac [2] x = 0 in DERIV_exp)
   1.256 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.257 +apply (drule_tac x = x in bspec, auto)
   1.258 +apply (drule_tac c = x in approx_mult1)
   1.259 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   1.260 +            simp add: mult.assoc)
   1.261 +apply (rule approx_add_right_cancel [where d="-1"])
   1.262 +apply (rule approx_sym [THEN [2] approx_trans2])
   1.263 +apply (auto simp add: mem_infmal_iff)
   1.264 +done
   1.265 +
   1.266 +lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
   1.267 +by (auto intro: STAR_exp_Infinitesimal)
   1.268 +
   1.269 +lemma STAR_exp_add:
   1.270 +  "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   1.271 +by transfer (rule exp_add)
   1.272 +
   1.273 +lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
   1.274 +apply (simp add: exphr_def)
   1.275 +apply (rule st_unique, simp)
   1.276 +apply (subst starfunNat_sumr [symmetric])
   1.277 +unfolding atLeast0LessThan
   1.278 +apply (rule NSLIMSEQ_D [THEN approx_sym])
   1.279 +apply (rule LIMSEQ_NSLIMSEQ)
   1.280 +apply (subst sums_def [symmetric])
   1.281 +apply (cut_tac exp_converges [where x=x], simp)
   1.282 +apply (rule HNatInfinite_whn)
   1.283 +done
   1.284 +
   1.285 +lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   1.286 +by transfer (rule exp_ge_add_one_self_aux)
   1.287 +
   1.288 +(* exp (oo) is infinite *)
   1.289 +lemma starfun_exp_HInfinite:
   1.290 +     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
   1.291 +apply (frule starfun_exp_ge_add_one_self)
   1.292 +apply (rule HInfinite_ge_HInfinite, assumption)
   1.293 +apply (rule order_trans [of _ "1+x"], auto) 
   1.294 +done
   1.295 +
   1.296 +lemma starfun_exp_minus:
   1.297 +  "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
   1.298 +by transfer (rule exp_minus)
   1.299 +
   1.300 +(* exp (-oo) is infinitesimal *)
   1.301 +lemma starfun_exp_Infinitesimal:
   1.302 +     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   1.303 +apply (subgoal_tac "\<exists>y. x = - y")
   1.304 +apply (rule_tac [2] x = "- x" in exI)
   1.305 +apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
   1.306 +            simp add: starfun_exp_minus HInfinite_minus_iff)
   1.307 +done
   1.308 +
   1.309 +lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
   1.310 +by transfer (rule exp_gt_one)
   1.311 +
   1.312 +abbreviation real_ln :: "real \<Rightarrow> real" where 
   1.313 +  "real_ln \<equiv> ln"
   1.314 +
   1.315 +lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
   1.316 +by transfer (rule ln_exp)
   1.317 +
   1.318 +lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
   1.319 +by transfer (rule exp_ln_iff)
   1.320 +
   1.321 +lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
   1.322 +by transfer (rule ln_unique)
   1.323 +
   1.324 +lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
   1.325 +by transfer (rule ln_less_self)
   1.326 +
   1.327 +lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
   1.328 +by transfer (rule ln_ge_zero)
   1.329 +
   1.330 +lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
   1.331 +by transfer (rule ln_gt_zero)
   1.332 +
   1.333 +lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
   1.334 +by transfer simp
   1.335 +
   1.336 +lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
   1.337 +apply (rule HFinite_bounded)
   1.338 +apply assumption 
   1.339 +apply (simp_all add: starfun_ln_less_self order_less_imp_le)
   1.340 +done
   1.341 +
   1.342 +lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
   1.343 +by transfer (rule ln_inverse)
   1.344 +
   1.345 +lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
   1.346 +by transfer (rule abs_exp_cancel)
   1.347 +
   1.348 +lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
   1.349 +by transfer (rule exp_less_mono)
   1.350 +
   1.351 +lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
   1.352 +apply (auto simp add: HFinite_def, rename_tac u)
   1.353 +apply (rule_tac x="( *f* exp) u" in rev_bexI)
   1.354 +apply (simp add: Reals_eq_Standard)
   1.355 +apply (simp add: starfun_abs_exp_cancel)
   1.356 +apply (simp add: starfun_exp_less_mono)
   1.357 +done
   1.358 +
   1.359 +lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   1.360 +     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
   1.361 +apply (simp add: STAR_exp_add)
   1.362 +apply (frule STAR_exp_Infinitesimal)
   1.363 +apply (drule approx_mult2)
   1.364 +apply (auto intro: starfun_exp_HFinite)
   1.365 +done
   1.366 +
   1.367 +(* using previous result to get to result *)
   1.368 +lemma starfun_ln_HInfinite:
   1.369 +     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   1.370 +apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   1.371 +apply (drule starfun_exp_HFinite)
   1.372 +apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   1.373 +done
   1.374 +
   1.375 +lemma starfun_exp_HInfinite_Infinitesimal_disj:
   1.376 + "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   1.377 +apply (insert linorder_linear [of x 0]) 
   1.378 +apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   1.379 +done
   1.380 +
   1.381 +(* check out this proof!!! *)
   1.382 +lemma starfun_ln_HFinite_not_Infinitesimal:
   1.383 +     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
   1.384 +apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   1.385 +apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   1.386 +apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   1.387 +            del: starfun_exp_ln_iff)
   1.388 +done
   1.389 +
   1.390 +(* we do proof by considering ln of 1/x *)
   1.391 +lemma starfun_ln_Infinitesimal_HInfinite:
   1.392 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   1.393 +apply (drule Infinitesimal_inverse_HInfinite)
   1.394 +apply (frule positive_imp_inverse_positive)
   1.395 +apply (drule_tac [2] starfun_ln_HInfinite)
   1.396 +apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   1.397 +done
   1.398 +
   1.399 +lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
   1.400 +by transfer (rule ln_less_zero)
   1.401 +
   1.402 +lemma starfun_ln_Infinitesimal_less_zero:
   1.403 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
   1.404 +by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   1.405 +
   1.406 +lemma starfun_ln_HInfinite_gt_zero:
   1.407 +     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
   1.408 +by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   1.409 +
   1.410 +
   1.411 +(*
   1.412 +Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
   1.413 +*)
   1.414 +
   1.415 +lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
   1.416 +unfolding sumhr_app
   1.417 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.418 +apply (rule NSBseqD2)
   1.419 +apply (rule NSconvergent_NSBseq)
   1.420 +apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.421 +apply (rule summable_iff_convergent [THEN iffD1])
   1.422 +using summable_norm_sin [of x]
   1.423 +apply (simp add: summable_rabs_cancel)
   1.424 +done
   1.425 +
   1.426 +lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   1.427 +by transfer (rule sin_zero)
   1.428 +
   1.429 +lemma STAR_sin_Infinitesimal [simp]:
   1.430 +  fixes x :: "'a::{real_normed_field,banach} star"
   1.431 +  shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
   1.432 +apply (case_tac "x = 0")
   1.433 +apply (cut_tac [2] x = 0 in DERIV_sin)
   1.434 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.435 +apply (drule bspec [where x = x], auto)
   1.436 +apply (drule approx_mult1 [where c = x])
   1.437 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.438 +           simp add: mult.assoc)
   1.439 +done
   1.440 +
   1.441 +lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
   1.442 +unfolding sumhr_app
   1.443 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.444 +apply (rule NSBseqD2)
   1.445 +apply (rule NSconvergent_NSBseq)
   1.446 +apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.447 +apply (rule summable_iff_convergent [THEN iffD1])
   1.448 +using summable_norm_cos [of x]
   1.449 +apply (simp add: summable_rabs_cancel)
   1.450 +done
   1.451 +
   1.452 +lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   1.453 +by transfer (rule cos_zero)
   1.454 +
   1.455 +lemma STAR_cos_Infinitesimal [simp]:
   1.456 +  fixes x :: "'a::{real_normed_field,banach} star"
   1.457 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
   1.458 +apply (case_tac "x = 0")
   1.459 +apply (cut_tac [2] x = 0 in DERIV_cos)
   1.460 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.461 +apply (drule bspec [where x = x])
   1.462 +apply auto
   1.463 +apply (drule approx_mult1 [where c = x])
   1.464 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.465 +            simp add: mult.assoc)
   1.466 +apply (rule approx_add_right_cancel [where d = "-1"])
   1.467 +apply simp
   1.468 +done
   1.469 +
   1.470 +lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   1.471 +by transfer (rule tan_zero)
   1.472 +
   1.473 +lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
   1.474 +apply (case_tac "x = 0")
   1.475 +apply (cut_tac [2] x = 0 in DERIV_tan)
   1.476 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.477 +apply (drule bspec [where x = x], auto)
   1.478 +apply (drule approx_mult1 [where c = x])
   1.479 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.480 +             simp add: mult.assoc)
   1.481 +done
   1.482 +
   1.483 +lemma STAR_sin_cos_Infinitesimal_mult:
   1.484 +  fixes x :: "'a::{real_normed_field,banach} star"
   1.485 +  shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
   1.486 +using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
   1.487 +by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   1.488 +
   1.489 +lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   1.490 +by simp
   1.491 +
   1.492 +(* lemmas *)
   1.493 +
   1.494 +lemma lemma_split_hypreal_of_real:
   1.495 +     "N \<in> HNatInfinite  
   1.496 +      ==> hypreal_of_real a =  
   1.497 +          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   1.498 +by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
   1.499 +
   1.500 +lemma STAR_sin_Infinitesimal_divide:
   1.501 +  fixes x :: "'a::{real_normed_field,banach} star"
   1.502 +  shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
   1.503 +using DERIV_sin [of "0::'a"]
   1.504 +by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.505 +
   1.506 +(*------------------------------------------------------------------------*) 
   1.507 +(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
   1.508 +(*------------------------------------------------------------------------*)
   1.509 +
   1.510 +lemma lemma_sin_pi:
   1.511 +     "n \<in> HNatInfinite  
   1.512 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
   1.513 +apply (rule STAR_sin_Infinitesimal_divide)
   1.514 +apply (auto simp add: zero_less_HNatInfinite)
   1.515 +done
   1.516 +
   1.517 +lemma STAR_sin_inverse_HNatInfinite:
   1.518 +     "n \<in> HNatInfinite  
   1.519 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
   1.520 +apply (frule lemma_sin_pi)
   1.521 +apply (simp add: divide_inverse)
   1.522 +done
   1.523 +
   1.524 +lemma Infinitesimal_pi_divide_HNatInfinite: 
   1.525 +     "N \<in> HNatInfinite  
   1.526 +      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   1.527 +apply (simp add: divide_inverse)
   1.528 +apply (auto intro: Infinitesimal_HFinite_mult2)
   1.529 +done
   1.530 +
   1.531 +lemma pi_divide_HNatInfinite_not_zero [simp]:
   1.532 +     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   1.533 +by (simp add: zero_less_HNatInfinite)
   1.534 +
   1.535 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   1.536 +     "n \<in> HNatInfinite  
   1.537 +      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   1.538 +          \<approx> hypreal_of_real pi"
   1.539 +apply (frule STAR_sin_Infinitesimal_divide
   1.540 +               [OF Infinitesimal_pi_divide_HNatInfinite 
   1.541 +                   pi_divide_HNatInfinite_not_zero])
   1.542 +apply (auto)
   1.543 +apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   1.544 +apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
   1.545 +done
   1.546 +
   1.547 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   1.548 +     "n \<in> HNatInfinite  
   1.549 +      ==> hypreal_of_hypnat n *  
   1.550 +          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   1.551 +          \<approx> hypreal_of_real pi"
   1.552 +apply (rule mult.commute [THEN subst])
   1.553 +apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   1.554 +done
   1.555 +
   1.556 +lemma starfunNat_pi_divide_n_Infinitesimal: 
   1.557 +     "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
   1.558 +by (auto intro!: Infinitesimal_HFinite_mult2 
   1.559 +         simp add: starfun_mult [symmetric] divide_inverse
   1.560 +                   starfun_inverse [symmetric] starfunNat_real_of_nat)
   1.561 +
   1.562 +lemma STAR_sin_pi_divide_n_approx:
   1.563 +     "N \<in> HNatInfinite ==>  
   1.564 +      ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>  
   1.565 +      hypreal_of_real pi/(hypreal_of_hypnat N)"
   1.566 +apply (simp add: starfunNat_real_of_nat [symmetric])
   1.567 +apply (rule STAR_sin_Infinitesimal)
   1.568 +apply (simp add: divide_inverse)
   1.569 +apply (rule Infinitesimal_HFinite_mult2)
   1.570 +apply (subst starfun_inverse)
   1.571 +apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
   1.572 +apply simp
   1.573 +done
   1.574 +
   1.575 +lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.576 +apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
   1.577 +apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
   1.578 +apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
   1.579 +apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   1.580 +apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   1.581 +            simp add: starfunNat_real_of_nat mult.commute divide_inverse)
   1.582 +done
   1.583 +
   1.584 +lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
   1.585 +apply (simp add: NSLIMSEQ_def, auto)
   1.586 +apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
   1.587 +apply (rule STAR_cos_Infinitesimal)
   1.588 +apply (auto intro!: Infinitesimal_HFinite_mult2 
   1.589 +            simp add: starfun_mult [symmetric] divide_inverse
   1.590 +                      starfun_inverse [symmetric] starfunNat_real_of_nat)
   1.591 +done
   1.592 +
   1.593 +lemma NSLIMSEQ_sin_cos_pi:
   1.594 +     "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.595 +by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   1.596 +
   1.597 +
   1.598 +text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
   1.599 +
   1.600 +lemma STAR_cos_Infinitesimal_approx:
   1.601 +  fixes x :: "'a::{real_normed_field,banach} star"
   1.602 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
   1.603 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.604 +apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   1.605 +            add.assoc [symmetric] numeral_2_eq_2)
   1.606 +done
   1.607 +
   1.608 +lemma STAR_cos_Infinitesimal_approx2:
   1.609 +  fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
   1.610 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
   1.611 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.612 +apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
   1.613 +            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   1.614 +done
   1.615 +
   1.616 +end