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