src/HOL/Real/Hyperreal/NSA.ML
changeset 10045 c76b73e16711
child 10230 5eb935d6cc69
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/NSA.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,2297 @@
     1.4 +(*  Title       : NSA.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Infinite numbers, Infinitesimals,
     1.8 +                  infinitely close relation  etc.
     1.9 +*) 
    1.10 +
    1.11 +fun CLAIM_SIMP str thms =
    1.12 +               prove_goal (the_context()) str
    1.13 +               (fn prems => [cut_facts_tac prems 1,
    1.14 +                   auto_tac (claset(),simpset() addsimps thms)]);
    1.15 +fun CLAIM str = CLAIM_SIMP str [];
    1.16 +
    1.17 +(*--------------------------------------------------------------------
    1.18 +     Closure laws for members of (embedded) set standard real SReal
    1.19 + --------------------------------------------------------------------*)
    1.20 +
    1.21 +Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x + y: SReal";
    1.22 +by (Step_tac 1);
    1.23 +by (res_inst_tac [("x","r + ra")] exI 1);
    1.24 +by (simp_tac (simpset() addsimps [hypreal_of_real_add]) 1);
    1.25 +qed "SReal_add";
    1.26 +
    1.27 +Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x * y: SReal";
    1.28 +by (Step_tac 1);
    1.29 +by (res_inst_tac [("x","r * ra")] exI 1);
    1.30 +by (simp_tac (simpset() addsimps [hypreal_of_real_mult]) 1);
    1.31 +qed "SReal_mult";
    1.32 +
    1.33 +Goalw [SReal_def] "[| x: SReal; x ~= 0 |] ==> hrinv x : SReal";
    1.34 +by (blast_tac (claset() addSDs [hypreal_of_real_hrinv2]) 1);
    1.35 +qed "SReal_hrinv";
    1.36 +
    1.37 +Goalw [SReal_def] "x: SReal ==> -x : SReal";
    1.38 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus RS sym]));
    1.39 +qed "SReal_minus";
    1.40 +
    1.41 +Goal "[| x + y : SReal; y: SReal |] ==> x: SReal";
    1.42 +by (dres_inst_tac [("x","y")] SReal_minus 1);
    1.43 +by (dtac SReal_add 1);
    1.44 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
    1.45 +qed "SReal_add_cancel";
    1.46 +
    1.47 +Goalw [SReal_def] "x: SReal ==> abs x : SReal";
    1.48 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_hrabs]));
    1.49 +qed "SReal_hrabs";
    1.50 +
    1.51 +Goalw [SReal_def] "hypreal_of_real #1 : SReal";
    1.52 +by (Auto_tac);
    1.53 +qed "SReal_hypreal_of_real_one";
    1.54 +
    1.55 +Goalw [SReal_def] "hypreal_of_real 0 : SReal";
    1.56 +by (Auto_tac);
    1.57 +qed "SReal_hypreal_of_real_zero";
    1.58 +
    1.59 +Goal "1hr : SReal";
    1.60 +by (simp_tac (simpset() addsimps [SReal_hypreal_of_real_one,
    1.61 +    hypreal_of_real_one RS sym]) 1);
    1.62 +qed "SReal_one";
    1.63 +
    1.64 +Goal "0 : SReal";
    1.65 +by (simp_tac (simpset() addsimps [rename_numerals 
    1.66 +    SReal_hypreal_of_real_zero,hypreal_of_real_zero RS sym]) 1);
    1.67 +qed "SReal_zero";
    1.68 +
    1.69 +Goal "1hr + 1hr : SReal";
    1.70 +by (rtac ([SReal_one,SReal_one] MRS SReal_add) 1);
    1.71 +qed "SReal_two";
    1.72 +
    1.73 +Addsimps [SReal_zero,SReal_two];
    1.74 +
    1.75 +Goal "r : SReal ==> r*hrinv(1hr + 1hr): SReal";
    1.76 +by (blast_tac (claset() addSIs [SReal_mult,SReal_hrinv,
    1.77 +    SReal_two,hypreal_two_not_zero]) 1);
    1.78 +qed "SReal_half";
    1.79 +
    1.80 +(* in general: move before previous thms!*)
    1.81 +Goalw [SReal_def] "hypreal_of_real  x: SReal";
    1.82 +by (Blast_tac 1);
    1.83 +qed "SReal_hypreal_of_real";
    1.84 +
    1.85 +Addsimps [SReal_hypreal_of_real];
    1.86 +
    1.87 +(* Infinitesimal ehr not in SReal *)
    1.88 +
    1.89 +Goalw [SReal_def] "ehr ~: SReal";
    1.90 +by (auto_tac (claset(),simpset() addsimps 
    1.91 +    [hypreal_of_real_not_eq_epsilon RS not_sym]));
    1.92 +qed "SReal_epsilon_not_mem";
    1.93 +
    1.94 +Goalw [SReal_def] "whr ~: SReal";
    1.95 +by (auto_tac (claset(),simpset() addsimps 
    1.96 +    [hypreal_of_real_not_eq_omega RS not_sym]));
    1.97 +qed "SReal_omega_not_mem";
    1.98 +
    1.99 +Goalw [SReal_def] "{x. hypreal_of_real x : SReal} = (UNIV::real set)";
   1.100 +by (Auto_tac);
   1.101 +qed "SReal_UNIV_real";
   1.102 +
   1.103 +Goalw [SReal_def] "(x: SReal) = (? y. x = hypreal_of_real  y)";
   1.104 +by (Auto_tac);
   1.105 +qed "SReal_iff";
   1.106 +
   1.107 +Goalw [SReal_def] "hypreal_of_real ``(UNIV::real set) = SReal";
   1.108 +by (Auto_tac);
   1.109 +qed "hypreal_of_real_image";
   1.110 +
   1.111 +Goalw [SReal_def] "inv hypreal_of_real ``SReal = (UNIV::real set)";
   1.112 +by (Auto_tac);
   1.113 +by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
   1.114 +by (Blast_tac 1);
   1.115 +qed "inv_hypreal_of_real_image";
   1.116 +
   1.117 +Goalw [SReal_def] 
   1.118 +      "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real `` Q";
   1.119 +by (Best_tac 1); 
   1.120 +qed "SReal_hypreal_of_real_image";
   1.121 +
   1.122 +Goal "[| x: SReal; y: SReal; x < y |] ==> EX r: SReal. x < r & r < y";
   1.123 +by (auto_tac (claset(),simpset() addsimps [SReal_iff]));
   1.124 +by (dtac real_dense 1 THEN Step_tac 1);
   1.125 +by (res_inst_tac [("x","hypreal_of_real r")] bexI 1);
   1.126 +by (Auto_tac);
   1.127 +qed "SReal_dense";
   1.128 +
   1.129 +(*------------------------------------------------------------------
   1.130 +                   Completeness of SReal
   1.131 + ------------------------------------------------------------------*)
   1.132 +Goal "P <= SReal ==> ((? x:P. y < x) = \ 
   1.133 +\     (? X. hypreal_of_real X : P & y < hypreal_of_real X))";
   1.134 +by (blast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
   1.135 +by (flexflex_tac );
   1.136 +qed "SReal_sup_lemma";
   1.137 +
   1.138 +Goal "[| P <= SReal; ? x. x: P; ? y : SReal. !x: P. x < y |] \
   1.139 +\     ==> (? X. X: {w. hypreal_of_real w : P}) & \
   1.140 +\         (? Y. !X: {w. hypreal_of_real w : P}. X < Y)";
   1.141 +by (rtac conjI 1);
   1.142 +by (fast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
   1.143 +by (Auto_tac THEN forward_tac [subsetD] 1 THEN assume_tac 1);
   1.144 +by (dtac (SReal_iff RS iffD1) 1);
   1.145 +by (Auto_tac THEN res_inst_tac [("x","ya")] exI 1);
   1.146 +by (auto_tac (claset() addDs [bspec],
   1.147 +   simpset() addsimps [hypreal_of_real_less_iff RS sym]));
   1.148 +qed "SReal_sup_lemma2";
   1.149 +
   1.150 +(*------------------------------------------------------
   1.151 +    lifting of ub and property of lub
   1.152 + -------------------------------------------------------*)
   1.153 +Goalw [isUb_def,setle_def] 
   1.154 +      "(isUb (SReal) (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
   1.155 +\      (isUb (UNIV :: real set) Q Y)";
   1.156 +by (blast_tac (claset() addIs [hypreal_of_real_le_iff RS iffD1,
   1.157 +                hypreal_of_real_le_iff RS iffD2,SReal_hypreal_of_real]) 1);
   1.158 +qed "hypreal_of_real_isUb_iff";
   1.159 +
   1.160 +Goalw [isLub_def,leastP_def] 
   1.161 +      "isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y) \
   1.162 +\      ==> isLub (UNIV :: real set) Q Y";
   1.163 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_isUb_iff,
   1.164 +               setge_def]));
   1.165 +by (blast_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2,
   1.166 +               hypreal_of_real_le_iff RS iffD2]) 1);
   1.167 +qed "hypreal_of_real_isLub1";
   1.168 +
   1.169 +Goalw [isLub_def,leastP_def] 
   1.170 +      "isLub (UNIV :: real set) Q Y \
   1.171 +\      ==> isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)";
   1.172 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_isUb_iff,
   1.173 +               setge_def]));
   1.174 +by (forw_inst_tac [("x2","x")] (isUbD2a RS (SReal_iff RS iffD1) RS exE) 1);
   1.175 +by (assume_tac 2);
   1.176 +by (dres_inst_tac [("x","xa")] spec 1);
   1.177 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_isUb_iff,
   1.178 +    hypreal_of_real_le_iff RS iffD1]));
   1.179 +qed "hypreal_of_real_isLub2";
   1.180 +
   1.181 +Goal
   1.182 +    "(isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
   1.183 +\    (isLub (UNIV :: real set) Q Y)";
   1.184 +by (blast_tac (claset() addIs [hypreal_of_real_isLub1,hypreal_of_real_isLub2]) 1);
   1.185 +qed "hypreal_of_real_isLub_iff";
   1.186 +
   1.187 +(* lemmas *)
   1.188 +Goalw [isUb_def] 
   1.189 +     "isUb SReal P Y \
   1.190 +\     ==> EX Yo. isUb SReal P (hypreal_of_real Yo)";
   1.191 +by (auto_tac (claset(),simpset() addsimps [SReal_iff]));
   1.192 +qed "lemma_isUb_hypreal_of_real";
   1.193 +
   1.194 +Goalw [isLub_def,leastP_def,isUb_def] 
   1.195 +      "isLub SReal P Y ==> EX Yo. isLub SReal P (hypreal_of_real Yo)";
   1.196 +by (auto_tac (claset(),simpset() addsimps [SReal_iff]));
   1.197 +qed "lemma_isLub_hypreal_of_real";
   1.198 +
   1.199 +Goalw [isLub_def,leastP_def,isUb_def] 
   1.200 +      "EX Yo. isLub SReal P (hypreal_of_real Yo) \
   1.201 +\      ==> EX Y. isLub SReal P Y";
   1.202 +by (Auto_tac);
   1.203 +qed "lemma_isLub_hypreal_of_real2";
   1.204 +
   1.205 +Goal "[| P <= SReal; EX x. x: P; \
   1.206 +\        EX Y. isUb SReal P Y |] \
   1.207 +\     ==> EX t. isLub SReal P t";
   1.208 +by (forward_tac [SReal_hypreal_of_real_image] 1);
   1.209 +by (Auto_tac THEN dtac lemma_isUb_hypreal_of_real 1);
   1.210 +by (auto_tac (claset() addSIs [reals_complete,
   1.211 +    lemma_isLub_hypreal_of_real2], simpset() addsimps 
   1.212 +    [hypreal_of_real_isLub_iff,hypreal_of_real_isUb_iff]));
   1.213 +qed "SReal_complete";
   1.214 +
   1.215 +(*--------------------------------------------------------------------
   1.216 +        Set of finite elements is a subring of the extended reals
   1.217 + --------------------------------------------------------------------*)
   1.218 +Goalw [HFinite_def] "[|x : HFinite;y : HFinite|] ==> (x+y) : HFinite";
   1.219 +by (blast_tac (claset() addSIs [SReal_add,hrabs_add_less]) 1);
   1.220 +qed "HFinite_add";
   1.221 +
   1.222 +Goalw [HFinite_def] "[|x : HFinite;y : HFinite|] ==> (x*y) : HFinite";
   1.223 +by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
   1.224 +qed "HFinite_mult";
   1.225 +
   1.226 +Goalw [HFinite_def] "(x:HFinite)=(-x:HFinite)";
   1.227 +by (simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
   1.228 +qed "HFinite_minus_iff";
   1.229 +
   1.230 +Goal "[| x: HFinite; y: HFinite|] ==> (x + -y): HFinite";
   1.231 +by (blast_tac (claset() addDs [HFinite_minus_iff RS iffD1] addIs [HFinite_add]) 1);
   1.232 +qed "HFinite_add_minus";
   1.233 +
   1.234 +Goalw [SReal_def,HFinite_def] "SReal <= HFinite";
   1.235 +by Auto_tac;
   1.236 +by (res_inst_tac [("x","1hr + abs(hypreal_of_real r)")] exI 1);
   1.237 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_hrabs,
   1.238 +    hypreal_of_real_one RS sym,hypreal_of_real_add RS sym,
   1.239 +    hypreal_of_real_zero RS sym]));
   1.240 +qed "SReal_subset_HFinite";
   1.241 +
   1.242 +Goal "hypreal_of_real x : HFinite";
   1.243 +by (auto_tac (claset() addIs [(SReal_subset_HFinite RS subsetD)],
   1.244 +              simpset()));
   1.245 +qed "HFinite_hypreal_of_real";
   1.246 +
   1.247 +Addsimps [HFinite_hypreal_of_real];
   1.248 +
   1.249 +Goalw [HFinite_def] "x : HFinite ==> EX t: SReal. abs x < t";
   1.250 +by (Auto_tac);
   1.251 +qed "HFiniteD";
   1.252 +
   1.253 +Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite";
   1.254 +by (auto_tac (claset(),simpset() addsimps [hrabs_idempotent]));
   1.255 +qed "HFinite_hrabs";
   1.256 +
   1.257 +Goalw [HFinite_def,Bex_def] "x ~: HFinite ==> abs x ~: HFinite";
   1.258 +by (auto_tac (claset() addDs [spec],simpset() addsimps [hrabs_idempotent]));
   1.259 +qed "not_HFinite_hrabs";
   1.260 +
   1.261 +goal NSA.thy "0 : HFinite";
   1.262 +by (rtac (SReal_zero RS (SReal_subset_HFinite RS subsetD)) 1);
   1.263 +qed "HFinite_zero";
   1.264 +Addsimps [HFinite_zero];
   1.265 +
   1.266 +goal NSA.thy "1hr : HFinite";
   1.267 +by (rtac (SReal_one RS (SReal_subset_HFinite RS subsetD)) 1);
   1.268 +qed "HFinite_one";
   1.269 +Addsimps [HFinite_one];
   1.270 +
   1.271 +Goal "[|x : HFinite; y <= x; 0 <= y |] ==> y: HFinite";
   1.272 +by (case_tac "x <= 0" 1);
   1.273 +by (dres_inst_tac [("j","x")] hypreal_le_trans 1);
   1.274 +by (dtac hypreal_le_anti_sym 2);
   1.275 +by (auto_tac (claset() addSDs [not_hypreal_leE],simpset()));
   1.276 +by (auto_tac (claset() addSIs [bexI]
   1.277 +    addIs [hypreal_le_less_trans],simpset() addsimps 
   1.278 +    [hrabs_eqI1,hrabs_eqI2,hrabs_minus_eqI1,HFinite_def]));
   1.279 +qed "HFinite_bounded"; 
   1.280 +
   1.281 +(*------------------------------------------------------------------
   1.282 +       Set of infinitesimals is a subring of the hyperreals   
   1.283 + ------------------------------------------------------------------*)
   1.284 +Goalw [Infinitesimal_def]
   1.285 +      "x : Infinitesimal ==> ALL r: SReal. 0 < r --> abs x < r";
   1.286 +by (Auto_tac);
   1.287 +qed "InfinitesimalD";
   1.288 +
   1.289 +Goalw [Infinitesimal_def] "0 : Infinitesimal";
   1.290 +by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
   1.291 +qed "Infinitesimal_zero";
   1.292 +
   1.293 +Addsimps [Infinitesimal_zero];
   1.294 +
   1.295 +Goalw [Infinitesimal_def] 
   1.296 +      "[| x : Infinitesimal; y : Infinitesimal |] \
   1.297 +\      ==> (x + y) : Infinitesimal";
   1.298 +by (Auto_tac);
   1.299 +by (rtac (hypreal_sum_of_halves RS subst) 1);
   1.300 +by (dtac hypreal_half_gt_zero 1);
   1.301 +by (dtac SReal_half 1);
   1.302 +by (auto_tac (claset() addSDs [bspec] 
   1.303 +    addIs [hrabs_add_less],simpset()));
   1.304 +qed "Infinitesimal_add";
   1.305 +
   1.306 +Goalw [Infinitesimal_def] 
   1.307 +     "(x:Infinitesimal) = (-x:Infinitesimal)";
   1.308 +by (full_simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
   1.309 +qed "Infinitesimal_minus_iff";
   1.310 +
   1.311 +Goal "x ~:Infinitesimal = (-x ~:Infinitesimal)";
   1.312 +by (full_simp_tac (simpset() addsimps [Infinitesimal_minus_iff RS sym]) 1);
   1.313 +qed "not_Infinitesimal_minus_iff";
   1.314 +
   1.315 +val prem1::prem2::rest = 
   1.316 +goal thy "[| x : Infinitesimal; y : Infinitesimal  |] \
   1.317 +\         ==> (x + -y):Infinitesimal";
   1.318 +by (full_simp_tac (simpset() addsimps [prem1,prem2,
   1.319 +    (Infinitesimal_minus_iff RS iffD1),Infinitesimal_add]) 1);
   1.320 +qed "Infinitesimal_add_minus";
   1.321 +
   1.322 +Goalw [Infinitesimal_def] 
   1.323 +      "[| x : Infinitesimal; y : Infinitesimal |] \
   1.324 +\      ==> (x * y) : Infinitesimal";
   1.325 +by (Auto_tac);
   1.326 +by (rtac (hypreal_mult_1_right RS subst) 1);
   1.327 +by (rtac hrabs_mult_less 1);
   1.328 +by (cut_facts_tac [SReal_one,hypreal_zero_less_one] 2);
   1.329 +by (ALLGOALS(blast_tac (claset() addSDs [bspec])));
   1.330 +qed "Infinitesimal_mult";
   1.331 +
   1.332 +Goal "[| x : Infinitesimal; y : HFinite |] \
   1.333 +\     ==> (x * y) : Infinitesimal";
   1.334 +by (auto_tac (claset() addSDs [HFiniteD],
   1.335 +    simpset() addsimps [Infinitesimal_def]));
   1.336 +by (forward_tac [hrabs_less_gt_zero] 1);
   1.337 +by (dtac (hypreal_hrinv_gt_zero RSN (2,hypreal_mult_less_mono2)) 1 
   1.338 +    THEN assume_tac 1);
   1.339 +by (dtac ((hypreal_not_refl2 RS not_sym) RSN (2,SReal_hrinv)) 1 
   1.340 +    THEN assume_tac 1);
   1.341 +by (dtac SReal_mult 1 THEN assume_tac 1);
   1.342 +by (thin_tac "hrinv t : SReal" 1);
   1.343 +by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hrabs_mult]));
   1.344 +by (dtac hrabs_mult_less 1 THEN assume_tac 1);
   1.345 +by (dtac (hypreal_not_refl2 RS not_sym) 1);
   1.346 +by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
   1.347 +     simpset() addsimps [hrabs_mult] @ hypreal_mult_ac));
   1.348 +qed "Infinitesimal_HFinite_mult";
   1.349 +
   1.350 +Goal "[| x : Infinitesimal; y : HFinite |] \
   1.351 +\     ==> (y * x) : Infinitesimal";
   1.352 +by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
   1.353 +              simpset() addsimps [hypreal_mult_commute]));
   1.354 +qed "Infinitesimal_HFinite_mult2";
   1.355 +
   1.356 +(*** rather long proof ***)
   1.357 +Goalw [HInfinite_def,Infinitesimal_def] 
   1.358 +      "x: HInfinite ==> hrinv x: Infinitesimal";
   1.359 +by (Auto_tac);
   1.360 +by (eres_inst_tac [("x","hrinv r")] ballE 1);
   1.361 +by (rtac (hrabs_hrinv RS ssubst) 1);
   1.362 +by (etac (((hypreal_hrinv_gt_zero RS hypreal_less_trans) 
   1.363 +   RS hypreal_not_refl2 RS not_sym) RS (hrabs_not_zero_iff 
   1.364 +   RS iffD2)) 1 THEN assume_tac 1);
   1.365 +by (forw_inst_tac [("x1","r"),("R3.0","abs x")] 
   1.366 +    (hypreal_hrinv_gt_zero RS hypreal_less_trans) 1);
   1.367 +by (assume_tac 1);
   1.368 +by (forw_inst_tac [("s","abs x"),("t","0")] 
   1.369 +              (hypreal_not_refl2 RS not_sym) 1);
   1.370 +by (dtac ((hypreal_hrinv_hrinv RS sym) RS subst) 1);
   1.371 +by (rotate_tac 2 1 THEN assume_tac 1);
   1.372 +by (dres_inst_tac [("x","abs x")] hypreal_hrinv_gt_zero 1);
   1.373 +by (rtac (hypreal_hrinv_less_iff RS ssubst) 1);
   1.374 +by (auto_tac (claset() addSDs [SReal_hrinv],
   1.375 +    simpset() addsimps [hypreal_not_refl2 RS not_sym,
   1.376 +    hypreal_less_not_refl]));
   1.377 +qed "HInfinite_hrinv_Infinitesimal";
   1.378 +
   1.379 +Goalw [HInfinite_def] 
   1.380 +   "[|x: HInfinite;y: HInfinite|] ==> (x*y): HInfinite";
   1.381 +by (Auto_tac);
   1.382 +by (cut_facts_tac [SReal_one] 1);
   1.383 +by (eres_inst_tac [("x","1hr")] ballE 1);
   1.384 +by (eres_inst_tac [("x","r")] ballE 1);
   1.385 +by (REPEAT(fast_tac (HOL_cs addSIs [hrabs_mult_gt]) 1));
   1.386 +qed "HInfinite_mult";
   1.387 +
   1.388 +Goalw [HInfinite_def] 
   1.389 +      "[|x: HInfinite; 0 <= y; 0 <= x|] \
   1.390 +\      ==> (x + y): HInfinite";
   1.391 +by (auto_tac (claset() addSIs  
   1.392 +    [hypreal_add_zero_less_le_mono],
   1.393 +    simpset() addsimps [hrabs_eqI1,
   1.394 +    hypreal_add_commute,hypreal_le_add_order]));
   1.395 +qed "HInfinite_add_ge_zero";
   1.396 +
   1.397 +Goal "[|x: HInfinite; 0 <= y; 0 <= x|] \
   1.398 +\      ==> (y + x): HInfinite";
   1.399 +by (auto_tac (claset() addSIs [HInfinite_add_ge_zero],
   1.400 +    simpset() addsimps [hypreal_add_commute]));
   1.401 +qed "HInfinite_add_ge_zero2";
   1.402 +
   1.403 +Goal "[|x: HInfinite; 0 < y; 0 < x|] \
   1.404 +\      ==> (x + y): HInfinite";
   1.405 +by (blast_tac (claset() addIs [HInfinite_add_ge_zero,
   1.406 +    hypreal_less_imp_le]) 1);
   1.407 +qed "HInfinite_add_gt_zero";
   1.408 +
   1.409 +goalw NSA.thy [HInfinite_def] 
   1.410 +     "(-x: HInfinite) = (x: HInfinite)";
   1.411 +by (auto_tac (claset(),simpset() addsimps 
   1.412 +    [hrabs_minus_cancel]));
   1.413 +qed "HInfinite_minus_iff";
   1.414 +
   1.415 +Goal "[|x: HInfinite; y <= 0; x <= 0|] \
   1.416 +\      ==> (x + y): HInfinite";
   1.417 +by (dtac (HInfinite_minus_iff RS iffD2) 1);
   1.418 +by (rtac (HInfinite_minus_iff RS iffD1) 1);
   1.419 +by (auto_tac (claset() addIs [HInfinite_add_ge_zero],
   1.420 +    simpset() addsimps [hypreal_minus_zero_le_iff RS sym,
   1.421 +    hypreal_minus_add_distrib]));
   1.422 +qed "HInfinite_add_le_zero";
   1.423 +
   1.424 +Goal "[|x: HInfinite; y < 0; x < 0|] \
   1.425 +\      ==> (x + y): HInfinite";
   1.426 +by (blast_tac (claset() addIs [HInfinite_add_le_zero,
   1.427 +    hypreal_less_imp_le]) 1);
   1.428 +qed "HInfinite_add_lt_zero";
   1.429 +
   1.430 +Goal "[|a: HFinite; b: HFinite; c: HFinite|] \ 
   1.431 +\     ==> a*a + b*b + c*c : HFinite";
   1.432 +by (auto_tac (claset() addIs [HFinite_mult,HFinite_add],
   1.433 +    simpset()));
   1.434 +qed "HFinite_sum_squares";
   1.435 +
   1.436 +Goal "!!x. x ~: Infinitesimal ==> x ~= 0";
   1.437 +by (Auto_tac);
   1.438 +qed "not_Infinitesimal_not_zero";
   1.439 +
   1.440 +Goal "!!x. x: HFinite - Infinitesimal ==> x ~= 0";
   1.441 +by (Auto_tac);
   1.442 +qed "not_Infinitesimal_not_zero2";
   1.443 +
   1.444 +Goal "!!x. x : Infinitesimal ==> abs x : Infinitesimal";
   1.445 +by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
   1.446 +by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
   1.447 +qed "Infinitesimal_hrabs";
   1.448 +
   1.449 +Goal "!!x. x ~: Infinitesimal ==> abs x ~: Infinitesimal";
   1.450 +by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
   1.451 +by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
   1.452 +qed "not_Infinitesimal_hrabs";
   1.453 +
   1.454 +Goal "!!x. abs x : Infinitesimal ==> x : Infinitesimal";
   1.455 +by (rtac ccontr 1);
   1.456 +by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1);
   1.457 +qed "hrabs_Infinitesimal_Infinitesimal";
   1.458 +
   1.459 +Goal "!!x. x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
   1.460 +by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1);
   1.461 +qed "HFinite_diff_Infinitesimal_hrabs";
   1.462 +
   1.463 +Goalw [Infinitesimal_def] 
   1.464 +      "!!x. [| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
   1.465 +by (auto_tac (claset() addSDs [bspec],simpset()));
   1.466 +by (dres_inst_tac [("i","e")] (hrabs_ge_self RS hypreal_le_less_trans) 1);
   1.467 +by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
   1.468 +qed "hrabs_less_Infinitesimal";
   1.469 +
   1.470 +Goal 
   1.471 + "!!x. [| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
   1.472 +by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq] addIs
   1.473 +    [hrabs_Infinitesimal_Infinitesimal,hrabs_less_Infinitesimal]) 1);
   1.474 +qed "hrabs_le_Infinitesimal";
   1.475 +
   1.476 +Goalw [Infinitesimal_def] 
   1.477 +      "!!x. [| e : Infinitesimal; \
   1.478 +\              e' : Infinitesimal; \
   1.479 +\              e' < x ; x < e |] ==> x : Infinitesimal";
   1.480 +by (auto_tac (claset() addSDs [bspec],simpset()));
   1.481 +by (dres_inst_tac [("i","e")] (hrabs_ge_self RS hypreal_le_less_trans) 1);
   1.482 +by (dtac (hrabs_interval_iff RS iffD1 RS conjunct1) 1);
   1.483 +by (fast_tac (claset() addIs [hypreal_less_trans,hrabs_interval_iff RS iffD2]) 1);
   1.484 +qed "Infinitesimal_interval";
   1.485 +
   1.486 +Goal "[| e : Infinitesimal; e' : Infinitesimal; \
   1.487 +\       e' <= x ; x <= e |] ==> x : Infinitesimal";
   1.488 +by (auto_tac (claset() addIs [Infinitesimal_interval],
   1.489 +    simpset() addsimps [hypreal_le_eq_less_or_eq]));
   1.490 +qed "Infinitesimal_interval2";
   1.491 +
   1.492 +Goalw [Infinitesimal_def] 
   1.493 +      "!! x y. [| x ~: Infinitesimal; \
   1.494 +\                 y ~: Infinitesimal|] \
   1.495 +\               ==> (x*y) ~:Infinitesimal";
   1.496 +by (Clarify_tac 1);
   1.497 +by (eres_inst_tac [("x","r*ra")] ballE 1);
   1.498 +by (fast_tac (claset() addIs [SReal_mult]) 2);
   1.499 +by (auto_tac (claset(),simpset() addsimps [hrabs_mult]));
   1.500 +by (blast_tac (claset() addSDs [hypreal_mult_order]) 1);
   1.501 +by (REPEAT(dtac hypreal_leI 1));
   1.502 +by (dtac hypreal_mult_le_ge_zero 1);
   1.503 +by (dres_inst_tac [("j","r*ra")] hypreal_less_le_trans 4);
   1.504 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   1.505 +qed "not_Infinitesimal_mult";
   1.506 +
   1.507 +Goal "!! x. x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
   1.508 +by (rtac ccontr 1);
   1.509 +by (dtac (de_Morgan_disj RS iffD1) 1);
   1.510 +by (fast_tac (claset() addDs [not_Infinitesimal_mult]) 1);
   1.511 +qed "Infinitesimal_mult_disj";
   1.512 +
   1.513 +Goal "!! x. x: HFinite-Infinitesimal ==> x ~= 0";
   1.514 +by (fast_tac (claset() addIs [Infinitesimal_zero]) 1);
   1.515 +qed "HFinite_Infinitesimal_not_zero";
   1.516 +
   1.517 +Goal "!! x. [| x : HFinite - Infinitesimal; \
   1.518 +\                  y : HFinite - Infinitesimal \
   1.519 +\               |] ==> (x*y) : HFinite - Infinitesimal";
   1.520 +by (Clarify_tac 1);
   1.521 +by (blast_tac (claset() addDs [HFinite_mult,not_Infinitesimal_mult]) 1);
   1.522 +qed "HFinite_Infinitesimal_diff_mult";
   1.523 +
   1.524 +Goalw [Infinitesimal_def,HFinite_def]  
   1.525 +      "Infinitesimal <= HFinite";
   1.526 +by (blast_tac (claset() addSIs [SReal_one] 
   1.527 +    addSEs [(hypreal_zero_less_one RSN (2,impE))]) 1);
   1.528 +qed "Infinitesimal_subset_HFinite";
   1.529 +
   1.530 +Goal "!!x. x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
   1.531 +by (etac (HFinite_hypreal_of_real RSN 
   1.532 +          (2,Infinitesimal_HFinite_mult)) 1);
   1.533 +qed "Infinitesimal_hypreal_of_real_mult";
   1.534 +
   1.535 +Goal "!!x. x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
   1.536 +by (etac (HFinite_hypreal_of_real RSN 
   1.537 +          (2,Infinitesimal_HFinite_mult2)) 1);
   1.538 +qed "Infinitesimal_hypreal_of_real_mult2";
   1.539 +
   1.540 +(*----------------------------------------------------------------------
   1.541 +                   Infinitely close relation @=
   1.542 + ----------------------------------------------------------------------*)
   1.543 +
   1.544 +Goalw [Infinitesimal_def,inf_close_def] 
   1.545 +        "x:Infinitesimal = (x @= 0)";
   1.546 +by (Simp_tac 1);
   1.547 +qed "mem_infmal_iff";
   1.548 +
   1.549 +Goalw [inf_close_def]" (x @= y) = (x + -y @= 0)";
   1.550 +by (Simp_tac 1);
   1.551 +qed "inf_close_minus_iff";
   1.552 +
   1.553 +Goalw [inf_close_def]" (x @= y) = (-y + x @= 0)";
   1.554 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.555 +qed "inf_close_minus_iff2";
   1.556 +
   1.557 +Goalw [inf_close_def,Infinitesimal_def]  "x @= x";
   1.558 +by (Simp_tac 1);
   1.559 +qed "inf_close_refl";
   1.560 +
   1.561 +Goalw [inf_close_def]  "!! x y. x @= y ==> y @= x";
   1.562 +by (rtac (hypreal_minus_distrib1 RS subst) 1);
   1.563 +by (etac (Infinitesimal_minus_iff RS iffD1) 1);
   1.564 +qed "inf_close_sym";
   1.565 +
   1.566 +val prem1::prem2::rest = 
   1.567 +goalw thy [inf_close_def]  "[| x @= y; y @= z |] ==> x @= z";
   1.568 +by (res_inst_tac [("y1","y")] (hypreal_add_minus_cancel1 RS subst) 1);
   1.569 +by (simp_tac (simpset() addsimps [([prem1,prem2] MRS Infinitesimal_add)]) 1);
   1.570 +qed "inf_close_trans";
   1.571 +
   1.572 +val prem1::prem2::rest = goal thy "[| r @= x; s @= x |] ==> r @= s";
   1.573 +by (rtac ([prem1,prem2 RS inf_close_sym] MRS inf_close_trans) 1);
   1.574 +qed "inf_close_trans2";
   1.575 +
   1.576 +val prem1::prem2::rest = goal thy "[| x @= r; x @= s|] ==> r @= s";
   1.577 +by (rtac ([prem1 RS inf_close_sym,prem2] MRS inf_close_trans) 1);
   1.578 +qed "inf_close_trans3";
   1.579 +
   1.580 +Goal "(x + -y : Infinitesimal) = (x @= y)";
   1.581 +by (auto_tac (claset(),simpset() addsimps 
   1.582 +    [inf_close_minus_iff RS sym,mem_infmal_iff]));
   1.583 +qed "Infinitesimal_inf_close_minus";
   1.584 +
   1.585 +Goal "(x + -y : Infinitesimal) = (y @= x)";
   1.586 +by (auto_tac (claset() addIs [inf_close_sym],
   1.587 +    simpset() addsimps [inf_close_minus_iff RS sym,
   1.588 +    mem_infmal_iff]));
   1.589 +qed "Infinitesimal_inf_close_minus2";
   1.590 +
   1.591 +Goalw [monad_def] "(x @= y) = (monad(x)=monad(y))";
   1.592 +by (auto_tac (claset() addDs [inf_close_sym] 
   1.593 +    addSEs [inf_close_trans,equalityCE],
   1.594 +    simpset() addsimps [inf_close_refl]));
   1.595 +qed "inf_close_monad_iff";
   1.596 +
   1.597 +Goal "!!x y. [| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
   1.598 +by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
   1.599 +by (fast_tac (claset() addIs [inf_close_trans2]) 1);
   1.600 +qed "Infinitesimal_inf_close";
   1.601 +
   1.602 +val prem1::prem2::rest = 
   1.603 +goalw thy [inf_close_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
   1.604 +by (rtac (hypreal_minus_add_distrib RS ssubst) 1);
   1.605 +by (rtac (hypreal_add_assoc RS ssubst) 1);
   1.606 +by (res_inst_tac [("y1","c")] (hypreal_add_left_commute RS subst) 1);
   1.607 +by (rtac (hypreal_add_assoc RS subst) 1);
   1.608 +by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1);
   1.609 +qed "inf_close_add";
   1.610 +
   1.611 +Goal "!!a. a @= b ==> -a @= -b";
   1.612 +by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
   1.613 +by (dtac (inf_close_minus_iff RS iffD1) 1);
   1.614 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.615 +qed "inf_close_minus";
   1.616 +
   1.617 +Goal "!!a. -a @= -b ==> a @= b";
   1.618 +by (auto_tac (claset() addDs [inf_close_minus],simpset()));
   1.619 +qed "inf_close_minus2";
   1.620 +
   1.621 +Goal "(-a @= -b) = (a @= b)";
   1.622 +by (blast_tac (claset() addIs [inf_close_minus,inf_close_minus2]) 1);
   1.623 +qed "inf_close_minus_cancel";
   1.624 +
   1.625 +Addsimps [inf_close_minus_cancel];
   1.626 +
   1.627 +Goal "!!a. [| a @= b; c @= d |] ==> a + -c @= b + -d";
   1.628 +by (blast_tac (claset() addSIs [inf_close_add,inf_close_minus]) 1);
   1.629 +qed "inf_close_add_minus";
   1.630 +
   1.631 +Goalw [inf_close_def] "!!a. [| a @= b; c: HFinite|] ==> a*c @= b*c"; 
   1.632 +by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult,
   1.633 +    hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym] 
   1.634 +    delsimps [hypreal_minus_mult_eq1 RS sym]) 1);
   1.635 +qed "inf_close_mult1";
   1.636 +
   1.637 +Goal "!!a. [|a @= b; c: HFinite|] ==> c*a @= c*b"; 
   1.638 +by (asm_simp_tac (simpset() addsimps [inf_close_mult1,hypreal_mult_commute]) 1);
   1.639 +qed "inf_close_mult2";
   1.640 +
   1.641 +val [prem1,prem2,prem3,prem4] = 
   1.642 +goal thy "[|a @= b; c @= d; b: HFinite; c: HFinite|] ==> a*c @= b*d";
   1.643 +by (fast_tac (claset() addIs [([prem1,prem4] MRS inf_close_mult1), 
   1.644 +    ([prem2,prem3] MRS inf_close_mult2),inf_close_trans]) 1);
   1.645 +qed "inf_close_mult_HFinite";
   1.646 +
   1.647 +Goal "!!u. [|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
   1.648 +by (fast_tac (claset() addIs [inf_close_mult2,inf_close_trans]) 1);
   1.649 +qed "inf_close_mult_subst";
   1.650 +
   1.651 +Goal "!!u. [| u @= x*v; x @= y; v: HFinite |] ==> u @= y*v";
   1.652 +by (fast_tac (claset() addIs [inf_close_mult1,inf_close_trans]) 1);
   1.653 +qed "inf_close_mult_subst2";
   1.654 +
   1.655 +Goal "!!u. [| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v";
   1.656 +by (auto_tac (claset() addIs [inf_close_mult_subst2],simpset()));
   1.657 +qed "inf_close_mult_subst_SReal";
   1.658 +
   1.659 +Goalw [inf_close_def]  "!!a. a = b ==> a @= b";
   1.660 +by (Asm_simp_tac 1);
   1.661 +qed "inf_close_eq_imp";
   1.662 +
   1.663 +Goal "!!x. x: Infinitesimal ==> -x @= x"; 
   1.664 +by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD1,
   1.665 +    mem_infmal_iff RS iffD1,inf_close_trans2]) 1);
   1.666 +qed "Infinitesimal_minus_inf_close";
   1.667 +
   1.668 +Goalw [inf_close_def]  "(EX y: Infinitesimal. x + -z = y) = (x @= z)";
   1.669 +by (Blast_tac 1);
   1.670 +qed "bex_Infinitesimal_iff";
   1.671 +
   1.672 +Goal "(EX y: Infinitesimal. x = z + y) = (x @= z)";
   1.673 +by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff4,
   1.674 +    bex_Infinitesimal_iff RS sym]) 1);
   1.675 +qed "bex_Infinitesimal_iff2";
   1.676 +
   1.677 +Goal "!!x. [| y: Infinitesimal; x + y = z |] ==> x @= z";
   1.678 +by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
   1.679 +by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
   1.680 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
   1.681 +    hypreal_add_assoc RS sym]));
   1.682 +qed "Infinitesimal_add_inf_close";
   1.683 +
   1.684 +Goal "!!y. y: Infinitesimal ==> x @= x + y";
   1.685 +by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
   1.686 +by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
   1.687 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
   1.688 +    hypreal_add_assoc RS sym]));
   1.689 +qed "Infinitesimal_add_inf_close_self";
   1.690 +
   1.691 +Goal "!!y. y: Infinitesimal ==> x @= y + x";
   1.692 +by (auto_tac (claset() addDs [Infinitesimal_add_inf_close_self],
   1.693 +    simpset() addsimps [hypreal_add_commute]));
   1.694 +qed "Infinitesimal_add_inf_close_self2";
   1.695 +
   1.696 +Goal "!!y. y: Infinitesimal ==> x @= x + -y";
   1.697 +by (blast_tac (claset() addSIs [Infinitesimal_add_inf_close_self,
   1.698 +    Infinitesimal_minus_iff RS iffD1]) 1);
   1.699 +qed "Infinitesimal_add_minus_inf_close_self";
   1.700 +
   1.701 +Goal "!!x. [| y: Infinitesimal; x+y @= z|] ==> x @= z";
   1.702 +by (dres_inst_tac [("x","x")] (Infinitesimal_add_inf_close_self RS inf_close_sym) 1);
   1.703 +by (etac (inf_close_trans3 RS inf_close_sym) 1);
   1.704 +by (assume_tac 1);
   1.705 +qed "Infinitesimal_add_cancel";
   1.706 +
   1.707 +Goal "!!x. [| y: Infinitesimal; x @= z + y|] ==> x @= z";
   1.708 +by (dres_inst_tac [("x","z")] (Infinitesimal_add_inf_close_self2  RS inf_close_sym) 1);
   1.709 +by (etac (inf_close_trans3 RS inf_close_sym) 1);
   1.710 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.711 +by (etac inf_close_sym 1);
   1.712 +qed "Infinitesimal_add_right_cancel";
   1.713 +
   1.714 +Goal "!!a. d + b  @= d + c ==> b @= c";
   1.715 +by (dtac (inf_close_minus_iff RS iffD1) 1);
   1.716 +by (asm_full_simp_tac (simpset() addsimps 
   1.717 +    [hypreal_minus_add_distrib,inf_close_minus_iff RS sym] 
   1.718 +    @ hypreal_add_ac) 1);
   1.719 +qed "inf_close_add_left_cancel";
   1.720 +
   1.721 +Goal "!!a. b + d @= c + d ==> b @= c";
   1.722 +by (rtac inf_close_add_left_cancel 1);
   1.723 +by (asm_full_simp_tac (simpset() addsimps 
   1.724 +    [hypreal_add_commute]) 1);
   1.725 +qed "inf_close_add_right_cancel";
   1.726 +
   1.727 +Goal "!!a. b @= c ==> d + b @= d + c";
   1.728 +by (rtac (inf_close_minus_iff RS iffD2) 1);
   1.729 +by (asm_full_simp_tac (simpset() addsimps 
   1.730 +    [hypreal_minus_add_distrib,inf_close_minus_iff RS sym] 
   1.731 +    @ hypreal_add_ac) 1);
   1.732 +qed "inf_close_add_mono1";
   1.733 +
   1.734 +Goal "!!a. b @= c ==> b + a @= c + a";
   1.735 +by (asm_simp_tac (simpset() addsimps 
   1.736 +    [hypreal_add_commute,inf_close_add_mono1]) 1);
   1.737 +qed "inf_close_add_mono2";
   1.738 +
   1.739 +Goal "(a + b @= a + c) = (b @= c)";
   1.740 +by (fast_tac (claset() addEs [inf_close_add_left_cancel,
   1.741 +    inf_close_add_mono1]) 1);
   1.742 +qed "inf_close_add_left_iff";
   1.743 +
   1.744 +Addsimps [inf_close_add_left_iff];
   1.745 +
   1.746 +Goal "(b + a @= c + a) = (b @= c)";
   1.747 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.748 +qed "inf_close_add_right_iff";
   1.749 +
   1.750 +Addsimps [inf_close_add_right_iff];
   1.751 +
   1.752 +Goal "!!x. [| x: HFinite; x @= y |] ==> y: HFinite";
   1.753 +by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
   1.754 +by (Step_tac 1);
   1.755 +by (dtac (Infinitesimal_subset_HFinite RS subsetD 
   1.756 +           RS (HFinite_minus_iff RS iffD1)) 1);
   1.757 +by (dtac HFinite_add 1);
   1.758 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.759 +qed "inf_close_HFinite";
   1.760 +
   1.761 +Goal "!!x. x @= hypreal_of_real D ==> x: HFinite";
   1.762 +by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
   1.763 +by (Auto_tac);
   1.764 +qed "inf_close_hypreal_of_real_HFinite";
   1.765 +
   1.766 +Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
   1.767 +\     ==> a*c @= hypreal_of_real b*hypreal_of_real d";
   1.768 +by (blast_tac (claset() addSIs [inf_close_mult_HFinite,
   1.769 +     inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
   1.770 +qed "inf_close_mult_hypreal_of_real";
   1.771 +
   1.772 +Goal "!!a. [| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
   1.773 +by (dtac (SReal_hrinv RS (SReal_subset_HFinite RS subsetD)) 1);
   1.774 +by (auto_tac (claset() addDs [inf_close_mult2],
   1.775 +    simpset() addsimps [hypreal_mult_assoc RS sym]));
   1.776 +qed "inf_close_SReal_mult_cancel_zero";
   1.777 +
   1.778 +(* REM comments: newly added *)
   1.779 +Goal "!!a. [| a: SReal; x @= 0 |] ==> x*a @= 0";
   1.780 +by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
   1.781 +              inf_close_mult1],simpset()));
   1.782 +qed "inf_close_mult_SReal1";
   1.783 +
   1.784 +Goal "!!a. [| a: SReal; x @= 0 |] ==> a*x @= 0";
   1.785 +by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
   1.786 +              inf_close_mult2],simpset()));
   1.787 +qed "inf_close_mult_SReal2";
   1.788 +
   1.789 +Goal "[|a : SReal; a ~= 0 |] ==> (a*x @= 0) = (x @= 0)";
   1.790 +by (blast_tac (claset() addIs [inf_close_SReal_mult_cancel_zero,
   1.791 +    inf_close_mult_SReal2]) 1);
   1.792 +qed "inf_close_mult_SReal_zero_cancel_iff";
   1.793 +Addsimps [inf_close_mult_SReal_zero_cancel_iff];
   1.794 +
   1.795 +Goal "!!a. [| a: SReal; a ~= 0; a* w @= a*z |] ==> w @= z";
   1.796 +by (dtac (SReal_hrinv RS (SReal_subset_HFinite RS subsetD)) 1);
   1.797 +by (auto_tac (claset() addDs [inf_close_mult2],
   1.798 +    simpset() addsimps [hypreal_mult_assoc RS sym]));
   1.799 +qed "inf_close_SReal_mult_cancel";
   1.800 +
   1.801 +Goal "!!a. [| a: SReal; a ~= 0|] ==> (a* w @= a*z) = (w @= z)";
   1.802 +by (auto_tac (claset() addSIs [inf_close_mult2,SReal_subset_HFinite RS subsetD] 
   1.803 +    addIs [inf_close_SReal_mult_cancel],simpset()));
   1.804 +qed "inf_close_SReal_mult_cancel_iff1";
   1.805 +Addsimps [inf_close_SReal_mult_cancel_iff1];
   1.806 +
   1.807 +Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
   1.808 +by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
   1.809 +by (Auto_tac);
   1.810 +by (dres_inst_tac [("x","-g")] hypreal_add_left_le_mono1 1);
   1.811 +by (dres_inst_tac [("x","-g")] hypreal_add_le_mono1 1);
   1.812 +by (res_inst_tac [("y","-y")] Infinitesimal_add_cancel 1);
   1.813 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym,
   1.814 +    Infinitesimal_minus_iff RS sym]));
   1.815 +by (rtac inf_close_sym 1);
   1.816 +by (simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   1.817 +by (rtac (inf_close_minus_iff RS iffD2) 1);
   1.818 +by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym,
   1.819 +    hypreal_add_commute]));
   1.820 +by (rtac Infinitesimal_interval2 1 THEN Auto_tac);
   1.821 +qed "inf_close_le_bound";
   1.822 +
   1.823 +Goal "[| z <= f; f @= g; g <= z |] ==> g @= z";
   1.824 +by (rtac inf_close_trans3 1);
   1.825 +by (auto_tac (claset() addIs [inf_close_le_bound],simpset()));
   1.826 +qed "inf_close_le_bound2";
   1.827 +
   1.828 +(*-----------------------------------------------------------------
   1.829 +    Zero is the only infinitesimal that is also a real
   1.830 + -----------------------------------------------------------------*)
   1.831 +
   1.832 +Goalw [Infinitesimal_def] 
   1.833 +      "[| x: SReal; y: Infinitesimal; 0 < x |] ==> y < x";
   1.834 +by (rtac (hrabs_ge_self RS hypreal_le_less_trans) 1);
   1.835 +by (Blast_tac 1);
   1.836 +qed "Infinitesimal_less_SReal";
   1.837 +
   1.838 +Goal "y: Infinitesimal ==> ALL r: SReal. 0 < r --> y < r";
   1.839 +by (blast_tac (claset() addIs [Infinitesimal_less_SReal]) 1);
   1.840 +qed "Infinitesimal_less_SReal2";
   1.841 +
   1.842 +Goalw [Infinitesimal_def] 
   1.843 +      "!!y. [| y: SReal; 0 < y|] ==> y ~: Infinitesimal";
   1.844 +by (auto_tac (claset() addSDs [bspec] addSEs [hypreal_less_irrefl],
   1.845 +    simpset() addsimps [hrabs_eqI2]));
   1.846 +qed "SReal_not_Infinitesimal";
   1.847 +
   1.848 +(* [| y : SReal; 0 < y; y : Infinitesimal |] ==> R *)
   1.849 +bind_thm("SReal_not_InfinitesimalE", (SReal_not_Infinitesimal RS notE));
   1.850 +
   1.851 +Goal "!!y. [| y : SReal; y < 0 |] ==> y ~:Infinitesimal";
   1.852 +by (blast_tac (claset() addDs [(hypreal_minus_zero_less_iff RS iffD2),
   1.853 +    SReal_minus,(Infinitesimal_minus_iff RS iffD1),SReal_not_Infinitesimal]) 1);
   1.854 +qed "SReal_minus_not_Infinitesimal";
   1.855 +
   1.856 +(* [| y : SReal; y < 0; y : Infinitesimal |] ==> R *)
   1.857 +bind_thm("SReal_minus_not_InfinitesimalE", (SReal_minus_not_Infinitesimal RS notE));
   1.858 +
   1.859 +Goal "SReal Int Infinitesimal = {0}";
   1.860 +by (auto_tac (claset(),simpset() addsimps [SReal_zero]));
   1.861 +by (cut_inst_tac [("x","x"),("y","0")] hypreal_linear 1);
   1.862 +by (blast_tac (claset() addIs [SReal_not_InfinitesimalE,
   1.863 +    SReal_minus_not_InfinitesimalE]) 1);
   1.864 +qed "SReal_Int_Infinitesimal_zero";
   1.865 +
   1.866 +Goal "0 : (SReal Int Infinitesimal)";
   1.867 +by (simp_tac (simpset() addsimps [SReal_zero]) 1);
   1.868 +qed "zero_mem_SReal_Int_Infinitesimal";
   1.869 +
   1.870 +Goal "!!x. [| x: SReal; x: Infinitesimal|] ==> x = 0";
   1.871 +by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
   1.872 +by (blast_tac (claset() addEs [equalityE]) 1);
   1.873 +qed "SReal_Infinitesimal_zero";
   1.874 +
   1.875 +Goal "!!x. [| x : SReal; x ~= 0 |] \
   1.876 +\              ==> x : HFinite - Infinitesimal";
   1.877 +by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
   1.878 +          SReal_subset_HFinite RS subsetD],simpset()));
   1.879 +qed "SReal_HFinite_diff_Infinitesimal";
   1.880 +
   1.881 +Goal "!!x. hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
   1.882 +by (rtac SReal_HFinite_diff_Infinitesimal 1);
   1.883 +by (Auto_tac);
   1.884 +qed "hypreal_of_real_HFinite_diff_Infinitesimal";
   1.885 +
   1.886 +Goal "1hr+1hr ~: Infinitesimal";
   1.887 +by (fast_tac (claset() addIs [SReal_two RS SReal_Infinitesimal_zero,
   1.888 +    hypreal_two_not_zero RS notE]) 1);
   1.889 +qed "two_not_Infinitesimal";
   1.890 +
   1.891 +Goal "1hr ~: Infinitesimal";
   1.892 +by (auto_tac (claset() addSDs [SReal_one RS SReal_Infinitesimal_zero],
   1.893 +    simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
   1.894 +qed "hypreal_one_not_Infinitesimal";
   1.895 +Addsimps [hypreal_one_not_Infinitesimal];
   1.896 +
   1.897 +Goal "!!x. [| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
   1.898 +by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
   1.899 +by (blast_tac (claset() addDs 
   1.900 +    [inf_close_sym RS (mem_infmal_iff RS iffD2),
   1.901 +     SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
   1.902 +qed "inf_close_SReal_not_zero";
   1.903 +
   1.904 +Goal "!!x. [| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
   1.905 +by (rtac inf_close_SReal_not_zero 1);
   1.906 +by (Auto_tac);
   1.907 +qed "inf_close_hypreal_of_real_not_zero";
   1.908 +
   1.909 +Goal "!!x. [| x @= y; y : HFinite - Infinitesimal |] \
   1.910 +\                  ==> x : HFinite - Infinitesimal";
   1.911 +by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
   1.912 +    simpset() addsimps [mem_infmal_iff]));
   1.913 +by (dtac inf_close_trans3 1 THEN assume_tac 1);
   1.914 +by (blast_tac (claset() addDs [inf_close_sym]) 1);
   1.915 +qed "HFinite_diff_Infinitesimal_inf_close";
   1.916 +
   1.917 +Goal "!!x. [| y ~= 0; y: Infinitesimal; \
   1.918 +\                 x*hrinv(y) : HFinite \
   1.919 +\              |] ==> x : Infinitesimal";
   1.920 +by (dtac Infinitesimal_HFinite_mult2 1);
   1.921 +by (assume_tac 1);
   1.922 +by (asm_full_simp_tac (simpset() 
   1.923 +    addsimps [hypreal_mult_assoc]) 1);
   1.924 +qed "Infinitesimal_ratio";
   1.925 +
   1.926 +(*------------------------------------------------------------------
   1.927 +       Standard Part Theorem: Every finite x: R* is infinitely 
   1.928 +       close to a unique real number (i.e a member of SReal)
   1.929 + ------------------------------------------------------------------*)
   1.930 +(*------------------------------------------------------------------
   1.931 +         Uniqueness: Two infinitely close reals are equal
   1.932 + ------------------------------------------------------------------*)
   1.933 +
   1.934 +Goal "!!x. [|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
   1.935 +by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
   1.936 +by (rewrite_goals_tac [inf_close_def]);
   1.937 +by (dres_inst_tac [("x","y")] SReal_minus 1);
   1.938 +by (dtac SReal_add 1 THEN assume_tac 1);
   1.939 +by (dtac SReal_Infinitesimal_zero 1 THEN assume_tac 1);
   1.940 +by (dtac sym 1);
   1.941 +by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff RS sym]) 1);
   1.942 +qed "SReal_inf_close_iff";
   1.943 +
   1.944 +Goal "(hypreal_of_real k @= hypreal_of_real m) = (k = m)";
   1.945 +by (auto_tac (claset(),simpset() addsimps [inf_close_refl,
   1.946 +    SReal_inf_close_iff,inj_hypreal_of_real RS injD]));
   1.947 +qed "hypreal_of_real_inf_close_iff";
   1.948 + 
   1.949 +Addsimps [hypreal_of_real_inf_close_iff];
   1.950 +
   1.951 +Goal "!!r. [| r: SReal; s: SReal; r @= x; s @= x|] ==> r = s";
   1.952 +by (blast_tac (claset() addIs [(SReal_inf_close_iff RS iffD1),
   1.953 +               inf_close_trans2]) 1);
   1.954 +qed "inf_close_unique_real";
   1.955 +
   1.956 +(*------------------------------------------------------------------
   1.957 +       Existence of unique real infinitely close
   1.958 + ------------------------------------------------------------------*)
   1.959 +(* lemma about lubs *)
   1.960 +Goal "!!(x::hypreal). [| isLub R S x; isLub R S y |] ==> x = y";
   1.961 +by (forward_tac [isLub_isUb] 1);
   1.962 +by (forw_inst_tac [("x","y")] isLub_isUb 1);
   1.963 +by (blast_tac (claset() addSIs [hypreal_le_anti_sym]
   1.964 +                addSDs [isLub_le_isUb]) 1);
   1.965 +qed "hypreal_isLub_unique";
   1.966 +
   1.967 +Goal "!!x. x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
   1.968 +by (dtac HFiniteD 1 THEN Step_tac 1);
   1.969 +by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
   1.970 +by (auto_tac (claset() addIs [hypreal_less_imp_le,setleI,isUbI,
   1.971 +    hypreal_less_trans],simpset() addsimps [hrabs_interval_iff]));
   1.972 +qed "lemma_st_part_ub";
   1.973 +
   1.974 +Goal "!!x. x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
   1.975 +by (dtac HFiniteD 1 THEN Step_tac 1);
   1.976 +by (dtac SReal_minus 1);
   1.977 +by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
   1.978 +qed "lemma_st_part_nonempty";
   1.979 +
   1.980 +Goal "{s. s: SReal & s < x} <= SReal";
   1.981 +by (Auto_tac);
   1.982 +qed "lemma_st_part_subset";
   1.983 +
   1.984 +Goal "!!x. x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
   1.985 +by (blast_tac (claset() addSIs [SReal_complete,lemma_st_part_ub,
   1.986 +    lemma_st_part_nonempty, lemma_st_part_subset]) 1);
   1.987 +qed "lemma_st_part_lub";
   1.988 +
   1.989 +Goal "((t::hypreal) + r <= t) = (r <= 0)";
   1.990 +by (Step_tac 1);
   1.991 +by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
   1.992 +by (dres_inst_tac [("x","t")] hypreal_add_left_le_mono1 2);
   1.993 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
   1.994 +qed "lemma_hypreal_le_left_cancel";
   1.995 +
   1.996 +Goal "!!x. [| x: HFinite; \
   1.997 +\                 isLub SReal {s. s: SReal & s < x} t; \
   1.998 +\                 r: SReal; 0 < r \
   1.999 +\              |] ==> x <= t + r";
  1.1000 +by (forward_tac [isLubD1a] 1);
  1.1001 +by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
  1.1002 +by (dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1);
  1.1003 +by (dres_inst_tac [("y","t + r")] (isLubD1 RS setleD) 1);
  1.1004 +by (auto_tac (claset(),simpset() addsimps [lemma_hypreal_le_left_cancel]));
  1.1005 +by (dtac hypreal_less_le_trans 1 THEN assume_tac 1);
  1.1006 +by (asm_full_simp_tac (simpset() addsimps [hypreal_less_not_refl]) 1);
  1.1007 +qed "lemma_st_part_le1";
  1.1008 +
  1.1009 +Goalw [setle_def] "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y";
  1.1010 +by (auto_tac (claset() addSDs [bspec,hypreal_le_less_trans]
  1.1011 +    addIs [hypreal_less_imp_le],simpset()));
  1.1012 +qed "hypreal_setle_less_trans";
  1.1013 +
  1.1014 +Goalw [isUb_def] 
  1.1015 +     "!!x::hypreal. [| isUb R S x; x < y; y: R |] ==> isUb R S y";
  1.1016 +by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
  1.1017 +qed "hypreal_gt_isUb";
  1.1018 +
  1.1019 +Goal "!!x. [| x: HFinite; x < y; y: SReal |] \
  1.1020 +\              ==> isUb SReal {s. s: SReal & s < x} y";
  1.1021 +by (auto_tac (claset() addDs [hypreal_less_trans]
  1.1022 +    addIs [hypreal_less_imp_le] addSIs [isUbI,setleI],simpset()));
  1.1023 +qed "lemma_st_part_gt_ub";
  1.1024 +
  1.1025 +Goal "!!t. t <= t + -r ==> r <= (0::hypreal)";
  1.1026 +by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
  1.1027 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
  1.1028 +by (dres_inst_tac [("x","r")] hypreal_add_left_le_mono1 1);
  1.1029 +by (Auto_tac);
  1.1030 +qed "lemma_minus_le_zero";
  1.1031 +
  1.1032 +Goal "[| x: HFinite; \
  1.1033 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1034 +\        r: SReal; 0 < r |] \
  1.1035 +\     ==> t + -r <= x";
  1.1036 +by (forward_tac [isLubD1a] 1);
  1.1037 +by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
  1.1038 +by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")] 
  1.1039 +    SReal_add 1 THEN assume_tac 1);
  1.1040 +by (dtac lemma_st_part_gt_ub 1 THEN REPEAT(assume_tac 1));
  1.1041 +by (dtac isLub_le_isUb 1 THEN assume_tac 1);
  1.1042 +by (dtac lemma_minus_le_zero 1);
  1.1043 +by (auto_tac (claset() addDs [hypreal_less_le_trans],
  1.1044 +    simpset() addsimps [hypreal_less_not_refl]));
  1.1045 +qed "lemma_st_part_le2";
  1.1046 +
  1.1047 +Goal "((x::hypreal) <= t + r) = (x + -t <= r)";
  1.1048 +by (Step_tac 1);
  1.1049 +by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
  1.1050 +by (dres_inst_tac [("x","t")] hypreal_add_le_mono1 2);
  1.1051 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1.1052 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 2);
  1.1053 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_commute]));
  1.1054 +qed "lemma_hypreal_le_swap";
  1.1055 +
  1.1056 +Goal "[| x: HFinite; \
  1.1057 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1058 +\        r: SReal; 0 < r |] \
  1.1059 +\     ==> x + -t <= r";
  1.1060 +by (blast_tac (claset() addSIs [lemma_hypreal_le_swap RS iffD1,
  1.1061 +                lemma_st_part_le1]) 1);
  1.1062 +qed "lemma_st_part1a";
  1.1063 +
  1.1064 +Goal "(t + -r <= x) = (-(x + -t) <= (r::hypreal))";
  1.1065 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
  1.1066 +    hypreal_add_commute,lemma_hypreal_le_swap  RS sym]));
  1.1067 +qed "lemma_hypreal_le_swap2";
  1.1068 +
  1.1069 +Goal "[| x: HFinite; \
  1.1070 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1071 +\        r: SReal; 0 < r |] \
  1.1072 +\     ==> -(x + -t) <= r";
  1.1073 +by (blast_tac (claset() addSIs [lemma_hypreal_le_swap2 RS iffD1,
  1.1074 +                lemma_st_part_le2]) 1);
  1.1075 +qed "lemma_st_part2a";
  1.1076 +
  1.1077 +Goal "x: SReal ==> isUb SReal {s. s: SReal & s < x} x";
  1.1078 +by (auto_tac (claset() addIs [isUbI, setleI,hypreal_less_imp_le],simpset()));
  1.1079 +qed "lemma_SReal_ub";
  1.1080 +
  1.1081 +Goal "x: SReal ==> isLub SReal {s. s: SReal & s < x} x";
  1.1082 +by (auto_tac (claset() addSIs [isLubI2,lemma_SReal_ub,setgeI],simpset()));
  1.1083 +by (forward_tac [isUbD2a] 1);
  1.1084 +by (res_inst_tac [("x","x"),("y","y")] hypreal_linear_less2 1);
  1.1085 +by (auto_tac (claset() addSIs [hypreal_less_imp_le,hypreal_le_refl],simpset()));
  1.1086 +by (EVERY1[dtac SReal_dense, assume_tac, assume_tac, Step_tac]);
  1.1087 +by (dres_inst_tac [("y","r")] isUbD 1);
  1.1088 +by (auto_tac (claset() addDs [hypreal_less_le_trans],
  1.1089 +    simpset() addsimps [hypreal_less_not_refl]));
  1.1090 +qed "lemma_SReal_lub";
  1.1091 +
  1.1092 +Goal "[| x: HFinite; \
  1.1093 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1094 +\        r: SReal; 0 < r |] \
  1.1095 +\     ==> x + -t ~= r";
  1.1096 +by (Auto_tac);
  1.1097 +by (forward_tac [isLubD1a RS SReal_minus] 1);
  1.1098 +by (dtac SReal_add_cancel 1 THEN assume_tac 1);
  1.1099 +by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
  1.1100 +by (dtac hypreal_isLub_unique 1 THEN assume_tac 1);
  1.1101 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
  1.1102 +qed "lemma_st_part_not_eq1";
  1.1103 +
  1.1104 +Goal "[| x: HFinite; \
  1.1105 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1106 +\        r: SReal; 0 < r |] \
  1.1107 +\     ==> -(x + -t) ~= r";
  1.1108 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib]));
  1.1109 +by (forward_tac [isLubD1a] 1);
  1.1110 +by (dtac SReal_add_cancel 1 THEN assume_tac 1);
  1.1111 +by (dres_inst_tac [("x","-x")] SReal_minus 1);
  1.1112 +by (Asm_full_simp_tac 1);
  1.1113 +by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
  1.1114 +by (dtac hypreal_isLub_unique 1 THEN assume_tac 1);
  1.1115 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
  1.1116 +qed "lemma_st_part_not_eq2";
  1.1117 +
  1.1118 +Goal "[| x: HFinite; \
  1.1119 +\        isLub SReal {s. s: SReal & s < x} t; \
  1.1120 +\        r: SReal; 0 < r |] \
  1.1121 +\     ==> abs (x + -t) < r";
  1.1122 +by (forward_tac [lemma_st_part1a] 1);
  1.1123 +by (forward_tac [lemma_st_part2a] 4);
  1.1124 +by (Auto_tac);
  1.1125 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1.1126 +by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
  1.1127 +    lemma_st_part_not_eq2],simpset() addsimps [hrabs_interval_iff2]));
  1.1128 +qed "lemma_st_part_major";
  1.1129 +
  1.1130 +Goal "[| x: HFinite; \
  1.1131 +\        isLub SReal {s. s: SReal & s < x} t |] \
  1.1132 +\     ==> ALL r: SReal. 0 < r --> abs (x + -t) < r";
  1.1133 +by (blast_tac (claset() addSDs [lemma_st_part_major]) 1);
  1.1134 +qed "lemma_st_part_major2";
  1.1135 +
  1.1136 +(*----------------------------------------------
  1.1137 +  Existence of real and Standard Part Theorem
  1.1138 + ----------------------------------------------*)
  1.1139 +Goal "x: HFinite ==> \
  1.1140 +\     EX t: SReal. ALL r: SReal. 0 < r --> abs (x + -t) < r";
  1.1141 +by (forward_tac [lemma_st_part_lub] 1 THEN Step_tac 1);
  1.1142 +by (forward_tac [isLubD1a] 1);
  1.1143 +by (blast_tac (claset() addDs [lemma_st_part_major2]) 1);
  1.1144 +qed "lemma_st_part_Ex";
  1.1145 +
  1.1146 +Goalw [inf_close_def,Infinitesimal_def] 
  1.1147 +          "x:HFinite ==> EX t: SReal. x @= t";
  1.1148 +by (blast_tac (claset() addSDs [lemma_st_part_Ex]) 1);
  1.1149 +qed "st_part_Ex";
  1.1150 +
  1.1151 +(*--------------------------------
  1.1152 +  Unique real infinitely close
  1.1153 + -------------------------------*)
  1.1154 +Goal "x:HFinite ==> EX! t. t: SReal & x @= t";
  1.1155 +by (dtac st_part_Ex 1 THEN Step_tac 1);
  1.1156 +by (dtac inf_close_sym 2 THEN dtac inf_close_sym 2 
  1.1157 +    THEN dtac inf_close_sym 2);
  1.1158 +by (auto_tac (claset() addSIs [inf_close_unique_real],simpset()));
  1.1159 +qed "st_part_Ex1";
  1.1160 +
  1.1161 +(*------------------------------------------------------------------
  1.1162 +       Finite and Infinite --- more theorems
  1.1163 + ------------------------------------------------------------------*)
  1.1164 +
  1.1165 +Goalw [HFinite_def,HInfinite_def] "HFinite Int HInfinite = {}";
  1.1166 +by (auto_tac (claset() addIs [hypreal_less_irrefl] 
  1.1167 +              addDs [hypreal_less_trans,bspec],
  1.1168 +              simpset()));
  1.1169 +qed "HFinite_Int_HInfinite_empty";
  1.1170 +Addsimps [HFinite_Int_HInfinite_empty];
  1.1171 +
  1.1172 +Goal "x: HFinite ==> x ~: HInfinite";
  1.1173 +by (EVERY1[Step_tac, dtac IntI, assume_tac]);
  1.1174 +by (Auto_tac);
  1.1175 +qed "HFinite_not_HInfinite";
  1.1176 +
  1.1177 +val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite";
  1.1178 +by (cut_facts_tac [prem] 1);
  1.1179 +by (Clarify_tac 1);
  1.1180 +by (auto_tac (claset() addSDs [spec],simpset() addsimps [HFinite_def,Bex_def]));
  1.1181 +by (dtac (hypreal_leI RS hypreal_le_imp_less_or_eq) 1);
  1.1182 +by (auto_tac (claset() addSDs [(SReal_subset_HFinite RS subsetD)],
  1.1183 +    simpset() addsimps [prem,hrabs_idempotent,prem RS not_HFinite_hrabs]));
  1.1184 +qed "not_HFinite_HInfinite";
  1.1185 +
  1.1186 +Goal "x : HInfinite | x : HFinite";
  1.1187 +by (blast_tac (claset() addIs [not_HFinite_HInfinite]) 1);
  1.1188 +qed "HInfinite_HFinite_disj";
  1.1189 +
  1.1190 +Goal "(x : HInfinite) = (x ~: HFinite)";
  1.1191 +by (blast_tac (claset() addDs [HFinite_not_HInfinite,
  1.1192 +               not_HFinite_HInfinite]) 1);
  1.1193 +qed "HInfinite_HFinite_iff";
  1.1194 +
  1.1195 +Goal "(x : HFinite) = (x ~: HInfinite)";
  1.1196 +by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
  1.1197 +qed "HFinite_HInfinite_iff";
  1.1198 +
  1.1199 +(*------------------------------------------------------------------
  1.1200 +       Finite, Infinite and Infinitesimal --- more theorems
  1.1201 + ------------------------------------------------------------------*)
  1.1202 +
  1.1203 +Goal "x ~: Infinitesimal ==> x : HInfinite | x : HFinite - Infinitesimal";
  1.1204 +by (fast_tac (claset() addIs [not_HFinite_HInfinite]) 1);
  1.1205 +qed "HInfinite_diff_HFinite_Infinitesimal_disj";
  1.1206 +
  1.1207 +Goal "[| x : HFinite; x ~: Infinitesimal |] ==> hrinv x : HFinite";
  1.1208 +by (cut_inst_tac [("x","hrinv x")] HInfinite_HFinite_disj 1);
  1.1209 +by (forward_tac [not_Infinitesimal_not_zero RS hypreal_hrinv_hrinv] 1);
  1.1210 +by (auto_tac (claset() addSDs [HInfinite_hrinv_Infinitesimal],simpset()));
  1.1211 +qed "HFinite_hrinv";
  1.1212 +
  1.1213 +Goal "x : HFinite - Infinitesimal ==> hrinv x : HFinite";
  1.1214 +by (blast_tac (claset() addIs [HFinite_hrinv]) 1);
  1.1215 +qed "HFinite_hrinv2";
  1.1216 +
  1.1217 +(* stronger statement possible in fact *)
  1.1218 +Goal "x ~: Infinitesimal ==> hrinv(x) : HFinite";
  1.1219 +by (dtac HInfinite_diff_HFinite_Infinitesimal_disj 1);
  1.1220 +by (blast_tac (claset() addIs [HFinite_hrinv,
  1.1221 +    HInfinite_hrinv_Infinitesimal,
  1.1222 +    Infinitesimal_subset_HFinite RS subsetD]) 1);
  1.1223 +qed "Infinitesimal_hrinv_HFinite";
  1.1224 +
  1.1225 +Goal "x : HFinite - Infinitesimal ==> hrinv x : HFinite - Infinitesimal";
  1.1226 +by (auto_tac (claset() addIs [Infinitesimal_hrinv_HFinite],simpset()));
  1.1227 +by (dtac Infinitesimal_HFinite_mult2 1);
  1.1228 +by (auto_tac (claset() addSDs [not_Infinitesimal_not_zero,
  1.1229 +    hypreal_mult_hrinv],simpset()));
  1.1230 +qed "HFinite_not_Infinitesimal_hrinv";
  1.1231 +
  1.1232 +Goal "[| x @= y; y :  HFinite - Infinitesimal |] \
  1.1233 +\     ==> hrinv x @= hrinv y";
  1.1234 +by (forward_tac [HFinite_diff_Infinitesimal_inf_close] 1);
  1.1235 +by (assume_tac 1);
  1.1236 +by (forward_tac [not_Infinitesimal_not_zero2] 1);
  1.1237 +by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
  1.1238 +by (REPEAT(dtac HFinite_hrinv2 1));
  1.1239 +by (dtac inf_close_mult2 1 THEN assume_tac 1);
  1.1240 +by (Auto_tac);
  1.1241 +by (dres_inst_tac [("c","hrinv x")] inf_close_mult1 1 
  1.1242 +    THEN assume_tac 1);
  1.1243 +by (auto_tac (claset() addIs [inf_close_sym],
  1.1244 +    simpset() addsimps [hypreal_mult_assoc]));
  1.1245 +qed "inf_close_hrinv";
  1.1246 +
  1.1247 +Goal "!!x. [| x: HFinite - Infinitesimal; \
  1.1248 +\                     h : Infinitesimal |] ==> hrinv(x + h) @= hrinv x";
  1.1249 +by (auto_tac (claset() addIs [inf_close_hrinv,
  1.1250 +    Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
  1.1251 +qed "hrinv_add_Infinitesimal_inf_close";
  1.1252 +
  1.1253 +Goal "!!x. [| x: HFinite - Infinitesimal; \
  1.1254 +\                     h : Infinitesimal |] ==> hrinv(h + x) @= hrinv x";
  1.1255 +by (rtac (hypreal_add_commute RS subst) 1);
  1.1256 +by (blast_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close]) 1);
  1.1257 +qed "hrinv_add_Infinitesimal_inf_close2";
  1.1258 +
  1.1259 +Goal 
  1.1260 +     "!!x. [| x: HFinite - Infinitesimal; \
  1.1261 +\             h : Infinitesimal |] ==> hrinv(x + h) + -hrinv x @= h"; 
  1.1262 +by (rtac inf_close_trans2 1);
  1.1263 +by (auto_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close,
  1.1264 +    inf_close_minus_iff RS iffD1],simpset() addsimps [mem_infmal_iff RS sym]));
  1.1265 +qed "hrinv_add_Infinitesimal_inf_close_Infinitesimal";
  1.1266 +
  1.1267 +Goal "(x : Infinitesimal) = (x*x : Infinitesimal)";
  1.1268 +by (auto_tac (claset() addIs [Infinitesimal_mult],simpset()));
  1.1269 +by (rtac ccontr 1 THEN forward_tac [Infinitesimal_hrinv_HFinite] 1);
  1.1270 +by (forward_tac [not_Infinitesimal_not_zero] 1);
  1.1271 +by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
  1.1272 +    simpset() addsimps [hypreal_mult_assoc]));
  1.1273 +qed "Infinitesimal_square_iff";
  1.1274 +Addsimps [Infinitesimal_square_iff RS sym];
  1.1275 +
  1.1276 +Goal "(x*x : HFinite) = (x : HFinite)";
  1.1277 +by (auto_tac (claset() addIs [HFinite_mult],simpset()));
  1.1278 +by (auto_tac (claset() addDs [HInfinite_mult],
  1.1279 +    simpset() addsimps [HFinite_HInfinite_iff]));
  1.1280 +qed "HFinite_square_iff";
  1.1281 +Addsimps [HFinite_square_iff];
  1.1282 +
  1.1283 +Goal "(x*x : HInfinite) = (x : HInfinite)";
  1.1284 +by (auto_tac (claset(),simpset() addsimps 
  1.1285 +    [HInfinite_HFinite_iff]));
  1.1286 +qed "HInfinite_square_iff";
  1.1287 +Addsimps [HInfinite_square_iff];
  1.1288 +
  1.1289 +Goal "!!a. [| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z";
  1.1290 +by (Step_tac 1);
  1.1291 +by (ftac HFinite_hrinv 1 THEN assume_tac 1);
  1.1292 +by (dtac not_Infinitesimal_not_zero 1);
  1.1293 +by (auto_tac (claset() addDs [inf_close_mult2],
  1.1294 +    simpset() addsimps [hypreal_mult_assoc RS sym]));
  1.1295 +qed "inf_close_HFinite_mult_cancel";
  1.1296 +
  1.1297 +Goal "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)";
  1.1298 +by (auto_tac (claset() addIs [inf_close_mult2,
  1.1299 +    inf_close_HFinite_mult_cancel],simpset()));
  1.1300 +qed "inf_close_HFinite_mult_cancel_iff1";
  1.1301 +
  1.1302 +(*------------------------------------------------------------------
  1.1303 +                  more about absolute value (hrabs)
  1.1304 + ------------------------------------------------------------------*)
  1.1305 +
  1.1306 +Goal "abs x @= x | abs x @= -x";
  1.1307 +by (cut_inst_tac [("x","x")] hrabs_disj 1);
  1.1308 +by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
  1.1309 +qed "inf_close_hrabs_disj";
  1.1310 +
  1.1311 +(*------------------------------------------------------------------
  1.1312 +                  Theorems about monads
  1.1313 + ------------------------------------------------------------------*)
  1.1314 +
  1.1315 +Goal "monad (abs x) <= monad(x) Un monad(-x)";
  1.1316 +by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
  1.1317 +by (Auto_tac);
  1.1318 +qed "monad_hrabs_Un_subset";
  1.1319 +
  1.1320 +Goal "!! e. e : Infinitesimal ==> monad (x+e) = monad x";
  1.1321 +by (fast_tac (claset() addSIs [Infinitesimal_add_inf_close_self RS inf_close_sym,
  1.1322 +    inf_close_monad_iff RS iffD1]) 1);
  1.1323 +qed "Infinitesimal_monad_eq";
  1.1324 +
  1.1325 +Goalw [monad_def] "(u:monad x) = (-u:monad (-x))";
  1.1326 +by (Auto_tac);
  1.1327 +qed "mem_monad_iff";
  1.1328 +
  1.1329 +Goalw [monad_def] "(x:Infinitesimal) = (x:monad 0)";
  1.1330 +by (auto_tac (claset() addIs [inf_close_sym],
  1.1331 +    simpset() addsimps [mem_infmal_iff]));
  1.1332 +qed "Infinitesimal_monad_zero_iff";
  1.1333 +
  1.1334 +Goal "(x:monad 0) = (-x:monad 0)";
  1.1335 +by (simp_tac (simpset() addsimps [Infinitesimal_monad_zero_iff RS sym,
  1.1336 +    Infinitesimal_minus_iff RS sym]) 1);
  1.1337 +qed "monad_zero_minus_iff";
  1.1338 +
  1.1339 +Goal "(x:monad 0) = (abs x:monad 0)";
  1.1340 +by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
  1.1341 +by (auto_tac (claset(),simpset() addsimps [monad_zero_minus_iff RS sym]));
  1.1342 +qed "monad_zero_hrabs_iff";
  1.1343 +
  1.1344 +Goalw [monad_def] "x:monad x";
  1.1345 +by (simp_tac (simpset() addsimps [inf_close_refl]) 1);
  1.1346 +qed "mem_monad_self";
  1.1347 +Addsimps [mem_monad_self];
  1.1348 +
  1.1349 +(*------------------------------------------------------------------
  1.1350 +         Proof that x @= y ==> abs x @= abs y
  1.1351 + ------------------------------------------------------------------*)
  1.1352 +Goal "x @= y ==> {x,y}<=monad x";
  1.1353 +by (Simp_tac 1);
  1.1354 +by (asm_full_simp_tac (simpset() addsimps 
  1.1355 +    [inf_close_monad_iff]) 1);
  1.1356 +qed "inf_close_subset_monad";
  1.1357 +
  1.1358 +Goal "x @= y ==> {x,y}<=monad y";
  1.1359 +by (dtac inf_close_sym 1);
  1.1360 +by (fast_tac (claset() addDs [inf_close_subset_monad]) 1);
  1.1361 +qed "inf_close_subset_monad2";
  1.1362 +
  1.1363 +Goalw [monad_def] "u:monad x ==> x @= u";
  1.1364 +by (Fast_tac 1);
  1.1365 +qed "mem_monad_inf_close";
  1.1366 +
  1.1367 +Goalw [monad_def] "x @= u ==> u:monad x";
  1.1368 +by (Fast_tac 1);
  1.1369 +qed "inf_close_mem_monad";
  1.1370 +
  1.1371 +Goalw [monad_def] "!!u. x @= u ==> x:monad u";
  1.1372 +by (blast_tac (claset() addSIs [inf_close_sym]) 1);
  1.1373 +qed "inf_close_mem_monad2";
  1.1374 +
  1.1375 +Goal "!! x y. [| x @= y;x:monad 0 |] ==> y:monad 0";
  1.1376 +by (dtac mem_monad_inf_close 1);
  1.1377 +by (fast_tac (claset() addIs [inf_close_mem_monad,inf_close_trans]) 1);
  1.1378 +qed "inf_close_mem_monad_zero";
  1.1379 +
  1.1380 +Goal "!! x y. [| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
  1.1381 +by (fast_tac (claset() addIs [(Infinitesimal_monad_zero_iff RS iffD1), 
  1.1382 +    inf_close_mem_monad_zero,(monad_zero_hrabs_iff RS iffD1),
  1.1383 +    mem_monad_inf_close,inf_close_trans3]) 1);
  1.1384 +qed "Infinitesimal_inf_close_hrabs";
  1.1385 +
  1.1386 +Goal "!! x. [| 0 < x; x ~:Infinitesimal |] \
  1.1387 +\     ==> ALL e: Infinitesimal. e < x";
  1.1388 +by (Step_tac 1 THEN rtac ccontr 1);
  1.1389 +by (auto_tac (claset() addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)] 
  1.1390 +    addSDs [hypreal_leI RS hypreal_le_imp_less_or_eq],simpset()));
  1.1391 +qed "Ball_Infinitesimal_less";
  1.1392 +
  1.1393 +Goal "!! x. [| 0 < x; x ~: Infinitesimal|] \
  1.1394 +\     ==> ALL u: monad x. 0 < u";
  1.1395 +by (Step_tac 1);
  1.1396 +by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
  1.1397 +by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1);
  1.1398 +by (eres_inst_tac [("x","-xa")] (Ball_Infinitesimal_less RS ballE) 1);
  1.1399 +by (dtac (hypreal_less_minus_iff RS iffD1) 2);
  1.1400 +by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
  1.1401 +qed "Ball_mem_monad_gt_zero";
  1.1402 +
  1.1403 +Goal "!! x. [| x < 0; x ~: Infinitesimal|] \
  1.1404 +\     ==> ALL u: monad x. u < 0";
  1.1405 +by (Step_tac 1);
  1.1406 +by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
  1.1407 +by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1);
  1.1408 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1.1409 +by (eres_inst_tac [("x","xa")] (Ball_Infinitesimal_less RS ballE) 1);
  1.1410 +by (dtac (hypreal_less_minus_iff2 RS iffD1) 2);
  1.1411 +by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym] @ hypreal_add_ac));
  1.1412 +qed "Ball_mem_monad_less_zero";
  1.1413 +
  1.1414 +Goal "[|0 < x; x ~: Infinitesimal; x @= y|] ==> 0 < y";
  1.1415 +by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero,
  1.1416 +    inf_close_subset_monad]) 1);
  1.1417 +qed "lemma_inf_close_gt_zero";
  1.1418 +
  1.1419 +Goal "[|x < 0; x ~: Infinitesimal; x @= y|] ==> y < 0";
  1.1420 +by (blast_tac (claset() addDs [Ball_mem_monad_less_zero,
  1.1421 +    inf_close_subset_monad]) 1);
  1.1422 +qed "lemma_inf_close_less_zero";
  1.1423 +
  1.1424 +Goal "[| x @= y; x < 0; x ~: Infinitesimal |] \
  1.1425 +\     ==> abs x @= abs y";
  1.1426 +by (forward_tac [lemma_inf_close_less_zero] 1);
  1.1427 +by (REPEAT(assume_tac 1));
  1.1428 +by (REPEAT(dtac hrabs_minus_eqI2 1));
  1.1429 +by (Auto_tac);
  1.1430 +qed "inf_close_hrabs1";
  1.1431 +
  1.1432 +Goal "[| x @= y; 0 < x; x ~: Infinitesimal |] \
  1.1433 +\     ==> abs x @= abs y";
  1.1434 +by (forward_tac [lemma_inf_close_gt_zero] 1);
  1.1435 +by (REPEAT(assume_tac 1));
  1.1436 +by (REPEAT(dtac hrabs_eqI2 1));
  1.1437 +by (Auto_tac);
  1.1438 +qed "inf_close_hrabs2";
  1.1439 +
  1.1440 +Goal "x @= y ==> abs x @= abs y";
  1.1441 +by (res_inst_tac [("Q","x:Infinitesimal")] (excluded_middle RS disjE) 1);
  1.1442 +by (res_inst_tac [("x1","x"),("y1","0")] (hypreal_linear RS disjE) 1);
  1.1443 +by (auto_tac (claset() addIs [inf_close_hrabs1,inf_close_hrabs2,
  1.1444 +    Infinitesimal_inf_close_hrabs],simpset()));
  1.1445 +qed "inf_close_hrabs";
  1.1446 +
  1.1447 +Goal "abs(x) @= 0 ==> x @= 0";
  1.1448 +by (cut_inst_tac [("x","x")] hrabs_disj 1);
  1.1449 +by (auto_tac (claset() addDs [inf_close_minus],simpset()));
  1.1450 +qed "inf_close_hrabs_zero_cancel";
  1.1451 +
  1.1452 +Goal "e: Infinitesimal ==> abs x @= abs(x+e)";
  1.1453 +by (fast_tac (claset() addIs [inf_close_hrabs,
  1.1454 +       Infinitesimal_add_inf_close_self]) 1);
  1.1455 +qed "inf_close_hrabs_add_Infinitesimal";
  1.1456 +
  1.1457 +Goal "e: Infinitesimal ==> abs x @= abs(x + -e)";
  1.1458 +by (fast_tac (claset() addIs [inf_close_hrabs,
  1.1459 +    Infinitesimal_add_minus_inf_close_self]) 1);
  1.1460 +qed "inf_close_hrabs_add_minus_Infinitesimal";
  1.1461 +
  1.1462 +Goal "[| e: Infinitesimal; e': Infinitesimal; \
  1.1463 +\        abs(x+e) = abs(y+e')|] ==> abs x @= abs y";
  1.1464 +by (dres_inst_tac [("x","x")] inf_close_hrabs_add_Infinitesimal 1);
  1.1465 +by (dres_inst_tac [("x","y")] inf_close_hrabs_add_Infinitesimal 1);
  1.1466 +by (auto_tac (claset() addIs [inf_close_trans2],simpset()));
  1.1467 +qed "hrabs_add_Infinitesimal_cancel";
  1.1468 +
  1.1469 +Goal "[| e: Infinitesimal; e': Infinitesimal; \
  1.1470 +\        abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y";
  1.1471 +by (dres_inst_tac [("x","x")] inf_close_hrabs_add_minus_Infinitesimal 1);
  1.1472 +by (dres_inst_tac [("x","y")] inf_close_hrabs_add_minus_Infinitesimal 1);
  1.1473 +by (auto_tac (claset() addIs [inf_close_trans2],simpset()));
  1.1474 +qed "hrabs_add_minus_Infinitesimal_cancel";
  1.1475 +
  1.1476 +(* interesting slightly counterintuitive theorem: necessary 
  1.1477 +   for proving that an open interval is an NS open set 
  1.1478 +*)
  1.1479 +Goalw [Infinitesimal_def] 
  1.1480 +      "[| xa: Infinitesimal; hypreal_of_real x < hypreal_of_real y |] \
  1.1481 +\      ==> hypreal_of_real x + xa < hypreal_of_real y";
  1.1482 +by (dtac (hypreal_less_minus_iff RS iffD1) 1 THEN Step_tac 1);
  1.1483 +by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1.1484 +by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
  1.1485 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_commute,
  1.1486 +    hypreal_of_real_minus RS sym, hypreal_of_real_add RS sym,
  1.1487 +    hrabs_interval_iff]));
  1.1488 +by (dres_inst_tac [("x1","xa")] (hypreal_less_minus_iff RS iffD1) 1);
  1.1489 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus,
  1.1490 +    hypreal_minus_add_distrib,hypreal_of_real_add] @ hypreal_add_ac));
  1.1491 +qed "Infinitesimal_add_hypreal_of_real_less";
  1.1492 +
  1.1493 +Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
  1.1494 +\     ==> abs (hypreal_of_real r + x) < hypreal_of_real y";
  1.1495 +by (dres_inst_tac [("x","hypreal_of_real r")] 
  1.1496 +    inf_close_hrabs_add_Infinitesimal 1);
  1.1497 +by (dtac (inf_close_sym RS (bex_Infinitesimal_iff2 RS iffD2)) 1);
  1.1498 +by (auto_tac (claset() addSIs [Infinitesimal_add_hypreal_of_real_less],
  1.1499 +        simpset() addsimps [hypreal_of_real_hrabs]));
  1.1500 +qed "Infinitesimal_add_hrabs_hypreal_of_real_less";
  1.1501 +
  1.1502 +Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
  1.1503 +\     ==> abs (x + hypreal_of_real r) < hypreal_of_real y";
  1.1504 +by (rtac (hypreal_add_commute RS subst) 1);
  1.1505 +by (etac Infinitesimal_add_hrabs_hypreal_of_real_less 1);
  1.1506 +by (assume_tac 1);
  1.1507 +qed "Infinitesimal_add_hrabs_hypreal_of_real_less2";
  1.1508 +
  1.1509 +Goalw [hypreal_le_def]
  1.1510 +      "[| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
  1.1511 +\      ==> hypreal_of_real x <= hypreal_of_real y";
  1.1512 +by (EVERY1[rtac notI, rtac swap, assume_tac]);
  1.1513 +by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
  1.1514 +by (auto_tac (claset() addDs [Infinitesimal_minus_iff RS iffD1]
  1.1515 +    addIs [Infinitesimal_add_hypreal_of_real_less],
  1.1516 +    simpset() addsimps [hypreal_add_assoc]));
  1.1517 +qed "Infinitesimal_add_cancel_hypreal_of_real_le";
  1.1518 +
  1.1519 +Goal "!!xa. [| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
  1.1520 +\                   ==> x <= y";
  1.1521 +by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
  1.1522 +               Infinitesimal_add_cancel_hypreal_of_real_le]) 1);
  1.1523 +qed "Infinitesimal_add_cancel_real_le";
  1.1524 +
  1.1525 +Goalw [hypreal_le_def]
  1.1526 +      "!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
  1.1527 +\               hypreal_of_real x + xa <= hypreal_of_real y + ya \
  1.1528 +\            |] ==> hypreal_of_real x <= hypreal_of_real y";
  1.1529 +by (EVERY1[rtac notI, rtac swap, assume_tac]);
  1.1530 +by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
  1.1531 +by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
  1.1532 +by (dtac Infinitesimal_add 1 THEN assume_tac 1);
  1.1533 +by (auto_tac (claset() addIs [Infinitesimal_add_hypreal_of_real_less],
  1.1534 +    simpset() addsimps [hypreal_add_assoc]));
  1.1535 +qed "hypreal_of_real_le_add_Infininitesimal_cancel";
  1.1536 +
  1.1537 +Goal "!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
  1.1538 +\               hypreal_of_real x + xa <= hypreal_of_real y + ya \
  1.1539 +\            |] ==> x <= y";
  1.1540 +by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
  1.1541 +               hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
  1.1542 +qed "hypreal_of_real_le_add_Infininitesimal_cancel2";
  1.1543 +
  1.1544 +Goal "[| hypreal_of_real x < e; e: Infinitesimal |] ==> hypreal_of_real x <= 0";
  1.1545 +by (rtac hypreal_leI 1 THEN Step_tac 1);
  1.1546 +by (dtac Infinitesimal_interval 1);
  1.1547 +by (dtac (SReal_hypreal_of_real RS SReal_Infinitesimal_zero) 4);
  1.1548 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
  1.1549 +qed "hypreal_of_real_less_Infinitesimal_le_zero";
  1.1550 +
  1.1551 +Goal "!!x. [| h: Infinitesimal; x ~= 0 |] \
  1.1552 +\                  ==> hypreal_of_real x + h ~= 0";
  1.1553 +by (res_inst_tac [("t","h")] (hypreal_minus_minus RS subst) 1);
  1.1554 +by (rtac (not_sym RS (hypreal_not_eq_minus_iff RS iffD1)) 1);
  1.1555 +by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
  1.1556 +by (auto_tac (claset() addDs [((hypreal_of_real_not_zero_iff RS iffD2) RS
  1.1557 +          hypreal_of_real_HFinite_diff_Infinitesimal)],simpset()));
  1.1558 +qed "Infinitesimal_add_not_zero";
  1.1559 +
  1.1560 +Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
  1.1561 +by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
  1.1562 +    Infinitesimal_interval2,hypreal_le_square,
  1.1563 +    Infinitesimal_zero]) 1);
  1.1564 +qed "Infinitesimal_square_cancel";
  1.1565 +Addsimps [Infinitesimal_square_cancel];
  1.1566 +
  1.1567 +Goal "x*x + y*y : HFinite ==> x*x : HFinite";
  1.1568 +by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
  1.1569 +    HFinite_bounded,hypreal_le_square,
  1.1570 +    HFinite_zero]) 1);
  1.1571 +qed "HFinite_square_cancel";
  1.1572 +Addsimps [HFinite_square_cancel];
  1.1573 +
  1.1574 +Goal "x*x + y*y : Infinitesimal ==> y*y : Infinitesimal";
  1.1575 +by (rtac Infinitesimal_square_cancel 1);
  1.1576 +by (rtac (hypreal_add_commute RS subst) 1);
  1.1577 +by (Simp_tac 1);
  1.1578 +qed "Infinitesimal_square_cancel2";
  1.1579 +Addsimps [Infinitesimal_square_cancel2];
  1.1580 +
  1.1581 +Goal "x*x + y*y : HFinite ==> y*y : HFinite";
  1.1582 +by (rtac HFinite_square_cancel 1);
  1.1583 +by (rtac (hypreal_add_commute RS subst) 1);
  1.1584 +by (Simp_tac 1);
  1.1585 +qed "HFinite_square_cancel2";
  1.1586 +Addsimps [HFinite_square_cancel2];
  1.1587 +
  1.1588 +Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal";
  1.1589 +by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
  1.1590 +    Infinitesimal_interval2,hypreal_le_square,
  1.1591 +    Infinitesimal_zero]) 1);
  1.1592 +qed "Infinitesimal_sum_square_cancel";
  1.1593 +Addsimps [Infinitesimal_sum_square_cancel];
  1.1594 +
  1.1595 +Goal "x*x + y*y + z*z : HFinite ==> x*x : HFinite";
  1.1596 +by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
  1.1597 +    HFinite_bounded,hypreal_le_square,
  1.1598 +    HFinite_zero]) 1);
  1.1599 +qed "HFinite_sum_square_cancel";
  1.1600 +Addsimps [HFinite_sum_square_cancel];
  1.1601 +
  1.1602 +Goal "y*y + x*x + z*z : Infinitesimal ==> x*x : Infinitesimal";
  1.1603 +by (rtac Infinitesimal_sum_square_cancel 1);
  1.1604 +by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1605 +qed "Infinitesimal_sum_square_cancel2";
  1.1606 +Addsimps [Infinitesimal_sum_square_cancel2];
  1.1607 +
  1.1608 +Goal "y*y + x*x + z*z : HFinite ==> x*x : HFinite";
  1.1609 +by (rtac HFinite_sum_square_cancel 1);
  1.1610 +by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1611 +qed "HFinite_sum_square_cancel2";
  1.1612 +Addsimps [HFinite_sum_square_cancel2];
  1.1613 +
  1.1614 +Goal "z*z + y*y + x*x : Infinitesimal ==> x*x : Infinitesimal";
  1.1615 +by (rtac Infinitesimal_sum_square_cancel 1);
  1.1616 +by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1617 +qed "Infinitesimal_sum_square_cancel3";
  1.1618 +Addsimps [Infinitesimal_sum_square_cancel3];
  1.1619 +
  1.1620 +Goal "z*z + y*y + x*x : HFinite ==> x*x : HFinite";
  1.1621 +by (rtac HFinite_sum_square_cancel 1);
  1.1622 +by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1623 +qed "HFinite_sum_square_cancel3";
  1.1624 +Addsimps [HFinite_sum_square_cancel3];
  1.1625 +
  1.1626 +Goal "[| y: monad x; 0 < hypreal_of_real e |] \
  1.1627 +\     ==> abs (y + -x) < hypreal_of_real e";
  1.1628 +by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
  1.1629 +by (dtac (bex_Infinitesimal_iff RS iffD2) 1);
  1.1630 +by (auto_tac (claset() addSDs [InfinitesimalD],simpset()));
  1.1631 +qed "monad_hrabs_less";
  1.1632 +
  1.1633 +Goal "x: monad (hypreal_of_real  a) ==> x: HFinite";
  1.1634 +by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
  1.1635 +by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
  1.1636 +by (step_tac (claset() addSDs 
  1.1637 +       [Infinitesimal_subset_HFinite RS subsetD]) 1);
  1.1638 +by (etac (SReal_hypreal_of_real RS (SReal_subset_HFinite 
  1.1639 +         RS subsetD) RS HFinite_add) 1);
  1.1640 +qed "mem_monad_SReal_HFinite";
  1.1641 +
  1.1642 +(*------------------------------------------------------------------
  1.1643 +              Theorems about standard part
  1.1644 + ------------------------------------------------------------------*)
  1.1645 +
  1.1646 +Goalw [st_def] "x: HFinite ==> st x @= x";
  1.1647 +by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
  1.1648 +by (rtac someI2 1);
  1.1649 +by (auto_tac (claset() addIs [inf_close_sym],simpset()));
  1.1650 +qed "st_inf_close_self";
  1.1651 +
  1.1652 +Goalw [st_def] "x: HFinite ==> st x: SReal";
  1.1653 +by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
  1.1654 +by (rtac someI2 1);
  1.1655 +by (auto_tac (claset() addIs [inf_close_sym],simpset()));
  1.1656 +qed "st_SReal";
  1.1657 +
  1.1658 +Goal "x: HFinite ==> st x: HFinite";
  1.1659 +by (etac (st_SReal RS (SReal_subset_HFinite RS subsetD)) 1);
  1.1660 +qed "st_HFinite";
  1.1661 +
  1.1662 +Goalw [st_def] "x: SReal ==> st x = x";
  1.1663 +by (rtac some_equality 1);
  1.1664 +by (fast_tac (claset() addIs [(SReal_subset_HFinite RS subsetD), 
  1.1665 +    inf_close_refl]) 1);
  1.1666 +by (blast_tac (claset() addDs [SReal_inf_close_iff RS iffD1]) 1);
  1.1667 +qed "st_SReal_eq";
  1.1668 +
  1.1669 +(* should be added to simpset *)
  1.1670 +Goal "st (hypreal_of_real x) = hypreal_of_real x";
  1.1671 +by (rtac (SReal_hypreal_of_real RS st_SReal_eq) 1);
  1.1672 +qed "st_hypreal_of_real";
  1.1673 +
  1.1674 +Goal "[| x: HFinite; y: HFinite; st x = st y |] ==> x @= y";
  1.1675 +by (auto_tac (claset() addSDs [st_inf_close_self] 
  1.1676 +              addSEs [inf_close_trans3],simpset()));
  1.1677 +qed "st_eq_inf_close";
  1.1678 +
  1.1679 +Goal "!! x. [| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
  1.1680 +by (EVERY1 [forward_tac [st_inf_close_self],
  1.1681 +    forw_inst_tac [("x","y")] st_inf_close_self,
  1.1682 +    dtac st_SReal,dtac st_SReal]);
  1.1683 +by (fast_tac (claset() addEs [inf_close_trans,
  1.1684 +    inf_close_trans2,SReal_inf_close_iff RS iffD1]) 1);
  1.1685 +qed "inf_close_st_eq";
  1.1686 +
  1.1687 +Goal "!! x y.  [| x: HFinite; y: HFinite|] \
  1.1688 +\                  ==> (x @= y) = (st x = st y)";
  1.1689 +by (blast_tac (claset() addIs [inf_close_st_eq,
  1.1690 +               st_eq_inf_close]) 1);
  1.1691 +qed "st_eq_inf_close_iff";
  1.1692 +
  1.1693 +Goal "!!x. [| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
  1.1694 +by (forward_tac [st_SReal_eq RS subst] 1);
  1.1695 +by (assume_tac 2);
  1.1696 +by (forward_tac [SReal_subset_HFinite RS subsetD] 1);
  1.1697 +by (forward_tac [Infinitesimal_subset_HFinite RS subsetD] 1);
  1.1698 +by (dtac st_SReal_eq 1);
  1.1699 +by (rtac inf_close_st_eq 1);
  1.1700 +by (auto_tac (claset() addIs  [HFinite_add],
  1.1701 +    simpset() addsimps [Infinitesimal_add_inf_close_self 
  1.1702 +    RS inf_close_sym]));
  1.1703 +qed "st_Infinitesimal_add_SReal";
  1.1704 +
  1.1705 +Goal "[| x: SReal; e: Infinitesimal |] \
  1.1706 +\     ==> st(e + x) = x";
  1.1707 +by (rtac (hypreal_add_commute RS subst) 1);
  1.1708 +by (blast_tac (claset() addSIs [st_Infinitesimal_add_SReal]) 1);
  1.1709 +qed "st_Infinitesimal_add_SReal2";
  1.1710 +
  1.1711 +Goal "x: HFinite ==> \
  1.1712 +\     EX e: Infinitesimal. x = st(x) + e";
  1.1713 +by (blast_tac (claset() addSDs [(st_inf_close_self RS 
  1.1714 +    inf_close_sym),bex_Infinitesimal_iff2 RS iffD2]) 1);
  1.1715 +qed "HFinite_st_Infinitesimal_add";
  1.1716 +
  1.1717 +Goal "[| x: HFinite; y: HFinite |] \
  1.1718 +\     ==> st (x + y) = st(x) + st(y)";
  1.1719 +by (forward_tac [HFinite_st_Infinitesimal_add] 1);
  1.1720 +by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
  1.1721 +by (Step_tac 1);
  1.1722 +by (subgoal_tac "st (x + y) = st ((st x + e) + (st y + ea))" 1);
  1.1723 +by (dtac sym 2 THEN dtac sym 2);
  1.1724 +by (Asm_full_simp_tac 2);
  1.1725 +by (asm_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1726 +by (REPEAT(dtac st_SReal 1));
  1.1727 +by (dtac SReal_add 1 THEN assume_tac 1);
  1.1728 +by (dtac Infinitesimal_add 1 THEN assume_tac 1);
  1.1729 +by (rtac (hypreal_add_assoc RS subst) 1);
  1.1730 +by (blast_tac (claset() addSIs [st_Infinitesimal_add_SReal2]) 1);
  1.1731 +qed "st_add";
  1.1732 +
  1.1733 +Goal "st 0 = 0";
  1.1734 +by (rtac (SReal_zero RS st_SReal_eq) 1);
  1.1735 +qed "st_zero";
  1.1736 +
  1.1737 +Goal "st 1hr = 1hr";
  1.1738 +by (rtac (SReal_one RS st_SReal_eq) 1);
  1.1739 +qed "st_one";
  1.1740 +
  1.1741 +Addsimps [st_zero,st_one];
  1.1742 +
  1.1743 +Goal "!!y. y: HFinite ==> st(-y) = -st(y)";
  1.1744 +by (forward_tac [HFinite_minus_iff RS iffD1] 1);
  1.1745 +by (rtac hypreal_add_minus_eq_minus 1);
  1.1746 +by (dtac (st_add RS sym) 1 THEN assume_tac 1);
  1.1747 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1.1748 +qed "st_minus";
  1.1749 +
  1.1750 +Goal "!!x. [| x: HFinite; y: HFinite |] \
  1.1751 +\              ==> st (x + -y) = st(x) + -st(y)";
  1.1752 +by (forw_inst_tac [("y1","y")] (st_minus RS sym) 1);
  1.1753 +by (dres_inst_tac [("x1","y")] (HFinite_minus_iff RS iffD1) 1);
  1.1754 +by (asm_simp_tac (simpset() addsimps [st_add]) 1);
  1.1755 +qed "st_add_minus";
  1.1756 +
  1.1757 +(* lemma *)
  1.1758 +Goal "!!x. [| x: HFinite; y: HFinite; \
  1.1759 +\                 e: Infinitesimal; \
  1.1760 +\                 ea : Infinitesimal \
  1.1761 +\              |] ==> e*y + x*ea + e*ea: Infinitesimal";
  1.1762 +by (forw_inst_tac [("x","e"),("y","y")] Infinitesimal_HFinite_mult 1);
  1.1763 +by (forw_inst_tac [("x","ea"),("y","x")] Infinitesimal_HFinite_mult 2);
  1.1764 +by (dtac Infinitesimal_mult 3);
  1.1765 +by (auto_tac (claset() addIs [Infinitesimal_add],
  1.1766 +    simpset() addsimps hypreal_add_ac @ hypreal_mult_ac));
  1.1767 +qed "lemma_st_mult";
  1.1768 +
  1.1769 +Goal "!!x. [| x: HFinite; y: HFinite |] \
  1.1770 +\              ==> st (x * y) = st(x) * st(y)";
  1.1771 +by (forward_tac [HFinite_st_Infinitesimal_add] 1);
  1.1772 +by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
  1.1773 +by (Step_tac 1);
  1.1774 +by (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))" 1);
  1.1775 +by (dtac sym 2 THEN dtac sym 2);
  1.1776 +by (Asm_full_simp_tac 2);
  1.1777 +by (thin_tac "x = st x + e" 1);
  1.1778 +by (thin_tac "y = st y + ea" 1);
  1.1779 +by (asm_full_simp_tac (simpset() addsimps 
  1.1780 +    [hypreal_add_mult_distrib,hypreal_add_mult_distrib2]) 1);
  1.1781 +by (REPEAT(dtac st_SReal 1));
  1.1782 +by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1.1783 +by (rtac st_Infinitesimal_add_SReal 1);
  1.1784 +by (blast_tac (claset() addSIs [SReal_mult]) 1);
  1.1785 +by (REPEAT(dtac (SReal_subset_HFinite RS subsetD) 1));
  1.1786 +by (rtac (hypreal_add_assoc RS subst) 1);
  1.1787 +by (blast_tac (claset() addSIs [lemma_st_mult]) 1);
  1.1788 +qed "st_mult";
  1.1789 +
  1.1790 +Goal "!! x. st(x) ~= 0 ==> x ~=0";
  1.1791 +by (fast_tac (claset() addIs [st_zero]) 1);
  1.1792 +qed "st_not_zero";
  1.1793 +
  1.1794 +Goal "!!x. x: Infinitesimal ==> st x = 0";
  1.1795 +by (rtac (st_zero RS subst) 1);
  1.1796 +by (rtac inf_close_st_eq 1);
  1.1797 +by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite 
  1.1798 +    RS subsetD],simpset() addsimps [mem_infmal_iff RS sym]));
  1.1799 +qed "st_Infinitesimal";
  1.1800 +
  1.1801 +Goal "!! x. st(x) ~= 0 ==> x ~: Infinitesimal";
  1.1802 +by (fast_tac (claset() addIs [st_Infinitesimal]) 1);
  1.1803 +qed "st_not_Infinitesimal";
  1.1804 +
  1.1805 +val [prem1,prem2] = 
  1.1806 +goal thy "[| x: HFinite; st x ~= 0 |] \
  1.1807 +\         ==> st(hrinv x) = hrinv (st x)";
  1.1808 +by (rtac ((prem2 RS hypreal_mult_left_cancel) RS iffD1) 1);
  1.1809 +by (auto_tac (claset(),simpset() addsimps [st_not_zero,
  1.1810 +    st_mult RS sym,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1]));
  1.1811 +qed "st_hrinv";
  1.1812 +
  1.1813 +val [prem1,prem2,prem3] = 
  1.1814 +goal thy "[| x: HFinite; y: HFinite; st y ~= 0 |] \
  1.1815 +\                 ==> st(x * hrinv y) = (st x) * hrinv (st y)";
  1.1816 +by (auto_tac (claset(),simpset() addsimps [st_not_zero,prem3,
  1.1817 +    st_mult,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1,st_hrinv]));
  1.1818 +qed "st_mult_hrinv";
  1.1819 +
  1.1820 +Goal "!!x. x: HFinite ==> st(st(x)) = st(x)";
  1.1821 +by (blast_tac (claset() addIs [st_HFinite,
  1.1822 +    st_inf_close_self,inf_close_st_eq]) 1);
  1.1823 +qed "st_idempotent";
  1.1824 +
  1.1825 +(*** lemmas ***)
  1.1826 +Goal "[| x: HFinite; y: HFinite; \
  1.1827 +\        xa: Infinitesimal; st x < st y \
  1.1828 +\     |] ==> st x + xa < st y";
  1.1829 +by (REPEAT(dtac st_SReal 1));
  1.1830 +by (auto_tac (claset() addSIs 
  1.1831 +    [Infinitesimal_add_hypreal_of_real_less],
  1.1832 +    simpset() addsimps [SReal_iff]));
  1.1833 +qed "Infinitesimal_add_st_less";
  1.1834 +
  1.1835 +Goalw [hypreal_le_def]
  1.1836 +     "[| x: HFinite; y: HFinite; \
  1.1837 +\        xa: Infinitesimal; st x <= st y + xa\
  1.1838 +\     |] ==> st x <= st y";
  1.1839 +by (auto_tac (claset() addDs [Infinitesimal_add_st_less],
  1.1840 +    simpset()));
  1.1841 +qed "Infinitesimal_add_st_le_cancel";
  1.1842 +
  1.1843 +Goal "[| x: HFinite; y: HFinite; x <= y |] \
  1.1844 +\     ==> st(x) <= st(y)";
  1.1845 +by (forward_tac [HFinite_st_Infinitesimal_add] 1);
  1.1846 +by (rotate_tac 1 1);
  1.1847 +by (forward_tac [HFinite_st_Infinitesimal_add] 1);
  1.1848 +by (Step_tac 1);
  1.1849 +by (rtac Infinitesimal_add_st_le_cancel 1);
  1.1850 +by (res_inst_tac [("x","ea"),("y","e")] 
  1.1851 +             Infinitesimal_add_minus 3);
  1.1852 +by (auto_tac (claset(),simpset() addsimps 
  1.1853 +    [hypreal_add_assoc RS sym]));
  1.1854 +by (res_inst_tac [("C","e")] hypreal_le_add_right_cancel 1);
  1.1855 +by (asm_full_simp_tac (simpset() addsimps 
  1.1856 +    [hypreal_add_assoc]) 1);
  1.1857 +qed "st_le";
  1.1858 +
  1.1859 +Goal "[| x: HFinite; 0 <= x |] ==> 0 <= st x";
  1.1860 +by (rtac (st_zero RS subst) 1);
  1.1861 +by (auto_tac (claset() addIs [st_le],simpset() 
  1.1862 +    delsimps [st_zero]));
  1.1863 +qed "st_zero_le";
  1.1864 +
  1.1865 +Goal "[| x: HFinite; x <= 0 |] ==> st x <= 0";
  1.1866 +by (rtac (st_zero RS subst) 1);
  1.1867 +by (auto_tac (claset() addIs [st_le],simpset() 
  1.1868 +    delsimps [st_zero]));
  1.1869 +qed "st_zero_ge";
  1.1870 +
  1.1871 +Goal "x: HFinite ==> abs(st x) = st(abs x)";
  1.1872 +by (case_tac "0 <= x" 1);
  1.1873 +by (auto_tac (claset() addSDs [not_hypreal_leE,
  1.1874 +    hypreal_less_imp_le],simpset() addsimps 
  1.1875 +    [st_zero_le,hrabs_eqI1, hrabs_minus_eqI1,
  1.1876 +     st_zero_ge,st_minus]));
  1.1877 +qed "st_hrabs";
  1.1878 +
  1.1879 +(*--------------------------------------------------------------------
  1.1880 +   Alternative definitions for HFinite using Free ultrafilter
  1.1881 + --------------------------------------------------------------------*)
  1.1882 +
  1.1883 +Goal "!!x. [| X: Rep_hypreal x; Y: Rep_hypreal x |] \
  1.1884 +\              ==> {n. X n = Y n} : FreeUltrafilterNat";
  1.1885 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1.1886 +by (Auto_tac);
  1.1887 +by (Ultra_tac 1);
  1.1888 +qed "FreeUltrafilterNat_Rep_hypreal";
  1.1889 +
  1.1890 +Goal "{n. Yb n < Y n} Int {n. -y = Yb n} <= {n. -y < Y n}";
  1.1891 +by (Auto_tac);
  1.1892 +qed "lemma_free1";
  1.1893 +
  1.1894 +Goal "{n. Xa n < Yc n} Int {n. y = Yc n} <= {n. Xa n < y}";
  1.1895 +by (Auto_tac);
  1.1896 +qed "lemma_free2";
  1.1897 +
  1.1898 +Goalw [HFinite_def] 
  1.1899 +    "x : HFinite ==> EX X: Rep_hypreal x. \
  1.1900 +\    EX u. {n. abs (X n) < u}:  FreeUltrafilterNat";
  1.1901 +by (auto_tac (claset(),simpset() addsimps 
  1.1902 +    [hrabs_interval_iff]));
  1.1903 +by (auto_tac (claset(),simpset() addsimps 
  1.1904 +    [hypreal_less_def,SReal_iff,hypreal_minus,
  1.1905 +     hypreal_of_real_def]));
  1.1906 +by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
  1.1907 +by (res_inst_tac [("x","Y")] bexI 1 THEN assume_tac 2);
  1.1908 +by (res_inst_tac [("x","y")] exI 1);
  1.1909 +by (Ultra_tac 1 THEN arith_tac 1);
  1.1910 +qed "HFinite_FreeUltrafilterNat";
  1.1911 +
  1.1912 +Goalw [HFinite_def] 
  1.1913 +     "EX X: Rep_hypreal x. \
  1.1914 +\      EX u. {n. abs (X n) < u}: FreeUltrafilterNat\
  1.1915 +\      ==>  x : HFinite";
  1.1916 +by (auto_tac (claset(),simpset() addsimps 
  1.1917 +    [hrabs_interval_iff]));
  1.1918 +by (res_inst_tac [("x","hypreal_of_real u")] bexI 1);
  1.1919 +by (auto_tac (claset() addSIs [exI],simpset() addsimps 
  1.1920 +    [hypreal_less_def,SReal_iff,hypreal_minus,
  1.1921 +     hypreal_of_real_def]));
  1.1922 +by (ALLGOALS(Ultra_tac THEN' arith_tac));
  1.1923 +qed "FreeUltrafilterNat_HFinite";
  1.1924 +
  1.1925 +Goal "(x : HFinite) = (EX X: Rep_hypreal x. \
  1.1926 +\          EX u. {n. abs (X n) < u}:  FreeUltrafilterNat)";
  1.1927 +by (blast_tac (claset() addSIs [HFinite_FreeUltrafilterNat,
  1.1928 +               FreeUltrafilterNat_HFinite]) 1);
  1.1929 +qed "HFinite_FreeUltrafilterNat_iff";
  1.1930 +
  1.1931 +(*--------------------------------------------------------------------
  1.1932 +   Alternative definitions for HInfinite using Free ultrafilter
  1.1933 + --------------------------------------------------------------------*)
  1.1934 +Goal "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) <= u}";
  1.1935 +by Auto_tac;
  1.1936 +qed "lemma_Compl_eq";
  1.1937 +
  1.1938 +Goal "- {n. abs (xa n) < (u::real)} = {n. u <= abs (xa n)}";
  1.1939 +by Auto_tac;
  1.1940 +qed "lemma_Compl_eq2";
  1.1941 +
  1.1942 +Goal "{n. abs (xa n) <= (u::real)} Int {n. u <= abs (xa n)} \
  1.1943 +\         = {n. abs(xa n) = u}";
  1.1944 +by Auto_tac;
  1.1945 +qed "lemma_Int_eq1";
  1.1946 +
  1.1947 +Goal "{n. abs (xa n) = u} <= {n. abs (xa n) < u + (#1::real)}";
  1.1948 +by Auto_tac;
  1.1949 +qed "lemma_FreeUltrafilterNat_one";
  1.1950 +
  1.1951 +(*-------------------------------------
  1.1952 +  Exclude this type of sets from free 
  1.1953 +  ultrafilter for Infinite numbers!
  1.1954 + -------------------------------------*)
  1.1955 +Goal "!!x. [| xa: Rep_hypreal x; \
  1.1956 +\                 {n. abs (xa n) = u} : FreeUltrafilterNat \
  1.1957 +\              |] ==> x: HFinite";
  1.1958 +by (rtac FreeUltrafilterNat_HFinite 1);
  1.1959 +by (res_inst_tac [("x","xa")] bexI 1);
  1.1960 +by (res_inst_tac [("x","u + #1")] exI 1);
  1.1961 +by (Ultra_tac 1 THEN assume_tac 1);
  1.1962 +qed "FreeUltrafilterNat_const_Finite";
  1.1963 +
  1.1964 +val [prem] = goal thy "x : HInfinite ==> EX X: Rep_hypreal x. \
  1.1965 +\          ALL u. {n. u < abs (X n)}:  FreeUltrafilterNat";
  1.1966 +by (cut_facts_tac [(prem RS (HInfinite_HFinite_iff RS iffD1))] 1);
  1.1967 +by (cut_inst_tac [("x","x")] Rep_hypreal_nonempty 1);
  1.1968 +by (auto_tac (claset(),simpset() delsimps [Rep_hypreal_nonempty] 
  1.1969 +    addsimps [HFinite_FreeUltrafilterNat_iff,Bex_def]));
  1.1970 +by (REPEAT(dtac spec 1));
  1.1971 +by (Auto_tac);
  1.1972 +by (dres_inst_tac [("x","u")] spec 1 THEN 
  1.1973 +    REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
  1.1974 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
  1.1975 +
  1.1976 +
  1.1977 +by (asm_full_simp_tac (simpset() addsimps [lemma_Compl_eq,
  1.1978 +    lemma_Compl_eq2,lemma_Int_eq1]) 1);
  1.1979 +by (auto_tac (claset() addDs [FreeUltrafilterNat_const_Finite],
  1.1980 +    simpset() addsimps [(prem RS (HInfinite_HFinite_iff RS iffD1))]));
  1.1981 +qed "HInfinite_FreeUltrafilterNat";
  1.1982 +
  1.1983 +(* yet more lemmas! *)
  1.1984 +Goal "{n. abs (Xa n) < u} Int {n. X n = Xa n} \
  1.1985 +\         <= {n. abs (X n) < (u::real)}";
  1.1986 +by (Auto_tac);
  1.1987 +qed "lemma_Int_HI";
  1.1988 +
  1.1989 +Goal "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}";
  1.1990 +by (auto_tac (claset() addIs [real_less_asym],simpset()));
  1.1991 +qed "lemma_Int_HIa";
  1.1992 +
  1.1993 +Goal "!!x. EX X: Rep_hypreal x. ALL u. \
  1.1994 +\              {n. u < abs (X n)}: FreeUltrafilterNat\
  1.1995 +\              ==>  x : HInfinite";
  1.1996 +by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
  1.1997 +by (Step_tac 1 THEN dtac HFinite_FreeUltrafilterNat 1);
  1.1998 +by (Auto_tac);
  1.1999 +by (dres_inst_tac [("x","u")] spec 1);
  1.2000 +by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
  1.2001 +by (dres_inst_tac [("Y","{n. X n = Xa n}")] FreeUltrafilterNat_Int 1);
  1.2002 +by (dtac (lemma_Int_HI RSN (2,FreeUltrafilterNat_subset)) 2);
  1.2003 +by (dres_inst_tac [("Y","{n. abs (X n) < u}")] FreeUltrafilterNat_Int 2);
  1.2004 +by (auto_tac (claset(),simpset() addsimps [lemma_Int_HIa,
  1.2005 +              FreeUltrafilterNat_empty]));
  1.2006 +qed "FreeUltrafilterNat_HInfinite";
  1.2007 +
  1.2008 +Goal "(x : HInfinite) = (EX X: Rep_hypreal x. \
  1.2009 +\          ALL u. {n. u < abs (X n)}:  FreeUltrafilterNat)";
  1.2010 +by (blast_tac (claset() addSIs [HInfinite_FreeUltrafilterNat,
  1.2011 +               FreeUltrafilterNat_HInfinite]) 1);
  1.2012 +qed "HInfinite_FreeUltrafilterNat_iff";
  1.2013 +
  1.2014 +(*--------------------------------------------------------------------
  1.2015 +   Alternative definitions for Infinitesimal using Free ultrafilter
  1.2016 + --------------------------------------------------------------------*)
  1.2017 +
  1.2018 +Goal "{n. - u < Yd n} Int {n. xa n = Yd n} <= {n. -u < xa n}";
  1.2019 +by (Auto_tac);
  1.2020 +qed "lemma_free4";
  1.2021 +
  1.2022 +Goal "{n. Yb n < u} Int {n. xa n = Yb n} <= {n. xa n < u}";
  1.2023 +by (Auto_tac);
  1.2024 +qed "lemma_free5";
  1.2025 +
  1.2026 +Goalw [Infinitesimal_def] 
  1.2027 +          "!!x. x : Infinitesimal ==> EX X: Rep_hypreal x. \
  1.2028 +\          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat";
  1.2029 +by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
  1.2030 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1.2031 +by (EVERY[Auto_tac, rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
  1.2032 +by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
  1.2033 +by (dres_inst_tac [("x","hypreal_of_real u")] bspec 1);
  1.2034 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
  1.2035 +by (thin_tac "0 < hypreal_of_real  u" 1);
  1.2036 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_def,       
  1.2037 +     hypreal_minus,hypreal_of_real_def,hypreal_of_real_zero]));
  1.2038 +by (Ultra_tac 1 THEN arith_tac 1);
  1.2039 +qed "Infinitesimal_FreeUltrafilterNat";
  1.2040 +
  1.2041 +Goalw [Infinitesimal_def] 
  1.2042 +          "!!x. EX X: Rep_hypreal x. \
  1.2043 +\               ALL u. 0 < u --> \
  1.2044 +\               {n. abs (X n) < u}:  FreeUltrafilterNat \
  1.2045 +\               ==> x : Infinitesimal";
  1.2046 +by (auto_tac (claset(),simpset() addsimps 
  1.2047 +    [hrabs_interval_iff,abs_interval_iff]));
  1.2048 +by (auto_tac (claset(),simpset() addsimps [SReal_iff,
  1.2049 +    hypreal_of_real_zero RS sym]));
  1.2050 +by (auto_tac (claset() addSIs [exI] 
  1.2051 +    addIs [FreeUltrafilterNat_subset],
  1.2052 +    simpset() addsimps [hypreal_less_def,
  1.2053 +    hypreal_minus,hypreal_of_real_def]));
  1.2054 +qed "FreeUltrafilterNat_Infinitesimal";
  1.2055 +
  1.2056 +Goal "(x : Infinitesimal) = (EX X: Rep_hypreal x. \
  1.2057 +\          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat)";
  1.2058 +by (blast_tac (claset() addSIs [Infinitesimal_FreeUltrafilterNat,
  1.2059 +               FreeUltrafilterNat_Infinitesimal]) 1);
  1.2060 +qed "Infinitesimal_FreeUltrafilterNat_iff";
  1.2061 +
  1.2062 +(*------------------------------------------------------------------------
  1.2063 +         Infinitesimals as smaller than 1/n for all n::nat (> 0)
  1.2064 + ------------------------------------------------------------------------*)
  1.2065 +Goal "(ALL r. 0 < r --> x < r) = (ALL n. x < rinv(real_of_posnat n))";
  1.2066 +by (auto_tac (claset(),simpset() addsimps 
  1.2067 +    [rename_numerals (real_of_posnat_gt_zero RS real_rinv_gt_zero)]));
  1.2068 +by (blast_tac (claset() addSDs [rename_numerals reals_Archimedean] 
  1.2069 +    addIs [real_less_trans]) 1);
  1.2070 +qed "lemma_Infinitesimal";
  1.2071 +
  1.2072 +Goal "(ALL r: SReal. 0 < r --> x < r) = \
  1.2073 +\     (ALL n. x < hrinv(hypreal_of_posnat n))";
  1.2074 +by (Step_tac 1);
  1.2075 +by (dres_inst_tac [("x","hypreal_of_real (rinv(real_of_posnat n))")] bspec 1);
  1.2076 +by (Full_simp_tac 1);
  1.2077 +by (rtac (real_of_posnat_gt_zero RS real_rinv_gt_zero RS 
  1.2078 +          (hypreal_of_real_less_iff RS iffD1) RSN(2,impE)) 1);
  1.2079 +by (assume_tac 2);
  1.2080 +by (asm_full_simp_tac (simpset() addsimps 
  1.2081 +   [real_not_refl2 RS not_sym RS hypreal_of_real_hrinv RS sym,
  1.2082 +   rename_numerals real_of_posnat_gt_zero,hypreal_of_real_zero,
  1.2083 +    hypreal_of_real_of_posnat]) 1);
  1.2084 +by (auto_tac (claset() addSDs [reals_Archimedean],
  1.2085 +    simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
  1.2086 +by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
  1.2087 +by (asm_full_simp_tac (simpset() addsimps 
  1.2088 +   [real_not_refl2 RS not_sym RS hypreal_of_real_hrinv RS sym,
  1.2089 +   rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
  1.2090 +by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
  1.2091 +qed "lemma_Infinitesimal2";
  1.2092 +
  1.2093 +Goalw [Infinitesimal_def] 
  1.2094 +      "Infinitesimal = {x. ALL n. abs x < hrinv (hypreal_of_posnat n)}";
  1.2095 +by (auto_tac (claset(),simpset() addsimps [lemma_Infinitesimal2]));
  1.2096 +qed "Infinitesimal_hypreal_of_posnat_iff";
  1.2097 +
  1.2098 +(*-----------------------------------------------------------------------------
  1.2099 +       Actual proof that omega (whr) is an infinite number and 
  1.2100 +       hence that epsilon (ehr) is an infinitesimal number.
  1.2101 + -----------------------------------------------------------------------------*)
  1.2102 +Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}";
  1.2103 +by (auto_tac (claset(),simpset() addsimps [less_Suc_eq]));
  1.2104 +qed "Suc_Un_eq";
  1.2105 +
  1.2106 +(*-------------------------------------------
  1.2107 +  Prove that any segment is finite and 
  1.2108 +  hence cannot belong to FreeUltrafilterNat
  1.2109 + -------------------------------------------*)
  1.2110 +Goal "finite {n::nat. n < m}";
  1.2111 +by (nat_ind_tac "m" 1);
  1.2112 +by (auto_tac (claset(),simpset() addsimps [Suc_Un_eq]));
  1.2113 +qed "finite_nat_segment";
  1.2114 +
  1.2115 +Goal "finite {n::nat. real_of_posnat n < real_of_posnat m}";
  1.2116 +by (auto_tac (claset() addIs [finite_nat_segment],simpset()));
  1.2117 +qed "finite_real_of_posnat_segment";
  1.2118 +
  1.2119 +Goal "finite {n. real_of_posnat n < u}";
  1.2120 +by (cut_inst_tac [("x","u")] reals_Archimedean2 1);
  1.2121 +by (Step_tac 1);
  1.2122 +by (rtac (finite_real_of_posnat_segment RSN (2,finite_subset)) 1);
  1.2123 +by (auto_tac (claset() addDs [real_less_trans],simpset()));
  1.2124 +qed "finite_real_of_posnat_less_real";
  1.2125 +
  1.2126 +Goal "{n. real_of_posnat n <= u} = \
  1.2127 +\     {n. real_of_posnat n < u} Un {n. u = real_of_posnat n}";
  1.2128 +by (auto_tac (claset() addDs [real_le_imp_less_or_eq],
  1.2129 +    simpset() addsimps [real_le_refl,real_less_imp_le]));
  1.2130 +qed "lemma_real_le_Un_eq";
  1.2131 +
  1.2132 +Goal "finite {n. real_of_posnat n <= u}";
  1.2133 +by (auto_tac (claset(),simpset() addsimps 
  1.2134 +    [lemma_real_le_Un_eq,lemma_finite_omega_set,
  1.2135 +     finite_real_of_posnat_less_real]));
  1.2136 +qed "finite_real_of_posnat_le_real";
  1.2137 +
  1.2138 +Goal "finite {n. abs(real_of_posnat n) <= u}";
  1.2139 +by (full_simp_tac (simpset() addsimps [rename_numerals 
  1.2140 +    real_of_posnat_gt_zero,abs_eqI2,
  1.2141 +    finite_real_of_posnat_le_real]) 1);
  1.2142 +qed "finite_rabs_real_of_posnat_le_real";
  1.2143 +
  1.2144 +Goal "{n. abs(real_of_posnat n) <= u} ~: FreeUltrafilterNat";
  1.2145 +by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
  1.2146 +    finite_rabs_real_of_posnat_le_real]) 1);
  1.2147 +qed "rabs_real_of_posnat_le_real_FreeUltrafilterNat";
  1.2148 +
  1.2149 +Goal "{n. u < real_of_posnat n} : FreeUltrafilterNat";
  1.2150 +by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
  1.2151 +by (auto_tac (claset(),simpset() addsimps 
  1.2152 +    [CLAIM_SIMP "- {n. u < real_of_posnat  n} = \
  1.2153 +\                {n. real_of_posnat n <= u}" 
  1.2154 +     [real_le_def],finite_real_of_posnat_le_real 
  1.2155 +                   RS FreeUltrafilterNat_finite]));
  1.2156 +qed "FreeUltrafilterNat_nat_gt_real";
  1.2157 +
  1.2158 +(*--------------------------------------------------------------
  1.2159 + The complement of {n. abs(real_of_posnat n) <= u} = 
  1.2160 + {n. u < abs (real_of_posnat n)} is in FreeUltrafilterNat 
  1.2161 + by property of (free) ultrafilters
  1.2162 + --------------------------------------------------------------*)
  1.2163 +Goal "- {n. abs (real_of_posnat  n) <= u} = \
  1.2164 +\     {n. u < abs (real_of_posnat  n)}";
  1.2165 +by (auto_tac (claset() addSDs [real_le_less_trans],
  1.2166 +   simpset() addsimps [not_real_leE,real_less_not_refl]));
  1.2167 +val lemma = result();
  1.2168 +
  1.2169 +Goal "{n. u < abs (real_of_posnat n)} : FreeUltrafilterNat";
  1.2170 +by (cut_inst_tac [("u","u")] rabs_real_of_posnat_le_real_FreeUltrafilterNat 1);
  1.2171 +by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
  1.2172 +    simpset() addsimps [lemma]));
  1.2173 +qed "FreeUltrafilterNat_omega";
  1.2174 +
  1.2175 +(*-----------------------------------------------
  1.2176 +       Omega is a member of HInfinite
  1.2177 + -----------------------------------------------*)
  1.2178 +Goalw [omega_def] "whr: HInfinite";
  1.2179 +by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite,
  1.2180 +    lemma_hyprel_refl,FreeUltrafilterNat_omega],simpset()));
  1.2181 +qed "HInfinite_omega";
  1.2182 +
  1.2183 +(*-----------------------------------------------
  1.2184 +       Epsilon is a member of Infinitesimal
  1.2185 + -----------------------------------------------*)
  1.2186 +
  1.2187 +Goal "ehr : Infinitesimal";
  1.2188 +by (auto_tac (claset() addSIs [HInfinite_hrinv_Infinitesimal,HInfinite_omega],
  1.2189 +    simpset() addsimps [hypreal_epsilon_hrinv_omega]));
  1.2190 +qed "Infinitesimal_epsilon";
  1.2191 +Addsimps [Infinitesimal_epsilon];
  1.2192 +
  1.2193 +Goal "ehr : HFinite";
  1.2194 +by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
  1.2195 +    simpset()));
  1.2196 +qed "HFinite_epsilon";
  1.2197 +Addsimps [HFinite_epsilon];
  1.2198 +
  1.2199 +Goal "ehr @= 0";
  1.2200 +by (simp_tac (simpset() addsimps [mem_infmal_iff RS sym]) 1);
  1.2201 +qed "epsilon_inf_close_zero";
  1.2202 +Addsimps [epsilon_inf_close_zero];
  1.2203 +
  1.2204 +(*------------------------------------------------------------------------
  1.2205 +  Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given 
  1.2206 +  that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
  1.2207 + -----------------------------------------------------------------------*)
  1.2208 +
  1.2209 +Goal "!!u. 0 < u ==> finite {n. u < rinv(real_of_posnat n)}";
  1.2210 +by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_rinv_iff]) 1);
  1.2211 +by (rtac finite_real_of_posnat_less_real 1);
  1.2212 +qed "finite_rinv_real_of_posnat_gt_real";
  1.2213 +
  1.2214 +Goal "{n. u <= rinv(real_of_posnat n)} = \
  1.2215 +\      {n. u < rinv(real_of_posnat n)} Un {n. u = rinv(real_of_posnat n)}";
  1.2216 +by (auto_tac (claset() addDs [real_le_imp_less_or_eq],
  1.2217 +    simpset() addsimps [real_le_refl,real_less_imp_le]));
  1.2218 +qed "lemma_real_le_Un_eq2";
  1.2219 +
  1.2220 +Goal "!!u. 0 < u ==> finite {n::nat. u = rinv(real_of_posnat  n)}";
  1.2221 +by (asm_simp_tac (simpset() addsimps [real_of_posnat_rinv_eq_iff]) 1);
  1.2222 +by (auto_tac (claset() addIs [lemma_finite_omega_set RSN 
  1.2223 +    (2,finite_subset)],simpset()));
  1.2224 +qed "lemma_finite_omega_set2";
  1.2225 +
  1.2226 +Goal "!!u. 0 < u ==> finite {n. u <= rinv(real_of_posnat n)}";
  1.2227 +by (auto_tac (claset(),simpset() addsimps 
  1.2228 +    [lemma_real_le_Un_eq2,lemma_finite_omega_set2,
  1.2229 +     finite_rinv_real_of_posnat_gt_real]));
  1.2230 +qed "finite_rinv_real_of_posnat_ge_real";
  1.2231 +
  1.2232 +Goal "!!u. 0 < u ==> \
  1.2233 +\    {n. u <= rinv(real_of_posnat n)} ~: FreeUltrafilterNat";
  1.2234 +by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
  1.2235 +    finite_rinv_real_of_posnat_ge_real]) 1);
  1.2236 +qed "rinv_real_of_posnat_ge_real_FreeUltrafilterNat";
  1.2237 +
  1.2238 +(*--------------------------------------------------------------
  1.2239 +    The complement of  {n. u <= rinv(real_of_posnat n)} =
  1.2240 +    {n. rinv(real_of_posnat n) < u} is in FreeUltrafilterNat 
  1.2241 +    by property of (free) ultrafilters
  1.2242 + --------------------------------------------------------------*)
  1.2243 +Goal "- {n. u <= rinv(real_of_posnat n)} = \
  1.2244 +\     {n. rinv(real_of_posnat n) < u}";
  1.2245 +by (auto_tac (claset() addSDs [real_le_less_trans],
  1.2246 +   simpset() addsimps [not_real_leE,real_less_not_refl]));
  1.2247 +val lemma = result();
  1.2248 +
  1.2249 +Goal "!!u. 0 < u ==> \
  1.2250 +\     {n. rinv(real_of_posnat n) < u} : FreeUltrafilterNat";
  1.2251 +by (cut_inst_tac [("u","u")]  rinv_real_of_posnat_ge_real_FreeUltrafilterNat 1);
  1.2252 +by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
  1.2253 +    simpset() addsimps [lemma]));
  1.2254 +qed "FreeUltrafilterNat_rinv_real_of_posnat";
  1.2255 +
  1.2256 +(*--------------------------------------------------------------
  1.2257 +      Example where we get a hyperreal from a real sequence
  1.2258 +      for which a particular property holds. The theorem is
  1.2259 +      used in proofs about equivalence of nonstandard and
  1.2260 +      standard neighbourhoods. Also used for equivalence of
  1.2261 +      nonstandard ans standard definitions of pointwise 
  1.2262 +      limit (the theorem was previously in REALTOPOS.thy).
  1.2263 + -------------------------------------------------------------*)
  1.2264 +(*-----------------------------------------------------
  1.2265 +    |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal 
  1.2266 + -----------------------------------------------------*)
  1.2267 +Goal "ALL n. abs(X n + -x) < rinv(real_of_posnat n) \ 
  1.2268 +\    ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
  1.2269 +by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals 
  1.2270 +    FreeUltrafilterNat_rinv_real_of_posnat,
  1.2271 +    FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [real_less_trans,
  1.2272 +    FreeUltrafilterNat_subset],simpset() addsimps [hypreal_minus,
  1.2273 +    hypreal_of_real_minus RS sym,hypreal_of_real_def,hypreal_add,
  1.2274 +    Infinitesimal_FreeUltrafilterNat_iff,hypreal_hrinv,hypreal_of_real_of_posnat]));
  1.2275 +qed "real_seq_to_hypreal_Infinitesimal";
  1.2276 +
  1.2277 +Goal "ALL n. abs(X n + -x) < rinv(real_of_posnat n) \ 
  1.2278 +\     ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
  1.2279 +by (rtac (inf_close_minus_iff RS ssubst) 1);
  1.2280 +by (rtac (mem_infmal_iff RS subst) 1);
  1.2281 +by (etac real_seq_to_hypreal_Infinitesimal 1);
  1.2282 +qed "real_seq_to_hypreal_inf_close";
  1.2283 +
  1.2284 +Goal "ALL n. abs(x + -X n) < rinv(real_of_posnat n) \ 
  1.2285 +\              ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
  1.2286 +by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
  1.2287 +        real_seq_to_hypreal_inf_close]) 1);
  1.2288 +qed "real_seq_to_hypreal_inf_close2";
  1.2289 +
  1.2290 +Goal "ALL n. abs(X n + -Y n) < rinv(real_of_posnat n) \ 
  1.2291 +\     ==> Abs_hypreal(hyprel^^{X}) + \
  1.2292 +\         -Abs_hypreal(hyprel^^{Y}) : Infinitesimal";
  1.2293 +by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals 
  1.2294 +    FreeUltrafilterNat_rinv_real_of_posnat,
  1.2295 +    FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [real_less_trans,
  1.2296 +    FreeUltrafilterNat_subset],simpset() addsimps 
  1.2297 +    [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add, 
  1.2298 +    hypreal_hrinv,hypreal_of_real_of_posnat]));
  1.2299 +qed "real_seq_to_hypreal_Infinitesimal2";
  1.2300 + 
  1.2301 \ No newline at end of file