converted Hyperreal/HTranscendental to Isar script
authorpaulson
Mon Mar 01 11:52:59 2004 +0100 (2004-03-01)
changeset 144204e72cd222e0b
parent 14419 a98803496711
child 14421 ee97b6463cb4
converted Hyperreal/HTranscendental to Isar script
src/HOL/Hyperreal/HTranscendental.ML
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.ML	Mon Mar 01 05:39:32 2004 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,739 +0,0 @@
     1.4 -(*  Title       : HTranscendental.ML
     1.5 -    Author      : Jacques D. Fleuriot
     1.6 -    Copyright   : 2001 University of Edinburgh
     1.7 -    Description : Nonstandard extensions of transcendental functions
     1.8 -*)
     1.9 -
    1.10 -val hpowr_Suc= thm"hpowr_Suc";
    1.11 -
    1.12 -(*-------------------------------------------------------------------------*)
    1.13 -(* NS extension of square root function                                    *)
    1.14 -(*-------------------------------------------------------------------------*)
    1.15 -
    1.16 -Goal "( *f* sqrt) 0 = 0";
    1.17 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
    1.18 -qed "STAR_sqrt_zero";
    1.19 -Addsimps [STAR_sqrt_zero];
    1.20 -
    1.21 -Goal "( *f* sqrt) 1 = 1";
    1.22 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
    1.23 -qed "STAR_sqrt_one";
    1.24 -Addsimps [STAR_sqrt_one];
    1.25 -
    1.26 -Goal "(( *f* sqrt)(x) ^ 2 = x) = (0 <= x)";
    1.27 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.28 -by (auto_tac (claset(),simpset() addsimps [hypreal_le,
    1.29 -    hypreal_zero_num, starfun,hrealpow,real_sqrt_pow2_iff] 
    1.30 -    delsimps [hpowr_Suc,realpow_Suc]));
    1.31 -qed "hypreal_sqrt_pow2_iff";
    1.32 -
    1.33 -Goal "0 < x ==> ( *f* sqrt) (x) ^ 2 = x";
    1.34 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.35 -by (auto_tac (claset() addIs [FreeUltrafilterNat_subset,
    1.36 -    real_sqrt_gt_zero_pow2],simpset() addsimps 
    1.37 -    [hypreal_less,starfun,hrealpow,hypreal_zero_num] 
    1.38 -    delsimps [hpowr_Suc,realpow_Suc]));
    1.39 -qed "hypreal_sqrt_gt_zero_pow2";
    1.40 -
    1.41 -Goal "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2";
    1.42 -by (forward_tac [hypreal_sqrt_gt_zero_pow2] 1);
    1.43 -by (Auto_tac);
    1.44 -qed "hypreal_sqrt_pow2_gt_zero";
    1.45 -
    1.46 -Goal "0 < x ==> ( *f* sqrt) (x) ~= 0";
    1.47 -by (forward_tac [hypreal_sqrt_pow2_gt_zero] 1);
    1.48 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
    1.49 -qed "hypreal_sqrt_not_zero";
    1.50 -
    1.51 -Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
    1.52 -by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_inverse RS sym) 1);
    1.53 -by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset()));
    1.54 -qed "hypreal_inverse_sqrt_pow2";
    1.55 -
    1.56 -Goalw [hypreal_zero_def] 
    1.57 -    "[|0 < x; 0 <y |] ==> \
    1.58 -\   ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)";
    1.59 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.60 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    1.61 -by (auto_tac (claset(),simpset() addsimps [starfun,
    1.62 -    hypreal_mult,hypreal_less,hypreal_zero_num]));
    1.63 -by (ultra_tac (claset() addIs [real_sqrt_mult_distrib],simpset()) 1);
    1.64 -qed "hypreal_sqrt_mult_distrib";
    1.65 -
    1.66 -Goal "[|0<=x; 0<=y |] ==> \
    1.67 -\    ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)";
    1.68 -by (auto_tac (claset() addIs [hypreal_sqrt_mult_distrib],
    1.69 -    simpset() addsimps [order_le_less]));
    1.70 -qed "hypreal_sqrt_mult_distrib2";
    1.71 -
    1.72 -Goal "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
    1.73 -by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym]));
    1.74 -by (rtac (hypreal_sqrt_gt_zero_pow2 RS subst) 1);
    1.75 -by (auto_tac (claset() addIs [Infinitesimal_mult] 
    1.76 -    addSDs [(hypreal_sqrt_gt_zero_pow2 RS ssubst)],simpset() addsimps [numeral_2_eq_2]));
    1.77 -qed "hypreal_sqrt_approx_zero";
    1.78 -Addsimps [hypreal_sqrt_approx_zero];
    1.79 -
    1.80 -Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
    1.81 -by (auto_tac (claset(), simpset() addsimps [order_le_less]));
    1.82 -qed "hypreal_sqrt_approx_zero2";
    1.83 -Addsimps [hypreal_sqrt_approx_zero2];
    1.84 -
    1.85 -Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)";
    1.86 -by (rtac hypreal_sqrt_approx_zero2 1);
    1.87 -by (REPEAT(rtac hypreal_le_add_order 1));
    1.88 -by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    1.89 -qed "hypreal_sqrt_sum_squares";
    1.90 -Addsimps [hypreal_sqrt_sum_squares];
    1.91 -
    1.92 -Goal  "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)";
    1.93 -by (rtac hypreal_sqrt_approx_zero2 1);
    1.94 -by (rtac hypreal_le_add_order 1);
    1.95 -by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    1.96 -qed "hypreal_sqrt_sum_squares2";
    1.97 -Addsimps [hypreal_sqrt_sum_squares2];
    1.98 -
    1.99 -Goal "0 < x ==> 0 < ( *f* sqrt)(x)";
   1.100 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.101 -by (auto_tac (claset(),simpset() addsimps 
   1.102 -    [starfun,hypreal_zero_def,hypreal_less,hypreal_zero_num]));
   1.103 -by (ultra_tac (claset() addIs [real_sqrt_gt_zero], simpset()) 1);
   1.104 -qed "hypreal_sqrt_gt_zero";
   1.105 -
   1.106 -Goal "0 <= x ==> 0 <= ( *f* sqrt)(x)";
   1.107 -by (auto_tac (claset() addIs [hypreal_sqrt_gt_zero],
   1.108 -    simpset() addsimps [order_le_less ]));
   1.109 -qed "hypreal_sqrt_ge_zero";
   1.110 -
   1.111 -Goal "( *f* sqrt)(x ^ 2) = abs(x)";
   1.112 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.113 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.114 -    hypreal_hrabs,hypreal_mult,numeral_2_eq_2]));
   1.115 -qed "hypreal_sqrt_hrabs";
   1.116 -Addsimps [hypreal_sqrt_hrabs];
   1.117 -
   1.118 -Goal "( *f* sqrt)(x*x) = abs(x)";
   1.119 -by (rtac (hrealpow_two RS subst) 1);
   1.120 -by (rtac (numeral_2_eq_2 RS subst) 1);
   1.121 -by (rtac hypreal_sqrt_hrabs 1);
   1.122 -qed "hypreal_sqrt_hrabs2";
   1.123 -Addsimps [hypreal_sqrt_hrabs2];
   1.124 -
   1.125 -Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
   1.126 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.127 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.128 -    hypreal_hrabs,hypnat_of_nat_eq,hyperpow]));
   1.129 -qed "hypreal_sqrt_hyperpow_hrabs";
   1.130 -Addsimps [hypreal_sqrt_hyperpow_hrabs];
   1.131 -
   1.132 -Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
   1.133 -by (res_inst_tac [("n","1")] power_inject_base 1);
   1.134 -by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
   1.135 -by (rtac (st_mult RS subst) 1);
   1.136 -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3);
   1.137 -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5);
   1.138 -by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le]));
   1.139 -by (ALLGOALS(rtac (HFinite_square_iff RS iffD1)));
   1.140 -by (auto_tac (claset(),
   1.141 -     simpset() addsimps [hypreal_sqrt_mult_distrib2 RS sym] 
   1.142 -    delsimps [HFinite_square_iff]));
   1.143 -qed "st_hypreal_sqrt";
   1.144 -
   1.145 -Goal "x <= ( *f* sqrt)(x ^ 2 + y ^ 2)";
   1.146 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.147 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.148 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
   1.149 -    hrealpow,hypreal_le] delsimps [hpowr_Suc,realpow_Suc]));
   1.150 -qed "hypreal_sqrt_sum_squares_ge1";
   1.151 -Addsimps [hypreal_sqrt_sum_squares_ge1];
   1.152 -
   1.153 -Goal "[| 0 <= x; x : HFinite |] ==> ( *f* sqrt) x : HFinite";
   1.154 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.155 -by (rtac (HFinite_square_iff RS iffD1) 1);
   1.156 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.157 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
   1.158 -qed "HFinite_hypreal_sqrt";
   1.159 -
   1.160 -Goal "[| 0 <= x; ( *f* sqrt) x : HFinite |] ==> x : HFinite";
   1.161 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.162 -by (dtac (HFinite_square_iff RS iffD2) 1);
   1.163 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.164 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] delsimps [HFinite_square_iff]));
   1.165 -qed "HFinite_hypreal_sqrt_imp_HFinite";
   1.166 -
   1.167 -Goal "0 <= x ==> (( *f* sqrt) x : HFinite) = (x : HFinite)";
   1.168 -by (blast_tac (claset() addIs [HFinite_hypreal_sqrt,
   1.169 -    HFinite_hypreal_sqrt_imp_HFinite]) 1);
   1.170 -qed "HFinite_hypreal_sqrt_iff";
   1.171 -Addsimps [HFinite_hypreal_sqrt_iff];
   1.172 -
   1.173 -Goal  "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)";
   1.174 -by (rtac HFinite_hypreal_sqrt_iff 1);
   1.175 -by (rtac  hypreal_le_add_order 1);
   1.176 -by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
   1.177 -qed "HFinite_sqrt_sum_squares";
   1.178 -Addsimps [HFinite_sqrt_sum_squares];
   1.179 -
   1.180 -Goal "[| 0 <= x; x : Infinitesimal |] ==> ( *f* sqrt) x : Infinitesimal";
   1.181 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.182 -by (rtac (Infinitesimal_square_iff RS iffD2) 1);
   1.183 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.184 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
   1.185 -qed "Infinitesimal_hypreal_sqrt";
   1.186 -
   1.187 -Goal "[| 0 <= x; ( *f* sqrt) x : Infinitesimal |] ==> x : Infinitesimal";
   1.188 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.189 -by (dtac (Infinitesimal_square_iff RS iffD1) 1);
   1.190 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.191 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] 
   1.192 -    delsimps [Infinitesimal_square_iff RS sym]));
   1.193 -qed "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
   1.194 -
   1.195 -Goal "0 <= x ==> (( *f* sqrt) x : Infinitesimal) = (x : Infinitesimal)";
   1.196 -by (blast_tac (claset() addIs [Infinitesimal_hypreal_sqrt_imp_Infinitesimal,
   1.197 -    Infinitesimal_hypreal_sqrt]) 1);
   1.198 -qed "Infinitesimal_hypreal_sqrt_iff";
   1.199 -Addsimps [Infinitesimal_hypreal_sqrt_iff];
   1.200 -
   1.201 -Goal  "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)";
   1.202 -by (rtac Infinitesimal_hypreal_sqrt_iff 1);
   1.203 -by (rtac hypreal_le_add_order 1);
   1.204 -by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
   1.205 -qed "Infinitesimal_sqrt_sum_squares";
   1.206 -Addsimps [Infinitesimal_sqrt_sum_squares];
   1.207 -
   1.208 -Goal "[| 0 <= x; x : HInfinite |] ==> ( *f* sqrt) x : HInfinite";
   1.209 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.210 -by (rtac (HInfinite_square_iff RS iffD1) 1);
   1.211 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.212 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
   1.213 -qed "HInfinite_hypreal_sqrt";
   1.214 -
   1.215 -Goal "[| 0 <= x; ( *f* sqrt) x : HInfinite |] ==> x : HInfinite";
   1.216 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
   1.217 -by (dtac (HInfinite_square_iff RS iffD2) 1);
   1.218 -by (dtac hypreal_sqrt_gt_zero_pow2 1);
   1.219 -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] 
   1.220 -    delsimps [HInfinite_square_iff]));
   1.221 -qed "HInfinite_hypreal_sqrt_imp_HInfinite";
   1.222 -
   1.223 -Goal "0 <= x ==> (( *f* sqrt) x : HInfinite) = (x : HInfinite)";
   1.224 -by (blast_tac (claset() addIs [HInfinite_hypreal_sqrt,
   1.225 -    HInfinite_hypreal_sqrt_imp_HInfinite]) 1);
   1.226 -qed "HInfinite_hypreal_sqrt_iff";
   1.227 -Addsimps [HInfinite_hypreal_sqrt_iff];
   1.228 -
   1.229 -Goal  "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)";
   1.230 -by (rtac HInfinite_hypreal_sqrt_iff 1);
   1.231 -by (rtac hypreal_le_add_order 1);
   1.232 -by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
   1.233 -qed "HInfinite_sqrt_sum_squares";
   1.234 -Addsimps [HInfinite_sqrt_sum_squares];
   1.235 -
   1.236 -Goal "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) : HFinite";
   1.237 -by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
   1.238 -    simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
   1.239 -    convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
   1.240 -    summable_exp]));
   1.241 -qed "HFinite_exp";
   1.242 -Addsimps [HFinite_exp];
   1.243 -
   1.244 -Goalw [exphr_def] "exphr 0 = 1";
   1.245 -by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
   1.246 -by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
   1.247 -by (rtac hypnat_one_less_hypnat_omega 1);
   1.248 -by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
   1.249 -    hypnat_one_def,hypnat_add,hypnat_omega_def,hypreal_add] 
   1.250 -    delsimps [hypnat_add_zero_left]));
   1.251 -by (simp_tac (simpset() addsimps [hypreal_one_num RS sym]) 1);
   1.252 -qed "exphr_zero";
   1.253 -Addsimps [exphr_zero];
   1.254 -
   1.255 -Goalw [coshr_def] "coshr 0 = 1";
   1.256 -by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
   1.257 -by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
   1.258 -by (rtac hypnat_one_less_hypnat_omega 1);
   1.259 -by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
   1.260 -    hypnat_one_def,hypnat_add,hypnat_omega_def,st_add RS sym,
   1.261 -    (hypreal_one_def RS meta_eq_to_obj_eq) RS sym, 
   1.262 -    (hypreal_zero_def RS meta_eq_to_obj_eq) RS sym] delsimps [hypnat_add_zero_left]));
   1.263 -qed "coshr_zero";
   1.264 -Addsimps [coshr_zero];
   1.265 -
   1.266 -Goalw [hypreal_zero_def,hypreal_one_def] "( *f* exp) 0 @= 1";
   1.267 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
   1.268 -qed "STAR_exp_zero_approx_one";
   1.269 -Addsimps [STAR_exp_zero_approx_one];
   1.270 -
   1.271 -Goal "x: Infinitesimal ==> ( *f* exp) x @= 1";
   1.272 -by (case_tac "x = 0" 1);
   1.273 -by (cut_inst_tac [("x","0")] DERIV_exp 2);
   1.274 -by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
   1.275 -    nsderiv_def]));
   1.276 -by (dres_inst_tac [("x","x")] bspec 1);
   1.277 -by Auto_tac;
   1.278 -by (dres_inst_tac [("c","x")] approx_mult1 1);
   1.279 -by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
   1.280 -    simpset() addsimps [hypreal_mult_assoc]));
   1.281 -by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
   1.282 -by (rtac (approx_sym RSN (2,approx_trans2)) 1);
   1.283 -by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff]));
   1.284 -qed "STAR_exp_Infinitesimal";
   1.285 -
   1.286 -Goal "( *f* exp) epsilon @= 1";
   1.287 -by (auto_tac (claset() addIs [STAR_exp_Infinitesimal],simpset()));
   1.288 -qed "STAR_exp_epsilon";
   1.289 -Addsimps [STAR_exp_epsilon];
   1.290 -
   1.291 -Goal "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y";
   1.292 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.293 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.294 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
   1.295 -    hypreal_mult,exp_add]));
   1.296 -qed "STAR_exp_add";
   1.297 -
   1.298 -Goalw [exphr_def] "exphr x = hypreal_of_real (exp x)";
   1.299 -by (rtac (st_hypreal_of_real  RS subst) 1);
   1.300 -by (rtac approx_st_eq 1);
   1.301 -by Auto_tac;
   1.302 -by (rtac (approx_minus_iff RS iffD2) 1);
   1.303 -by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym,
   1.304 -    hypreal_of_real_def,hypnat_zero_def,hypnat_omega_def,sumhr,
   1.305 -    hypreal_minus,hypreal_add]));
   1.306 -by (rtac NSLIMSEQ_zero_Infinitesimal_hypreal 1);
   1.307 -by (cut_inst_tac [("x3","x")] (exp_converges RS ((sums_def RS 
   1.308 -    meta_eq_to_obj_eq) RS iffD1)) 1);
   1.309 -by (dres_inst_tac [("b","- exp x")] (LIMSEQ_const RSN (2,LIMSEQ_add)) 1);
   1.310 -by (auto_tac (claset(),simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
   1.311 -qed "exphr_hypreal_of_real_exp_eq";
   1.312 -
   1.313 -Goal "0 <= x ==> (1 + x) <= ( *f* exp) x";
   1.314 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.315 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
   1.316 -    hypreal_le,hypreal_zero_num,hypreal_one_num]));
   1.317 -by (Ultra_tac 1);
   1.318 -qed "starfun_exp_ge_add_one_self";
   1.319 -Addsimps [starfun_exp_ge_add_one_self];
   1.320 -
   1.321 -(* exp (oo) is infinite *)
   1.322 -Goal "[| x : HInfinite; 0 <= x |] ==> ( *f* exp) x : HInfinite";
   1.323 -by (ftac starfun_exp_ge_add_one_self 1);
   1.324 -by (rtac HInfinite_ge_HInfinite 1);
   1.325 -by (rtac hypreal_le_trans 2);
   1.326 -by (TRYALL(assume_tac) THEN Simp_tac 1);
   1.327 -qed "starfun_exp_HInfinite";
   1.328 -
   1.329 -Goal "( *f* exp) (-x) = inverse(( *f* exp) x)";
   1.330 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.331 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_inverse,
   1.332 -    hypreal_minus,exp_minus]));
   1.333 -qed "starfun_exp_minus";
   1.334 -
   1.335 -(* exp (-oo) is infinitesimal *)
   1.336 -Goal "[| x : HInfinite; x <= 0 |] ==> ( *f* exp) x : Infinitesimal";
   1.337 -by (subgoal_tac "EX y. x = - y" 1);
   1.338 -by (res_inst_tac [("x","- x")] exI 2);
   1.339 -by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,
   1.340 -    starfun_exp_HInfinite] addIs [(starfun_exp_minus RS ssubst)],
   1.341 -     simpset() addsimps [HInfinite_minus_iff]));
   1.342 -qed "starfun_exp_Infinitesimal";
   1.343 -
   1.344 -Goal "0 < x ==> 1 < ( *f* exp) x";
   1.345 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.346 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num,
   1.347 -    hypreal_zero_num,hypreal_less]));
   1.348 -by (Ultra_tac 1);
   1.349 -qed "starfun_exp_gt_one";
   1.350 -Addsimps [starfun_exp_gt_one];
   1.351 -
   1.352 -(* needs derivative of inverse function
   1.353 -   TRY a NS one today!!!
   1.354 -
   1.355 -Goal "x @= 1 ==> ( *f* ln) x @= 1";
   1.356 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.357 -by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
   1.358 -
   1.359 -
   1.360 -Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
   1.361 -
   1.362 -*)
   1.363 -
   1.364 -
   1.365 -Goal "( *f* ln) (( *f* exp) x) = x";
   1.366 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.367 -by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.368 -qed "starfun_ln_exp";
   1.369 -Addsimps [starfun_ln_exp];
   1.370 -
   1.371 -Goal "(( *f* exp)(( *f* ln) x) = x) = (0 < x)";
   1.372 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.373 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.374 -    hypreal_zero_num,hypreal_less]));
   1.375 -qed "starfun_exp_ln_iff";
   1.376 -Addsimps [starfun_exp_ln_iff];
   1.377 -
   1.378 -Goal "( *f* exp) u = x ==> ( *f* ln) x = u";
   1.379 -by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.380 -qed "starfun_exp_ln_eq";
   1.381 -
   1.382 -Goal "0 < x ==> ( *f* ln) x < x";
   1.383 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.384 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.385 -    hypreal_zero_num,hypreal_less]));
   1.386 -by (Ultra_tac 1);
   1.387 -qed "starfun_ln_less_self";
   1.388 -Addsimps [starfun_ln_less_self];
   1.389 -
   1.390 -Goal "1 <= x ==> 0 <= ( *f* ln) x";
   1.391 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.392 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.393 -    hypreal_zero_num,hypreal_le,hypreal_one_num]));
   1.394 -by (Ultra_tac 1);
   1.395 -qed "starfun_ln_ge_zero";
   1.396 -Addsimps [starfun_ln_ge_zero];
   1.397 -
   1.398 -Goal "1 < x ==> 0 < ( *f* ln) x";
   1.399 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.400 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.401 -    hypreal_zero_num,hypreal_less,hypreal_one_num]));
   1.402 -by (Ultra_tac 1);
   1.403 -qed "starfun_ln_gt_zero";
   1.404 -Addsimps [starfun_ln_gt_zero];
   1.405 -
   1.406 -Goal "[| 0 < x; x ~= 1 |] ==> ( *f* ln) x ~= 0";
   1.407 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.408 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.409 -    hypreal_zero_num,hypreal_less,hypreal_one_num]));
   1.410 -by (ultra_tac (claset() addIs [ccontr] addDs [ln_not_eq_zero],simpset()) 1);
   1.411 -qed "starfun_ln_not_eq_zero";
   1.412 -Addsimps [starfun_ln_not_eq_zero];
   1.413 -
   1.414 -Goal "[| x: HFinite; 1 <= x |] ==> ( *f* ln) x : HFinite";
   1.415 -by (rtac HFinite_bounded 1);
   1.416 -by (rtac order_less_imp_le 2);
   1.417 -by (rtac starfun_ln_less_self 2);
   1.418 -by (rtac order_less_le_trans 2);
   1.419 -by Auto_tac;
   1.420 -qed "starfun_ln_HFinite";
   1.421 -
   1.422 -Goal "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x";
   1.423 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.424 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.425 -    hypreal_zero_num,hypreal_minus,hypreal_inverse,
   1.426 -    hypreal_less]));
   1.427 -by (Ultra_tac 1);
   1.428 -by (auto_tac (claset(),simpset() addsimps [ln_inverse]));
   1.429 -qed "starfun_ln_inverse";
   1.430 -
   1.431 -Goal "x : HFinite ==> ( *f* exp) x : HFinite";
   1.432 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.433 -by (auto_tac (claset(),simpset() addsimps [starfun,
   1.434 -    HFinite_FreeUltrafilterNat_iff]));
   1.435 -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.436 -by Auto_tac;
   1.437 -by (res_inst_tac [("x","exp u")] exI 1);
   1.438 -by (Ultra_tac 1 THEN arith_tac 1);
   1.439 -qed "starfun_exp_HFinite";
   1.440 -
   1.441 -Goal "[|x: Infinitesimal; z: HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z";
   1.442 -by (simp_tac (simpset() addsimps [STAR_exp_add]) 1);
   1.443 -by (ftac STAR_exp_Infinitesimal 1);
   1.444 -by (dtac approx_mult2 1);
   1.445 -by (auto_tac (claset() addIs [starfun_exp_HFinite],simpset()));
   1.446 -qed "starfun_exp_add_HFinite_Infinitesimal_approx";
   1.447 -
   1.448 -(* using previous result to get to result *)
   1.449 -Goal "[| x : HInfinite; 0 < x |] ==> ( *f* ln) x : HInfinite";
   1.450 -by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
   1.451 -by (dtac starfun_exp_HFinite 1);
   1.452 -by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS iffD2,
   1.453 -    HFinite_HInfinite_iff]));
   1.454 -qed "starfun_ln_HInfinite";
   1.455 -
   1.456 -Goal "x : HInfinite ==> ( *f* exp) x : HInfinite | ( *f* exp) x : Infinitesimal";
   1.457 -by (cut_inst_tac [("x","x")] (CLAIM "x <= (0::hypreal) | 0 <= x") 1);
   1.458 -by (auto_tac (claset() addIs [starfun_exp_HInfinite,starfun_exp_Infinitesimal],
   1.459 -    simpset()));
   1.460 -qed "starfun_exp_HInfinite_Infinitesimal_disj";
   1.461 -
   1.462 -(* check out this proof!!! *)
   1.463 -Goal "[| x : HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x : HFinite";
   1.464 -by (rtac ccontr 1 THEN dtac (HInfinite_HFinite_iff RS iffD2) 1);
   1.465 -by (dtac starfun_exp_HInfinite_Infinitesimal_disj 1);
   1.466 -by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS sym,
   1.467 -    HInfinite_HFinite_iff] delsimps [starfun_exp_ln_iff]));
   1.468 -qed "starfun_ln_HFinite_not_Infinitesimal";
   1.469 -
   1.470 -(* we do proof by considering ln of 1/x *)
   1.471 -Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x : HInfinite";
   1.472 -by (dtac Infinitesimal_inverse_HInfinite 1);
   1.473 -by (ftac positive_imp_inverse_positive 1);
   1.474 -by (dtac starfun_ln_HInfinite 2);
   1.475 -by (auto_tac (claset(),simpset() addsimps [starfun_ln_inverse,
   1.476 -    HInfinite_minus_iff]));
   1.477 -qed "starfun_ln_Infinitesimal_HInfinite";
   1.478 -
   1.479 -Goal "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0";
   1.480 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.481 -by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num,
   1.482 -     hypreal_one_num,hypreal_less,starfun]));
   1.483 -by (ultra_tac (claset() addIs [ln_less_zero],simpset()) 1);
   1.484 -qed "starfun_ln_less_zero";
   1.485 -
   1.486 -Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0";
   1.487 -by (auto_tac (claset() addSIs [starfun_ln_less_zero],simpset() 
   1.488 -    addsimps [Infinitesimal_def]));
   1.489 -by (dres_inst_tac [("x","1")] bspec 1);
   1.490 -by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
   1.491 -qed "starfun_ln_Infinitesimal_less_zero";
   1.492 -
   1.493 -Goal "[| x : HInfinite; 0 < x |] ==> 0 < ( *f* ln) x";
   1.494 -by (auto_tac (claset() addSIs [starfun_ln_gt_zero],simpset() 
   1.495 -    addsimps [HInfinite_def]));
   1.496 -by (dres_inst_tac [("x","1")] bspec 1);
   1.497 -by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
   1.498 -qed "starfun_ln_HInfinite_gt_zero";
   1.499 -
   1.500 -(*
   1.501 -Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x";
   1.502 -*)
   1.503 -
   1.504 -Goal "sumhr (0, whn, %n. (if even(n) then 0 else \
   1.505 -\             ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n) \
   1.506 -\             : HFinite";
   1.507 -by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
   1.508 -    simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
   1.509 -    convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym]));
   1.510 -by (rtac (CLAIM "1 = Suc 0" RS ssubst) 1);
   1.511 -by (rtac summable_sin 1);
   1.512 -qed "HFinite_sin";
   1.513 -Addsimps [HFinite_sin];
   1.514 -
   1.515 -Goal "( *f* sin) 0 = 0";
   1.516 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
   1.517 -qed "STAR_sin_zero";
   1.518 -Addsimps [STAR_sin_zero];
   1.519 -
   1.520 -Goal "x : Infinitesimal ==> ( *f* sin) x @= x";
   1.521 -by (case_tac "x = 0" 1);
   1.522 -by (cut_inst_tac [("x","0")] DERIV_sin 2);
   1.523 -by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
   1.524 -    nsderiv_def,hypreal_of_real_zero]));
   1.525 -by (dres_inst_tac [("x","x")] bspec 1);
   1.526 -by Auto_tac;
   1.527 -by (dres_inst_tac [("c","x")] approx_mult1 1);
   1.528 -by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
   1.529 -    simpset() addsimps [hypreal_mult_assoc]));
   1.530 -qed "STAR_sin_Infinitesimal";
   1.531 -Addsimps [STAR_sin_Infinitesimal];
   1.532 -
   1.533 -Goal "sumhr (0, whn, %n. (if even(n) then \
   1.534 -\           ((- 1) ^ (n div 2))/(real (fact n)) else \
   1.535 -\           0) * x ^ n) : HFinite";
   1.536 -by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
   1.537 -    simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
   1.538 -    convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
   1.539 -    summable_cos]));
   1.540 -qed "HFinite_cos";
   1.541 -Addsimps [HFinite_cos];
   1.542 -
   1.543 -Goal "( *f* cos) 0 = 1";
   1.544 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num,
   1.545 -    hypreal_one_num]));
   1.546 -qed "STAR_cos_zero";
   1.547 -Addsimps [STAR_cos_zero];
   1.548 -
   1.549 -Goal "x : Infinitesimal ==> ( *f* cos) x @= 1";
   1.550 -by (case_tac "x = 0" 1);
   1.551 -by (cut_inst_tac [("x","0")] DERIV_cos 2);
   1.552 -by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
   1.553 -    nsderiv_def,hypreal_of_real_zero]));
   1.554 -by (dres_inst_tac [("x","x")] bspec 1);
   1.555 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero,
   1.556 -    hypreal_of_real_one]));
   1.557 -by (dres_inst_tac [("c","x")] approx_mult1 1);
   1.558 -by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
   1.559 -    simpset() addsimps [hypreal_mult_assoc,hypreal_of_real_one]));
   1.560 -by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
   1.561 -by Auto_tac;
   1.562 -qed "STAR_cos_Infinitesimal";
   1.563 -Addsimps [STAR_cos_Infinitesimal];
   1.564 -
   1.565 -Goal "( *f* tan) 0 = 0";
   1.566 -by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
   1.567 -qed "STAR_tan_zero";
   1.568 -Addsimps [STAR_tan_zero];
   1.569 -
   1.570 -Goal "x : Infinitesimal ==> ( *f* tan) x @= x";
   1.571 -by (case_tac "x = 0" 1);
   1.572 -by (cut_inst_tac [("x","0")] DERIV_tan 2);
   1.573 -by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
   1.574 -    nsderiv_def,hypreal_of_real_zero]));
   1.575 -by (dres_inst_tac [("x","x")] bspec 1);
   1.576 -by Auto_tac;
   1.577 -by (dres_inst_tac [("c","x")] approx_mult1 1);
   1.578 -by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
   1.579 -    simpset() addsimps [hypreal_mult_assoc]));
   1.580 -qed "STAR_tan_Infinitesimal";
   1.581 -
   1.582 -Goal "x : Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x";
   1.583 -by (rtac (simplify (simpset()) (read_instantiate  
   1.584 -          [("d","1")] approx_mult_HFinite)) 1);
   1.585 -by (auto_tac (claset(),simpset() addsimps [Infinitesimal_subset_HFinite 
   1.586 -    RS subsetD]));
   1.587 -qed "STAR_sin_cos_Infinitesimal_mult";
   1.588 -
   1.589 -Goal "hypreal_of_real pi : HFinite";
   1.590 -by (Simp_tac 1);
   1.591 -qed "HFinite_pi";
   1.592 -
   1.593 -(* lemmas *)
   1.594 -
   1.595 -Goal "N : HNatInfinite \
   1.596 -\     ==> hypreal_of_real a = \
   1.597 -\         hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)";
   1.598 -by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   1.599 -    HNatInfinite_not_eq_zero]));
   1.600 -val lemma_split_hypreal_of_real = result();
   1.601 -
   1.602 -Goal "[|x : Infinitesimal; x ~= 0 |] ==> ( *f* sin) x/x @= 1";
   1.603 -by (cut_inst_tac [("x","0")] DERIV_sin 1);
   1.604 -by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
   1.605 -    nsderiv_def,hypreal_of_real_zero,hypreal_of_real_one]));
   1.606 -qed "STAR_sin_Infinitesimal_divide";
   1.607 -
   1.608 -(*------------------------------------------------------------------------*) 
   1.609 -(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
   1.610 -(*------------------------------------------------------------------------*)
   1.611 -
   1.612 -Goal "n : HNatInfinite \
   1.613 -\     ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1";
   1.614 -by (rtac STAR_sin_Infinitesimal_divide 1);
   1.615 -by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
   1.616 -val lemma_sin_pi = result();
   1.617 -
   1.618 -Goal "n : HNatInfinite \
   1.619 -\     ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1";
   1.620 -by (forward_tac [lemma_sin_pi] 1);
   1.621 -by (auto_tac (claset(),simpset() addsimps [hypreal_divide_def]));
   1.622 -qed "STAR_sin_inverse_HNatInfinite";
   1.623 -
   1.624 -Goalw [hypreal_divide_def] 
   1.625 -     "N : HNatInfinite \
   1.626 -\     ==> hypreal_of_real pi/(hypreal_of_hypnat N) : Infinitesimal";
   1.627 -by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult2],simpset()));
   1.628 -qed "Infinitesimal_pi_divide_HNatInfinite";
   1.629 -
   1.630 -Goal "N : HNatInfinite \
   1.631 -\     ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0";
   1.632 -by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
   1.633 -qed "pi_divide_HNatInfinite_not_zero";
   1.634 -Addsimps [pi_divide_HNatInfinite_not_zero];
   1.635 -
   1.636 -Goal "n : HNatInfinite \
   1.637 -\     ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n \
   1.638 -\         @= hypreal_of_real pi";
   1.639 -by (ftac ([Infinitesimal_pi_divide_HNatInfinite,pi_divide_HNatInfinite_not_zero] 
   1.640 -          MRS STAR_sin_Infinitesimal_divide) 1);
   1.641 -by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_distrib]));
   1.642 -by (res_inst_tac [("a","inverse(hypreal_of_real pi)")] approx_SReal_mult_cancel 1);
   1.643 -by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @ mult_ac));
   1.644 -qed "STAR_sin_pi_divide_HNatInfinite_approx_pi";
   1.645 -
   1.646 -Goal "n : HNatInfinite \
   1.647 -\     ==> hypreal_of_hypnat n * \
   1.648 -\         ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \
   1.649 -\         @= hypreal_of_real pi";
   1.650 -by (rtac (hypreal_mult_commute RS subst) 1);
   1.651 -by (etac STAR_sin_pi_divide_HNatInfinite_approx_pi 1);
   1.652 -qed "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
   1.653 -
   1.654 -(*** more theorems ***)
   1.655 -
   1.656 -Goalw [real_divide_def] 
   1.657 -     "N : HNatInfinite \
   1.658 -\     ==> ( *fNat* (%x. pi / real x)) N : Infinitesimal";
   1.659 -by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
   1.660 -    simpset() addsimps [starfunNat_mult RS sym,starfunNat_inverse RS sym,
   1.661 -    starfunNat_real_of_nat]));
   1.662 -qed "starfunNat_pi_divide_n_Infinitesimal";
   1.663 -
   1.664 -Goal "N : HNatInfinite ==> \
   1.665 -\     ( *f* sin) (( *fNat* (%x. pi / real x)) N) @= \
   1.666 -\     hypreal_of_real pi/(hypreal_of_hypnat N)";
   1.667 -by (auto_tac (claset() addSIs [STAR_sin_Infinitesimal,
   1.668 -    Infinitesimal_HFinite_mult2],simpset() addsimps [starfunNat_mult RS sym,
   1.669 -    hypreal_divide_def,real_divide_def,starfunNat_inverse_real_of_nat_eq]));
   1.670 -qed "STAR_sin_pi_divide_n_approx";
   1.671 -
   1.672 -(*** move to NSA ***)
   1.673 -Goalw [hypnat_zero_def] "(n <= (0::hypnat)) = (n = 0)";
   1.674 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.675 -by (auto_tac (claset(),simpset() addsimps [hypnat_le]));
   1.676 -qed "hypnat_le_zero_cancel";
   1.677 -AddIffs [hypnat_le_zero_cancel];
   1.678 -
   1.679 -Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N";
   1.680 -by (rtac ccontr 1);
   1.681 -by (auto_tac (claset(),
   1.682 -   simpset() addsimps [hypreal_of_hypnat_zero RS sym, linorder_not_less]));
   1.683 -qed "HNatInfinite_hypreal_of_hypnat_gt_zero";
   1.684 -
   1.685 -bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero",
   1.686 -          HNatInfinite_hypreal_of_hypnat_gt_zero RS hypreal_not_refl2 RS not_sym);
   1.687 -(*** END: move to NSA ***)
   1.688 -
   1.689 -Goalw [NSLIMSEQ_def] "(%n. real n * sin (pi / real n)) ----NS> pi";
   1.690 -by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
   1.691 -    starfunNat_real_of_nat]));
   1.692 -by (res_inst_tac [("f1","sin")]  (starfun_stafunNat_o2 RS subst) 1);
   1.693 -by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
   1.694 -    starfunNat_real_of_nat,real_divide_def]));
   1.695 -by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   1.696 -by (auto_tac (claset() addDs [STAR_sin_pi_divide_HNatInfinite_approx_pi],
   1.697 -    simpset() addsimps [starfunNat_real_of_nat,hypreal_mult_commute,
   1.698 -    symmetric hypreal_divide_def]));
   1.699 -qed "NSLIMSEQ_sin_pi";
   1.700 -
   1.701 -Goalw [NSLIMSEQ_def] "(%n. cos (pi / real n))----NS> 1";
   1.702 -by Auto_tac;
   1.703 -by (res_inst_tac [("f1","cos")]  (starfun_stafunNat_o2 RS subst) 1);
   1.704 -by (rtac STAR_cos_Infinitesimal 1);
   1.705 -by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
   1.706 -    simpset() addsimps [starfunNat_mult RS sym,real_divide_def,
   1.707 -    starfunNat_inverse RS sym,starfunNat_real_of_nat]));
   1.708 -qed "NSLIMSEQ_cos_one";
   1.709 -
   1.710 -Goal "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi";
   1.711 -by (rtac (simplify (simpset()) 
   1.712 -    ([NSLIMSEQ_sin_pi,NSLIMSEQ_cos_one] MRS NSLIMSEQ_mult)) 1);
   1.713 -qed "NSLIMSEQ_sin_cos_pi";
   1.714 -
   1.715 -(*------------------------------------------------------------------------*)
   1.716 -(* A familiar approximation to cos x when x is small                      *)
   1.717 -(*------------------------------------------------------------------------*)
   1.718 -
   1.719 -Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2";
   1.720 -by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
   1.721 -by (auto_tac (claset(),simpset() addsimps [Infinitesimal_approx_minus RS sym,
   1.722 -    hypreal_diff_def,hypreal_add_assoc RS sym,numeral_2_eq_2]));
   1.723 -qed "STAR_cos_Infinitesimal_approx";
   1.724 -
   1.725 -(* move to NSA *)
   1.726 -Goalw [hypreal_divide_def] 
   1.727 -  "[| x : Infinitesimal; y : Reals; y ~= 0 |] ==> x/y : Infinitesimal";
   1.728 -by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult]
   1.729 -    addSDs [SReal_inverse RS (SReal_subset_HFinite RS subsetD)],simpset()));
   1.730 -qed "Infinitesimal_SReal_divide";
   1.731 -
   1.732 -Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2";
   1.733 -by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
   1.734 -by (auto_tac (claset() addIs [Infinitesimal_SReal_divide],
   1.735 -    simpset() addsimps [Infinitesimal_approx_minus RS sym,
   1.736 -    numeral_2_eq_2]));
   1.737 -qed "STAR_cos_Infinitesimal_approx2";
   1.738 -
   1.739 -
   1.740 -
   1.741 -
   1.742 -
     2.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 01 05:39:32 2004 +0100
     2.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 01 11:52:59 2004 +0100
     2.3 @@ -1,23 +1,740 @@
     2.4  (*  Title       : HTranscendental.thy
     2.5      Author      : Jacques D. Fleuriot
     2.6      Copyright   : 2001 University of Edinburgh
     2.7 -    Description : Nonstandard extensions of transcendental functions
     2.8 +
     2.9 +Converted to Isar and polished by lcp
    2.10  *)
    2.11  
    2.12 -HTranscendental = Transcendental + IntFloor + 
    2.13 +header{*Nonstandard Extensions of Transcendental Functions*}
    2.14 +
    2.15 +theory HTranscendental = Transcendental + IntFloor:
    2.16  
    2.17  constdefs
    2.18  
    2.19 -
    2.20 -    (* define exponential function using standard part *)
    2.21 -    exphr :: real => hypreal
    2.22 +  exphr :: "real => hypreal"
    2.23 +    --{*define exponential function using standard part *}
    2.24      "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
    2.25  
    2.26 -    sinhr :: real => hypreal
    2.27 +  sinhr :: "real => hypreal"
    2.28      "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
    2.29               ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
    2.30    
    2.31 -    coshr :: real => hypreal
    2.32 +  coshr :: "real => hypreal"
    2.33      "coshr x == st(sumhr (0, whn, %n. (if even(n) then
    2.34              ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
    2.35 -end
    2.36 \ No newline at end of file
    2.37 +
    2.38 +
    2.39 +subsection{*Nonstandard Extension of Square Root Function*}
    2.40 +
    2.41 +lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
    2.42 +by (simp add: starfun hypreal_zero_num)
    2.43 +
    2.44 +lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
    2.45 +by (simp add: starfun hypreal_one_num)
    2.46 +
    2.47 +lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
    2.48 +apply (rule eq_Abs_hypreal [of x])
    2.49 +apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
    2.50 +                      real_sqrt_pow2_iff 
    2.51 +            simp del: hpowr_Suc realpow_Suc)
    2.52 +done
    2.53 +
    2.54 +lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    2.55 +apply (rule eq_Abs_hypreal [of x])
    2.56 +apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
    2.57 +            simp add: hypreal_less starfun hrealpow hypreal_zero_num 
    2.58 +            simp del: hpowr_Suc realpow_Suc)
    2.59 +done
    2.60 +
    2.61 +lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
    2.62 +by (frule hypreal_sqrt_gt_zero_pow2, auto)
    2.63 +
    2.64 +lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
    2.65 +apply (frule hypreal_sqrt_pow2_gt_zero)
    2.66 +apply (auto simp add: numeral_2_eq_2)
    2.67 +done
    2.68 +
    2.69 +lemma hypreal_inverse_sqrt_pow2:
    2.70 +     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
    2.71 +apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
    2.72 +apply (auto dest: hypreal_sqrt_gt_zero_pow2)
    2.73 +done
    2.74 +
    2.75 +lemma hypreal_sqrt_mult_distrib: 
    2.76 +    "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    2.77 +apply (rule eq_Abs_hypreal [of x])
    2.78 +apply (rule eq_Abs_hypreal [of y])
    2.79 +apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
    2.80 +apply (auto intro: real_sqrt_mult_distrib) 
    2.81 +done
    2.82 +
    2.83 +lemma hypreal_sqrt_mult_distrib2:
    2.84 +     "[|0\<le>x; 0\<le>y |] ==>  
    2.85 +     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    2.86 +by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
    2.87 +
    2.88 +lemma hypreal_sqrt_approx_zero [simp]:
    2.89 +     "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    2.90 +apply (auto simp add: mem_infmal_iff [symmetric])
    2.91 +apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    2.92 +apply (auto intro: Infinitesimal_mult 
    2.93 +            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
    2.94 +            simp add: numeral_2_eq_2)
    2.95 +done
    2.96 +
    2.97 +lemma hypreal_sqrt_approx_zero2 [simp]:
    2.98 +     "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    2.99 +by (auto simp add: order_le_less)
   2.100 +
   2.101 +lemma hypreal_sqrt_sum_squares [simp]:
   2.102 +     "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
   2.103 +apply (rule hypreal_sqrt_approx_zero2)
   2.104 +apply (rule hypreal_le_add_order)+
   2.105 +apply (auto simp add: zero_le_square)
   2.106 +done
   2.107 +
   2.108 +lemma hypreal_sqrt_sum_squares2 [simp]:
   2.109 +     "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
   2.110 +apply (rule hypreal_sqrt_approx_zero2)
   2.111 +apply (rule hypreal_le_add_order)
   2.112 +apply (auto simp add: zero_le_square)
   2.113 +done
   2.114 +
   2.115 +lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
   2.116 +apply (rule eq_Abs_hypreal [of x])
   2.117 +apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
   2.118 +apply (auto intro: real_sqrt_gt_zero)
   2.119 +done
   2.120 +
   2.121 +lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
   2.122 +by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
   2.123 +
   2.124 +lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
   2.125 +apply (rule eq_Abs_hypreal [of x])
   2.126 +apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
   2.127 +done
   2.128 +
   2.129 +lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
   2.130 +apply (rule hrealpow_two [THEN subst])
   2.131 +apply (rule numeral_2_eq_2 [THEN subst])
   2.132 +apply (rule hypreal_sqrt_hrabs)
   2.133 +done
   2.134 +
   2.135 +lemma hypreal_sqrt_hyperpow_hrabs [simp]:
   2.136 +     "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
   2.137 +apply (rule eq_Abs_hypreal [of x])
   2.138 +apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
   2.139 +done
   2.140 +
   2.141 +lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
   2.142 +apply (rule HFinite_square_iff [THEN iffD1])
   2.143 +apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
   2.144 +done
   2.145 +
   2.146 +lemma st_hypreal_sqrt:
   2.147 +     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
   2.148 +apply (rule power_inject_base [where n=1])
   2.149 +apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
   2.150 +apply (rule st_mult [THEN subst])
   2.151 +apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
   2.152 +apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
   2.153 +apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
   2.154 +done
   2.155 +
   2.156 +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
   2.157 +apply (rule eq_Abs_hypreal [of x])
   2.158 +apply (rule eq_Abs_hypreal [of y])
   2.159 +apply (simp add: starfun hypreal_add hrealpow hypreal_le 
   2.160 +            del: hpowr_Suc realpow_Suc)
   2.161 +done
   2.162 +
   2.163 +lemma HFinite_hypreal_sqrt:
   2.164 +     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
   2.165 +apply (auto simp add: order_le_less)
   2.166 +apply (rule HFinite_square_iff [THEN iffD1])
   2.167 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.168 +apply (simp add: numeral_2_eq_2)
   2.169 +done
   2.170 +
   2.171 +lemma HFinite_hypreal_sqrt_imp_HFinite:
   2.172 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
   2.173 +apply (auto simp add: order_le_less)
   2.174 +apply (drule HFinite_square_iff [THEN iffD2])
   2.175 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.176 +apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
   2.177 +done
   2.178 +
   2.179 +lemma HFinite_hypreal_sqrt_iff [simp]:
   2.180 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
   2.181 +by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
   2.182 +
   2.183 +lemma HFinite_sqrt_sum_squares [simp]:
   2.184 +     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
   2.185 +apply (rule HFinite_hypreal_sqrt_iff)
   2.186 +apply (rule hypreal_le_add_order)
   2.187 +apply (auto simp add: zero_le_square)
   2.188 +done
   2.189 +
   2.190 +lemma Infinitesimal_hypreal_sqrt:
   2.191 +     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
   2.192 +apply (auto simp add: order_le_less)
   2.193 +apply (rule Infinitesimal_square_iff [THEN iffD2])
   2.194 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.195 +apply (simp add: numeral_2_eq_2)
   2.196 +done
   2.197 +
   2.198 +lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
   2.199 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
   2.200 +apply (auto simp add: order_le_less)
   2.201 +apply (drule Infinitesimal_square_iff [THEN iffD1])
   2.202 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.203 +apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
   2.204 +done
   2.205 +
   2.206 +lemma Infinitesimal_hypreal_sqrt_iff [simp]:
   2.207 +     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   2.208 +by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
   2.209 +
   2.210 +lemma Infinitesimal_sqrt_sum_squares [simp]:
   2.211 +     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
   2.212 +apply (rule Infinitesimal_hypreal_sqrt_iff)
   2.213 +apply (rule hypreal_le_add_order)
   2.214 +apply (auto simp add: zero_le_square)
   2.215 +done
   2.216 +
   2.217 +lemma HInfinite_hypreal_sqrt:
   2.218 +     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
   2.219 +apply (auto simp add: order_le_less)
   2.220 +apply (rule HInfinite_square_iff [THEN iffD1])
   2.221 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.222 +apply (simp add: numeral_2_eq_2)
   2.223 +done
   2.224 +
   2.225 +lemma HInfinite_hypreal_sqrt_imp_HInfinite:
   2.226 +     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
   2.227 +apply (auto simp add: order_le_less)
   2.228 +apply (drule HInfinite_square_iff [THEN iffD2])
   2.229 +apply (drule hypreal_sqrt_gt_zero_pow2)
   2.230 +apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
   2.231 +done
   2.232 +
   2.233 +lemma HInfinite_hypreal_sqrt_iff [simp]:
   2.234 +     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
   2.235 +by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
   2.236 +
   2.237 +lemma HInfinite_sqrt_sum_squares [simp]:
   2.238 +     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
   2.239 +apply (rule HInfinite_hypreal_sqrt_iff)
   2.240 +apply (rule hypreal_le_add_order)
   2.241 +apply (auto simp add: zero_le_square)
   2.242 +done
   2.243 +
   2.244 +lemma HFinite_exp [simp]:
   2.245 +     "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
   2.246 +by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   2.247 +         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   2.248 +                   convergent_NSconvergent_iff [symmetric] 
   2.249 +                   summable_convergent_sumr_iff [symmetric] summable_exp)
   2.250 +
   2.251 +lemma exphr_zero [simp]: "exphr 0 = 1"
   2.252 +apply (simp add: exphr_def sumhr_split_add
   2.253 +                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   2.254 +apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
   2.255 +                 hypnat_omega_def hypreal_add 
   2.256 +            del: hypnat_add_zero_left)
   2.257 +apply (simp add: hypreal_one_num [symmetric])
   2.258 +done
   2.259 +
   2.260 +lemma coshr_zero [simp]: "coshr 0 = 1"
   2.261 +apply (simp add: coshr_def sumhr_split_add
   2.262 +                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
   2.263 +apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def 
   2.264 +         hypnat_add hypnat_omega_def st_add [symmetric] 
   2.265 +         hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
   2.266 +       del: hypnat_add_zero_left)
   2.267 +done
   2.268 +
   2.269 +lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
   2.270 +by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
   2.271 +
   2.272 +lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
   2.273 +apply (case_tac "x = 0")
   2.274 +apply (cut_tac [2] x = 0 in DERIV_exp)
   2.275 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   2.276 +apply (drule_tac x = x in bspec, auto)
   2.277 +apply (drule_tac c = x in approx_mult1)
   2.278 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
   2.279 +            simp add: mult_assoc)
   2.280 +apply (rule approx_add_right_cancel [where d="-1"])
   2.281 +apply (rule approx_sym [THEN [2] approx_trans2])
   2.282 +apply (auto simp add: mem_infmal_iff)
   2.283 +done
   2.284 +
   2.285 +lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   2.286 +by (auto intro: STAR_exp_Infinitesimal)
   2.287 +
   2.288 +lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
   2.289 +apply (rule eq_Abs_hypreal [of x])
   2.290 +apply (rule eq_Abs_hypreal [of y])
   2.291 +apply (simp add: starfun hypreal_add hypreal_mult exp_add)
   2.292 +done
   2.293 +
   2.294 +lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
   2.295 +apply (simp add: exphr_def)
   2.296 +apply (rule st_hypreal_of_real [THEN subst])
   2.297 +apply (rule approx_st_eq, auto)
   2.298 +apply (rule approx_minus_iff [THEN iffD2])
   2.299 +apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
   2.300 +apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
   2.301 +apply (insert exp_converges [of x]) 
   2.302 +apply (simp add: sums_def) 
   2.303 +apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
   2.304 +apply (simp add: LIMSEQ_NSLIMSEQ_iff)
   2.305 +done
   2.306 +
   2.307 +lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
   2.308 +apply (rule eq_Abs_hypreal [of x])
   2.309 +apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
   2.310 +done
   2.311 +
   2.312 +(* exp (oo) is infinite *)
   2.313 +lemma starfun_exp_HInfinite:
   2.314 +     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
   2.315 +apply (frule starfun_exp_ge_add_one_self)
   2.316 +apply (rule HInfinite_ge_HInfinite, assumption)
   2.317 +apply (rule order_trans [of _ "1+x"], auto) 
   2.318 +done
   2.319 +
   2.320 +lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
   2.321 +apply (rule eq_Abs_hypreal [of x])
   2.322 +apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
   2.323 +done
   2.324 +
   2.325 +(* exp (-oo) is infinitesimal *)
   2.326 +lemma starfun_exp_Infinitesimal:
   2.327 +     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
   2.328 +apply (subgoal_tac "\<exists>y. x = - y")
   2.329 +apply (rule_tac [2] x = "- x" in exI)
   2.330 +apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
   2.331 +            simp add: starfun_exp_minus HInfinite_minus_iff)
   2.332 +done
   2.333 +
   2.334 +lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
   2.335 +apply (rule eq_Abs_hypreal [of x])
   2.336 +apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
   2.337 +done
   2.338 +
   2.339 +(* needs derivative of inverse function
   2.340 +   TRY a NS one today!!!
   2.341 +
   2.342 +Goal "x @= 1 ==> ( *f* ln) x @= 1"
   2.343 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.344 +by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
   2.345 +
   2.346 +
   2.347 +Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
   2.348 +
   2.349 +*)
   2.350 +
   2.351 +
   2.352 +lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
   2.353 +apply (rule eq_Abs_hypreal [of x])
   2.354 +apply (simp add: starfun)
   2.355 +done
   2.356 +
   2.357 +lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
   2.358 +apply (rule eq_Abs_hypreal [of x])
   2.359 +apply (simp add: starfun hypreal_zero_num hypreal_less)
   2.360 +done
   2.361 +
   2.362 +lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
   2.363 +by (auto simp add: starfun)
   2.364 +
   2.365 +lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
   2.366 +apply (rule eq_Abs_hypreal [of x])
   2.367 +apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
   2.368 +done
   2.369 +
   2.370 +lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
   2.371 +apply (rule eq_Abs_hypreal [of x])
   2.372 +apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
   2.373 +done
   2.374 +
   2.375 +lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
   2.376 +apply (rule eq_Abs_hypreal [of x])
   2.377 +apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   2.378 +done
   2.379 +
   2.380 +lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
   2.381 +apply (rule eq_Abs_hypreal [of x])
   2.382 +apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   2.383 +apply (auto dest: ln_not_eq_zero) 
   2.384 +done
   2.385 +
   2.386 +lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
   2.387 +apply (rule HFinite_bounded)
   2.388 +apply (rule_tac [2] order_less_imp_le)
   2.389 +apply (rule_tac [2] starfun_ln_less_self)
   2.390 +apply (rule_tac [2] order_less_le_trans, auto)
   2.391 +done
   2.392 +
   2.393 +lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
   2.394 +apply (rule eq_Abs_hypreal [of x])
   2.395 +apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
   2.396 +apply (simp add: ln_inverse)
   2.397 +done
   2.398 +
   2.399 +lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
   2.400 +apply (rule eq_Abs_hypreal [of x])
   2.401 +apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
   2.402 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   2.403 +apply (rule_tac x = "exp u" in exI)
   2.404 +apply (ultra, arith)
   2.405 +done
   2.406 +
   2.407 +lemma starfun_exp_add_HFinite_Infinitesimal_approx:
   2.408 +     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
   2.409 +apply (simp add: STAR_exp_add)
   2.410 +apply (frule STAR_exp_Infinitesimal)
   2.411 +apply (drule approx_mult2)
   2.412 +apply (auto intro: starfun_exp_HFinite)
   2.413 +done
   2.414 +
   2.415 +(* using previous result to get to result *)
   2.416 +lemma starfun_ln_HInfinite:
   2.417 +     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   2.418 +apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   2.419 +apply (drule starfun_exp_HFinite)
   2.420 +apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   2.421 +done
   2.422 +
   2.423 +lemma starfun_exp_HInfinite_Infinitesimal_disj:
   2.424 + "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
   2.425 +apply (insert linorder_linear [of x 0]) 
   2.426 +apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
   2.427 +done
   2.428 +
   2.429 +(* check out this proof!!! *)
   2.430 +lemma starfun_ln_HFinite_not_Infinitesimal:
   2.431 +     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
   2.432 +apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   2.433 +apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   2.434 +apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   2.435 +            del: starfun_exp_ln_iff)
   2.436 +done
   2.437 +
   2.438 +(* we do proof by considering ln of 1/x *)
   2.439 +lemma starfun_ln_Infinitesimal_HInfinite:
   2.440 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   2.441 +apply (drule Infinitesimal_inverse_HInfinite)
   2.442 +apply (frule positive_imp_inverse_positive)
   2.443 +apply (drule_tac [2] starfun_ln_HInfinite)
   2.444 +apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   2.445 +done
   2.446 +
   2.447 +lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
   2.448 +apply (rule eq_Abs_hypreal [of x])
   2.449 +apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
   2.450 +apply (auto intro: ln_less_zero) 
   2.451 +done
   2.452 +
   2.453 +lemma starfun_ln_Infinitesimal_less_zero:
   2.454 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
   2.455 +apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   2.456 +apply (drule bspec [where x = 1])
   2.457 +apply (auto simp add: abs_if)
   2.458 +done
   2.459 +
   2.460 +lemma starfun_ln_HInfinite_gt_zero:
   2.461 +     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
   2.462 +apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   2.463 +apply (drule bspec [where x = 1])
   2.464 +apply (auto simp add: abs_if)
   2.465 +done
   2.466 +
   2.467 +(*
   2.468 +Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
   2.469 +*)
   2.470 +
   2.471 +lemma HFinite_sin [simp]:
   2.472 +     "sumhr (0, whn, %n. (if even(n) then 0 else  
   2.473 +              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
   2.474 +              \<in> HFinite"
   2.475 +apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   2.476 +            simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   2.477 +                      convergent_NSconvergent_iff [symmetric] 
   2.478 +                      summable_convergent_sumr_iff [symmetric])
   2.479 +apply (simp only: One_nat_def summable_sin)
   2.480 +done
   2.481 +
   2.482 +lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
   2.483 +by (simp add: starfun hypreal_zero_num)
   2.484 +
   2.485 +lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
   2.486 +apply (case_tac "x = 0")
   2.487 +apply (cut_tac [2] x = 0 in DERIV_sin)
   2.488 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   2.489 +apply (drule bspec [where x = x], auto)
   2.490 +apply (drule approx_mult1 [where c = x])
   2.491 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   2.492 +           simp add: mult_assoc)
   2.493 +done
   2.494 +
   2.495 +lemma HFinite_cos [simp]:
   2.496 +     "sumhr (0, whn, %n. (if even(n) then  
   2.497 +            ((- 1) ^ (n div 2))/(real (fact n)) else  
   2.498 +            0) * x ^ n) \<in> HFinite"
   2.499 +by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
   2.500 +         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
   2.501 +                   convergent_NSconvergent_iff [symmetric] 
   2.502 +                   summable_convergent_sumr_iff [symmetric] summable_cos)
   2.503 +
   2.504 +lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
   2.505 +by (simp add: starfun hypreal_zero_num hypreal_one_num)
   2.506 +
   2.507 +lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
   2.508 +apply (case_tac "x = 0")
   2.509 +apply (cut_tac [2] x = 0 in DERIV_cos)
   2.510 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   2.511 +apply (drule bspec [where x = x])
   2.512 +apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
   2.513 +apply (drule approx_mult1 [where c = x])
   2.514 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   2.515 +            simp add: mult_assoc hypreal_of_real_one)
   2.516 +apply (rule approx_add_right_cancel [where d = "-1"], auto)
   2.517 +done
   2.518 +
   2.519 +lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   2.520 +by (simp add: starfun hypreal_zero_num)
   2.521 +
   2.522 +lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
   2.523 +apply (case_tac "x = 0")
   2.524 +apply (cut_tac [2] x = 0 in DERIV_tan)
   2.525 +apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
   2.526 +apply (drule bspec [where x = x], auto)
   2.527 +apply (drule approx_mult1 [where c = x])
   2.528 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   2.529 +             simp add: mult_assoc)
   2.530 +done
   2.531 +
   2.532 +lemma STAR_sin_cos_Infinitesimal_mult:
   2.533 +     "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
   2.534 +apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) 
   2.535 +apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   2.536 +done
   2.537 +
   2.538 +lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
   2.539 +by simp
   2.540 +
   2.541 +(* lemmas *)
   2.542 +
   2.543 +lemma lemma_split_hypreal_of_real:
   2.544 +     "N \<in> HNatInfinite  
   2.545 +      ==> hypreal_of_real a =  
   2.546 +          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
   2.547 +by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
   2.548 +
   2.549 +lemma STAR_sin_Infinitesimal_divide:
   2.550 +     "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
   2.551 +apply (cut_tac x = 0 in DERIV_sin)
   2.552 +apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
   2.553 +done
   2.554 +
   2.555 +(*------------------------------------------------------------------------*) 
   2.556 +(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
   2.557 +(*------------------------------------------------------------------------*)
   2.558 +
   2.559 +lemma lemma_sin_pi:
   2.560 +     "n \<in> HNatInfinite  
   2.561 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
   2.562 +apply (rule STAR_sin_Infinitesimal_divide)
   2.563 +apply (auto simp add: HNatInfinite_not_eq_zero)
   2.564 +done
   2.565 +
   2.566 +lemma STAR_sin_inverse_HNatInfinite:
   2.567 +     "n \<in> HNatInfinite  
   2.568 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
   2.569 +apply (frule lemma_sin_pi)
   2.570 +apply (simp add: divide_inverse_zero)
   2.571 +done
   2.572 +
   2.573 +lemma Infinitesimal_pi_divide_HNatInfinite: 
   2.574 +     "N \<in> HNatInfinite  
   2.575 +      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   2.576 +apply (simp add: divide_inverse_zero)
   2.577 +apply (auto intro: Infinitesimal_HFinite_mult2)
   2.578 +done
   2.579 +
   2.580 +lemma pi_divide_HNatInfinite_not_zero [simp]:
   2.581 +     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
   2.582 +by (simp add: HNatInfinite_not_eq_zero)
   2.583 +
   2.584 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   2.585 +     "n \<in> HNatInfinite  
   2.586 +      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   2.587 +          @= hypreal_of_real pi"
   2.588 +apply (frule STAR_sin_Infinitesimal_divide
   2.589 +               [OF Infinitesimal_pi_divide_HNatInfinite 
   2.590 +                   pi_divide_HNatInfinite_not_zero])
   2.591 +apply (auto simp add: hypreal_inverse_distrib)
   2.592 +apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   2.593 +apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
   2.594 +done
   2.595 +
   2.596 +lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   2.597 +     "n \<in> HNatInfinite  
   2.598 +      ==> hypreal_of_hypnat n *  
   2.599 +          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   2.600 +          @= hypreal_of_real pi"
   2.601 +apply (rule mult_commute [THEN subst])
   2.602 +apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   2.603 +done
   2.604 +
   2.605 +lemma starfunNat_pi_divide_n_Infinitesimal: 
   2.606 +     "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
   2.607 +by (auto intro!: Infinitesimal_HFinite_mult2 
   2.608 +         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   2.609 +                   starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   2.610 +
   2.611 +lemma STAR_sin_pi_divide_n_approx:
   2.612 +     "N \<in> HNatInfinite ==>  
   2.613 +      ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
   2.614 +      hypreal_of_real pi/(hypreal_of_hypnat N)"
   2.615 +by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
   2.616 +         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   2.617 +                   starfunNat_inverse_real_of_nat_eq)
   2.618 +
   2.619 +lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
   2.620 +apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
   2.621 +apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
   2.622 +apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
   2.623 +apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
   2.624 +apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   2.625 +            simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
   2.626 +done
   2.627 +
   2.628 +lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
   2.629 +apply (simp add: NSLIMSEQ_def, auto)
   2.630 +apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
   2.631 +apply (rule STAR_cos_Infinitesimal)
   2.632 +apply (auto intro!: Infinitesimal_HFinite_mult2 
   2.633 +            simp add: starfunNat_mult [symmetric] divide_inverse_zero
   2.634 +                      starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   2.635 +done
   2.636 +
   2.637 +lemma NSLIMSEQ_sin_cos_pi:
   2.638 +     "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
   2.639 +by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   2.640 +
   2.641 +
   2.642 +text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
   2.643 +
   2.644 +lemma STAR_cos_Infinitesimal_approx:
   2.645 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
   2.646 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   2.647 +apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   2.648 +            diff_minus add_assoc [symmetric] numeral_2_eq_2)
   2.649 +done
   2.650 +
   2.651 +lemma STAR_cos_Infinitesimal_approx2:
   2.652 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
   2.653 +apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   2.654 +apply (auto intro: Infinitesimal_SReal_divide 
   2.655 +            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
   2.656 +done
   2.657 +
   2.658 +ML
   2.659 +{*
   2.660 +val STAR_sqrt_zero = thm "STAR_sqrt_zero";
   2.661 +val STAR_sqrt_one = thm "STAR_sqrt_one";
   2.662 +val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
   2.663 +val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
   2.664 +val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
   2.665 +val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
   2.666 +val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
   2.667 +val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
   2.668 +val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
   2.669 +val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
   2.670 +val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
   2.671 +val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
   2.672 +val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
   2.673 +val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
   2.674 +val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
   2.675 +val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
   2.676 +val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
   2.677 +val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
   2.678 +val star_sqrt_HFinite = thm "star_sqrt_HFinite";
   2.679 +val st_hypreal_sqrt = thm "st_hypreal_sqrt";
   2.680 +val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
   2.681 +val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
   2.682 +val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
   2.683 +val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
   2.684 +val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
   2.685 +val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
   2.686 +val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
   2.687 +val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
   2.688 +val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
   2.689 +val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
   2.690 +val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
   2.691 +val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
   2.692 +val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
   2.693 +val HFinite_exp = thm "HFinite_exp";
   2.694 +val exphr_zero = thm "exphr_zero";
   2.695 +val coshr_zero = thm "coshr_zero";
   2.696 +val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
   2.697 +val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
   2.698 +val STAR_exp_epsilon = thm "STAR_exp_epsilon";
   2.699 +val STAR_exp_add = thm "STAR_exp_add";
   2.700 +val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
   2.701 +val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
   2.702 +val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
   2.703 +val starfun_exp_minus = thm "starfun_exp_minus";
   2.704 +val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
   2.705 +val starfun_exp_gt_one = thm "starfun_exp_gt_one";
   2.706 +val starfun_ln_exp = thm "starfun_ln_exp";
   2.707 +val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
   2.708 +val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
   2.709 +val starfun_ln_less_self = thm "starfun_ln_less_self";
   2.710 +val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
   2.711 +val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
   2.712 +val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
   2.713 +val starfun_ln_HFinite = thm "starfun_ln_HFinite";
   2.714 +val starfun_ln_inverse = thm "starfun_ln_inverse";
   2.715 +val starfun_exp_HFinite = thm "starfun_exp_HFinite";
   2.716 +val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
   2.717 +val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
   2.718 +val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
   2.719 +val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
   2.720 +val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
   2.721 +val starfun_ln_less_zero = thm "starfun_ln_less_zero";
   2.722 +val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
   2.723 +val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
   2.724 +val HFinite_sin = thm "HFinite_sin";
   2.725 +val STAR_sin_zero = thm "STAR_sin_zero";
   2.726 +val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
   2.727 +val HFinite_cos = thm "HFinite_cos";
   2.728 +val STAR_cos_zero = thm "STAR_cos_zero";
   2.729 +val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
   2.730 +val STAR_tan_zero = thm "STAR_tan_zero";
   2.731 +val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
   2.732 +val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
   2.733 +val HFinite_pi = thm "HFinite_pi";
   2.734 +val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
   2.735 +val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
   2.736 +val lemma_sin_pi = thm "lemma_sin_pi";
   2.737 +val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
   2.738 +val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
   2.739 +val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
   2.740 +val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
   2.741 +val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
   2.742 +val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
   2.743 +val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
   2.744 +val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
   2.745 +val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
   2.746 +val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
   2.747 +val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
   2.748 +val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
   2.749 +*}
   2.750 +
   2.751 +
   2.752 +end
     3.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Mon Mar 01 05:39:32 2004 +0100
     3.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Mar 01 11:52:59 2004 +0100
     3.3 @@ -395,6 +395,11 @@
     3.4      by (simp add: hypnat_mult_less_mono2)
     3.5  qed
     3.6  
     3.7 +lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
     3.8 +apply (rule eq_Abs_hypnat [of n])
     3.9 +apply (simp add: hypnat_zero_def hypnat_le)
    3.10 +done
    3.11 +
    3.12  lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
    3.13  apply (rule eq_Abs_hypnat [of m])
    3.14  apply (rule eq_Abs_hypnat [of n])
    3.15 @@ -809,6 +814,12 @@
    3.16  apply (drule_tac x = "m + 1" in spec, ultra)
    3.17  done
    3.18  
    3.19 +lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
    3.20 +     "N \<in> HNatInfinite ==> 0 < hypreal_of_hypnat N"
    3.21 +apply (rule ccontr)
    3.22 +apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
    3.23 +done
    3.24 +
    3.25  
    3.26  ML
    3.27  {*
     4.1 --- a/src/HOL/Hyperreal/NSA.thy	Mon Mar 01 05:39:32 2004 +0100
     4.2 +++ b/src/HOL/Hyperreal/NSA.thy	Mon Mar 01 11:52:59 2004 +0100
     4.3 @@ -1,6 +1,8 @@
     4.4  (*  Title       : NSA.thy
     4.5      Author      : Jacques D. Fleuriot
     4.6      Copyright   : 1998  University of Cambridge
     4.7 +
     4.8 +Converted to Isar and polished by lcp
     4.9  *)
    4.10  
    4.11  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    4.12 @@ -43,9 +45,7 @@
    4.13  
    4.14  
    4.15  
    4.16 -(*--------------------------------------------------------------------
    4.17 -     Closure laws for members of (embedded) set standard real Reals
    4.18 - --------------------------------------------------------------------*)
    4.19 +subsection{*Closure Laws for  Standard Reals*}
    4.20  
    4.21  lemma SReal_add [simp]:
    4.22       "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
    4.23 @@ -80,7 +80,8 @@
    4.24  done
    4.25  declare SReal_minus_iff [simp]
    4.26  
    4.27 -lemma SReal_add_cancel: "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
    4.28 +lemma SReal_add_cancel:
    4.29 +     "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
    4.30  apply (drule_tac x = y in SReal_minus)
    4.31  apply (drule SReal_add, assumption, auto)
    4.32  done
    4.33 @@ -146,11 +147,12 @@
    4.34  done
    4.35  
    4.36  lemma SReal_hypreal_of_real_image:
    4.37 -      "[| \<exists>x. x: P; P <= Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
    4.38 +      "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
    4.39  apply (simp add: SReal_def, blast)
    4.40  done
    4.41  
    4.42 -lemma SReal_dense: "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
    4.43 +lemma SReal_dense:
    4.44 +     "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
    4.45  apply (auto simp add: SReal_iff)
    4.46  apply (drule real_dense, safe)
    4.47  apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
    4.48 @@ -159,12 +161,13 @@
    4.49  (*------------------------------------------------------------------
    4.50                     Completeness of Reals
    4.51   ------------------------------------------------------------------*)
    4.52 -lemma SReal_sup_lemma: "P <= Reals ==> ((\<exists>x \<in> P. y < x) =
    4.53 +lemma SReal_sup_lemma:
    4.54 +     "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
    4.55        (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
    4.56  by (blast dest!: SReal_iff [THEN iffD1])
    4.57  
    4.58  lemma SReal_sup_lemma2:
    4.59 -     "[| P <= Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
    4.60 +     "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
    4.61        ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
    4.62            (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
    4.63  apply (rule conjI)
    4.64 @@ -202,10 +205,10 @@
    4.65  apply (auto simp add: hypreal_of_real_isUb_iff)
    4.66  done
    4.67  
    4.68 -lemma hypreal_of_real_isLub_iff: "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
    4.69 +lemma hypreal_of_real_isLub_iff:
    4.70 +     "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
    4.71        (isLub (UNIV :: real set) Q Y)"
    4.72 -apply (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
    4.73 -done
    4.74 +by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
    4.75  
    4.76  (* lemmas *)
    4.77  lemma lemma_isUb_hypreal_of_real:
    4.78 @@ -220,16 +223,17 @@
    4.79       "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
    4.80  by (auto simp add: isLub_def leastP_def isUb_def)
    4.81  
    4.82 -lemma SReal_complete: "[| P <= Reals;  \<exists>x. x \<in> P;  \<exists>Y. isUb Reals P Y |]
    4.83 +lemma SReal_complete:
    4.84 +     "[| P \<subseteq> Reals;  \<exists>x. x \<in> P;  \<exists>Y. isUb Reals P Y |]
    4.85        ==> \<exists>t::hypreal. isLub Reals P t"
    4.86  apply (frule SReal_hypreal_of_real_image)
    4.87  apply (auto, drule lemma_isUb_hypreal_of_real)
    4.88  apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
    4.89  done
    4.90  
    4.91 -(*--------------------------------------------------------------------
    4.92 -        Set of finite elements is a subring of the extended reals
    4.93 - --------------------------------------------------------------------*)
    4.94 +
    4.95 +subsection{* Set of Finite Elements is a Subring of the Extended Reals*}
    4.96 +
    4.97  lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
    4.98  apply (simp add: HFinite_def)
    4.99  apply (blast intro!: SReal_add hrabs_add_less)
   4.100 @@ -243,7 +247,7 @@
   4.101  lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
   4.102  by (simp add: HFinite_def)
   4.103  
   4.104 -lemma SReal_subset_HFinite: "Reals <= HFinite"
   4.105 +lemma SReal_subset_HFinite: "Reals \<subseteq> HFinite"
   4.106  apply (auto simp add: SReal_def HFinite_def)
   4.107  apply (rule_tac x = "1 + abs (hypreal_of_real r) " in exI)
   4.108  apply (auto simp add: hypreal_of_real_hrabs)
   4.109 @@ -278,21 +282,20 @@
   4.110  done
   4.111  declare HFinite_1 [simp]
   4.112  
   4.113 -lemma HFinite_bounded: "[|x \<in> HFinite; y <= x; 0 <= y |] ==> y \<in> HFinite"
   4.114 -apply (case_tac "x <= 0")
   4.115 +lemma HFinite_bounded: "[|x \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
   4.116 +apply (case_tac "x \<le> 0")
   4.117  apply (drule_tac y = x in order_trans)
   4.118  apply (drule_tac [2] hypreal_le_anti_sym)
   4.119  apply (auto simp add: linorder_not_le)
   4.120  apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
   4.121  done
   4.122  
   4.123 -(*------------------------------------------------------------------
   4.124 -       Set of infinitesimals is a subring of the hyperreals
   4.125 - ------------------------------------------------------------------*)
   4.126 +
   4.127 +subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}
   4.128 +
   4.129  lemma InfinitesimalD:
   4.130        "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
   4.131 -apply (simp add: Infinitesimal_def)
   4.132 -done
   4.133 +by (simp add: Infinitesimal_def)
   4.134  
   4.135  lemma Infinitesimal_zero: "0 \<in> Infinitesimal"
   4.136  by (simp add: Infinitesimal_def)
   4.137 @@ -316,7 +319,8 @@
   4.138  by (simp add: Infinitesimal_def)
   4.139  declare Infinitesimal_minus_iff [simp]
   4.140  
   4.141 -lemma Infinitesimal_diff: "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
   4.142 +lemma Infinitesimal_diff:
   4.143 +     "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
   4.144  by (simp add: hypreal_diff_def Infinitesimal_add)
   4.145  
   4.146  lemma Infinitesimal_mult:
   4.147 @@ -326,7 +330,8 @@
   4.148  apply (cut_tac [2] a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto)
   4.149  done
   4.150  
   4.151 -lemma Infinitesimal_HFinite_mult: "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
   4.152 +lemma Infinitesimal_HFinite_mult:
   4.153 +     "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
   4.154  apply (auto dest!: HFiniteD simp add: Infinitesimal_def)
   4.155  apply (frule hrabs_less_gt_zero)
   4.156  apply (drule_tac x = "r/t" in bspec)
   4.157 @@ -337,7 +342,8 @@
   4.158  apply (auto simp add: zero_less_divide_iff)
   4.159  done
   4.160  
   4.161 -lemma Infinitesimal_HFinite_mult2: "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
   4.162 +lemma Infinitesimal_HFinite_mult2:
   4.163 +     "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
   4.164  by (auto dest: Infinitesimal_HFinite_mult simp add: hypreal_mult_commute)
   4.165  
   4.166  (*** rather long proof ***)
   4.167 @@ -351,8 +357,6 @@
   4.168  apply (auto simp add: SReal_inverse)
   4.169  done
   4.170  
   4.171 -
   4.172 -
   4.173  lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
   4.174  apply (simp add: HInfinite_def, auto)
   4.175  apply (erule_tac x = 1 in ballE)
   4.176 @@ -363,32 +367,36 @@
   4.177  done
   4.178  
   4.179  lemma HInfinite_add_ge_zero:
   4.180 -      "[|x \<in> HInfinite; 0 <= y; 0 <= x|] ==> (x + y): HInfinite"
   4.181 +      "[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
   4.182  by (auto intro!: hypreal_add_zero_less_le_mono 
   4.183         simp add: abs_if hypreal_add_commute hypreal_le_add_order HInfinite_def)
   4.184  
   4.185 -lemma HInfinite_add_ge_zero2: "[|x \<in> HInfinite; 0 <= y; 0 <= x|] ==> (y + x): HInfinite"
   4.186 +lemma HInfinite_add_ge_zero2:
   4.187 +     "[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite"
   4.188  by (auto intro!: HInfinite_add_ge_zero simp add: hypreal_add_commute)
   4.189  
   4.190 -lemma HInfinite_add_gt_zero: "[|x \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
   4.191 +lemma HInfinite_add_gt_zero:
   4.192 +     "[|x \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
   4.193  by (blast intro: HInfinite_add_ge_zero order_less_imp_le)
   4.194  
   4.195  lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)"
   4.196  by (simp add: HInfinite_def)
   4.197  
   4.198 -lemma HInfinite_add_le_zero: "[|x \<in> HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite"
   4.199 +lemma HInfinite_add_le_zero:
   4.200 +     "[|x \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
   4.201  apply (drule HInfinite_minus_iff [THEN iffD2])
   4.202  apply (rule HInfinite_minus_iff [THEN iffD1])
   4.203  apply (auto intro: HInfinite_add_ge_zero)
   4.204  done
   4.205  
   4.206 -lemma HInfinite_add_lt_zero: "[|x \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
   4.207 +lemma HInfinite_add_lt_zero:
   4.208 +     "[|x \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
   4.209  by (blast intro: HInfinite_add_le_zero order_less_imp_le)
   4.210  
   4.211 -lemma HFinite_sum_squares: "[|a: HFinite; b: HFinite; c: HFinite|]
   4.212 +lemma HFinite_sum_squares:
   4.213 +     "[|a: HFinite; b: HFinite; c: HFinite|]
   4.214        ==> a*a + b*b + c*c \<in> HFinite"
   4.215 -apply (auto intro: HFinite_mult HFinite_add)
   4.216 -done
   4.217 +by (auto intro: HFinite_mult HFinite_add)
   4.218  
   4.219  lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0"
   4.220  by auto
   4.221 @@ -400,27 +408,27 @@
   4.222  by (auto simp add: hrabs_def)
   4.223  declare Infinitesimal_hrabs_iff [iff]
   4.224  
   4.225 -lemma HFinite_diff_Infinitesimal_hrabs: "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
   4.226 +lemma HFinite_diff_Infinitesimal_hrabs:
   4.227 +     "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
   4.228  by blast
   4.229  
   4.230  lemma hrabs_less_Infinitesimal:
   4.231        "[| e \<in> Infinitesimal; abs x < e |] ==> x \<in> Infinitesimal"
   4.232 -apply (auto simp add: Infinitesimal_def abs_less_iff)
   4.233 -done
   4.234 +by (auto simp add: Infinitesimal_def abs_less_iff)
   4.235  
   4.236 -lemma hrabs_le_Infinitesimal: "[| e \<in> Infinitesimal; abs x <= e |] ==> x \<in> Infinitesimal"
   4.237 +lemma hrabs_le_Infinitesimal:
   4.238 +     "[| e \<in> Infinitesimal; abs x \<le> e |] ==> x \<in> Infinitesimal"
   4.239  by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal)
   4.240  
   4.241  lemma Infinitesimal_interval:
   4.242        "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |] 
   4.243         ==> x \<in> Infinitesimal"
   4.244 -apply (auto simp add: Infinitesimal_def abs_less_iff)
   4.245 -done
   4.246 +by (auto simp add: Infinitesimal_def abs_less_iff)
   4.247  
   4.248 -lemma Infinitesimal_interval2: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.249 -         e' <= x ; x <= e |] ==> x \<in> Infinitesimal"
   4.250 -apply (auto intro: Infinitesimal_interval simp add: order_le_less)
   4.251 -done
   4.252 +lemma Infinitesimal_interval2:
   4.253 +     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.254 +         e' \<le> x ; x \<le> e |] ==> x \<in> Infinitesimal"
   4.255 +by (auto intro: Infinitesimal_interval simp add: order_le_less)
   4.256  
   4.257  lemma not_Infinitesimal_mult:
   4.258       "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
   4.259 @@ -432,7 +440,8 @@
   4.260  apply (cut_tac c = ra and d = "abs y" and a = r and b = "abs x" in mult_mono, auto)
   4.261  done
   4.262  
   4.263 -lemma Infinitesimal_mult_disj: "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
   4.264 +lemma Infinitesimal_mult_disj:
   4.265 +     "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
   4.266  apply (rule ccontr)
   4.267  apply (drule de_Morgan_disj [THEN iffD1])
   4.268  apply (fast dest: not_Infinitesimal_mult)
   4.269 @@ -441,7 +450,8 @@
   4.270  lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0"
   4.271  by blast
   4.272  
   4.273 -lemma HFinite_Infinitesimal_diff_mult: "[| x \<in> HFinite - Infinitesimal;
   4.274 +lemma HFinite_Infinitesimal_diff_mult:
   4.275 +     "[| x \<in> HFinite - Infinitesimal;
   4.276                     y \<in> HFinite - Infinitesimal
   4.277                  |] ==> (x*y) \<in> HFinite - Infinitesimal"
   4.278  apply clarify
   4.279 @@ -449,20 +459,21 @@
   4.280  done
   4.281  
   4.282  lemma Infinitesimal_subset_HFinite:
   4.283 -      "Infinitesimal <= HFinite"
   4.284 +      "Infinitesimal \<subseteq> HFinite"
   4.285  apply (simp add: Infinitesimal_def HFinite_def, auto)
   4.286  apply (rule_tac x = 1 in bexI, auto)
   4.287  done
   4.288  
   4.289 -lemma Infinitesimal_hypreal_of_real_mult: "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
   4.290 +lemma Infinitesimal_hypreal_of_real_mult:
   4.291 +     "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
   4.292  by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult])
   4.293  
   4.294 -lemma Infinitesimal_hypreal_of_real_mult2: "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
   4.295 +lemma Infinitesimal_hypreal_of_real_mult2:
   4.296 +     "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
   4.297  by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2])
   4.298  
   4.299 -(*----------------------------------------------------------------------
   4.300 -                   Infinitely close relation @=
   4.301 - ----------------------------------------------------------------------*)
   4.302 +
   4.303 +subsection{*The Infinitely Close Relation*}
   4.304  
   4.305  lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
   4.306  by (simp add: Infinitesimal_def approx_def)
   4.307 @@ -631,7 +642,8 @@
   4.308  apply (auto dest: approx_sym elim!: approx_trans equalityCE)
   4.309  done
   4.310  
   4.311 -lemma Infinitesimal_approx: "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
   4.312 +lemma Infinitesimal_approx:
   4.313 +     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
   4.314  apply (simp add: mem_infmal_iff)
   4.315  apply (blast intro: approx_trans approx_sym)
   4.316  done
   4.317 @@ -676,7 +688,8 @@
   4.318  lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
   4.319  by (blast intro: approx_mult1 approx_trans)
   4.320  
   4.321 -lemma approx_mult_subst_SReal: "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
   4.322 +lemma approx_mult_subst_SReal:
   4.323 +     "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
   4.324  by (auto intro: approx_mult_subst2)
   4.325  
   4.326  lemma approx_eq_imp: "a = b ==> a @= b"
   4.327 @@ -715,7 +728,8 @@
   4.328  apply (erule approx_trans3 [THEN approx_sym], assumption)
   4.329  done
   4.330  
   4.331 -lemma Infinitesimal_add_right_cancel: "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
   4.332 +lemma Infinitesimal_add_right_cancel:
   4.333 +     "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
   4.334  apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
   4.335  apply (erule approx_trans3 [THEN approx_sym])
   4.336  apply (simp add: hypreal_add_commute)
   4.337 @@ -762,19 +776,22 @@
   4.338  lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
   4.339  by (rule approx_sym [THEN [2] approx_HFinite], auto)
   4.340  
   4.341 -lemma approx_mult_HFinite: "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
   4.342 +lemma approx_mult_HFinite:
   4.343 +     "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
   4.344  apply (rule approx_trans)
   4.345  apply (rule_tac [2] approx_mult2)
   4.346  apply (rule approx_mult1)
   4.347  prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   4.348  done
   4.349  
   4.350 -lemma approx_mult_hypreal_of_real: "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
   4.351 +lemma approx_mult_hypreal_of_real:
   4.352 +     "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
   4.353        ==> a*c @= hypreal_of_real b*hypreal_of_real d"
   4.354  apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real)
   4.355  done
   4.356  
   4.357 -lemma approx_SReal_mult_cancel_zero: "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   4.358 +lemma approx_SReal_mult_cancel_zero:
   4.359 +     "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   4.360  apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   4.361  apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
   4.362  done
   4.363 @@ -786,20 +803,23 @@
   4.364  lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
   4.365  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   4.366  
   4.367 -lemma approx_mult_SReal_zero_cancel_iff: "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   4.368 +lemma approx_mult_SReal_zero_cancel_iff:
   4.369 +     "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   4.370  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   4.371  declare approx_mult_SReal_zero_cancel_iff [simp]
   4.372  
   4.373 -lemma approx_SReal_mult_cancel: "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   4.374 +lemma approx_SReal_mult_cancel:
   4.375 +     "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   4.376  apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   4.377  apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
   4.378  done
   4.379  
   4.380 -lemma approx_SReal_mult_cancel_iff1: "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   4.381 +lemma approx_SReal_mult_cancel_iff1:
   4.382 +     "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   4.383  by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel)
   4.384  declare approx_SReal_mult_cancel_iff1 [simp]
   4.385  
   4.386 -lemma approx_le_bound: "[| z <= f; f @= g; g <= z |] ==> f @= z"
   4.387 +lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
   4.388  apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   4.389  apply (rule_tac x = "g+y-z" in bexI)
   4.390  apply (simp (no_asm))
   4.391 @@ -807,9 +827,8 @@
   4.392  apply (rule_tac [2] Infinitesimal_zero, auto)
   4.393  done
   4.394  
   4.395 -(*-----------------------------------------------------------------
   4.396 -    Zero is the only infinitesimal that is also a real
   4.397 - -----------------------------------------------------------------*)
   4.398 +
   4.399 +subsection{* Zero is the Only Infinitesimal that is Also a Real*}
   4.400  
   4.401  lemma Infinitesimal_less_SReal:
   4.402       "[| x \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
   4.403 @@ -817,7 +836,8 @@
   4.404  apply (rule abs_ge_self [THEN order_le_less_trans], auto)
   4.405  done
   4.406  
   4.407 -lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
   4.408 +lemma Infinitesimal_less_SReal2:
   4.409 +     "y \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
   4.410  by (blast intro: Infinitesimal_less_SReal)
   4.411  
   4.412  lemma SReal_not_Infinitesimal:
   4.413 @@ -826,7 +846,8 @@
   4.414  apply (auto simp add: hrabs_def)
   4.415  done
   4.416  
   4.417 -lemma SReal_minus_not_Infinitesimal: "[| y < 0;  y \<in> Reals |] ==> y \<notin> Infinitesimal"
   4.418 +lemma SReal_minus_not_Infinitesimal:
   4.419 +     "[| y < 0;  y \<in> Reals |] ==> y \<notin> Infinitesimal"
   4.420  apply (subst Infinitesimal_minus_iff [symmetric])
   4.421  apply (rule SReal_not_Infinitesimal, auto)
   4.422  done
   4.423 @@ -840,20 +861,24 @@
   4.424  lemma SReal_Infinitesimal_zero: "[| x \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
   4.425  by (cut_tac SReal_Int_Infinitesimal_zero, blast)
   4.426  
   4.427 -lemma SReal_HFinite_diff_Infinitesimal: "[| x \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   4.428 +lemma SReal_HFinite_diff_Infinitesimal:
   4.429 +     "[| x \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   4.430  by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
   4.431  
   4.432 -lemma hypreal_of_real_HFinite_diff_Infinitesimal: "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
   4.433 +lemma hypreal_of_real_HFinite_diff_Infinitesimal:
   4.434 +     "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
   4.435  by (rule SReal_HFinite_diff_Infinitesimal, auto)
   4.436  
   4.437 -lemma hypreal_of_real_Infinitesimal_iff_0: "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
   4.438 +lemma hypreal_of_real_Infinitesimal_iff_0:
   4.439 +     "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
   4.440  apply auto
   4.441  apply (rule ccontr)
   4.442  apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto)
   4.443  done
   4.444  declare hypreal_of_real_Infinitesimal_iff_0 [iff]
   4.445  
   4.446 -lemma number_of_not_Infinitesimal: "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
   4.447 +lemma number_of_not_Infinitesimal:
   4.448 +     "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
   4.449  by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
   4.450  declare number_of_not_Infinitesimal [simp]
   4.451  
   4.452 @@ -870,7 +895,8 @@
   4.453  apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   4.454  done
   4.455  
   4.456 -lemma HFinite_diff_Infinitesimal_approx: "[| x @= y; y \<in> HFinite - Infinitesimal |]
   4.457 +lemma HFinite_diff_Infinitesimal_approx:
   4.458 +     "[| x @= y; y \<in> HFinite - Infinitesimal |]
   4.459        ==> x \<in> HFinite - Infinitesimal"
   4.460  apply (auto intro: approx_sym [THEN [2] approx_HFinite]
   4.461              simp add: mem_infmal_iff)
   4.462 @@ -880,18 +906,25 @@
   4.463  
   4.464  (*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the
   4.465    HFinite premise.*)
   4.466 -lemma Infinitesimal_ratio: "[| y \<noteq> 0;  y \<in> Infinitesimal;  x/y \<in> HFinite |] ==> x \<in> Infinitesimal"
   4.467 +lemma Infinitesimal_ratio:
   4.468 +     "[| y \<noteq> 0;  y \<in> Infinitesimal;  x/y \<in> HFinite |] ==> x \<in> Infinitesimal"
   4.469  apply (drule Infinitesimal_HFinite_mult2, assumption)
   4.470  apply (simp add: hypreal_divide_def hypreal_mult_assoc)
   4.471  done
   4.472  
   4.473 +lemma Infinitesimal_SReal_divide: 
   4.474 +  "[| x \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
   4.475 +apply (simp add: divide_inverse_zero)
   4.476 +apply (auto intro!: Infinitesimal_HFinite_mult 
   4.477 +            dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   4.478 +done
   4.479 +
   4.480  (*------------------------------------------------------------------
   4.481         Standard Part Theorem: Every finite x: R* is infinitely
   4.482         close to a unique real number (i.e a member of Reals)
   4.483   ------------------------------------------------------------------*)
   4.484 -(*------------------------------------------------------------------
   4.485 -         Uniqueness: Two infinitely close reals are equal
   4.486 - ------------------------------------------------------------------*)
   4.487 +
   4.488 +subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
   4.489  
   4.490  lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
   4.491  apply auto
   4.492 @@ -903,7 +936,8 @@
   4.493  apply (simp add: hypreal_eq_minus_iff [symmetric])
   4.494  done
   4.495  
   4.496 -lemma number_of_approx_iff: "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
   4.497 +lemma number_of_approx_iff:
   4.498 +     "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
   4.499  by (auto simp add: SReal_approx_iff)
   4.500  declare number_of_approx_iff [simp]
   4.501  
   4.502 @@ -915,14 +949,16 @@
   4.503                "~ (0 @= 1)" "~ (1 @= 0)"
   4.504  by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
   4.505  
   4.506 -lemma hypreal_of_real_approx_iff: "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
   4.507 +lemma hypreal_of_real_approx_iff:
   4.508 +     "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
   4.509  apply auto
   4.510  apply (rule inj_hypreal_of_real [THEN injD])
   4.511  apply (rule SReal_approx_iff [THEN iffD1], auto)
   4.512  done
   4.513  declare hypreal_of_real_approx_iff [simp]
   4.514  
   4.515 -lemma hypreal_of_real_approx_number_of_iff: "(hypreal_of_real k @= number_of w) = (k = number_of w)"
   4.516 +lemma hypreal_of_real_approx_number_of_iff:
   4.517 +     "(hypreal_of_real k @= number_of w) = (k = number_of w)"
   4.518  by (subst hypreal_of_real_approx_iff [symmetric], auto)
   4.519  declare hypreal_of_real_approx_number_of_iff [simp]
   4.520  
   4.521 @@ -932,12 +968,13 @@
   4.522                "(hypreal_of_real k @= 1) = (k = 1)"
   4.523    by (simp_all add:  hypreal_of_real_approx_iff [symmetric])
   4.524  
   4.525 -lemma approx_unique_real: "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
   4.526 +lemma approx_unique_real:
   4.527 +     "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
   4.528  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
   4.529  
   4.530 -(*------------------------------------------------------------------
   4.531 -       Existence of unique real infinitely close
   4.532 - ------------------------------------------------------------------*)
   4.533 +
   4.534 +subsection{* Existence of Unique Real Infinitely Close*}
   4.535 +
   4.536  (* lemma about lubs *)
   4.537  lemma hypreal_isLub_unique:
   4.538       "[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)"
   4.539 @@ -946,7 +983,8 @@
   4.540  apply (blast intro!: hypreal_le_anti_sym dest!: isLub_le_isUb)
   4.541  done
   4.542  
   4.543 -lemma lemma_st_part_ub: "x \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
   4.544 +lemma lemma_st_part_ub:
   4.545 +     "x \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
   4.546  apply (drule HFiniteD, safe)
   4.547  apply (rule exI, rule isUbI)
   4.548  apply (auto intro: setleI isUbI simp add: abs_less_iff)
   4.549 @@ -959,28 +997,31 @@
   4.550  apply (auto simp add: abs_less_iff)
   4.551  done
   4.552  
   4.553 -lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} <= Reals"
   4.554 +lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals"
   4.555  by auto
   4.556  
   4.557 -lemma lemma_st_part_lub: "x \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
   4.558 +lemma lemma_st_part_lub:
   4.559 +     "x \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
   4.560  by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)
   4.561  
   4.562 -lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r <= t) = (r <= 0)"
   4.563 +lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)"
   4.564  apply safe
   4.565  apply (drule_tac c = "-t" in add_left_mono)
   4.566  apply (drule_tac [2] c = t in add_left_mono)
   4.567  apply (auto simp add: hypreal_add_assoc [symmetric])
   4.568  done
   4.569  
   4.570 -lemma lemma_st_part_le1: "[| x \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
   4.571 -         r \<in> Reals;  0 < r |] ==> x <= t + r"
   4.572 +lemma lemma_st_part_le1:
   4.573 +     "[| x \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
   4.574 +         r \<in> Reals;  0 < r |] ==> x \<le> t + r"
   4.575  apply (frule isLubD1a)
   4.576  apply (rule ccontr, drule linorder_not_le [THEN iffD2])
   4.577  apply (drule_tac x = t in SReal_add, assumption)
   4.578  apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto)
   4.579  done
   4.580  
   4.581 -lemma hypreal_setle_less_trans: "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y"
   4.582 +lemma hypreal_setle_less_trans:
   4.583 +     "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y"
   4.584  apply (simp add: setle_def)
   4.585  apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
   4.586  done
   4.587 @@ -991,20 +1032,21 @@
   4.588  apply (blast intro: hypreal_setle_less_trans)
   4.589  done
   4.590  
   4.591 -lemma lemma_st_part_gt_ub: "[| x \<in> HFinite; x < y; y \<in> Reals |]
   4.592 -               ==> isUb Reals {s. s \<in> Reals & s < x} y"
   4.593 -apply (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
   4.594 -done
   4.595 +lemma lemma_st_part_gt_ub:
   4.596 +     "[| x \<in> HFinite; x < y; y \<in> Reals |]
   4.597 +      ==> isUb Reals {s. s \<in> Reals & s < x} y"
   4.598 +by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
   4.599  
   4.600 -lemma lemma_minus_le_zero: "t <= t + -r ==> r <= (0::hypreal)"
   4.601 +lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
   4.602  apply (drule_tac c = "-t" in add_left_mono)
   4.603  apply (auto simp add: hypreal_add_assoc [symmetric])
   4.604  done
   4.605  
   4.606 -lemma lemma_st_part_le2: "[| x \<in> HFinite;
   4.607 +lemma lemma_st_part_le2:
   4.608 +     "[| x \<in> HFinite;
   4.609           isLub Reals {s. s \<in> Reals & s < x} t;
   4.610           r \<in> Reals; 0 < r |]
   4.611 -      ==> t + -r <= x"
   4.612 +      ==> t + -r \<le> x"
   4.613  apply (frule isLubD1a)
   4.614  apply (rule ccontr, drule linorder_not_le [THEN iffD1])
   4.615  apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption)
   4.616 @@ -1014,30 +1056,33 @@
   4.617  apply (auto dest: order_less_le_trans)
   4.618  done
   4.619  
   4.620 -lemma lemma_hypreal_le_swap: "((x::hypreal) <= t + r) = (x + -t <= r)"
   4.621 +lemma lemma_hypreal_le_swap: "((x::hypreal) \<le> t + r) = (x + -t \<le> r)"
   4.622  by auto
   4.623  
   4.624 -lemma lemma_st_part1a: "[| x \<in> HFinite;
   4.625 +lemma lemma_st_part1a:
   4.626 +     "[| x \<in> HFinite;
   4.627           isLub Reals {s. s \<in> Reals & s < x} t;
   4.628           r \<in> Reals; 0 < r |]
   4.629 -      ==> x + -t <= r"
   4.630 -apply (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
   4.631 -done
   4.632 +      ==> x + -t \<le> r"
   4.633 +by (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
   4.634  
   4.635 -lemma lemma_hypreal_le_swap2: "(t + -r <= x) = (-(x + -t) <= (r::hypreal))"
   4.636 +lemma lemma_hypreal_le_swap2: "(t + -r \<le> x) = (-(x + -t) \<le> (r::hypreal))"
   4.637  by auto
   4.638  
   4.639 -lemma lemma_st_part2a: "[| x \<in> HFinite;
   4.640 +lemma lemma_st_part2a:
   4.641 +     "[| x \<in> HFinite;
   4.642           isLub Reals {s. s \<in> Reals & s < x} t;
   4.643           r \<in> Reals;  0 < r |]
   4.644 -      ==> -(x + -t) <= r"
   4.645 +      ==> -(x + -t) \<le> r"
   4.646  apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2)
   4.647  done
   4.648  
   4.649 -lemma lemma_SReal_ub: "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
   4.650 +lemma lemma_SReal_ub:
   4.651 +     "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
   4.652  by (auto intro: isUbI setleI order_less_imp_le)
   4.653  
   4.654 -lemma lemma_SReal_lub: "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
   4.655 +lemma lemma_SReal_lub:
   4.656 +     "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
   4.657  apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
   4.658  apply (frule isUbD2a)
   4.659  apply (rule_tac x = x and y = y in linorder_cases)
   4.660 @@ -1047,7 +1092,8 @@
   4.661  apply (auto dest: order_less_le_trans)
   4.662  done
   4.663  
   4.664 -lemma lemma_st_part_not_eq1: "[| x \<in> HFinite;
   4.665 +lemma lemma_st_part_not_eq1:
   4.666 +     "[| x \<in> HFinite;
   4.667           isLub Reals {s. s \<in> Reals & s < x} t;
   4.668           r \<in> Reals; 0 < r |]
   4.669        ==> x + -t \<noteq> r"
   4.670 @@ -1058,7 +1104,8 @@
   4.671  apply (drule hypreal_isLub_unique, assumption, auto)
   4.672  done
   4.673  
   4.674 -lemma lemma_st_part_not_eq2: "[| x \<in> HFinite;
   4.675 +lemma lemma_st_part_not_eq2:
   4.676 +     "[| x \<in> HFinite;
   4.677           isLub Reals {s. s \<in> Reals & s < x} t;
   4.678           r \<in> Reals; 0 < r |]
   4.679        ==> -(x + -t) \<noteq> r"
   4.680 @@ -1070,7 +1117,8 @@
   4.681  apply (drule hypreal_isLub_unique, assumption, auto)
   4.682  done
   4.683  
   4.684 -lemma lemma_st_part_major: "[| x \<in> HFinite;
   4.685 +lemma lemma_st_part_major:
   4.686 +     "[| x \<in> HFinite;
   4.687           isLub Reals {s. s \<in> Reals & s < x} t;
   4.688           r \<in> Reals; 0 < r |]
   4.689        ==> abs (x + -t) < r"
   4.690 @@ -1080,17 +1128,16 @@
   4.691  apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
   4.692  done
   4.693  
   4.694 -lemma lemma_st_part_major2: "[| x \<in> HFinite;
   4.695 -         isLub Reals {s. s \<in> Reals & s < x} t |]
   4.696 +lemma lemma_st_part_major2:
   4.697 +     "[| x \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
   4.698        ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
   4.699 -apply (blast dest!: lemma_st_part_major)
   4.700 -done
   4.701 +by (blast dest!: lemma_st_part_major)
   4.702  
   4.703  (*----------------------------------------------
   4.704    Existence of real and Standard Part Theorem
   4.705   ----------------------------------------------*)
   4.706 -lemma lemma_st_part_Ex: "x \<in> HFinite ==>
   4.707 -      \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
   4.708 +lemma lemma_st_part_Ex:
   4.709 +     "x \<in> HFinite ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
   4.710  apply (frule lemma_st_part_lub, safe)
   4.711  apply (frule isLubD1a)
   4.712  apply (blast dest: lemma_st_part_major2)
   4.713 @@ -1111,9 +1158,7 @@
   4.714  apply (auto intro!: approx_unique_real)
   4.715  done
   4.716  
   4.717 -(*------------------------------------------------------------------
   4.718 -       Finite and Infinite --- more theorems
   4.719 - ------------------------------------------------------------------*)
   4.720 +subsection{* Finite, Infinite and Infinitesimal*}
   4.721  
   4.722  lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}"
   4.723  
   4.724 @@ -1143,17 +1188,15 @@
   4.725  by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)
   4.726  
   4.727  lemma HFinite_HInfinite_iff: "(x \<in> HFinite) = (x \<notin> HInfinite)"
   4.728 -apply (simp (no_asm) add: HInfinite_HFinite_iff)
   4.729 -done
   4.730 +by (simp add: HInfinite_HFinite_iff)
   4.731 +
   4.732  
   4.733 -(*------------------------------------------------------------------
   4.734 -       Finite, Infinite and Infinitesimal --- more theorems
   4.735 - ------------------------------------------------------------------*)
   4.736 -
   4.737 -lemma HInfinite_diff_HFinite_Infinitesimal_disj: "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
   4.738 +lemma HInfinite_diff_HFinite_Infinitesimal_disj:
   4.739 +     "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
   4.740  by (fast intro: not_HFinite_HInfinite)
   4.741  
   4.742 -lemma HFinite_inverse: "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
   4.743 +lemma HFinite_inverse:
   4.744 +     "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
   4.745  apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
   4.746  apply (auto dest!: HInfinite_inverse_Infinitesimal)
   4.747  done
   4.748 @@ -1162,18 +1205,21 @@
   4.749  by (blast intro: HFinite_inverse)
   4.750  
   4.751  (* stronger statement possible in fact *)
   4.752 -lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
   4.753 +lemma Infinitesimal_inverse_HFinite:
   4.754 +     "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
   4.755  apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
   4.756  apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
   4.757  done
   4.758  
   4.759 -lemma HFinite_not_Infinitesimal_inverse: "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
   4.760 +lemma HFinite_not_Infinitesimal_inverse:
   4.761 +     "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
   4.762  apply (auto intro: Infinitesimal_inverse_HFinite)
   4.763  apply (drule Infinitesimal_HFinite_mult2, assumption)
   4.764  apply (simp add: not_Infinitesimal_not_zero hypreal_mult_inverse)
   4.765  done
   4.766  
   4.767 -lemma approx_inverse: "[| x @= y; y \<in>  HFinite - Infinitesimal |]
   4.768 +lemma approx_inverse:
   4.769 +     "[| x @= y; y \<in>  HFinite - Infinitesimal |]
   4.770        ==> inverse x @= inverse y"
   4.771  apply (frule HFinite_diff_Infinitesimal_approx, assumption)
   4.772  apply (frule not_Infinitesimal_not_zero2)
   4.773 @@ -1187,18 +1233,21 @@
   4.774  (*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
   4.775  lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   4.776  
   4.777 -lemma inverse_add_Infinitesimal_approx: "[| x \<in> HFinite - Infinitesimal;
   4.778 +lemma inverse_add_Infinitesimal_approx:
   4.779 +     "[| x \<in> HFinite - Infinitesimal;
   4.780           h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
   4.781  apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
   4.782  done
   4.783  
   4.784 -lemma inverse_add_Infinitesimal_approx2: "[| x \<in> HFinite - Infinitesimal;
   4.785 +lemma inverse_add_Infinitesimal_approx2:
   4.786 +     "[| x \<in> HFinite - Infinitesimal;
   4.787           h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
   4.788  apply (rule hypreal_add_commute [THEN subst])
   4.789  apply (blast intro: inverse_add_Infinitesimal_approx)
   4.790  done
   4.791  
   4.792 -lemma inverse_add_Infinitesimal_approx_Infinitesimal: "[| x \<in> HFinite - Infinitesimal;
   4.793 +lemma inverse_add_Infinitesimal_approx_Infinitesimal:
   4.794 +     "[| x \<in> HFinite - Infinitesimal;
   4.795           h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
   4.796  apply (rule approx_trans2)
   4.797  apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric])
   4.798 @@ -1222,36 +1271,43 @@
   4.799  by (auto simp add: HInfinite_HFinite_iff)
   4.800  declare HInfinite_square_iff [simp]
   4.801  
   4.802 -lemma approx_HFinite_mult_cancel: "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   4.803 +lemma approx_HFinite_mult_cancel:
   4.804 +     "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   4.805  apply safe
   4.806  apply (frule HFinite_inverse, assumption)
   4.807  apply (drule not_Infinitesimal_not_zero)
   4.808  apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
   4.809  done
   4.810  
   4.811 -lemma approx_HFinite_mult_cancel_iff1: "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
   4.812 +lemma approx_HFinite_mult_cancel_iff1:
   4.813 +     "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
   4.814  by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
   4.815  
   4.816 -lemma HInfinite_HFinite_add_cancel: "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
   4.817 +lemma HInfinite_HFinite_add_cancel:
   4.818 +     "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
   4.819  apply (rule ccontr)
   4.820  apply (drule HFinite_HInfinite_iff [THEN iffD2])
   4.821  apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)
   4.822  done
   4.823  
   4.824 -lemma HInfinite_HFinite_add: "[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite"
   4.825 +lemma HInfinite_HFinite_add:
   4.826 +     "[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite"
   4.827  apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)
   4.828  apply (auto simp add: hypreal_add_assoc HFinite_minus_iff)
   4.829  done
   4.830  
   4.831 -lemma HInfinite_ge_HInfinite: "[| x \<in> HInfinite; x <= y; 0 <= x |] ==> y \<in> HInfinite"
   4.832 +lemma HInfinite_ge_HInfinite:
   4.833 +     "[| x \<in> HInfinite; x \<le> y; 0 \<le> x |] ==> y \<in> HInfinite"
   4.834  by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)
   4.835  
   4.836 -lemma Infinitesimal_inverse_HInfinite: "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
   4.837 +lemma Infinitesimal_inverse_HInfinite:
   4.838 +     "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
   4.839  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   4.840  apply (auto dest: Infinitesimal_HFinite_mult2)
   4.841  done
   4.842  
   4.843 -lemma HInfinite_HFinite_not_Infinitesimal_mult: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
   4.844 +lemma HInfinite_HFinite_not_Infinitesimal_mult:
   4.845 +     "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
   4.846        ==> x * y \<in> HInfinite"
   4.847  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   4.848  apply (frule HFinite_Infinitesimal_not_zero)
   4.849 @@ -1260,10 +1316,10 @@
   4.850  apply (auto simp add: hypreal_mult_assoc HFinite_HInfinite_iff)
   4.851  done
   4.852  
   4.853 -lemma HInfinite_HFinite_not_Infinitesimal_mult2: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
   4.854 +lemma HInfinite_HFinite_not_Infinitesimal_mult2:
   4.855 +     "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
   4.856        ==> y * x \<in> HInfinite"
   4.857 -apply (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
   4.858 -done
   4.859 +by (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
   4.860  
   4.861  lemma HInfinite_gt_SReal: "[| x \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
   4.862  by (auto dest!: bspec simp add: HInfinite_def hrabs_def order_less_imp_le)
   4.863 @@ -1277,18 +1333,13 @@
   4.864  done
   4.865  declare not_HInfinite_one [simp]
   4.866  
   4.867 -(*------------------------------------------------------------------
   4.868 -                  more about absolute value (hrabs)
   4.869 - ------------------------------------------------------------------*)
   4.870 -
   4.871  lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
   4.872  by (cut_tac x = x in hrabs_disj, auto)
   4.873  
   4.874 -(*------------------------------------------------------------------
   4.875 -                  Theorems about monads
   4.876 - ------------------------------------------------------------------*)
   4.877  
   4.878 -lemma monad_hrabs_Un_subset: "monad (abs x) <= monad(x) Un monad(-x)"
   4.879 +subsection{*Theorems about Monads*}
   4.880 +
   4.881 +lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x) Un monad(-x)"
   4.882  by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
   4.883  
   4.884  lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
   4.885 @@ -1316,12 +1367,12 @@
   4.886  (*------------------------------------------------------------------
   4.887           Proof that x @= y ==> abs x @= abs y
   4.888   ------------------------------------------------------------------*)
   4.889 -lemma approx_subset_monad: "x @= y ==> {x,y}<=monad x"
   4.890 +lemma approx_subset_monad: "x @= y ==> {x,y}\<le>monad x"
   4.891  apply (simp (no_asm))
   4.892  apply (simp add: approx_monad_iff)
   4.893  done
   4.894  
   4.895 -lemma approx_subset_monad2: "x @= y ==> {x,y}<=monad y"
   4.896 +lemma approx_subset_monad2: "x @= y ==> {x,y}\<le>monad y"
   4.897  apply (drule approx_sym)
   4.898  apply (fast dest: approx_subset_monad)
   4.899  done
   4.900 @@ -1342,42 +1393,50 @@
   4.901  apply (fast intro: approx_mem_monad approx_trans)
   4.902  done
   4.903  
   4.904 -lemma Infinitesimal_approx_hrabs: "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
   4.905 +lemma Infinitesimal_approx_hrabs:
   4.906 +     "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
   4.907  apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
   4.908  apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
   4.909  done
   4.910  
   4.911 -lemma less_Infinitesimal_less: "[| 0 < x;  x \<notin>Infinitesimal;  e :Infinitesimal |] ==> e < x"
   4.912 +lemma less_Infinitesimal_less:
   4.913 +     "[| 0 < x;  x \<notin>Infinitesimal;  e :Infinitesimal |] ==> e < x"
   4.914  apply (rule ccontr)
   4.915  apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval] 
   4.916              dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
   4.917  done
   4.918  
   4.919 -lemma Ball_mem_monad_gt_zero: "[| 0 < x;  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
   4.920 +lemma Ball_mem_monad_gt_zero:
   4.921 +     "[| 0 < x;  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
   4.922  apply (drule mem_monad_approx [THEN approx_sym])
   4.923  apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
   4.924  apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
   4.925  done
   4.926  
   4.927 -lemma Ball_mem_monad_less_zero: "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
   4.928 +lemma Ball_mem_monad_less_zero:
   4.929 +     "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
   4.930  apply (drule mem_monad_approx [THEN approx_sym])
   4.931  apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
   4.932  apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
   4.933  done
   4.934  
   4.935 -lemma lemma_approx_gt_zero: "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
   4.936 +lemma lemma_approx_gt_zero:
   4.937 +     "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
   4.938  by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
   4.939  
   4.940 -lemma lemma_approx_less_zero: "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   4.941 +lemma lemma_approx_less_zero:
   4.942 +     "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   4.943  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
   4.944  
   4.945 -lemma approx_hrabs1: "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   4.946 +lemma approx_hrabs1:
   4.947 +     "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   4.948  apply (frule lemma_approx_less_zero)
   4.949  apply (assumption+)
   4.950  apply (simp add: abs_if) 
   4.951  done
   4.952  
   4.953 -lemma approx_hrabs2: "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   4.954 +lemma approx_hrabs2:
   4.955 +     "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   4.956  apply (frule lemma_approx_gt_zero)
   4.957  apply (assumption+)
   4.958  apply (simp add: abs_if) 
   4.959 @@ -1397,17 +1456,20 @@
   4.960  lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
   4.961  by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
   4.962  
   4.963 -lemma approx_hrabs_add_minus_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
   4.964 +lemma approx_hrabs_add_minus_Infinitesimal:
   4.965 +     "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
   4.966  by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
   4.967  
   4.968 -lemma hrabs_add_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.969 +lemma hrabs_add_Infinitesimal_cancel:
   4.970 +     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.971           abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
   4.972  apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
   4.973  apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
   4.974  apply (auto intro: approx_trans2)
   4.975  done
   4.976  
   4.977 -lemma hrabs_add_minus_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.978 +lemma hrabs_add_minus_Infinitesimal_cancel:
   4.979 +     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   4.980           abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
   4.981  apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
   4.982  apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
   4.983 @@ -1424,8 +1486,7 @@
   4.984       "[| x < y;  u \<in> Infinitesimal |]
   4.985        ==> hypreal_of_real x + u < hypreal_of_real y"
   4.986  apply (simp add: Infinitesimal_def)
   4.987 -apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec)
   4.988 - apply (simp add: );  
   4.989 +apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)  
   4.990  apply (auto simp add: add_commute abs_less_iff SReal_add SReal_minus)
   4.991  apply (simp add: compare_rls) 
   4.992  done
   4.993 @@ -1438,39 +1499,45 @@
   4.994  apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: hypreal_of_real_hrabs)
   4.995  done
   4.996  
   4.997 -lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: "[| x \<in> Infinitesimal;  abs(hypreal_of_real r) < hypreal_of_real y |]
   4.998 +lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
   4.999 +     "[| x \<in> Infinitesimal;  abs(hypreal_of_real r) < hypreal_of_real y |]
  4.1000        ==> abs (x + hypreal_of_real r) < hypreal_of_real y"
  4.1001  apply (rule hypreal_add_commute [THEN subst])
  4.1002  apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
  4.1003  done
  4.1004  
  4.1005 -lemma hypreal_of_real_le_add_Infininitesimal_cancel: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  4.1006 -         hypreal_of_real x + u <= hypreal_of_real y + v |]
  4.1007 -      ==> hypreal_of_real x <= hypreal_of_real y"
  4.1008 +lemma hypreal_of_real_le_add_Infininitesimal_cancel:
  4.1009 +     "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  4.1010 +         hypreal_of_real x + u \<le> hypreal_of_real y + v |]
  4.1011 +      ==> hypreal_of_real x \<le> hypreal_of_real y"
  4.1012  apply (simp add: linorder_not_less [symmetric], auto)
  4.1013  apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
  4.1014  apply (auto simp add: Infinitesimal_diff)
  4.1015  done
  4.1016  
  4.1017 -lemma hypreal_of_real_le_add_Infininitesimal_cancel2: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  4.1018 -         hypreal_of_real x + u <= hypreal_of_real y + v |]
  4.1019 -      ==> x <= y"
  4.1020 +lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
  4.1021 +     "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  4.1022 +         hypreal_of_real x + u \<le> hypreal_of_real y + v |]
  4.1023 +      ==> x \<le> y"
  4.1024  apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel)
  4.1025  done
  4.1026  
  4.1027 -lemma hypreal_of_real_less_Infinitesimal_le_zero: "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x <= 0"
  4.1028 +lemma hypreal_of_real_less_Infinitesimal_le_zero:
  4.1029 +     "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
  4.1030  apply (rule linorder_not_less [THEN iffD1], safe)
  4.1031  apply (drule Infinitesimal_interval)
  4.1032  apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
  4.1033  done
  4.1034  
  4.1035  (*used once, in Lim/NSDERIV_inverse*)
  4.1036 -lemma Infinitesimal_add_not_zero: "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
  4.1037 +lemma Infinitesimal_add_not_zero:
  4.1038 +     "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
  4.1039  apply auto
  4.1040  apply (subgoal_tac "h = - hypreal_of_real x", auto)
  4.1041  done
  4.1042  
  4.1043 -lemma Infinitesimal_square_cancel: "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1044 +lemma Infinitesimal_square_cancel:
  4.1045 +     "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1046  apply (rule Infinitesimal_interval2)
  4.1047  apply (rule_tac [3] zero_le_square, assumption)
  4.1048  apply (auto simp add: zero_le_square)
  4.1049 @@ -1483,7 +1550,8 @@
  4.1050  done
  4.1051  declare HFinite_square_cancel [simp]
  4.1052  
  4.1053 -lemma Infinitesimal_square_cancel2: "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
  4.1054 +lemma Infinitesimal_square_cancel2:
  4.1055 +     "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
  4.1056  apply (rule Infinitesimal_square_cancel)
  4.1057  apply (rule hypreal_add_commute [THEN subst])
  4.1058  apply (simp (no_asm))
  4.1059 @@ -1497,7 +1565,8 @@
  4.1060  done
  4.1061  declare HFinite_square_cancel2 [simp]
  4.1062  
  4.1063 -lemma Infinitesimal_sum_square_cancel: "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1064 +lemma Infinitesimal_sum_square_cancel:
  4.1065 +     "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1066  apply (rule Infinitesimal_interval2, assumption)
  4.1067  apply (rule_tac [2] zero_le_square, simp)
  4.1068  apply (insert zero_le_square [of y]) 
  4.1069 @@ -1513,25 +1582,29 @@
  4.1070  done
  4.1071  declare HFinite_sum_square_cancel [simp]
  4.1072  
  4.1073 -lemma Infinitesimal_sum_square_cancel2: "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1074 +lemma Infinitesimal_sum_square_cancel2:
  4.1075 +     "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1076  apply (rule Infinitesimal_sum_square_cancel)
  4.1077  apply (simp add: add_ac)
  4.1078  done
  4.1079  declare Infinitesimal_sum_square_cancel2 [simp]
  4.1080  
  4.1081 -lemma HFinite_sum_square_cancel2: "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
  4.1082 +lemma HFinite_sum_square_cancel2:
  4.1083 +     "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
  4.1084  apply (rule HFinite_sum_square_cancel)
  4.1085  apply (simp add: add_ac)
  4.1086  done
  4.1087  declare HFinite_sum_square_cancel2 [simp]
  4.1088  
  4.1089 -lemma Infinitesimal_sum_square_cancel3: "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1090 +lemma Infinitesimal_sum_square_cancel3:
  4.1091 +     "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  4.1092  apply (rule Infinitesimal_sum_square_cancel)
  4.1093  apply (simp add: add_ac)
  4.1094  done
  4.1095  declare Infinitesimal_sum_square_cancel3 [simp]
  4.1096  
  4.1097 -lemma HFinite_sum_square_cancel3: "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
  4.1098 +lemma HFinite_sum_square_cancel3:
  4.1099 +     "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
  4.1100  apply (rule HFinite_sum_square_cancel)
  4.1101  apply (simp add: add_ac)
  4.1102  done
  4.1103 @@ -1544,16 +1617,16 @@
  4.1104  apply (auto dest!: InfinitesimalD)
  4.1105  done
  4.1106  
  4.1107 -lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real  a) ==> x \<in> HFinite"
  4.1108 +lemma mem_monad_SReal_HFinite:
  4.1109 +     "x \<in> monad (hypreal_of_real  a) ==> x \<in> HFinite"
  4.1110  apply (drule mem_monad_approx [THEN approx_sym])
  4.1111  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
  4.1112  apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
  4.1113  apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
  4.1114  done
  4.1115  
  4.1116 -(*------------------------------------------------------------------
  4.1117 -              Theorems about standard part
  4.1118 - ------------------------------------------------------------------*)
  4.1119 +
  4.1120 +subsection{* Theorems about Standard Part*}
  4.1121  
  4.1122  lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
  4.1123  apply (simp add: st_def)
  4.1124 @@ -1596,11 +1669,13 @@
  4.1125      by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
  4.1126  qed
  4.1127  
  4.1128 -lemma st_eq_approx_iff: "[| x \<in> HFinite; y \<in> HFinite|]
  4.1129 +lemma st_eq_approx_iff:
  4.1130 +     "[| x \<in> HFinite; y \<in> HFinite|]
  4.1131                     ==> (x @= y) = (st x = st y)"
  4.1132  by (blast intro: approx_st_eq st_eq_approx)
  4.1133  
  4.1134 -lemma st_Infinitesimal_add_SReal: "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
  4.1135 +lemma st_Infinitesimal_add_SReal:
  4.1136 +     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
  4.1137  apply (frule st_SReal_eq [THEN subst])
  4.1138  prefer 2 apply assumption
  4.1139  apply (frule SReal_subset_HFinite [THEN subsetD])
  4.1140 @@ -1610,16 +1685,15 @@
  4.1141  apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym])
  4.1142  done
  4.1143  
  4.1144 -lemma st_Infinitesimal_add_SReal2: "[| x \<in> Reals; e \<in> Infinitesimal |]
  4.1145 -      ==> st(e + x) = x"
  4.1146 +lemma st_Infinitesimal_add_SReal2:
  4.1147 +     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x"
  4.1148  apply (rule hypreal_add_commute [THEN subst])
  4.1149  apply (blast intro!: st_Infinitesimal_add_SReal)
  4.1150  done
  4.1151  
  4.1152 -lemma HFinite_st_Infinitesimal_add: "x \<in> HFinite ==>
  4.1153 -      \<exists>e \<in> Infinitesimal. x = st(x) + e"
  4.1154 -apply (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
  4.1155 -done
  4.1156 +lemma HFinite_st_Infinitesimal_add:
  4.1157 +     "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = st(x) + e"
  4.1158 +by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
  4.1159  
  4.1160  lemma st_add: 
  4.1161    assumes x: "x \<in> HFinite" and y: "y \<in> HFinite"
  4.1162 @@ -1655,8 +1729,7 @@
  4.1163    thus ?thesis by arith
  4.1164  qed
  4.1165  
  4.1166 -lemma st_diff:
  4.1167 -     "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x-y) = st(x) - st(y)"
  4.1168 +lemma st_diff: "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x-y) = st(x) - st(y)"
  4.1169  apply (simp add: hypreal_diff_def)
  4.1170  apply (frule_tac y1 = y in st_minus [symmetric])
  4.1171  apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2])
  4.1172 @@ -1664,18 +1737,16 @@
  4.1173  done
  4.1174  
  4.1175  (* lemma *)
  4.1176 -lemma lemma_st_mult: "[| x \<in> HFinite; y \<in> HFinite;
  4.1177 -         e \<in> Infinitesimal;
  4.1178 -         ea \<in> Infinitesimal |]
  4.1179 -       ==> e*y + x*ea + e*ea \<in> Infinitesimal"
  4.1180 +lemma lemma_st_mult:
  4.1181 +     "[| x \<in> HFinite; y \<in> HFinite; e \<in> Infinitesimal; ea \<in> Infinitesimal |]
  4.1182 +      ==> e*y + x*ea + e*ea \<in> Infinitesimal"
  4.1183  apply (frule_tac x = e and y = y in Infinitesimal_HFinite_mult)
  4.1184  apply (frule_tac [2] x = ea and y = x in Infinitesimal_HFinite_mult)
  4.1185  apply (drule_tac [3] Infinitesimal_mult)
  4.1186  apply (auto intro: Infinitesimal_add simp add: add_ac mult_ac)
  4.1187  done
  4.1188  
  4.1189 -lemma st_mult: "[| x \<in> HFinite; y \<in> HFinite |]
  4.1190 -               ==> st (x * y) = st(x) * st(y)"
  4.1191 +lemma st_mult: "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x * y) = st(x) * st(y)"
  4.1192  apply (frule HFinite_st_Infinitesimal_add)
  4.1193  apply (frule_tac x = y in HFinite_st_Infinitesimal_add, safe)
  4.1194  apply (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))")
  4.1195 @@ -1697,20 +1768,23 @@
  4.1196  apply (subst numeral_0_eq_0 [symmetric])
  4.1197  apply (rule st_number_of [THEN subst])
  4.1198  apply (rule approx_st_eq)
  4.1199 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mem_infmal_iff [symmetric])
  4.1200 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
  4.1201 +            simp add: mem_infmal_iff [symmetric])
  4.1202  done
  4.1203  
  4.1204  lemma st_not_Infinitesimal: "st(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
  4.1205  by (fast intro: st_Infinitesimal)
  4.1206  
  4.1207 -lemma st_inverse: "[| x \<in> HFinite; st x \<noteq> 0 |]
  4.1208 +lemma st_inverse:
  4.1209 +     "[| x \<in> HFinite; st x \<noteq> 0 |]
  4.1210        ==> st(inverse x) = inverse (st x)"
  4.1211  apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1])
  4.1212  apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
  4.1213  apply (subst hypreal_mult_inverse, auto)
  4.1214  done
  4.1215  
  4.1216 -lemma st_divide: "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
  4.1217 +lemma st_divide:
  4.1218 +     "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
  4.1219        ==> st(x/y) = (st x) / (st y)"
  4.1220  apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
  4.1221  done
  4.1222 @@ -1720,22 +1794,22 @@
  4.1223  by (blast intro: st_HFinite st_approx_self approx_st_eq)
  4.1224  declare st_idempotent [simp]
  4.1225  
  4.1226 -(*** lemmas ***)
  4.1227 -lemma Infinitesimal_add_st_less: "[| x \<in> HFinite; y \<in> HFinite;
  4.1228 -         u \<in> Infinitesimal; st x < st y
  4.1229 -      |] ==> st x + u < st y"
  4.1230 +lemma Infinitesimal_add_st_less:
  4.1231 +     "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |] 
  4.1232 +      ==> st x + u < st y"
  4.1233  apply (drule st_SReal)+
  4.1234  apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
  4.1235  done
  4.1236  
  4.1237 -lemma Infinitesimal_add_st_le_cancel: "[| x \<in> HFinite; y \<in> HFinite;
  4.1238 -         u \<in> Infinitesimal; st x <= st y + u
  4.1239 -      |] ==> st x <= st y"
  4.1240 +lemma Infinitesimal_add_st_le_cancel:
  4.1241 +     "[| x \<in> HFinite; y \<in> HFinite;
  4.1242 +         u \<in> Infinitesimal; st x \<le> st y + u
  4.1243 +      |] ==> st x \<le> st y"
  4.1244  apply (simp add: linorder_not_less [symmetric])
  4.1245  apply (auto dest: Infinitesimal_add_st_less)
  4.1246  done
  4.1247  
  4.1248 -lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x <= y |] ==> st(x) <= st(y)"
  4.1249 +lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x \<le> y |] ==> st(x) \<le> st(y)"
  4.1250  apply (frule HFinite_st_Infinitesimal_add)
  4.1251  apply (rotate_tac 1)
  4.1252  apply (frule HFinite_st_Infinitesimal_add, safe)
  4.1253 @@ -1744,13 +1818,13 @@
  4.1254  apply (auto simp add: hypreal_add_assoc [symmetric])
  4.1255  done
  4.1256  
  4.1257 -lemma st_zero_le: "[| 0 <= x;  x \<in> HFinite |] ==> 0 <= st x"
  4.1258 +lemma st_zero_le: "[| 0 \<le> x;  x \<in> HFinite |] ==> 0 \<le> st x"
  4.1259  apply (subst numeral_0_eq_0 [symmetric])
  4.1260  apply (rule st_number_of [THEN subst])
  4.1261  apply (rule st_le, auto)
  4.1262  done
  4.1263  
  4.1264 -lemma st_zero_ge: "[| x <= 0;  x \<in> HFinite |] ==> st x <= 0"
  4.1265 +lemma st_zero_ge: "[| x \<le> 0;  x \<in> HFinite |] ==> st x \<le> 0"
  4.1266  apply (subst numeral_0_eq_0 [symmetric])
  4.1267  apply (rule st_number_of [THEN subst])
  4.1268  apply (rule st_le, auto)
  4.1269 @@ -1764,14 +1838,12 @@
  4.1270  
  4.1271  
  4.1272  
  4.1273 -(*--------------------------------------------------------------------
  4.1274 -   Alternative definitions for HFinite using Free ultrafilter
  4.1275 - --------------------------------------------------------------------*)
  4.1276 +subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
  4.1277  
  4.1278 -lemma FreeUltrafilterNat_Rep_hypreal: "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
  4.1279 +lemma FreeUltrafilterNat_Rep_hypreal:
  4.1280 +     "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
  4.1281        ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
  4.1282 -apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
  4.1283 -done
  4.1284 +by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
  4.1285  
  4.1286  lemma HFinite_FreeUltrafilterNat:
  4.1287      "x \<in> HFinite 
  4.1288 @@ -1793,33 +1865,37 @@
  4.1289  apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
  4.1290  done
  4.1291  
  4.1292 -lemma HFinite_FreeUltrafilterNat_iff: "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
  4.1293 +lemma HFinite_FreeUltrafilterNat_iff:
  4.1294 +     "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
  4.1295             \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
  4.1296  apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
  4.1297  done
  4.1298  
  4.1299 -(*--------------------------------------------------------------------
  4.1300 -   Alternative definitions for HInfinite using Free ultrafilter
  4.1301 - --------------------------------------------------------------------*)
  4.1302 -lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) <= u}"
  4.1303 +
  4.1304 +subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*}
  4.1305 +
  4.1306 +lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) \<le> u}"
  4.1307  by auto
  4.1308  
  4.1309 -lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u <= abs (xa n)}"
  4.1310 +lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u \<le> abs (xa n)}"
  4.1311  by auto
  4.1312  
  4.1313 -lemma lemma_Int_eq1: "{n. abs (xa n) <= (u::real)} Int {n. u <= abs (xa n)}
  4.1314 +lemma lemma_Int_eq1:
  4.1315 +     "{n. abs (xa n) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
  4.1316            = {n. abs(xa n) = u}"
  4.1317  apply auto
  4.1318  done
  4.1319  
  4.1320 -lemma lemma_FreeUltrafilterNat_one: "{n. abs (xa n) = u} <= {n. abs (xa n) < u + (1::real)}"
  4.1321 +lemma lemma_FreeUltrafilterNat_one:
  4.1322 +     "{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
  4.1323  by auto
  4.1324  
  4.1325  (*-------------------------------------
  4.1326    Exclude this type of sets from free
  4.1327    ultrafilter for Infinite numbers!
  4.1328   -------------------------------------*)
  4.1329 -lemma FreeUltrafilterNat_const_Finite: "[| xa: Rep_hypreal x;
  4.1330 +lemma FreeUltrafilterNat_const_Finite:
  4.1331 +     "[| xa: Rep_hypreal x;
  4.1332                    {n. abs (xa n) = u} \<in> FreeUltrafilterNat
  4.1333                 |] ==> x \<in> HFinite"
  4.1334  apply (rule FreeUltrafilterNat_HFinite)
  4.1335 @@ -1844,16 +1920,15 @@
  4.1336        add: HInfinite_HFinite_iff [THEN iffD1])
  4.1337  done
  4.1338  
  4.1339 -(* yet more lemmas! *)
  4.1340 -lemma lemma_Int_HI: "{n. abs (Xa n) < u} Int {n. X n = Xa n}
  4.1341 -          <= {n. abs (X n) < (u::real)}"
  4.1342 -apply auto
  4.1343 -done
  4.1344 +lemma lemma_Int_HI:
  4.1345 +     "{n. abs (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. abs (X n) < (u::real)}"
  4.1346 +by auto
  4.1347  
  4.1348  lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
  4.1349  by (auto intro: order_less_asym)
  4.1350  
  4.1351 -lemma FreeUltrafilterNat_HInfinite: "\<exists>X \<in> Rep_hypreal x. \<forall>u.
  4.1352 +lemma FreeUltrafilterNat_HInfinite:
  4.1353 +     "\<exists>X \<in> Rep_hypreal x. \<forall>u.
  4.1354                 {n. u < abs (X n)} \<in> FreeUltrafilterNat
  4.1355                 ==>  x \<in> HInfinite"
  4.1356  apply (rule HInfinite_HFinite_iff [THEN iffD2])
  4.1357 @@ -1866,15 +1941,13 @@
  4.1358  apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty)
  4.1359  done
  4.1360  
  4.1361 -lemma HInfinite_FreeUltrafilterNat_iff: "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
  4.1362 +lemma HInfinite_FreeUltrafilterNat_iff:
  4.1363 +     "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
  4.1364             \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
  4.1365 -apply (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
  4.1366 -done
  4.1367 +by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
  4.1368  
  4.1369 -(*--------------------------------------------------------------------
  4.1370 -   Alternative definitions for Infinitesimal using Free ultrafilter
  4.1371 - --------------------------------------------------------------------*)
  4.1372  
  4.1373 +subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
  4.1374  
  4.1375  lemma Infinitesimal_FreeUltrafilterNat:
  4.1376            "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
  4.1377 @@ -1900,7 +1973,8 @@
  4.1378  apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
  4.1379  done
  4.1380  
  4.1381 -lemma Infinitesimal_FreeUltrafilterNat_iff: "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
  4.1382 +lemma Infinitesimal_FreeUltrafilterNat_iff:
  4.1383 +     "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
  4.1384             \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
  4.1385  apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
  4.1386  done
  4.1387 @@ -1909,17 +1983,19 @@
  4.1388           Infinitesimals as smaller than 1/n for all n::nat (> 0)
  4.1389   ------------------------------------------------------------------------*)
  4.1390  
  4.1391 -lemma lemma_Infinitesimal: "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
  4.1392 +lemma lemma_Infinitesimal:
  4.1393 +     "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
  4.1394  apply (auto simp add: real_of_nat_Suc_gt_zero)
  4.1395  apply (blast dest!: reals_Archimedean intro: order_less_trans)
  4.1396  done
  4.1397  
  4.1398  lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
  4.1399  apply (induct n)
  4.1400 -apply (simp_all add: SReal_add);
  4.1401 +apply (simp_all add: SReal_add)
  4.1402  done 
  4.1403   
  4.1404 -lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
  4.1405 +lemma lemma_Infinitesimal2:
  4.1406 +     "(\<forall>r \<in> Reals. 0 < r --> x < r) =
  4.1407        (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
  4.1408  apply safe
  4.1409  apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
  4.1410 @@ -1966,33 +2042,35 @@
  4.1411  apply (auto dest: order_less_trans)
  4.1412  done
  4.1413  
  4.1414 -lemma lemma_real_le_Un_eq: "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}"
  4.1415 +lemma lemma_real_le_Un_eq:
  4.1416 +     "{n. f n \<le> u} = {n. f n < u} Un {n. u = (f n :: real)}"
  4.1417  by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
  4.1418  
  4.1419 -lemma finite_real_of_nat_le_real: "finite {n::nat. real n <= u}"
  4.1420 +lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
  4.1421  by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
  4.1422  
  4.1423 -lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) <= u}"
  4.1424 +lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
  4.1425  apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)
  4.1426  done
  4.1427  
  4.1428 -lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: "{n. abs(real n) <= u} \<notin> FreeUltrafilterNat"
  4.1429 +lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
  4.1430 +     "{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
  4.1431  by (blast intro!: FreeUltrafilterNat_finite finite_rabs_real_of_nat_le_real)
  4.1432  
  4.1433  lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
  4.1434  apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
  4.1435 -apply (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}")
  4.1436 +apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
  4.1437  prefer 2 apply force
  4.1438  apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat_finite])
  4.1439  done
  4.1440  
  4.1441  (*--------------------------------------------------------------
  4.1442 - The complement of {n. abs(real n) <= u} =
  4.1443 + The complement of {n. abs(real n) \<le> u} =
  4.1444   {n. u < abs (real n)} is in FreeUltrafilterNat
  4.1445   by property of (free) ultrafilters
  4.1446   --------------------------------------------------------------*)
  4.1447  
  4.1448 -lemma Compl_real_le_eq: "- {n::nat. real n <= u} = {n. u < real n}"
  4.1449 +lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
  4.1450  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
  4.1451  
  4.1452  (*-----------------------------------------------
  4.1453 @@ -2038,8 +2116,8 @@
  4.1454    that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
  4.1455   -----------------------------------------------------------------------*)
  4.1456  
  4.1457 -lemma real_of_nat_less_inverse_iff: "0 < u  ==>
  4.1458 -      (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
  4.1459 +lemma real_of_nat_less_inverse_iff:
  4.1460 +     "0 < u  ==> (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
  4.1461  apply (simp add: inverse_eq_divide)
  4.1462  apply (subst pos_less_divide_eq, assumption)
  4.1463  apply (subst pos_less_divide_eq)
  4.1464 @@ -2047,18 +2125,21 @@
  4.1465  apply (simp add: real_mult_commute)
  4.1466  done
  4.1467  
  4.1468 -lemma finite_inverse_real_of_posnat_gt_real: "0 < u ==> finite {n. u < inverse(real(Suc n))}"
  4.1469 +lemma finite_inverse_real_of_posnat_gt_real:
  4.1470 +     "0 < u ==> finite {n. u < inverse(real(Suc n))}"
  4.1471  apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)
  4.1472  apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])
  4.1473  apply (rule finite_real_of_nat_less_real)
  4.1474  done
  4.1475  
  4.1476 -lemma lemma_real_le_Un_eq2: "{n. u <= inverse(real(Suc n))} =
  4.1477 +lemma lemma_real_le_Un_eq2:
  4.1478 +     "{n. u \<le> inverse(real(Suc n))} =
  4.1479       {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"
  4.1480  apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
  4.1481  done
  4.1482  
  4.1483 -lemma real_of_nat_inverse_le_iff: "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))"
  4.1484 +lemma real_of_nat_inverse_le_iff:
  4.1485 +     "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))"
  4.1486  apply (simp (no_asm) add: linorder_not_less [symmetric])
  4.1487  apply (simp (no_asm) add: inverse_eq_divide)
  4.1488  apply (subst pos_less_divide_eq)
  4.1489 @@ -2066,7 +2147,8 @@
  4.1490  apply (simp (no_asm) add: real_mult_commute)
  4.1491  done
  4.1492  
  4.1493 -lemma real_of_nat_inverse_eq_iff: "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
  4.1494 +lemma real_of_nat_inverse_eq_iff:
  4.1495 +     "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
  4.1496  by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
  4.1497  
  4.1498  lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
  4.1499 @@ -2075,59 +2157,64 @@
  4.1500  apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute)
  4.1501  done
  4.1502  
  4.1503 -lemma finite_inverse_real_of_posnat_ge_real: "0 < u ==> finite {n. u <= inverse(real(Suc n))}"
  4.1504 +lemma finite_inverse_real_of_posnat_ge_real:
  4.1505 +     "0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
  4.1506  by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_omega_set2 finite_inverse_real_of_posnat_gt_real)
  4.1507  
  4.1508 -lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: "0 < u ==>
  4.1509 -       {n. u <= inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
  4.1510 -apply (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
  4.1511 -done
  4.1512 +lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
  4.1513 +     "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
  4.1514 +by (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
  4.1515  
  4.1516  (*--------------------------------------------------------------
  4.1517 -    The complement of  {n. u <= inverse(real(Suc n))} =
  4.1518 +    The complement of  {n. u \<le> inverse(real(Suc n))} =
  4.1519      {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
  4.1520      by property of (free) ultrafilters
  4.1521   --------------------------------------------------------------*)
  4.1522 -lemma Compl_le_inverse_eq: "- {n. u <= inverse(real(Suc n))} =
  4.1523 +lemma Compl_le_inverse_eq:
  4.1524 +     "- {n. u \<le> inverse(real(Suc n))} =
  4.1525        {n. inverse(real(Suc n)) < u}"
  4.1526  apply (auto dest!: order_le_less_trans simp add: linorder_not_le)
  4.1527  done
  4.1528  
  4.1529 -lemma FreeUltrafilterNat_inverse_real_of_posnat: "0 < u ==>
  4.1530 +lemma FreeUltrafilterNat_inverse_real_of_posnat:
  4.1531 +     "0 < u ==>
  4.1532        {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
  4.1533  apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
  4.1534  apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_le_inverse_eq)
  4.1535  done
  4.1536  
  4.1537 -(*--------------------------------------------------------------
  4.1538 -      Example where we get a hyperreal from a real sequence
  4.1539 +text{* Example where we get a hyperreal from a real sequence
  4.1540        for which a particular property holds. The theorem is
  4.1541        used in proofs about equivalence of nonstandard and
  4.1542        standard neighbourhoods. Also used for equivalence of
  4.1543        nonstandard ans standard definitions of pointwise
  4.1544 -      limit (the theorem was previously in REALTOPOS.thy).
  4.1545 - -------------------------------------------------------------*)
  4.1546 +      limit.*}
  4.1547 +
  4.1548  (*-----------------------------------------------------
  4.1549      |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
  4.1550   -----------------------------------------------------*)
  4.1551 -lemma real_seq_to_hypreal_Infinitesimal: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
  4.1552 +lemma real_seq_to_hypreal_Infinitesimal:
  4.1553 +     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
  4.1554       ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
  4.1555  apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
  4.1556  done
  4.1557  
  4.1558 -lemma real_seq_to_hypreal_approx: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
  4.1559 +lemma real_seq_to_hypreal_approx:
  4.1560 +     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
  4.1561        ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
  4.1562  apply (subst approx_minus_iff)
  4.1563  apply (rule mem_infmal_iff [THEN subst])
  4.1564  apply (erule real_seq_to_hypreal_Infinitesimal)
  4.1565  done
  4.1566  
  4.1567 -lemma real_seq_to_hypreal_approx2: "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
  4.1568 +lemma real_seq_to_hypreal_approx2:
  4.1569 +     "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
  4.1570                 ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
  4.1571  apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
  4.1572  done
  4.1573  
  4.1574 -lemma real_seq_to_hypreal_Infinitesimal2: "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
  4.1575 +lemma real_seq_to_hypreal_Infinitesimal2:
  4.1576 +     "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
  4.1577        ==> Abs_hypreal(hyprel``{X}) +
  4.1578            -Abs_hypreal(hyprel``{Y}) \<in> Infinitesimal"
  4.1579  by (auto intro!: bexI
  4.1580 @@ -2351,7 +2438,3 @@
  4.1581  *}
  4.1582  
  4.1583  end
  4.1584 -
  4.1585 -
  4.1586 -
  4.1587 -
     5.1 --- a/src/HOL/IsaMakefile	Mon Mar 01 05:39:32 2004 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Mon Mar 01 11:52:59 2004 +0100
     5.3 @@ -146,7 +146,8 @@
     5.4    Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
     5.5    Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
     5.6    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
     5.7 -  Hyperreal/HyperArith.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
     5.8 +  Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
     5.9 +  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
    5.10    Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
    5.11    Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
    5.12    Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.thy\