src/HOL/Hyperreal/Star.ML
author nipkow
Fri Feb 07 16:40:23 2003 +0100 (2003-02-07)
changeset 13810 c3fbfd472365
parent 12486 0ed8bdd883e0
child 14299 0b5c0b0a3eba
permissions -rw-r--r--
(*f -> ( *f because of new comments
     1 (*  Title       : STAR.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : *-transforms
     5 *) 
     6 
     7 (*--------------------------------------------------------
     8    Preamble - Pulling "EX" over "ALL"
     9  ---------------------------------------------------------*)
    10  
    11 (* This proof does not need AC and was suggested by the 
    12    referee for the JCM Paper: let f(x) be least y such 
    13    that  Q(x,y) 
    14 *)
    15 Goal "ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)";
    16 by (res_inst_tac [("x","%x. LEAST y. Q x y")] exI 1);
    17 by (blast_tac (claset() addIs [LeastI]) 1);
    18 qed "no_choice";
    19 
    20 (*------------------------------------------------------------
    21     Properties of the *-transform applied to sets of reals
    22  ------------------------------------------------------------*)
    23 
    24 Goalw [starset_def] "*s*(UNIV::real set) = (UNIV::hypreal set)";
    25 by (Auto_tac);
    26 qed "STAR_real_set";
    27 Addsimps [STAR_real_set];
    28 
    29 Goalw [starset_def] "*s* {} = {}";
    30 by (Step_tac 1);
    31 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    32 by (dres_inst_tac [("x","%n. xa n")] bspec 1);
    33 by (Auto_tac);
    34 qed "STAR_empty_set";
    35 Addsimps [STAR_empty_set];
    36 
    37 Goalw [starset_def] "*s* (A Un B) = *s* A Un *s* B";
    38 by (Auto_tac);
    39 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
    40 by (dtac FreeUltrafilterNat_Compl_mem 1);
    41 by (dtac bspec 1 THEN assume_tac 1);
    42 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    43 by (Auto_tac);
    44 by (Fuf_tac 1);
    45 qed "STAR_Un";
    46 
    47 Goalw [starset_def] "*s* (A Int B) = *s* A Int *s* B";
    48 by (Auto_tac);
    49 by (blast_tac (claset() addIs [FreeUltrafilterNat_Int,
    50                FreeUltrafilterNat_subset]) 3);
    51 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
    52 qed "STAR_Int";
    53 
    54 Goalw [starset_def] "*s* -A = -( *s* A)";
    55 by (Auto_tac);
    56 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    57 by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
    58 by (REPEAT(Step_tac 1) THEN Auto_tac);
    59 by (Fuf_empty_tac 1);
    60 by (dtac FreeUltrafilterNat_Compl_mem 1);
    61 by (Fuf_tac 1);
    62 qed "STAR_Compl";
    63 
    64 goal Set.thy "(A - B) = (A Int (- B))";
    65 by (Step_tac 1);
    66 qed "set_diff_iff2";
    67 
    68 Goal "x ~: *s* F ==> x : *s* (- F)";
    69 by (auto_tac (claset(),simpset() addsimps [STAR_Compl]));
    70 qed "STAR_mem_Compl";
    71 
    72 Goal "*s* (A - B) = *s* A - *s* B";
    73 by (auto_tac (claset(),simpset() addsimps 
    74          [set_diff_iff2,STAR_Int,STAR_Compl]));
    75 qed "STAR_diff";
    76 
    77 Goalw [starset_def] "A <= B ==> *s* A <= *s* B";
    78 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
    79 qed "STAR_subset";
    80 
    81 Goalw [starset_def,hypreal_of_real_def] 
    82           "a : A ==> hypreal_of_real a : *s* A";
    83 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
    84 qed "STAR_mem";
    85 
    86 Goalw [starset_def] "hypreal_of_real ` A <= *s* A";
    87 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
    88 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
    89 qed "STAR_hypreal_of_real_image_subset";
    90 
    91 Goalw [starset_def] "*s* X Int Reals = hypreal_of_real ` X";
    92 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,SReal_def]));
    93 by (fold_tac [hypreal_of_real_def]);
    94 by (rtac imageI 1 THEN rtac ccontr 1);
    95 by (dtac bspec 1);
    96 by (rtac lemma_hyprel_refl 1);
    97 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
    98 by (Auto_tac);
    99 qed "STAR_hypreal_of_real_Int";
   100 
   101 Goal "x ~: hypreal_of_real ` A ==> ALL y: A. x ~= hypreal_of_real y";
   102 by (Auto_tac);
   103 qed "lemma_not_hyprealA";
   104 
   105 Goal "- {n. X n = xa} = {n. X n ~= xa}";
   106 by (Auto_tac);
   107 qed "lemma_Compl_eq";
   108 
   109 Goalw [starset_def]
   110     "ALL n. (X n) ~: M \
   111 \         ==> Abs_hypreal(hyprel``{X}) ~: *s* M";
   112 by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   113 by (Auto_tac);
   114 qed "STAR_real_seq_to_hypreal";
   115 
   116 Goalw [starset_def] "*s* {x} = {hypreal_of_real x}";
   117 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
   118 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   119 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
   120 qed "STAR_singleton";
   121 Addsimps [STAR_singleton];
   122 
   123 Goal "x ~: F ==> hypreal_of_real x ~: *s* F";
   124 by (auto_tac (claset(),simpset() addsimps
   125     [starset_def,hypreal_of_real_def]));
   126 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   127 by (Auto_tac);
   128 qed "STAR_not_mem";
   129 
   130 Goal "[| x : *s* A; A <= B |] ==> x : *s* B";
   131 by (blast_tac (claset() addDs [STAR_subset]) 1);
   132 qed "STAR_subset_closed";
   133 
   134 (*------------------------------------------------------------------ 
   135    Nonstandard extension of a set (defined using a constant 
   136    sequence) as a special case of an internal set
   137  -----------------------------------------------------------------*)
   138 
   139 Goalw [starset_n_def,starset_def] 
   140      "ALL n. (As n = A) ==> *sn* As = *s* A";
   141 by (Auto_tac);
   142 qed "starset_n_starset";
   143 
   144 
   145 (*----------------------------------------------------------------*)
   146 (* Theorems about nonstandard extensions of functions             *)
   147 (*----------------------------------------------------------------*)
   148 
   149 (*----------------------------------------------------------------*) 
   150 (* Nonstandard extension of a function (defined using a           *)
   151 (* constant sequence) as a special case of an internal function   *)
   152 (*----------------------------------------------------------------*)
   153 
   154 Goalw [starfun_n_def,starfun_def] 
   155      "ALL n. (F n = f) ==> *fn* F = *f* f";
   156 by (Auto_tac);
   157 qed "starfun_n_starfun";
   158 
   159 
   160 (* 
   161    Prove that hrabs is a nonstandard extension of rabs without
   162    use of congruence property (proved after this for general
   163    nonstandard extensions of real valued functions). This makes 
   164    proof much longer- see comments at end of HREALABS.thy where
   165    we proved a congruence theorem for hrabs. 
   166 
   167    NEW!!! No need to prove all the lemmas anymore. Use the ultrafilter
   168    tactic! 
   169 *)
   170   
   171 Goalw [is_starext_def] "is_starext abs abs";
   172 by (Step_tac 1);
   173 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   174 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   175 by Auto_tac;
   176 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   177 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   178 by (auto_tac (claset() addSDs [spec],
   179               simpset() addsimps [hypreal_minus,hrabs_def, hypreal_zero_def,
   180                 hypreal_le_def, hypreal_less_def]));
   181 by (TRYALL(Ultra_tac));
   182 by (TRYALL(arith_tac));
   183 qed "hrabs_is_starext_rabs";
   184 
   185 Goal "[| X: Rep_hypreal z; Y: Rep_hypreal z |] \
   186 \     ==> {n. X n = Y n} : FreeUltrafilterNat";
   187 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   188 by (Auto_tac THEN Fuf_tac 1);
   189 qed "Rep_hypreal_FreeUltrafilterNat";
   190 
   191 (*-----------------------------------------------------------------------
   192     Nonstandard extension of functions- congruence 
   193  -----------------------------------------------------------------------*) 
   194 
   195 Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})";
   196 by Safe_tac;
   197 by (ALLGOALS(Fuf_tac));
   198 qed "starfun_congruent";
   199 
   200 Goalw [starfun_def]
   201       "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) = \
   202 \      Abs_hypreal(hyprel `` {%n. f (X n)})";
   203 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   204 by (simp_tac (simpset() addsimps 
   205    [hyprel_in_hypreal RS Abs_hypreal_inverse,[equiv_hyprel,
   206    starfun_congruent] MRS UN_equiv_class]) 1);
   207 qed "starfun";
   208 
   209 (*-------------------------------------------
   210   multiplication: ( *f ) x ( *g ) = *(f x g)  
   211  ------------------------------------------*)
   212 Goal "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa";
   213 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   214 by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult]));
   215 qed "starfun_mult";
   216 Addsimps [starfun_mult RS sym];
   217 
   218 (*---------------------------------------
   219   addition: ( *f ) + ( *g ) = *(f + g)  
   220  ---------------------------------------*)
   221 Goal "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa";
   222 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   223 by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add]));
   224 qed "starfun_add";
   225 Addsimps [starfun_add RS sym];
   226 
   227 (*--------------------------------------------
   228   subtraction: ( *f ) + -( *g ) = *(f + -g)  
   229  -------------------------------------------*)
   230 
   231 Goal "- ( *f* f) x = ( *f* (%x. - f x)) x";
   232 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   233 by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus]));
   234 qed "starfun_minus";
   235 Addsimps [starfun_minus RS sym];
   236 
   237 (*FIXME: delete*)
   238 Goal "( *f* f) xa + -( *f* g) xa = ( *f* (%x. f x + -g x)) xa";
   239 by (Simp_tac 1);
   240 qed "starfun_add_minus";
   241 Addsimps [starfun_add_minus RS sym];
   242 
   243 Goalw [hypreal_diff_def,real_diff_def]
   244   "( *f* f) xa  - ( *f* g) xa = ( *f* (%x. f x - g x)) xa";
   245 by (rtac starfun_add_minus 1);
   246 qed "starfun_diff";
   247 Addsimps [starfun_diff RS sym];
   248 
   249 (*--------------------------------------
   250   composition: ( *f ) o ( *g ) = *(f o g)  
   251  ---------------------------------------*)
   252 
   253 Goal "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"; 
   254 by (rtac ext 1);
   255 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   256 by (auto_tac (claset(),simpset() addsimps [starfun]));
   257 qed "starfun_o2";
   258 
   259 Goalw [o_def] "( *f* f) o ( *f* g) = ( *f* (f o g))";
   260 by (simp_tac (simpset() addsimps [starfun_o2]) 1);
   261 qed "starfun_o";
   262 
   263 (*--------------------------------------
   264   NS extension of constant function
   265  --------------------------------------*)
   266 Goal "( *f* (%x. k)) xa = hypreal_of_real  k";
   267 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   268 by (auto_tac (claset(),simpset() addsimps [starfun,
   269     hypreal_of_real_def]));
   270 qed "starfun_const_fun";
   271 
   272 Addsimps [starfun_const_fun];
   273 
   274 (*----------------------------------------------------
   275    the NS extension of the identity function
   276  ----------------------------------------------------*)
   277 
   278 Goal "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a";
   279 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   280 by (auto_tac (claset(),simpset() addsimps [starfun]));
   281 qed "starfun_Idfun_approx";
   282 
   283 Goal "( *f* (%x. x)) x = x";
   284 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   285 by (auto_tac (claset(),simpset() addsimps [starfun]));
   286 qed "starfun_Id";
   287 Addsimps [starfun_Id];  
   288 
   289 (*----------------------------------------------------------------------
   290       the *-function is a (nonstandard) extension of the function
   291  ----------------------------------------------------------------------*)
   292 
   293 Goalw [is_starext_def] "is_starext ( *f* f) f";
   294 by (Auto_tac);
   295 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   296 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   297 by (auto_tac (claset() addSIs [bexI] ,simpset() addsimps [starfun]));
   298 qed "is_starext_starfun";
   299 
   300 (*----------------------------------------------------------------------
   301      Any nonstandard extension is in fact the *-function
   302  ----------------------------------------------------------------------*)
   303 
   304 Goalw [is_starext_def] "is_starext F f ==> F = *f* f";
   305 by (rtac ext 1);
   306 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   307 by (dres_inst_tac [("x","x")] spec 1);
   308 by (dres_inst_tac [("x","( *f* f) x")] spec 1);
   309 by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   310     simpset() addsimps [starfun]));
   311 by (Fuf_empty_tac 1);
   312 qed "is_starfun_starext";
   313 
   314 Goal "(is_starext F f) = (F = *f* f)";
   315 by (blast_tac (claset() addIs [is_starfun_starext,is_starext_starfun]) 1);
   316 qed "is_starext_starfun_iff";
   317 
   318 (*--------------------------------------------------------
   319    extented function has same solution as its standard
   320    version for real arguments. i.e they are the same
   321    for all real arguments
   322  -------------------------------------------------------*)
   323 Goal "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)";
   324 by (auto_tac (claset(),simpset() addsimps 
   325      [starfun,hypreal_of_real_def]));
   326 qed "starfun_eq";
   327 
   328 Addsimps [starfun_eq];
   329 
   330 Goal "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)";
   331 by (Auto_tac);
   332 qed "starfun_approx";
   333 
   334 (* useful for NS definition of derivatives *)
   335 Goal "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)";
   336 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   337 by (auto_tac (claset(),simpset() addsimps [starfun,
   338     hypreal_of_real_def,hypreal_add]));
   339 qed "starfun_lambda_cancel";
   340 
   341 Goal "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)";
   342 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   343 by (auto_tac (claset(),simpset() addsimps [starfun,
   344     hypreal_of_real_def,hypreal_add]));
   345 qed "starfun_lambda_cancel2";
   346 
   347 Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m; \
   348 \                 l: HFinite; m: HFinite  \
   349 \              |] ==>  ( *f* (%x. f x * g x)) xa @= l * m";
   350 by (dtac approx_mult_HFinite 1);
   351 by (REPEAT(assume_tac 1));
   352 by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
   353               simpset()));
   354 qed "starfun_mult_HFinite_approx";
   355 
   356 Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m \
   357 \              |] ==>  ( *f* (%x. f x + g x)) xa @= l + m";
   358 by (auto_tac (claset() addIs [approx_add], simpset()));
   359 qed "starfun_add_approx";
   360 
   361 (*----------------------------------------------------
   362     Examples: hrabs is nonstandard extension of rabs 
   363               inverse is nonstandard extension of inverse
   364  ---------------------------------------------------*)
   365 
   366 (* can be proved easily using theorem "starfun" and *)
   367 (* properties of ultrafilter as for inverse below we  *)
   368 (* use the theorem we proved above instead          *)
   369 
   370 Goal "*f* abs = abs";
   371 by (rtac (hrabs_is_starext_rabs RS 
   372           (is_starext_starfun_iff RS iffD1) RS sym) 1);
   373 qed "starfun_rabs_hrabs";
   374 
   375 Goal "( *f* inverse) x = inverse(x)";
   376 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   377 by (auto_tac (claset(),
   378             simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
   379 qed "starfun_inverse_inverse";
   380 Addsimps [starfun_inverse_inverse];
   381 
   382 Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x";
   383 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   384 by (auto_tac (claset(),
   385               simpset() addsimps [starfun, hypreal_inverse]));
   386 qed "starfun_inverse";
   387 Addsimps [starfun_inverse RS sym];
   388 
   389 Goalw [hypreal_divide_def,real_divide_def]
   390   "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa";
   391 by Auto_tac;
   392 qed "starfun_divide";
   393 Addsimps [starfun_divide RS sym];
   394 
   395 Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x";
   396 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   397 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   398                        addSDs [FreeUltrafilterNat_Compl_mem],
   399     simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
   400 qed "starfun_inverse2";
   401 
   402 (*-------------------------------------------------------------
   403     General lemma/theorem needed for proofs in elementary
   404     topology of the reals
   405  ------------------------------------------------------------*)
   406 Goalw [starset_def] 
   407       "( *f* f) x : *s* A ==> x : *s* {x. f x : A}";
   408 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   409 by (auto_tac (claset(),simpset() addsimps [starfun]));
   410 by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1);
   411 by (Auto_tac THEN Fuf_tac 1);
   412 qed "starfun_mem_starset";
   413 
   414 (*------------------------------------------------------------
   415    Alternative definition for hrabs with rabs function
   416    applied entrywise to equivalence class representative.
   417    This is easily proved using starfun and ns extension thm
   418  ------------------------------------------------------------*)
   419 Goal "abs (Abs_hypreal (hyprel `` {X})) = \
   420 \                 Abs_hypreal(hyprel `` {%n. abs (X n)})";
   421 by (simp_tac (simpset() addsimps [starfun_rabs_hrabs RS sym,starfun]) 1);
   422 qed "hypreal_hrabs";
   423 
   424 (*----------------------------------------------------------------
   425    nonstandard extension of set through nonstandard extension
   426    of rabs function i.e hrabs. A more general result should be 
   427    where we replace rabs by some arbitrary function f and hrabs
   428    by its NS extenson ( *f* f). See second NS set extension below.
   429  ----------------------------------------------------------------*)
   430 Goalw [starset_def]
   431    "*s* {x. abs (x + - y) < r} = \
   432 \    {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
   433 by (Step_tac 1);
   434 by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
   435 by (auto_tac (claset() addSIs [exI] addSDs [bspec],
   436           simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
   437                               hypreal_hrabs,hypreal_less_def]));
   438 by (Fuf_tac 1);
   439 qed "STAR_rabs_add_minus";
   440 
   441 Goalw [starset_def]
   442   "*s* {x. abs (f x + - y) < r} = \
   443 \      {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}";
   444 by (Step_tac 1);
   445 by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
   446 by (auto_tac (claset() addSIs [exI] addSDs [bspec],
   447     simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
   448     hypreal_hrabs,hypreal_less_def,starfun]));
   449 by (Fuf_tac 1);
   450 qed "STAR_starfun_rabs_add_minus";
   451 
   452 (*-------------------------------------------------------------------
   453    Another characterization of Infinitesimal and one of @= relation. 
   454    In this theory since hypreal_hrabs proved here. (To Check:) Maybe 
   455    move both if possible? 
   456  -------------------------------------------------------------------*)
   457 Goal "(x:Infinitesimal) = \
   458 \     (EX X:Rep_hypreal(x). \
   459 \       ALL m. {n. abs(X n) < inverse(real(Suc m))} \
   460 \              : FreeUltrafilterNat)";
   461 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   462 by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
   463 	simpset() addsimps [Infinitesimal_hypreal_of_nat_iff,
   464 	    hypreal_of_real_def,hypreal_inverse,
   465 	    hypreal_hrabs,hypreal_less, hypreal_of_nat_def])); 
   466 by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero, 
   467 			  real_not_refl2 RS not_sym]) 1) ;
   468 by (dres_inst_tac [("x","n")] spec 1);
   469 by (Fuf_tac 1);
   470 qed  "Infinitesimal_FreeUltrafilterNat_iff2";
   471 
   472 Goal "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = \
   473 \     (ALL m. {n. abs (X n + - Y n) < \
   474 \                 inverse(real(Suc m))} : FreeUltrafilterNat)";
   475 by (stac approx_minus_iff 1);
   476 by (rtac (mem_infmal_iff RS subst) 1);
   477 by (auto_tac (claset(), 
   478               simpset() addsimps [hypreal_minus, hypreal_add,
   479                                   Infinitesimal_FreeUltrafilterNat_iff2]));
   480 by (dres_inst_tac [("x","m")] spec 1);
   481 by (Fuf_tac 1);
   482 qed "approx_FreeUltrafilterNat_iff";
   483 
   484 Goal "inj starfun";
   485 by (rtac injI 1);
   486 by (rtac ext 1 THEN rtac ccontr 1);
   487 by (dres_inst_tac [("x","Abs_hypreal(hyprel ``{%n. xa})")] fun_cong 1);
   488 by (auto_tac (claset(),simpset() addsimps [starfun]));
   489 qed "inj_starfun";