src/HOL/Real/Hyperreal/Star.ML
changeset 10045 c76b73e16711
child 10095 16292f1471ad
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Star.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,499 @@
     1.4 +(*  Title       : STAR.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : *-transforms
     1.8 +*) 
     1.9 +
    1.10 +(*--------------------------------------------------------
    1.11 +   Preamble - Pulling "?" over "!"
    1.12 + ---------------------------------------------------------*)
    1.13 + 
    1.14 +(* This proof does not need AC and was suggested by the 
    1.15 +   referee for the JCM Paper: let f(x) be least y such 
    1.16 +   that  Q(x,y) 
    1.17 +*)
    1.18 +Goal "!!Q. ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)";
    1.19 +by (res_inst_tac [("x","%x. LEAST y. Q x y")] exI 1);
    1.20 +by (blast_tac (claset() addIs [LeastI]) 1);
    1.21 +qed "no_choice";
    1.22 +
    1.23 +(*------------------------------------------------------------
    1.24 +    Properties of the *-transform applied to sets of reals
    1.25 + ------------------------------------------------------------*)
    1.26 +
    1.27 +Goalw [starset_def] "*s*(UNIV::real set) = (UNIV::hypreal set)";
    1.28 +by (Auto_tac);
    1.29 +qed "STAR_real_set";
    1.30 +Addsimps [STAR_real_set];
    1.31 +
    1.32 +Goalw [starset_def] "*s* {} = {}";
    1.33 +by (Step_tac 1);
    1.34 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.35 +by (dres_inst_tac [("x","%n. xa n")] bspec 1);
    1.36 +by (Auto_tac);
    1.37 +qed "STAR_empty_set";
    1.38 +Addsimps [STAR_empty_set];
    1.39 +
    1.40 +Goalw [starset_def] "*s* (A Un B) = *s* A Un *s* B";
    1.41 +by (Auto_tac);
    1.42 +by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
    1.43 +by (dtac FreeUltrafilterNat_Compl_mem 1);
    1.44 +by (dtac bspec 1 THEN assume_tac 1);
    1.45 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.46 +by (Auto_tac);
    1.47 +by (Fuf_tac 1);
    1.48 +qed "STAR_Un";
    1.49 +
    1.50 +Goalw [starset_def] "*s* (A Int B) = *s* A Int *s* B";
    1.51 +by (Auto_tac);
    1.52 +by (blast_tac (claset() addIs [FreeUltrafilterNat_Int,
    1.53 +               FreeUltrafilterNat_subset]) 3);
    1.54 +by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
    1.55 +qed "STAR_Int";
    1.56 +
    1.57 +Goalw [starset_def] "*s* -A = -(*s* A)";
    1.58 +by (Auto_tac);
    1.59 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.60 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
    1.61 +by (REPEAT(Step_tac 1) THEN Auto_tac);
    1.62 +by (Fuf_empty_tac 1);
    1.63 +by (dtac FreeUltrafilterNat_Compl_mem 1);
    1.64 +by (Fuf_tac 1);
    1.65 +qed "STAR_Compl";
    1.66 +
    1.67 +goal Set.thy "(A - B) = (A Int (- B))";
    1.68 +by (Step_tac 1);
    1.69 +qed "set_diff_iff2";
    1.70 +
    1.71 +Goal "!!x. x ~: *s* F ==> x : *s* (- F)";
    1.72 +by (auto_tac (claset(),simpset() addsimps [STAR_Compl]));
    1.73 +qed "STAR_mem_Compl";
    1.74 +
    1.75 +Goal "*s* (A - B) = *s* A - *s* B";
    1.76 +by (auto_tac (claset(),simpset() addsimps 
    1.77 +         [set_diff_iff2,STAR_Int,STAR_Compl]));
    1.78 +qed "STAR_diff";
    1.79 +
    1.80 +Goalw [starset_def] "!!A. A <= B ==> *s* A <= *s* B";
    1.81 +by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
    1.82 +qed "STAR_subset";
    1.83 +
    1.84 +Goalw [starset_def,hypreal_of_real_def] 
    1.85 +          "!!A. a : A ==> hypreal_of_real a : *s* A";
    1.86 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
    1.87 +qed "STAR_mem";
    1.88 +
    1.89 +Goalw [starset_def] "hypreal_of_real `` A <= *s* A";
    1.90 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
    1.91 +by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
    1.92 +qed "STAR_hypreal_of_real_image_subset";
    1.93 +
    1.94 +Goalw [starset_def] "*s* X Int SReal = hypreal_of_real `` X";
    1.95 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,SReal_def]));
    1.96 +by (fold_tac [hypreal_of_real_def]);
    1.97 +by (rtac imageI 1 THEN rtac ccontr 1);
    1.98 +by (dtac bspec 1);
    1.99 +by (rtac lemma_hyprel_refl 1);
   1.100 +by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
   1.101 +by (Auto_tac);
   1.102 +qed "STAR_hypreal_of_real_Int";
   1.103 +
   1.104 +Goal "!!x. x ~: hypreal_of_real `` A ==> ALL y: A. x ~= hypreal_of_real y";
   1.105 +by (Auto_tac);
   1.106 +qed "lemma_not_hyprealA";
   1.107 +
   1.108 +Goal "- {n. X n = xa} = {n. X n ~= xa}";
   1.109 +by (Auto_tac);
   1.110 +qed "lemma_Compl_eq";
   1.111 +
   1.112 +Goalw [starset_def]
   1.113 +    "!!M. ALL n. (X n) ~: M \
   1.114 +\         ==> Abs_hypreal(hyprel^^{X}) ~: *s* M";
   1.115 +by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.116 +by (Auto_tac);
   1.117 +qed "STAR_real_seq_to_hypreal";
   1.118 +
   1.119 +Goalw [starset_def] "*s* {x} = {hypreal_of_real x}";
   1.120 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
   1.121 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.122 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
   1.123 +qed "STAR_singleton";
   1.124 +Addsimps [STAR_singleton];
   1.125 +
   1.126 +Goal "!!x. x ~: F ==> hypreal_of_real x ~: *s* F";
   1.127 +by (auto_tac (claset(),simpset() addsimps
   1.128 +    [starset_def,hypreal_of_real_def]));
   1.129 +by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.130 +by (Auto_tac);
   1.131 +qed "STAR_not_mem";
   1.132 +
   1.133 +Goal "!!x. [| x : *s* A; A <= B |] ==> x : *s* B";
   1.134 +by (blast_tac (claset() addDs [STAR_subset]) 1);
   1.135 +qed "STAR_subset_closed";
   1.136 +
   1.137 +(*------------------------------------------------------------------ 
   1.138 +   Nonstandard extension of a set (defined using a constant 
   1.139 +   sequence) as a special case of an internal set
   1.140 + -----------------------------------------------------------------*)
   1.141 +
   1.142 +Goalw [starset_n_def,starset_def] 
   1.143 +     "!!A. ALL n. (As n = A) ==> *sn* As = *s* A";
   1.144 +by (Auto_tac);
   1.145 +qed "starset_n_starset";
   1.146 +
   1.147 +
   1.148 +(*----------------------------------------------------------------*)
   1.149 +(* Theorems about nonstandard extensions of functions             *)
   1.150 +(*----------------------------------------------------------------*)
   1.151 +
   1.152 +(*----------------------------------------------------------------*) 
   1.153 +(* Nonstandard extension of a function (defined using a           *)
   1.154 +(* constant sequence) as a special case of an internal function   *)
   1.155 +(*----------------------------------------------------------------*)
   1.156 +
   1.157 +Goalw [starfun_n_def,starfun_def] 
   1.158 +     "!!A. ALL n. (F n = f) ==> *fn* F = *f* f";
   1.159 +by (Auto_tac);
   1.160 +qed "starfun_n_starfun";
   1.161 +
   1.162 +
   1.163 +(* 
   1.164 +   Prove that hrabs is a nonstandard extension of rabs without
   1.165 +   use of congruence property (proved after this for general
   1.166 +   nonstandard extensions of real valued functions). This makes 
   1.167 +   proof much longer- see comments at end of HREALABS.thy where
   1.168 +   we proved a congruence theorem for hrabs. 
   1.169 +
   1.170 +   NEW!!! No need to prove all the lemmas anymore. Use the ultrafilter
   1.171 +   tactic! 
   1.172 +*)
   1.173 +  
   1.174 +Goalw [is_starext_def] "is_starext abs abs";
   1.175 +by (Step_tac 1);
   1.176 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.177 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.178 +by Auto_tac;
   1.179 +by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.180 +by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.181 +by (auto_tac (claset() addSDs [spec],simpset() addsimps [hypreal_minus,hrabs_def,
   1.182 +    hypreal_zero_def,hypreal_le_def,hypreal_less_def]));
   1.183 +by (TRYALL(Ultra_tac));
   1.184 +by (TRYALL(arith_tac));
   1.185 +qed "hrabs_is_starext_rabs";
   1.186 +
   1.187 +Goal "!!z. [| X: Rep_hypreal z; Y: Rep_hypreal z |] \
   1.188 +\              ==> {n. X n = Y n} : FreeUltrafilterNat";
   1.189 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   1.190 +by (Auto_tac THEN Fuf_tac 1);
   1.191 +qed "Rep_hypreal_FreeUltrafilterNat";
   1.192 +
   1.193 +(*-----------------------------------------------------------------------
   1.194 +    Nonstandard extension of functions- congruence 
   1.195 + -----------------------------------------------------------------------*) 
   1.196 +
   1.197 +Goalw [congruent_def] "congruent hyprel (%X. hyprel^^{%n. f (X n)})";
   1.198 +by (safe_tac (claset()));
   1.199 +by (ALLGOALS(Fuf_tac));
   1.200 +qed "starfun_congruent";
   1.201 +
   1.202 +Goalw [starfun_def]
   1.203 +      "(*f* f) (Abs_hypreal(hyprel^^{%n. X n})) = \
   1.204 +\      Abs_hypreal(hyprel ^^ {%n. f (X n)})";
   1.205 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   1.206 +by (simp_tac (simpset() addsimps 
   1.207 +   [hyprel_in_hypreal RS Abs_hypreal_inverse,[equiv_hyprel,
   1.208 +   starfun_congruent] MRS UN_equiv_class]) 1);
   1.209 +qed "starfun";
   1.210 +
   1.211 +(*-------------------------------------------
   1.212 +  multiplication: ( *f ) x ( *g ) = *(f x g)  
   1.213 + ------------------------------------------*)
   1.214 +Goal "(*f* f) xa * (*f* g) xa = (*f* (%x. f x * g x)) xa";
   1.215 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.216 +by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult]));
   1.217 +qed "starfun_mult";
   1.218 +
   1.219 +(*---------------------------------------
   1.220 +  addition: ( *f ) + ( *g ) = *(f + g)  
   1.221 + ---------------------------------------*)
   1.222 +Goal "(*f* f) xa + (*f* g) xa = (*f* (%x. f x + g x)) xa";
   1.223 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.224 +by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add]));
   1.225 +qed "starfun_add";
   1.226 +
   1.227 +(*--------------------------------------------
   1.228 +  subtraction: ( *f ) + -( *g ) = *(f + -g)  
   1.229 + -------------------------------------------*)
   1.230 +Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa";
   1.231 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.232 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.233 +    hypreal_minus,hypreal_add]));
   1.234 +qed "starfun_add_minus";
   1.235 +
   1.236 +Goalw [hypreal_diff_def,real_diff_def]
   1.237 +  "(*f* f) xa  - (*f* g) xa = (*f* (%x. f x - g x)) xa";
   1.238 +by (rtac starfun_add_minus 1);
   1.239 +qed "starfun_diff";
   1.240 +
   1.241 +(*--------------------------------------
   1.242 +  composition: ( *f ) o ( *g ) = *(f o g)  
   1.243 + ---------------------------------------*)
   1.244 +
   1.245 +Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))";
   1.246 +by (rtac ext 1);
   1.247 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.248 +by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.249 +qed "starfun_o2";
   1.250 +
   1.251 +Goalw [o_def] "(*f* f) o (*f* g) = (*f* (f o g))";
   1.252 +by (simp_tac (simpset() addsimps [starfun_o2]) 1);
   1.253 +qed "starfun_o";
   1.254 +
   1.255 +(*--------------------------------------
   1.256 +  NS extension of constant function
   1.257 + --------------------------------------*)
   1.258 +Goal "(*f* (%x. k)) xa = hypreal_of_real  k";
   1.259 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.260 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.261 +    hypreal_of_real_def]));
   1.262 +qed "starfun_const_fun";
   1.263 +
   1.264 +Addsimps [starfun_const_fun];
   1.265 +
   1.266 +Goal "- (*f* f) x = (*f* (%x. - f x)) x";
   1.267 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.268 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.269 +              hypreal_minus]));
   1.270 +qed "starfun_minus";
   1.271 +
   1.272 +(*----------------------------------------------------
   1.273 +   the NS extension of the identity function
   1.274 + ----------------------------------------------------*)
   1.275 +
   1.276 +Goal "!!x. x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real  a";
   1.277 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.278 +by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.279 +qed "starfun_Idfun_inf_close";
   1.280 +
   1.281 +Goal "(*f* (%x. x)) x = x";
   1.282 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.283 +by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.284 +qed "starfun_Id";
   1.285 +
   1.286 +(*----------------------------------------------------------------------
   1.287 +      the *-function is a (nonstandard) extension of the function
   1.288 + ----------------------------------------------------------------------*)
   1.289 +
   1.290 +Goalw [is_starext_def] "is_starext (*f* f) f";
   1.291 +by (Auto_tac);
   1.292 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.293 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.294 +by (auto_tac (claset() addSIs [bexI] ,simpset() addsimps [starfun]));
   1.295 +qed "is_starext_starfun";
   1.296 +
   1.297 +(*----------------------------------------------------------------------
   1.298 +     Any nonstandard extension is in fact the *-function
   1.299 + ----------------------------------------------------------------------*)
   1.300 +
   1.301 +Goalw [is_starext_def] "!!f. is_starext F f ==> F = *f* f";
   1.302 +by (rtac ext 1);
   1.303 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.304 +by (dres_inst_tac [("x","x")] spec 1);
   1.305 +by (dres_inst_tac [("x","(*f* f) x")] spec 1);
   1.306 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   1.307 +    simpset() addsimps [starfun]));
   1.308 +by (Fuf_empty_tac 1);
   1.309 +qed "is_starfun_starext";
   1.310 +
   1.311 +Goal "(is_starext F f) = (F = *f* f)";
   1.312 +by (blast_tac (claset() addIs [is_starfun_starext,is_starext_starfun]) 1);
   1.313 +qed "is_starext_starfun_iff";
   1.314 +
   1.315 +(*--------------------------------------------------------
   1.316 +   extented function has same solution as its standard
   1.317 +   version for real arguments. i.e they are the same
   1.318 +   for all real arguments
   1.319 + -------------------------------------------------------*)
   1.320 +Goal "(*f* f) (hypreal_of_real a) = hypreal_of_real (f a)";
   1.321 +by (auto_tac (claset(),simpset() addsimps 
   1.322 +     [starfun,hypreal_of_real_def]));
   1.323 +qed "starfun_eq";
   1.324 +
   1.325 +Addsimps [starfun_eq];
   1.326 +
   1.327 +Goal "(*f* f) (hypreal_of_real a) @= hypreal_of_real (f a)";
   1.328 +by (Auto_tac);
   1.329 +qed "starfun_inf_close";
   1.330 +
   1.331 +(* useful for NS definition of derivatives *)
   1.332 +Goal "(*f* (%h. f (x + h))) xa  = (*f* f) (hypreal_of_real  x + xa)";
   1.333 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.334 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.335 +    hypreal_of_real_def,hypreal_add]));
   1.336 +qed "starfun_lambda_cancel";
   1.337 +
   1.338 +Goal "(*f* (%h. f(g(x + h)))) xa = (*f* (f o g)) (hypreal_of_real x + xa)";
   1.339 +by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   1.340 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.341 +    hypreal_of_real_def,hypreal_add]));
   1.342 +qed "starfun_lambda_cancel2";
   1.343 +
   1.344 +Goal "!!f. [| (*f* f) xa @= l; (*f* g) xa @= m; \
   1.345 +\                 l: HFinite; m: HFinite  \
   1.346 +\              |] ==>  (*f* (%x. f x * g x)) xa @= l * m";
   1.347 +by (dtac inf_close_mult_HFinite 1);
   1.348 +by (REPEAT(assume_tac 1));
   1.349 +by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
   1.350 +              simpset() addsimps [starfun_mult]));
   1.351 +qed "starfun_mult_HFinite_inf_close";
   1.352 +
   1.353 +Goal "!!f. [| (*f* f) xa @= l; (*f* g) xa @= m \
   1.354 +\              |] ==>  (*f* (%x. f x + g x)) xa @= l + m";
   1.355 +by (auto_tac (claset() addIs [inf_close_add],
   1.356 +              simpset() addsimps [starfun_add RS sym]));
   1.357 +qed "starfun_add_inf_close";
   1.358 +
   1.359 +(*----------------------------------------------------
   1.360 +    Examples: hrabs is nonstandard extension of rabs 
   1.361 +              hrinv is nonstandard extension of rinv
   1.362 + ---------------------------------------------------*)
   1.363 +
   1.364 +(* can be proved easily using theorem "starfun" and *)
   1.365 +(* properties of ultrafilter as for hrinv below we  *)
   1.366 +(* use the theorem we proved above instead          *)
   1.367 +
   1.368 +Goal "*f* abs = abs";
   1.369 +by (rtac (hrabs_is_starext_rabs RS 
   1.370 +    (is_starext_starfun_iff RS iffD1) RS sym) 1);
   1.371 +qed "starfun_rabs_hrabs";
   1.372 +
   1.373 +Goal "!!x. x ~= 0 ==> (*f* rinv) x = hrinv(x)";
   1.374 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.375 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.376 +    hypreal_hrinv,hypreal_zero_def]));
   1.377 +by (dtac FreeUltrafilterNat_Compl_mem 1);
   1.378 +by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],simpset()));
   1.379 +qed "starfun_rinv_hrinv";
   1.380 +
   1.381 +(* more specifically *)
   1.382 +Goal "(*f* rinv) ehr = hrinv (ehr)";
   1.383 +by (rtac (hypreal_epsilon_not_zero RS starfun_rinv_hrinv) 1);
   1.384 +qed "starfun_rinv_epsilon";
   1.385 +
   1.386 +Goal "ALL x. f x ~= 0 ==> \
   1.387 +\     hrinv ((*f* f) x) = (*f* (%x. rinv (f x))) x";
   1.388 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.389 +by (auto_tac (claset(),simpset() addsimps [starfun,
   1.390 +              hypreal_hrinv]));
   1.391 +qed "starfun_hrinv";
   1.392 +
   1.393 +Goal "(*f* f) x ~= 0 ==> \
   1.394 +\     hrinv ((*f* f) x) = (*f* (%x. rinv (f x))) x";
   1.395 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.396 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   1.397 +    addSDs [FreeUltrafilterNat_Compl_mem],
   1.398 +    simpset() addsimps [starfun,hypreal_hrinv,
   1.399 +    hypreal_zero_def]));
   1.400 +qed "starfun_hrinv2";
   1.401 +
   1.402 +Goal "a ~= hypreal_of_real b ==> \
   1.403 +\     (*f* (%z. rinv (z + -b))) a = hrinv(a + -hypreal_of_real b)";
   1.404 +by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
   1.405 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   1.406 +    addSDs [FreeUltrafilterNat_Compl_mem],
   1.407 +    simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
   1.408 +    hypreal_minus,hypreal_hrinv,rename_numerals 
   1.409 +    (real_eq_minus_iff2 RS sym)]));
   1.410 +qed "starfun_hrinv3";
   1.411 +
   1.412 +Goal 
   1.413 +     "!!f. a + hypreal_of_real b ~= 0 ==> \
   1.414 +\          (*f* (%z. rinv (z + b))) a = hrinv(a + hypreal_of_real b)";
   1.415 +by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
   1.416 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   1.417 +    addSDs [FreeUltrafilterNat_Compl_mem],
   1.418 +    simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
   1.419 +    hypreal_hrinv,hypreal_zero_def]));
   1.420 +qed "starfun_hrinv4";
   1.421 +
   1.422 +(*-------------------------------------------------------------
   1.423 +    General lemma/theorem needed for proofs in elementary
   1.424 +    topology of the reals
   1.425 + ------------------------------------------------------------*)
   1.426 +Goalw [starset_def] 
   1.427 +      "!!A. (*f* f) x : *s* A ==> x : *s* {x. f x : A}";
   1.428 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.429 +by (auto_tac (claset(),simpset() addsimps [starfun]));
   1.430 +by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1);
   1.431 +by (Auto_tac THEN Fuf_tac 1);
   1.432 +qed "starfun_mem_starset";
   1.433 +
   1.434 +(*------------------------------------------------------------
   1.435 +   Alternative definition for hrabs with rabs function
   1.436 +   applied entrywise to equivalence class representative.
   1.437 +   This is easily proved using starfun and ns extension thm
   1.438 + ------------------------------------------------------------*)
   1.439 +Goal "abs (Abs_hypreal (hyprel ^^ {X})) = \
   1.440 +\                 Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
   1.441 +by (simp_tac (simpset() addsimps [starfun_rabs_hrabs RS sym,starfun]) 1);
   1.442 +qed "hypreal_hrabs";
   1.443 +
   1.444 +(*----------------------------------------------------------------
   1.445 +   nonstandard extension of set through nonstandard extension
   1.446 +   of rabs function i.e hrabs. A more general result should be 
   1.447 +   where we replace rabs by some arbitrary function f and hrabs
   1.448 +   by its NS extenson ( *f* f). See second NS set extension below.
   1.449 + ----------------------------------------------------------------*)
   1.450 +Goalw [starset_def]
   1.451 +   "*s* {x. abs (x + - y) < r} = {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
   1.452 +by (Step_tac 1);
   1.453 +by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
   1.454 +by (auto_tac (claset() addSIs [exI] addSDs [bspec],
   1.455 +    simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
   1.456 +    hypreal_hrabs,hypreal_less_def]));
   1.457 +by (Fuf_tac 1);
   1.458 +qed "STAR_rabs_add_minus";
   1.459 +
   1.460 +Goalw [starset_def]
   1.461 +  "*s* {x. abs (f x + - y) < r} = \
   1.462 +\      {x. abs((*f* f) x + -hypreal_of_real y) < hypreal_of_real r}";
   1.463 +by (Step_tac 1);
   1.464 +by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
   1.465 +by (auto_tac (claset() addSIs [exI] addSDs [bspec],
   1.466 +    simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
   1.467 +    hypreal_hrabs,hypreal_less_def,starfun]));
   1.468 +by (Fuf_tac 1);
   1.469 +qed "STAR_starfun_rabs_add_minus";
   1.470 +
   1.471 +(*-------------------------------------------------------------------
   1.472 +   Another charaterization of Infinitesimal and one of @= relation. 
   1.473 +   In this theory since hypreal_hrabs proved here. (To Check:) Maybe 
   1.474 +   move both if possible? 
   1.475 + -------------------------------------------------------------------*)
   1.476 +Goal "(x:Infinitesimal) = (EX X:Rep_hypreal(x). \
   1.477 +\              ALL m. {n. abs(X n) < rinv(real_of_posnat m)}:FreeUltrafilterNat)";
   1.478 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.479 +by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
   1.480 +    simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
   1.481 +    hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_hrinv,
   1.482 +    hypreal_hrabs,hypreal_less])); 
   1.483 +by (dres_inst_tac [("x","n")] spec 1);
   1.484 +by (Fuf_tac 1);
   1.485 +qed  "Infinitesimal_FreeUltrafilterNat_iff2";
   1.486 +
   1.487 +Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \
   1.488 +\     (ALL m. {n. abs (X n + - Y n) < \
   1.489 +\                 rinv(real_of_posnat m)} : FreeUltrafilterNat)";
   1.490 +by (rtac (inf_close_minus_iff RS ssubst) 1);
   1.491 +by (rtac (mem_infmal_iff RS subst) 1);
   1.492 +by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
   1.493 +              hypreal_add,Infinitesimal_FreeUltrafilterNat_iff2]));
   1.494 +by (dres_inst_tac [("x","m")] spec 1);
   1.495 +by (Fuf_tac 1);
   1.496 +qed "inf_close_FreeUltrafilterNat_iff";
   1.497 +
   1.498 +
   1.499 +
   1.500 +
   1.501 +
   1.502 +