merged
authorpaulson
Mon Apr 29 00:36:54 2019 +0100 (6 months ago)
changeset 702112388e0d2827b
parent 70207 511352b4d5d3
parent 70210 1ececb77b27a
child 70213 ff8386fc191d
child 70221 bca14283e1a8
merged
     1.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sun Apr 28 22:22:29 2019 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Mon Apr 29 00:36:54 2019 +0100
     1.3 @@ -12,602 +12,524 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  exphr :: "real => hypreal" where
     1.8 +  exphr :: "real \<Rightarrow> hypreal" where
     1.9      \<comment> \<open>define exponential function using standard part\<close>
    1.10 -  "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
    1.11 +  "exphr x \<equiv>  st(sumhr (0, whn, \<lambda>n. inverse (fact n) * (x ^ n)))"
    1.12  
    1.13  definition
    1.14 -  sinhr :: "real => hypreal" where
    1.15 -  "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))"
    1.16 +  sinhr :: "real \<Rightarrow> hypreal" where
    1.17 +  "sinhr x \<equiv> st(sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n))"
    1.18    
    1.19  definition
    1.20 -  coshr :: "real => hypreal" where
    1.21 -  "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
    1.22 +  coshr :: "real \<Rightarrow> hypreal" where
    1.23 +  "coshr x \<equiv> st(sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n))"
    1.24  
    1.25  
    1.26  subsection\<open>Nonstandard Extension of Square Root Function\<close>
    1.27  
    1.28  lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
    1.29 -by (simp add: starfun star_n_zero_num)
    1.30 +  by (simp add: starfun star_n_zero_num)
    1.31  
    1.32  lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    1.33 -by (simp add: starfun star_n_one_num)
    1.34 +  by (simp add: starfun star_n_one_num)
    1.35  
    1.36  lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
    1.37 -apply (cases x)
    1.38 -apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
    1.39 -            simp del: hpowr_Suc power_Suc)
    1.40 -done
    1.41 -
    1.42 -lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    1.43 -by (transfer, simp)
    1.44 +proof (cases x)
    1.45 +  case (star_n X)
    1.46 +  then show ?thesis
    1.47 +    by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc)
    1.48 +qed
    1.49  
    1.50 -lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
    1.51 -by (frule hypreal_sqrt_gt_zero_pow2, auto)
    1.52 +lemma hypreal_sqrt_gt_zero_pow2: "\<And>x. 0 < x \<Longrightarrow> ( *f* sqrt) (x) ^ 2 = x"
    1.53 +  by transfer simp
    1.54  
    1.55 -lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
    1.56 -apply (frule hypreal_sqrt_pow2_gt_zero)
    1.57 -apply (auto simp add: numeral_2_eq_2)
    1.58 -done
    1.59 +lemma hypreal_sqrt_pow2_gt_zero: "0 < x \<Longrightarrow> 0 < ( *f* sqrt) (x) ^ 2"
    1.60 +  by (frule hypreal_sqrt_gt_zero_pow2, auto)
    1.61 +
    1.62 +lemma hypreal_sqrt_not_zero: "0 < x \<Longrightarrow> ( *f* sqrt) (x) \<noteq> 0"
    1.63 +  using hypreal_sqrt_gt_zero_pow2 by fastforce
    1.64  
    1.65  lemma hypreal_inverse_sqrt_pow2:
    1.66 -     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    1.67 -apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
    1.68 -apply (auto dest: hypreal_sqrt_gt_zero_pow2)
    1.69 -done
    1.70 +     "0 < x \<Longrightarrow> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    1.71 +  by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse)
    1.72  
    1.73  lemma hypreal_sqrt_mult_distrib: 
    1.74 -    "!!x y. [|0 < x; 0 <y |] ==>
    1.75 +    "\<And>x y. \<lbrakk>0 < x; 0 <y\<rbrakk> \<Longrightarrow>
    1.76        ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.77 -apply transfer
    1.78 -apply (auto intro: real_sqrt_mult) 
    1.79 -done
    1.80 +  by transfer (auto intro: real_sqrt_mult) 
    1.81  
    1.82  lemma hypreal_sqrt_mult_distrib2:
    1.83 -     "[|0\<le>x; 0\<le>y |] ==>  
    1.84 -     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.85 +     "\<lbrakk>0\<le>x; 0\<le>y\<rbrakk> \<Longrightarrow>  ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.86  by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
    1.87  
    1.88  lemma hypreal_sqrt_approx_zero [simp]:
    1.89 -     "0 < x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
    1.90 -apply (auto simp add: mem_infmal_iff [symmetric])
    1.91 -apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    1.92 -apply (auto intro: Infinitesimal_mult 
    1.93 -            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
    1.94 -            simp add: numeral_2_eq_2)
    1.95 -done
    1.96 +  assumes "0 < x"
    1.97 +  shows "(( *f* sqrt) x \<approx> 0) \<longleftrightarrow> (x \<approx> 0)"
    1.98 +proof -
    1.99 +  have "( *f* sqrt) x \<in> Infinitesimal \<longleftrightarrow> ((*f* sqrt) x)\<^sup>2 \<in> Infinitesimal"
   1.100 +    by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff)
   1.101 +  also have "... \<longleftrightarrow> x \<in> Infinitesimal"
   1.102 +    by (simp add: assms hypreal_sqrt_gt_zero_pow2)
   1.103 +  finally show ?thesis
   1.104 +    using mem_infmal_iff by blast
   1.105 +qed
   1.106  
   1.107  lemma hypreal_sqrt_approx_zero2 [simp]:
   1.108 -     "0 \<le> x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
   1.109 -by (auto simp add: order_le_less)
   1.110 +  "0 \<le> x \<Longrightarrow> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
   1.111 +  by (auto simp add: order_le_less)
   1.112  
   1.113 -lemma hypreal_sqrt_sum_squares [simp]:
   1.114 -     "(( *f* sqrt)(x*x + y*y + z*z) \<approx> 0) = (x*x + y*y + z*z \<approx> 0)"
   1.115 -apply (rule hypreal_sqrt_approx_zero2)
   1.116 -apply (rule add_nonneg_nonneg)+
   1.117 -apply (auto)
   1.118 -done
   1.119 +lemma hypreal_sqrt_gt_zero: "\<And>x. 0 < x \<Longrightarrow> 0 < ( *f* sqrt)(x)"
   1.120 +  by transfer (simp add: real_sqrt_gt_zero)
   1.121  
   1.122 -lemma hypreal_sqrt_sum_squares2 [simp]:
   1.123 -     "(( *f* sqrt)(x*x + y*y) \<approx> 0) = (x*x + y*y \<approx> 0)"
   1.124 -apply (rule hypreal_sqrt_approx_zero2)
   1.125 -apply (rule add_nonneg_nonneg)
   1.126 -apply (auto)
   1.127 -done
   1.128 +lemma hypreal_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt)(x)"
   1.129 +  by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   1.130  
   1.131 -lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
   1.132 -apply transfer
   1.133 -apply (auto intro: real_sqrt_gt_zero)
   1.134 -done
   1.135 +lemma hypreal_sqrt_hrabs [simp]: "\<And>x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
   1.136 +  by transfer simp
   1.137  
   1.138 -lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
   1.139 -by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   1.140 -
   1.141 -lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
   1.142 -by (transfer, simp)
   1.143 -
   1.144 -lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
   1.145 -by (transfer, simp)
   1.146 +lemma hypreal_sqrt_hrabs2 [simp]: "\<And>x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
   1.147 +  by transfer simp
   1.148  
   1.149  lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   1.150 -     "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
   1.151 -by (transfer, simp)
   1.152 +  "\<And>x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
   1.153 +  by transfer simp
   1.154  
   1.155  lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
   1.156 -apply (rule HFinite_square_iff [THEN iffD1])
   1.157 -apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
   1.158 -done
   1.159 +  by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square)
   1.160  
   1.161  lemma st_hypreal_sqrt:
   1.162 -     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   1.163 -apply (rule power_inject_base [where n=1])
   1.164 -apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
   1.165 -apply (rule st_mult [THEN subst])
   1.166 -apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.167 -apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
   1.168 -apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
   1.169 -done
   1.170 +  assumes "x \<in> HFinite" "0 \<le> x"
   1.171 +  shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   1.172 +proof (rule power_inject_base)
   1.173 +  show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1"
   1.174 +    using assms hypreal_sqrt_pow2_iff [of x]
   1.175 +    by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult)
   1.176 +  show "0 \<le> st ((*f* sqrt) x)"
   1.177 +    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite)
   1.178 +  show "0 \<le> (*f* sqrt) (st x)"
   1.179 +    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le)
   1.180 +qed
   1.181  
   1.182 -lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
   1.183 -by transfer (rule real_sqrt_sum_squares_ge1)
   1.184 -
   1.185 -lemma HFinite_hypreal_sqrt:
   1.186 -     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
   1.187 -apply (auto simp add: order_le_less)
   1.188 -apply (rule HFinite_square_iff [THEN iffD1])
   1.189 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.190 -apply (simp add: numeral_2_eq_2)
   1.191 -done
   1.192 +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\<And>x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
   1.193 +  by transfer (rule real_sqrt_sum_squares_ge1)
   1.194  
   1.195  lemma HFinite_hypreal_sqrt_imp_HFinite:
   1.196 -     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
   1.197 -apply (auto simp add: order_le_less)
   1.198 -apply (drule HFinite_square_iff [THEN iffD2])
   1.199 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.200 -apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
   1.201 -done
   1.202 +  "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HFinite\<rbrakk> \<Longrightarrow> x \<in> HFinite"
   1.203 +  by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2)
   1.204  
   1.205  lemma HFinite_hypreal_sqrt_iff [simp]:
   1.206 -     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   1.207 -by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
   1.208 -
   1.209 -lemma HFinite_sqrt_sum_squares [simp]:
   1.210 -     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
   1.211 -apply (rule HFinite_hypreal_sqrt_iff)
   1.212 -apply (rule add_nonneg_nonneg)
   1.213 -apply (auto)
   1.214 -done
   1.215 +  "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   1.216 +  by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite)
   1.217  
   1.218  lemma Infinitesimal_hypreal_sqrt:
   1.219 -     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
   1.220 -apply (auto simp add: order_le_less)
   1.221 -apply (rule Infinitesimal_square_iff [THEN iffD2])
   1.222 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.223 -apply (simp add: numeral_2_eq_2)
   1.224 -done
   1.225 +     "\<lbrakk>0 \<le> x; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
   1.226 +  by (simp add: mem_infmal_iff)
   1.227  
   1.228  lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
   1.229 -     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
   1.230 -apply (auto simp add: order_le_less)
   1.231 -apply (drule Infinitesimal_square_iff [THEN iffD1])
   1.232 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.233 -apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
   1.234 -done
   1.235 +     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
   1.236 +  using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast
   1.237  
   1.238  lemma Infinitesimal_hypreal_sqrt_iff [simp]:
   1.239 -     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   1.240 +     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   1.241  by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
   1.242  
   1.243 -lemma Infinitesimal_sqrt_sum_squares [simp]:
   1.244 -     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
   1.245 -apply (rule Infinitesimal_hypreal_sqrt_iff)
   1.246 -apply (rule add_nonneg_nonneg)
   1.247 -apply (auto)
   1.248 -done
   1.249 -
   1.250  lemma HInfinite_hypreal_sqrt:
   1.251 -     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
   1.252 -apply (auto simp add: order_le_less)
   1.253 -apply (rule HInfinite_square_iff [THEN iffD1])
   1.254 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.255 -apply (simp add: numeral_2_eq_2)
   1.256 -done
   1.257 +     "\<lbrakk>0 \<le> x; x \<in> HInfinite\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HInfinite"
   1.258 +  by (simp add: HInfinite_HFinite_iff)
   1.259  
   1.260  lemma HInfinite_hypreal_sqrt_imp_HInfinite:
   1.261 -     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
   1.262 -apply (auto simp add: order_le_less)
   1.263 -apply (drule HInfinite_square_iff [THEN iffD2])
   1.264 -apply (drule hypreal_sqrt_gt_zero_pow2)
   1.265 -apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
   1.266 -done
   1.267 +     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HInfinite\<rbrakk> \<Longrightarrow> x \<in> HInfinite"
   1.268 +  using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast
   1.269  
   1.270  lemma HInfinite_hypreal_sqrt_iff [simp]:
   1.271 -     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   1.272 +     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   1.273  by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
   1.274  
   1.275 -lemma HInfinite_sqrt_sum_squares [simp]:
   1.276 -     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
   1.277 -apply (rule HInfinite_hypreal_sqrt_iff)
   1.278 -apply (rule add_nonneg_nonneg)
   1.279 -apply (auto)
   1.280 -done
   1.281 -
   1.282  lemma HFinite_exp [simp]:
   1.283 -     "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \<in> HFinite"
   1.284 -unfolding sumhr_app
   1.285 -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.286 -apply (rule NSBseqD2)
   1.287 -apply (rule NSconvergent_NSBseq)
   1.288 -apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.289 -apply (rule summable_iff_convergent [THEN iffD1])
   1.290 -apply (rule summable_exp)
   1.291 -done
   1.292 +  "sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n) \<in> HFinite"
   1.293 +  unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan
   1.294 +  by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp)
   1.295  
   1.296  lemma exphr_zero [simp]: "exphr 0 = 1"
   1.297 -apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
   1.298 -apply (rule st_unique, simp)
   1.299 -apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   1.300 -apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   1.301 -apply (rule_tac x="whn" in spec)
   1.302 -apply (unfold sumhr_app, transfer, simp add: power_0_left)
   1.303 -done
   1.304 +proof -
   1.305 +  have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \<lambda>n. inverse (fact n) * 0 ^ n)"
   1.306 +    unfolding sumhr_app by transfer (simp add: power_0_left)
   1.307 +  then have "sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \<lambda>n. inverse (fact n) * 0 ^ n) \<approx> 1"
   1.308 +    by auto
   1.309 +  then show ?thesis
   1.310 +    unfolding exphr_def
   1.311 +    using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
   1.312 +qed
   1.313  
   1.314  lemma coshr_zero [simp]: "coshr 0 = 1"
   1.315 -apply (simp add: coshr_def sumhr_split_add
   1.316 -                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   1.317 -apply (rule st_unique, simp)
   1.318 -apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
   1.319 -apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
   1.320 -apply (rule_tac x="whn" in spec)
   1.321 -apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
   1.322 -done
   1.323 +  proof -
   1.324 +  have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, x, \<lambda>n. cos_coeff n * 0 ^ n)"
   1.325 +    unfolding sumhr_app by transfer (simp add: power_0_left)
   1.326 +  then have "sumhr (0, 1, \<lambda>n. cos_coeff n * 0 ^ n) + sumhr (1, whn, \<lambda>n. cos_coeff n * 0 ^ n) \<approx> 1"
   1.327 +    by auto
   1.328 +  then show ?thesis
   1.329 +    unfolding coshr_def
   1.330 +    using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
   1.331 +qed
   1.332  
   1.333  lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
   1.334 -apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
   1.335 -apply (transfer, simp)
   1.336 -done
   1.337 +  proof -
   1.338 +  have "(*f* exp) (0::real star) = 1"
   1.339 +    by transfer simp
   1.340 +  then show ?thesis
   1.341 +    by auto
   1.342 +qed
   1.343  
   1.344 -lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
   1.345 -apply (case_tac "x = 0")
   1.346 -apply (cut_tac [2] x = 0 in DERIV_exp)
   1.347 -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.348 -apply (drule_tac x = x in bspec, auto)
   1.349 -apply (drule_tac c = x in approx_mult1)
   1.350 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   1.351 -            simp add: mult.assoc)
   1.352 -apply (rule approx_add_right_cancel [where d="-1"])
   1.353 -apply (rule approx_sym [THEN [2] approx_trans2])
   1.354 -apply (auto simp add: mem_infmal_iff)
   1.355 -done
   1.356 +lemma STAR_exp_Infinitesimal: 
   1.357 +  assumes "x \<in> Infinitesimal" shows "( *f* exp) (x::hypreal) \<approx> 1"
   1.358 +proof (cases "x = 0")
   1.359 +  case False
   1.360 +  have "NSDERIV exp 0 :> 1"
   1.361 +    by (metis DERIV_exp NSDERIV_DERIV_iff exp_zero)
   1.362 +  then have "((*f* exp) x - 1) / x \<approx> 1"
   1.363 +    using nsderiv_def False NSDERIVD2 assms by fastforce
   1.364 +  then have "(*f* exp) x - 1 \<approx> x"
   1.365 +    using NSDERIVD4 \<open>NSDERIV exp 0 :> 1\<close> assms by fastforce
   1.366 +  then show ?thesis
   1.367 +    by (meson Infinitesimal_approx approx_minus_iff approx_trans2 assms not_Infinitesimal_not_zero)
   1.368 +qed auto
   1.369  
   1.370  lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
   1.371 -by (auto intro: STAR_exp_Infinitesimal)
   1.372 +  by (auto intro: STAR_exp_Infinitesimal)
   1.373  
   1.374  lemma STAR_exp_add:
   1.375 -  "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   1.376 -by transfer (rule exp_add)
   1.377 +  "\<And>(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   1.378 +  by transfer (rule exp_add)
   1.379  
   1.380  lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
   1.381 -apply (simp add: exphr_def)
   1.382 -apply (rule st_unique, simp)
   1.383 -apply (subst starfunNat_sumr [symmetric])
   1.384 -unfolding atLeast0LessThan
   1.385 -apply (rule NSLIMSEQ_D [THEN approx_sym])
   1.386 -apply (rule LIMSEQ_NSLIMSEQ)
   1.387 -apply (subst sums_def [symmetric])
   1.388 -apply (cut_tac exp_converges [where x=x], simp)
   1.389 -apply (rule HNatInfinite_whn)
   1.390 -done
   1.391 +proof -
   1.392 +  have "(\<lambda>n. inverse (fact n) * x ^ n) sums exp x"
   1.393 +    using exp_converges [of x] by simp
   1.394 +  then have "(\<lambda>n. \<Sum>n<n. inverse (fact n) * x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S exp x"
   1.395 +    using NSsums_def sums_NSsums_iff by blast
   1.396 +  then have "hypreal_of_real (exp x) \<approx> sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n)"
   1.397 +    unfolding starfunNat_sumr [symmetric] atLeast0LessThan
   1.398 +    using HNatInfinite_whn NSLIMSEQ_iff approx_sym by blast
   1.399 +  then show ?thesis
   1.400 +    unfolding exphr_def using st_eq_approx_iff by auto
   1.401 +qed
   1.402  
   1.403 -lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   1.404 -by transfer (rule exp_ge_add_one_self_aux)
   1.405 +lemma starfun_exp_ge_add_one_self [simp]: "\<And>x::hypreal. 0 \<le> x \<Longrightarrow> (1 + x) \<le> ( *f* exp) x"
   1.406 +  by transfer (rule exp_ge_add_one_self_aux)
   1.407  
   1.408 -(* exp (oo) is infinite *)
   1.409 +text\<open>exp maps infinities to infinities\<close>
   1.410  lemma starfun_exp_HInfinite:
   1.411 -     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
   1.412 -apply (frule starfun_exp_ge_add_one_self)
   1.413 -apply (rule HInfinite_ge_HInfinite, assumption)
   1.414 -apply (rule order_trans [of _ "1+x"], auto) 
   1.415 -done
   1.416 +  fixes x :: hypreal
   1.417 +  assumes "x \<in> HInfinite" "0 \<le> x"
   1.418 +  shows "( *f* exp) x \<in> HInfinite"
   1.419 +proof -
   1.420 +  have "x \<le> 1 + x"
   1.421 +    by simp
   1.422 +  also have "\<dots> \<le> (*f* exp) x"
   1.423 +    by (simp add: \<open>0 \<le> x\<close>)
   1.424 +  finally show ?thesis
   1.425 +    using HInfinite_ge_HInfinite assms by blast
   1.426 +qed
   1.427  
   1.428  lemma starfun_exp_minus:
   1.429 -  "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
   1.430 -by transfer (rule exp_minus)
   1.431 +  "\<And>x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
   1.432 +  by transfer (rule exp_minus)
   1.433  
   1.434 -(* exp (-oo) is infinitesimal *)
   1.435 +text\<open>exp maps infinitesimals to infinitesimals\<close>
   1.436  lemma starfun_exp_Infinitesimal:
   1.437 -     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   1.438 -apply (subgoal_tac "\<exists>y. x = - y")
   1.439 -apply (rule_tac [2] x = "- x" in exI)
   1.440 -apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
   1.441 -            simp add: starfun_exp_minus HInfinite_minus_iff)
   1.442 -done
   1.443 +  fixes x :: hypreal
   1.444 +  assumes "x \<in> HInfinite" "x \<le> 0"
   1.445 +  shows "( *f* exp) x \<in> Infinitesimal"
   1.446 +proof -
   1.447 +  obtain y where "x = -y" "y \<ge> 0"
   1.448 +    by (metis abs_of_nonpos assms(2) eq_abs_iff')
   1.449 +  then have "( *f* exp) y \<in> HInfinite"
   1.450 +    using HInfinite_minus_iff assms(1) starfun_exp_HInfinite by blast
   1.451 +  then show ?thesis
   1.452 +    by (simp add: HInfinite_inverse_Infinitesimal \<open>x = - y\<close> starfun_exp_minus)
   1.453 +qed
   1.454  
   1.455 -lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
   1.456 -by transfer (rule exp_gt_one)
   1.457 +lemma starfun_exp_gt_one [simp]: "\<And>x::hypreal. 0 < x \<Longrightarrow> 1 < ( *f* exp) x"
   1.458 +  by transfer (rule exp_gt_one)
   1.459  
   1.460  abbreviation real_ln :: "real \<Rightarrow> real" where 
   1.461    "real_ln \<equiv> ln"
   1.462  
   1.463 -lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
   1.464 -by transfer (rule ln_exp)
   1.465 +lemma starfun_ln_exp [simp]: "\<And>x. ( *f* real_ln) (( *f* exp) x) = x"
   1.466 +  by transfer (rule ln_exp)
   1.467  
   1.468 -lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
   1.469 -by transfer (rule exp_ln_iff)
   1.470 +lemma starfun_exp_ln_iff [simp]: "\<And>x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
   1.471 +  by transfer (rule exp_ln_iff)
   1.472  
   1.473 -lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
   1.474 -by transfer (rule ln_unique)
   1.475 +lemma starfun_exp_ln_eq: "\<And>u x. ( *f* exp) u = x \<Longrightarrow> ( *f* real_ln) x = u"
   1.476 +  by transfer (rule ln_unique)
   1.477  
   1.478 -lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
   1.479 -by transfer (rule ln_less_self)
   1.480 -
   1.481 -lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
   1.482 -by transfer (rule ln_ge_zero)
   1.483 +lemma starfun_ln_less_self [simp]: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) x < x"
   1.484 +  by transfer (rule ln_less_self)
   1.485  
   1.486 -lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
   1.487 -by transfer (rule ln_gt_zero)
   1.488 +lemma starfun_ln_ge_zero [simp]: "\<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ( *f* real_ln) x"
   1.489 +  by transfer (rule ln_ge_zero)
   1.490  
   1.491 -lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
   1.492 -by transfer simp
   1.493 +lemma starfun_ln_gt_zero [simp]: "\<And>x .1 < x \<Longrightarrow> 0 < ( *f* real_ln) x"
   1.494 +  by transfer (rule ln_gt_zero)
   1.495  
   1.496 -lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
   1.497 -apply (rule HFinite_bounded)
   1.498 -apply assumption 
   1.499 -apply (simp_all add: starfun_ln_less_self order_less_imp_le)
   1.500 -done
   1.501 +lemma starfun_ln_not_eq_zero [simp]: "\<And>x. \<lbrakk>0 < x; x \<noteq> 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<noteq> 0"
   1.502 +  by transfer simp
   1.503  
   1.504 -lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
   1.505 -by transfer (rule ln_inverse)
   1.506 +lemma starfun_ln_HFinite: "\<lbrakk>x \<in> HFinite; 1 \<le> x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
   1.507 +  by (metis HFinite_HInfinite_iff less_le_trans starfun_exp_HInfinite starfun_exp_ln_iff starfun_ln_ge_zero zero_less_one)
   1.508 +
   1.509 +lemma starfun_ln_inverse: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) (inverse x) = -( *f* ln) x"
   1.510 +  by transfer (rule ln_inverse)
   1.511  
   1.512  lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
   1.513 -by transfer (rule abs_exp_cancel)
   1.514 +  by transfer (rule abs_exp_cancel)
   1.515  
   1.516  lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
   1.517 -by transfer (rule exp_less_mono)
   1.518 +  by transfer (rule exp_less_mono)
   1.519  
   1.520 -lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
   1.521 -apply (auto simp add: HFinite_def, rename_tac u)
   1.522 -apply (rule_tac x="( *f* exp) u" in rev_bexI)
   1.523 -apply (simp add: Reals_eq_Standard)
   1.524 -apply (simp add: starfun_abs_exp_cancel)
   1.525 -apply (simp add: starfun_exp_less_mono)
   1.526 -done
   1.527 +lemma starfun_exp_HFinite: 
   1.528 +  fixes x :: hypreal
   1.529 +  assumes "x \<in> HFinite"
   1.530 +  shows "( *f* exp) x \<in> HFinite"
   1.531 +proof -
   1.532 +  obtain u where "u \<in> \<real>" "\<bar>x\<bar> < u"
   1.533 +    using HFiniteD assms by force
   1.534 +  with assms have "\<bar>(*f* exp) x\<bar> < (*f* exp) u" 
   1.535 +    using starfun_abs_exp_cancel starfun_exp_less_mono by auto
   1.536 +  with \<open>u \<in> \<real>\<close> show ?thesis
   1.537 +    by (force simp: HFinite_def Reals_eq_Standard)
   1.538 +qed
   1.539  
   1.540  lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   1.541 -     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
   1.542 -apply (simp add: STAR_exp_add)
   1.543 -apply (frule STAR_exp_Infinitesimal)
   1.544 -apply (drule approx_mult2)
   1.545 -apply (auto intro: starfun_exp_HFinite)
   1.546 -done
   1.547 +  fixes x :: hypreal
   1.548 +  shows "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
   1.549 +  using STAR_exp_Infinitesimal approx_mult2 starfun_exp_HFinite by (fastforce simp add: STAR_exp_add)
   1.550  
   1.551 -(* using previous result to get to result *)
   1.552  lemma starfun_ln_HInfinite:
   1.553 -     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   1.554 -apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   1.555 -apply (drule starfun_exp_HFinite)
   1.556 -apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   1.557 -done
   1.558 +  "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
   1.559 +  by (metis HInfinite_HFinite_iff starfun_exp_HFinite starfun_exp_ln_iff)
   1.560  
   1.561  lemma starfun_exp_HInfinite_Infinitesimal_disj:
   1.562 - "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   1.563 -apply (insert linorder_linear [of x 0]) 
   1.564 -apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   1.565 -done
   1.566 +  fixes x :: hypreal
   1.567 +  shows "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
   1.568 +  by (meson linear starfun_exp_HInfinite starfun_exp_Infinitesimal)
   1.569  
   1.570 -(* check out this proof!!! *)
   1.571  lemma starfun_ln_HFinite_not_Infinitesimal:
   1.572 -     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
   1.573 -apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   1.574 -apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   1.575 -apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   1.576 -            del: starfun_exp_ln_iff)
   1.577 -done
   1.578 +     "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
   1.579 +  by (metis DiffD1 DiffD2 HInfinite_HFinite_iff starfun_exp_HInfinite_Infinitesimal_disj starfun_exp_ln_iff)
   1.580  
   1.581  (* we do proof by considering ln of 1/x *)
   1.582  lemma starfun_ln_Infinitesimal_HInfinite:
   1.583 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   1.584 -apply (drule Infinitesimal_inverse_HInfinite)
   1.585 -apply (frule positive_imp_inverse_positive)
   1.586 -apply (drule_tac [2] starfun_ln_HInfinite)
   1.587 -apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   1.588 -done
   1.589 +  assumes "x \<in> Infinitesimal" "0 < x"
   1.590 +  shows "( *f* real_ln) x \<in> HInfinite"
   1.591 +proof -
   1.592 +  have "inverse x \<in> HInfinite"
   1.593 +    using Infinitesimal_inverse_HInfinite assms by blast
   1.594 +  then show ?thesis
   1.595 +    using HInfinite_minus_iff assms(2) starfun_ln_HInfinite starfun_ln_inverse by fastforce
   1.596 +qed
   1.597  
   1.598 -lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
   1.599 -by transfer (rule ln_less_zero)
   1.600 +lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
   1.601 +  by transfer (rule ln_less_zero)
   1.602  
   1.603  lemma starfun_ln_Infinitesimal_less_zero:
   1.604 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
   1.605 -by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   1.606 +  "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
   1.607 +  by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   1.608  
   1.609  lemma starfun_ln_HInfinite_gt_zero:
   1.610 -     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
   1.611 -by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   1.612 +  "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x"
   1.613 +  by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   1.614  
   1.615  
   1.616 -(*
   1.617 -Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
   1.618 -*)
   1.619 -
   1.620 -lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
   1.621 -unfolding sumhr_app
   1.622 -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.623 -apply (rule NSBseqD2)
   1.624 -apply (rule NSconvergent_NSBseq)
   1.625 -apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.626 -apply (rule summable_iff_convergent [THEN iffD1])
   1.627 -using summable_norm_sin [of x]
   1.628 -apply (simp add: summable_rabs_cancel)
   1.629 -done
   1.630 +lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite"
   1.631 +proof -
   1.632 +  have "summable (\<lambda>i. sin_coeff i * x ^ i)"
   1.633 +    using summable_norm_sin [of x] by (simp add: summable_rabs_cancel)
   1.634 +  then have "(*f* (\<lambda>n. \<Sum>n<n. sin_coeff n * x ^ n)) whn \<in> HFinite"
   1.635 +    unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff
   1.636 +    using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
   1.637 +  then show ?thesis
   1.638 +    unfolding sumhr_app
   1.639 +    by (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.640 +qed
   1.641  
   1.642  lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   1.643 -by transfer (rule sin_zero)
   1.644 +  by transfer (rule sin_zero)
   1.645  
   1.646  lemma STAR_sin_Infinitesimal [simp]:
   1.647    fixes x :: "'a::{real_normed_field,banach} star"
   1.648 -  shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
   1.649 -apply (case_tac "x = 0")
   1.650 -apply (cut_tac [2] x = 0 in DERIV_sin)
   1.651 -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.652 -apply (drule bspec [where x = x], auto)
   1.653 -apply (drule approx_mult1 [where c = x])
   1.654 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.655 -           simp add: mult.assoc)
   1.656 -done
   1.657 +  assumes "x \<in> Infinitesimal"
   1.658 +  shows "( *f* sin) x \<approx> x"
   1.659 +proof (cases "x = 0")
   1.660 +  case False
   1.661 +  have "NSDERIV sin 0 :> 1"
   1.662 +    by (metis DERIV_sin NSDERIV_DERIV_iff cos_zero)
   1.663 +  then have "(*f* sin) x / x \<approx> 1"
   1.664 +    using False NSDERIVD2 assms by fastforce
   1.665 +  with assms show ?thesis
   1.666 +    unfolding star_one_def
   1.667 +    by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite)
   1.668 +qed auto
   1.669  
   1.670 -lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
   1.671 -unfolding sumhr_app
   1.672 -apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.673 -apply (rule NSBseqD2)
   1.674 -apply (rule NSconvergent_NSBseq)
   1.675 -apply (rule convergent_NSconvergent_iff [THEN iffD1])
   1.676 -apply (rule summable_iff_convergent [THEN iffD1])
   1.677 -using summable_norm_cos [of x]
   1.678 -apply (simp add: summable_rabs_cancel)
   1.679 -done
   1.680 +lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite"
   1.681 +proof -
   1.682 +  have "summable (\<lambda>i. cos_coeff i * x ^ i)"
   1.683 +    using summable_norm_cos [of x] by (simp add: summable_rabs_cancel)
   1.684 +  then have "(*f* (\<lambda>n. \<Sum>n<n. cos_coeff n * x ^ n)) whn \<in> HFinite"
   1.685 +    unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff
   1.686 +    using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
   1.687 +  then show ?thesis
   1.688 +    unfolding sumhr_app
   1.689 +    by (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
   1.690 +qed
   1.691  
   1.692  lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   1.693 -by transfer (rule cos_zero)
   1.694 +  by transfer (rule cos_zero)
   1.695  
   1.696  lemma STAR_cos_Infinitesimal [simp]:
   1.697    fixes x :: "'a::{real_normed_field,banach} star"
   1.698 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
   1.699 -apply (case_tac "x = 0")
   1.700 -apply (cut_tac [2] x = 0 in DERIV_cos)
   1.701 -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.702 -apply (drule bspec [where x = x])
   1.703 -apply auto
   1.704 -apply (drule approx_mult1 [where c = x])
   1.705 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.706 -            simp add: mult.assoc)
   1.707 -apply (rule approx_add_right_cancel [where d = "-1"])
   1.708 -apply simp
   1.709 -done
   1.710 +  assumes "x \<in> Infinitesimal"
   1.711 +  shows "( *f* cos) x \<approx> 1"
   1.712 +proof (cases "x = 0")
   1.713 +  case False
   1.714 +  have "NSDERIV cos 0 :> 0"
   1.715 +    by (metis DERIV_cos NSDERIV_DERIV_iff add.inverse_neutral sin_zero)
   1.716 +  then have "(*f* cos) x - 1 \<approx> 0"
   1.717 +    using NSDERIV_approx assms by fastforce
   1.718 +  with assms show ?thesis
   1.719 +    using approx_minus_iff by blast
   1.720 +qed auto
   1.721  
   1.722  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   1.723 -by transfer (rule tan_zero)
   1.724 +  by transfer (rule tan_zero)
   1.725  
   1.726 -lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
   1.727 -apply (case_tac "x = 0")
   1.728 -apply (cut_tac [2] x = 0 in DERIV_tan)
   1.729 -apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.730 -apply (drule bspec [where x = x], auto)
   1.731 -apply (drule approx_mult1 [where c = x])
   1.732 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.733 -             simp add: mult.assoc)
   1.734 -done
   1.735 +lemma STAR_tan_Infinitesimal [simp]:
   1.736 +  assumes "x \<in> Infinitesimal"
   1.737 +  shows "( *f* tan) x \<approx> x"
   1.738 +proof (cases "x = 0")
   1.739 +  case False
   1.740 +  have "NSDERIV tan 0 :> 1"
   1.741 +    using DERIV_tan [of 0] by (simp add: NSDERIV_DERIV_iff)
   1.742 +  then have "(*f* tan) x / x \<approx> 1"
   1.743 +    using False NSDERIVD2 assms by fastforce
   1.744 +  with assms show ?thesis
   1.745 +    unfolding star_one_def
   1.746 +    by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite)
   1.747 +qed auto
   1.748  
   1.749  lemma STAR_sin_cos_Infinitesimal_mult:
   1.750    fixes x :: "'a::{real_normed_field,banach} star"
   1.751 -  shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
   1.752 -using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
   1.753 -by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   1.754 +  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x"
   1.755 +  using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
   1.756 +  by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   1.757  
   1.758  lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   1.759 -by simp
   1.760 -
   1.761 -(* lemmas *)
   1.762 +  by simp
   1.763  
   1.764 -lemma lemma_split_hypreal_of_real:
   1.765 -     "N \<in> HNatInfinite  
   1.766 -      ==> hypreal_of_real a =  
   1.767 -          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   1.768 -by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
   1.769  
   1.770  lemma STAR_sin_Infinitesimal_divide:
   1.771    fixes x :: "'a::{real_normed_field,banach} star"
   1.772 -  shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
   1.773 -using DERIV_sin [of "0::'a"]
   1.774 -by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.775 +  shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1"
   1.776 +  using DERIV_sin [of "0::'a"]
   1.777 +  by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   1.778  
   1.779 -(*------------------------------------------------------------------------*) 
   1.780 -(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
   1.781 -(*------------------------------------------------------------------------*)
   1.782 +subsection \<open>Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ \<close> 
   1.783  
   1.784  lemma lemma_sin_pi:
   1.785 -     "n \<in> HNatInfinite  
   1.786 -      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
   1.787 -apply (rule STAR_sin_Infinitesimal_divide)
   1.788 -apply (auto simp add: zero_less_HNatInfinite)
   1.789 -done
   1.790 +  "n \<in> HNatInfinite  
   1.791 +      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
   1.792 +  by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite)
   1.793  
   1.794  lemma STAR_sin_inverse_HNatInfinite:
   1.795       "n \<in> HNatInfinite  
   1.796 -      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
   1.797 -apply (frule lemma_sin_pi)
   1.798 -apply (simp add: divide_inverse)
   1.799 -done
   1.800 +      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
   1.801 +  by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi)
   1.802  
   1.803  lemma Infinitesimal_pi_divide_HNatInfinite: 
   1.804       "N \<in> HNatInfinite  
   1.805 -      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   1.806 -apply (simp add: divide_inverse)
   1.807 -apply (auto intro: Infinitesimal_HFinite_mult2)
   1.808 -done
   1.809 +      \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   1.810 +  by (simp add: Infinitesimal_HFinite_mult2 field_class.field_divide_inverse)
   1.811  
   1.812  lemma pi_divide_HNatInfinite_not_zero [simp]:
   1.813 -     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   1.814 -by (simp add: zero_less_HNatInfinite)
   1.815 +  "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   1.816 +  by (simp add: zero_less_HNatInfinite)
   1.817  
   1.818  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   1.819 -     "n \<in> HNatInfinite  
   1.820 -      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   1.821 -          \<approx> hypreal_of_real pi"
   1.822 -apply (frule STAR_sin_Infinitesimal_divide
   1.823 -               [OF Infinitesimal_pi_divide_HNatInfinite 
   1.824 -                   pi_divide_HNatInfinite_not_zero])
   1.825 -apply (auto)
   1.826 -apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   1.827 -apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
   1.828 -done
   1.829 +  assumes "n \<in> HNatInfinite"
   1.830 +  shows "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) * hypreal_of_hypnat n \<approx>
   1.831 +         hypreal_of_real pi"
   1.832 +proof -
   1.833 +  have "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) / (hypreal_of_real pi / hypreal_of_hypnat n) \<approx> 1"
   1.834 +    using Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal_divide assms pi_divide_HNatInfinite_not_zero by blast
   1.835 +  then have "hypreal_of_hypnat n * star_of sin \<star> (hypreal_of_real pi / hypreal_of_hypnat n) / hypreal_of_real pi \<approx> 1"
   1.836 +    by (simp add: mult.commute starfun_def)
   1.837 +  then show ?thesis
   1.838 +    apply (simp add: starfun_def field_simps)
   1.839 +    by (metis (no_types, lifting) approx_mult_subst_star_of approx_refl mult_cancel_right1 nonzero_eq_divide_eq pi_neq_zero star_of_eq_0)
   1.840 +qed
   1.841  
   1.842  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   1.843       "n \<in> HNatInfinite  
   1.844 -      ==> hypreal_of_hypnat n *  
   1.845 -          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   1.846 -          \<approx> hypreal_of_real pi"
   1.847 -apply (rule mult.commute [THEN subst])
   1.848 -apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   1.849 -done
   1.850 +      \<Longrightarrow> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \<approx> hypreal_of_real pi"
   1.851 +  by (metis STAR_sin_pi_divide_HNatInfinite_approx_pi mult.commute)
   1.852  
   1.853  lemma starfunNat_pi_divide_n_Infinitesimal: 
   1.854 -     "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
   1.855 -by (auto intro!: Infinitesimal_HFinite_mult2 
   1.856 -         simp add: starfun_mult [symmetric] divide_inverse
   1.857 -                   starfun_inverse [symmetric] starfunNat_real_of_nat)
   1.858 +     "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal"
   1.859 +  by (simp add: Infinitesimal_HFinite_mult2 divide_inverse starfunNat_real_of_nat)
   1.860  
   1.861  lemma STAR_sin_pi_divide_n_approx:
   1.862 -     "N \<in> HNatInfinite ==>  
   1.863 -      ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>  
   1.864 -      hypreal_of_real pi/(hypreal_of_hypnat N)"
   1.865 -apply (simp add: starfunNat_real_of_nat [symmetric])
   1.866 -apply (rule STAR_sin_Infinitesimal)
   1.867 -apply (simp add: divide_inverse)
   1.868 -apply (rule Infinitesimal_HFinite_mult2)
   1.869 -apply (subst starfun_inverse)
   1.870 -apply (erule starfunNat_inverse_real_of_nat_Infinitesimal)
   1.871 -apply simp
   1.872 -done
   1.873 +  assumes "N \<in> HNatInfinite"
   1.874 +  shows "( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi/(hypreal_of_hypnat N)"
   1.875 +proof -
   1.876 +  have "\<exists>s. (*f* sin) ((*f* (\<lambda>n. pi / real n)) N) \<approx> s \<and> hypreal_of_real pi / hypreal_of_hypnat N \<approx> s"
   1.877 +    by (metis (lifting) Infinitesimal_approx Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal assms starfunNat_pi_divide_n_Infinitesimal)
   1.878 +  then show ?thesis
   1.879 +    by (meson approx_trans2)
   1.880 +qed
   1.881  
   1.882 -lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.883 -apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
   1.884 -apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
   1.885 -apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
   1.886 -apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   1.887 -apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   1.888 -            simp add: starfunNat_real_of_nat mult.commute divide_inverse)
   1.889 -done
   1.890 +lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.891 +proof -
   1.892 +  have *: "hypreal_of_hypnat N * (*f* sin) ((*f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi"
   1.893 +    if "N \<in> HNatInfinite"
   1.894 +    for N :: "nat star"
   1.895 +    using that
   1.896 +    by simp (metis STAR_sin_pi_divide_HNatInfinite_approx_pi2 starfunNat_real_of_nat)
   1.897 +  show ?thesis
   1.898 +    by (simp add: NSLIMSEQ_def starfunNat_real_of_nat) (metis * starfun_o2)
   1.899 +qed
   1.900  
   1.901 -lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
   1.902 -apply (simp add: NSLIMSEQ_def, auto)
   1.903 -apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
   1.904 -apply (rule STAR_cos_Infinitesimal)
   1.905 -apply (auto intro!: Infinitesimal_HFinite_mult2 
   1.906 -            simp add: starfun_mult [symmetric] divide_inverse
   1.907 -                      starfun_inverse [symmetric] starfunNat_real_of_nat)
   1.908 -done
   1.909 +lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
   1.910 +proof -
   1.911 +  have "(*f* cos) ((*f* (\<lambda>x. pi / real x)) N) \<approx> 1"
   1.912 +    if "N \<in> HNatInfinite" for N 
   1.913 +    using that STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal by blast
   1.914 +  then show ?thesis
   1.915 +    by (simp add: NSLIMSEQ_def) (metis STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal starfun_o2)
   1.916 +qed
   1.917  
   1.918  lemma NSLIMSEQ_sin_cos_pi:
   1.919 -     "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.920 -by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   1.921 +  "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
   1.922 +  using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force
   1.923  
   1.924  
   1.925  text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
   1.926  
   1.927  lemma STAR_cos_Infinitesimal_approx:
   1.928    fixes x :: "'a::{real_normed_field,banach} star"
   1.929 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
   1.930 -apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.931 -apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   1.932 -            add.assoc [symmetric] numeral_2_eq_2)
   1.933 -done
   1.934 +  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2"
   1.935 +  by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square)
   1.936  
   1.937  lemma STAR_cos_Infinitesimal_approx2:
   1.938    fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
   1.939 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
   1.940 -apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   1.941 -apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
   1.942 -            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   1.943 -done
   1.944 +  assumes "x \<in> Infinitesimal"
   1.945 +  shows "( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
   1.946 +proof -
   1.947 +  have "1 \<approx> 1 - x\<^sup>2 / 2"
   1.948 +    using assms
   1.949 +    by (auto intro: Infinitesimal_SReal_divide simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   1.950 +  then show ?thesis
   1.951 +    using STAR_cos_Infinitesimal approx_trans assms by blast
   1.952 +qed
   1.953  
   1.954  end