src/HOL/Hyperreal/Lim.ML

 (***           End of Purely Standard Proofs                     ***)
 (***-------------------------------------------------------------***)
 (*--------------------------------------------------------------
        Standard and NS definitions of Limit
  --------------------------------------------------------------*)
-Goalw [LIM_def,NSLIM_def,inf_close_def] 
+Goalw [LIM_def,NSLIM_def,approx_def] 
       "f -- x --> L ==> f -- x --NS> L";
 by (asm_full_simp_tac
     (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
 by (Step_tac 1);
 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);

  ---------------------------------------------------------------------*)
 
 Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
 \        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
 \     ==> ALL n::nat. EX xa.  xa ~= x & \
-\             abs(xa + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f xa + -L)";
+\             abs(xa + -x) < inverse(real(Suc n)) & r <= abs(f xa + -L)";
 by (Clarify_tac 1); 
 by (cut_inst_tac [("n1","n")]
     (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIM = result();
 
 Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
 \        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
 \     ==> EX X. ALL n::nat. X n ~= x & \
-\               abs(X n + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f (X n) + -L)";
+\               abs(X n + -x) < inverse(real(Suc n)) & r <= abs(f (X n) + -L)";
 by (dtac lemma_LIM 1);
 by (dtac choice 1);
 by (Blast_tac 1);
 val lemma_skolemize_LIM2 = result();
 
 Goal "ALL n. X n ~= x & \
-\         abs (X n + - x) < inverse (real_of_nat(Suc n)) & \
+\         abs (X n + - x) < inverse (real(Suc n)) & \
 \         r <= abs (f (X n) + - L) ==> \
-\         ALL n. abs (X n + - x) < inverse (real_of_nat(Suc n))";
+\         ALL n. abs (X n + - x) < inverse (real(Suc n))";
 by (Auto_tac );
 val lemma_simp = result();
  
 (*-------------------
     NSLIM => LIM
  -------------------*)
 
-Goalw [LIM_def,NSLIM_def,inf_close_def] 
+Goalw [LIM_def,NSLIM_def,approx_def] 
      "f -- x --NS> L ==> f -- x --> L";
 by (asm_full_simp_tac
     (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
 by (fold_tac [real_le_def]);

  ------------------------------------------------*)
 
 Goalw [NSLIM_def]
      "[| f -- x --NS> l; g -- x --NS> m |] \
 \     ==> (%x. f(x) * g(x)) -- x --NS> (l * m)";
-by (auto_tac (claset() addSIs [inf_close_mult_HFinite],  simpset()));
+by (auto_tac (claset() addSIs [approx_mult_HFinite],  simpset()));
 qed "NSLIM_mult";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
 \     ==> (%x. f(x) * g(x)) -- x --> (l * m)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_mult]) 1);

       Note the much shorter proof
  ----------------------------------------------*)
 Goalw [NSLIM_def]
      "[| f -- x --NS> l; g -- x --NS> m |] \
 \     ==> (%x. f(x) + g(x)) -- x --NS> (l + m)";
-by (auto_tac (claset() addSIs [inf_close_add], simpset()));
+by (auto_tac (claset() addSIs [approx_add], simpset()));
 qed "NSLIM_add";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
 \     ==> (%x. f(x) + g(x)) -- x --> (l + m)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_add]) 1);

      "[| f -- a --NS> L;  L ~= #0 |] \
 \     ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
 by (Clarify_tac 1);
 by (dtac spec 1);
 by (auto_tac (claset(), 
-              simpset() addsimps [hypreal_of_real_inf_close_inverse]));  
+              simpset() addsimps [hypreal_of_real_approx_inverse]));  
 qed "NSLIM_inverse";
 
 Goal "[| f -- a --> L; \
 \        L ~= #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);

 (*--------------------------
    NSLIM_not_zero
  --------------------------*)
 Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)";
 by Auto_tac;
-by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1);
-by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self RS inf_close_sym],
+by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1);
+by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym],
               simpset() addsimps [rename_numerals hypreal_epsilon_not_zero]));
 qed "NSLIM_not_zero";
 
 (* [| k ~= #0; (%x. k) -- x --NS> #0 |] ==> R *)
 bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);

 
 (*----------------------------
     NSLIM_self
  ----------------------------*)
 Goalw [NSLIM_def] "(%x. x) -- a --NS> a";
-by (auto_tac (claset() addIs [starfun_Idfun_inf_close],simpset()));
+by (auto_tac (claset() addIs [starfun_Idfun_approx],simpset()));
 qed "NSLIM_self";
 
 Goal "(%x. x) -- a --> a";
 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff,NSLIM_self]) 1);
 qed "LIM_self2";

 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
 by (Step_tac 1);
 by (Asm_full_simp_tac 1);
 by (rtac ((mem_infmal_iff RS iffD2) RS 
-    (Infinitesimal_add_inf_close_self RS inf_close_sym)) 1);
-by (rtac (inf_close_minus_iff2 RS iffD1) 4);
+    (Infinitesimal_add_approx_self RS approx_sym)) 1);
+by (rtac (approx_minus_iff2 RS iffD1) 4);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3);
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 4);
 by (auto_tac (claset(),
        simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus,
-              hypreal_add, real_add_assoc, inf_close_refl, hypreal_zero_def]));
+              hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def]));
 qed "NSLIM_h_iff";
 
 Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
 by (rtac NSLIM_h_iff 1);
 qed "NSLIM_isCont_iff";

  --------------------------------------------------------------------------*)
 (*------------------------
      sum continuous
  ------------------------*)
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
-by (auto_tac (claset() addIs [inf_close_add],
+by (auto_tac (claset() addIs [approx_add],
               simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
 qed "isCont_add";
 
 (*------------------------
      mult continuous
  ------------------------*)
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+by (auto_tac (claset() addSIs [starfun_mult_HFinite_approx],
               simpset() delsimps [starfun_mult RS sym]
 			addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
 qed "isCont_mult";
 
 (*-------------------------------------------

 by (Simp_tac 1);
 qed "isNSCont_const";
 Addsimps [isNSCont_const];
 
 Goalw [isNSCont_def]  "isNSCont abs a";
-by (auto_tac (claset() addIs [inf_close_hrabs],
+by (auto_tac (claset() addIs [approx_hrabs],
               simpset() addsimps [hypreal_of_real_hrabs RS sym,
                                   starfun_rabs_hrabs]));
 qed "isNSCont_rabs";
 Addsimps [isNSCont_rabs];
 

   is always an open set
  ------------------------------------------------------------*%)
 Goal "[| isNSopen A; ALL x. isNSCont f x |] \
 \              ==> isNSopen {x. f x : A}";
 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
 by (dres_inst_tac [("x","a")] spec 1);
 by (dtac isNSContD 1 THEN assume_tac 1);
 by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","( *f* f) x")] inf_close_mem_monad2 1);
+by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
 by (blast_tac (claset() addIs [starfun_mem_starset]) 1);
 qed "isNSCont_isNSopen";
 
 Goalw [isNSCont_def]
           "ALL A. isNSopen A --> isNSopen {x. f x : A} \
 \              ==> isNSCont f x";
 by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS 
-     (inf_close_minus_iff RS iffD2)],simpset() addsimps 
+     (approx_minus_iff RS iffD2)],simpset() addsimps 
       [Infinitesimal_def,SReal_iff]));
 by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
 by (etac (isNSopen_open_interval RSN (2,impE)) 1);
 by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
 by (dres_inst_tac [("x","x")] spec 1);
-by (auto_tac (claset() addDs [inf_close_sym RS inf_close_mem_monad],
+by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
     simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
 qed "isNSopen_isNSCont";
 
 Goal "(ALL x. isNSCont f x) = \
 \     (ALL A. isNSopen A --> isNSopen {x. f(x) : A})";

 Goalw [isUCont_def,isCont_def,LIM_def]
      "isUCont f ==> EX x. isCont f x";
 by (Force_tac 1);
 qed "isUCont_isCont";
 
-Goalw [isNSUCont_def,isUCont_def,inf_close_def] 
+Goalw [isNSUCont_def,isUCont_def,approx_def] 
      "isUCont f ==> isNSUCont f";
 by (asm_full_simp_tac (simpset() addsimps 
     [Infinitesimal_FreeUltrafilterNat_iff]) 1);
 by (Step_tac 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);

 by (Ultra_tac 1);
 qed "isUCont_isNSUCont";
 
 Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
 \     ==> ALL n::nat. EX z y.  \
-\              abs(z + -y) < inverse(real_of_nat(Suc n)) & \
+\              abs(z + -y) < inverse(real(Suc n)) & \
 \              r <= abs(f z + -f y)";
 by (Clarify_tac 1); 
 by (cut_inst_tac [("n1","n")]
     (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIMu = result();
 
 Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s  & r <= abs (f z + -f y)) \
 \     ==> EX X Y. ALL n::nat. \
-\              abs(X n + -(Y n)) < inverse(real_of_nat(Suc n)) & \
+\              abs(X n + -(Y n)) < inverse(real(Suc n)) & \
 \              r <= abs(f (X n) + -f (Y n))";
 by (dtac lemma_LIMu 1);
 by (dtac choice 1);
 by (Step_tac 1);
 by (dtac choice 1);
 by (Blast_tac 1);
 val lemma_skolemize_LIM2u = result();
 
-Goal "ALL n. abs (X n + -Y n) < inverse (real_of_nat(Suc n)) & \
+Goal "ALL n. abs (X n + -Y n) < inverse (real(Suc n)) & \
 \         r <= abs (f (X n) + - f(Y n)) ==> \
-\         ALL n. abs (X n + - Y n) < inverse (real_of_nat(Suc n))";
+\         ALL n. abs (X n + - Y n) < inverse (real(Suc n))";
 by (Auto_tac );
 val lemma_simpu = result();
 
-Goalw [isNSUCont_def,isUCont_def,inf_close_def] 
+Goalw [isNSUCont_def,isUCont_def,approx_def] 
      "isNSUCont f ==> isUCont f";
 by (asm_full_simp_tac (simpset() addsimps 
                        [Infinitesimal_FreeUltrafilterNat_iff]) 1);
 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
 by (fold_tac [real_le_def]);

 qed "DERIV_unique";
 
 Goalw [nsderiv_def] 
      "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
 by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1);
-by (auto_tac (claset() addSDs [inst "x" "ehr" bspec] 
+by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec] 
                        addSIs [inj_hypreal_of_real RS injD] 
-                       addDs [inf_close_trans3],
+                       addDs [approx_trans3],
               simpset()));
 qed "NSDeriv_unique";
 
 (*------------------------------------------------------------------------
                           Differentiable

 by (auto_tac (claset(), 
               simpset() addsimps [hypreal_diff_def, hypreal_of_real_zero]));
 by (dres_inst_tac [("x","u")] spec 1);
 by Auto_tac;
 by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
-     inf_close_mult1 1);
+     approx_mult1 1);
 by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
 by (subgoal_tac "(*f* (%z. z - x)) u ~= (0::hypreal)" 2);
 by (rotate_tac ~1 2);
 by (auto_tac (claset(),
     simpset() addsimps [real_diff_def, hypreal_diff_def, 
-		(inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  
+		(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  
 			Infinitesimal_subset_HFinite RS subsetD]));
 qed "NSDERIVD5";
 
 Goal "(NSDERIV f x :> D) ==> \
 \     (ALL h: Infinitesimal. \

 \                hypreal_of_real (f x))@= (hypreal_of_real D) * h)";
 by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
 by (case_tac "h = (0::hypreal)" 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def]));
 by (dres_inst_tac [("x","h")] bspec 1);
-by (dres_inst_tac [("c","h")] inf_close_mult1 2);
+by (dres_inst_tac [("c","h")] approx_mult1 2);
 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
               simpset() addsimps [hypreal_diff_def]));
 qed "NSDERIVD4";
 
 Goal "(NSDERIV f x :> D) ==> \
 \     (ALL h: Infinitesimal - {0}. \
 \              ((*f* f)(hypreal_of_real x + h) - \
 \                hypreal_of_real (f x))@= (hypreal_of_real D) * h)";
 by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
 by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
-by (dres_inst_tac [("c","h")] inf_close_mult1 2);
+by (dres_inst_tac [("c","h")] approx_mult1 2);
 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
               simpset() addsimps [hypreal_mult_assoc, hypreal_diff_def]));
 qed "NSDERIVD3";
 
 (*--------------------------------------------------------------

  --------------------------------------------------*)
 Goalw [nsderiv_def]
       "NSDERIV f x :> D ==> isNSCont f x";
 by (auto_tac (claset(),simpset() addsimps 
         [isNSCont_NSLIM_iff,NSLIM_def]));
-by (dtac (inf_close_minus_iff RS iffD1) 1);
+by (dtac (approx_minus_iff RS iffD1) 1);
 by (dtac (hypreal_not_eq_minus_iff RS iffD1) 1);
 by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1);
 by (asm_full_simp_tac (simpset() addsimps 
     [hypreal_add_assoc RS sym]) 2);
 by (auto_tac (claset(),simpset() addsimps 
     [mem_infmal_iff RS sym,hypreal_add_commute]));
-by (dres_inst_tac [("c","xa + -hypreal_of_real x")] inf_close_mult1 1);
+by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1);
 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite
     RS subsetD],simpset() addsimps [hypreal_mult_assoc]));
 by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN
     (2,Infinitesimal_HFinite_mult) RS (mem_infmal_iff RS iffD1)) 1);
-by (blast_tac (claset() addIs [inf_close_trans,
+by (blast_tac (claset() addIs [approx_trans,
     hypreal_mult_commute RS subst,
-    (inf_close_minus_iff RS iffD2)]) 1);
+    (approx_minus_iff RS iffD2)]) 1);
 qed "NSDERIV_isNSCont";
 
 (* Now Sandard proof *)
 Goal "DERIV f x :> D ==> isCont f x";
 by (asm_full_simp_tac (simpset() addsimps 

 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
            NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
 by (auto_tac (claset(),
        simpset() addsimps [hypreal_add_divide_distrib]));
 by (dres_inst_tac [("b","hypreal_of_real Da"),
-                   ("d","hypreal_of_real Db")] inf_close_add 1);
+                   ("d","hypreal_of_real Db")] approx_add 1);
 by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
 qed "NSDERIV_add";
 
 (* Standard theorem *)
 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \

 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
 by (auto_tac (claset(),
         simpset() delsimps [hypreal_times_divide1_eq]
 		  addsimps [hypreal_times_divide1_eq RS sym]));
 by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
-by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
-by (auto_tac (claset() addSIs [inf_close_add_mono1],
+by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
+by (auto_tac (claset() addSIs [approx_add_mono1],
       simpset() addsimps [hypreal_add_mult_distrib, hypreal_add_mult_distrib2, 
 			  hypreal_mult_commute, hypreal_add_assoc]));
 by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")]
     (hypreal_add_commute RS subst) 1);
-by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS inf_close_sym,
+by (auto_tac (claset() addSIs [Infinitesimal_add_approx_self2 RS approx_sym,
 			       Infinitesimal_add, Infinitesimal_mult,
 			       Infinitesimal_hypreal_of_real_mult,
 			       Infinitesimal_hypreal_of_real_mult2],
 	      simpset() addsimps [hypreal_add_assoc RS sym]));
 qed "NSDERIV_mult";

 \     ==> increment f x h @= #0";
 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs 
     [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps 
     [hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym]));
 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
-qed "increment_inf_close_zero";
+qed "increment_approx_zero";
 
 (*---------------------------------------------------------------
    Similarly to the above, the chain rule admits an entirely
    straightforward derivation. Compare this with Harrison's
    HOL proof of the chain rule, which proved to be trickier and

      "[| NSDERIV f x :> D;  h: Infinitesimal;  h ~= #0 |]  \
 \     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) @= #0";    
 by (asm_full_simp_tac (simpset() addsimps 
     [mem_infmal_iff RS sym]) 1);
 by (rtac Infinitesimal_ratio 1);
-by (rtac inf_close_hypreal_of_real_HFinite 3);
+by (rtac approx_hypreal_of_real_HFinite 3);
 by Auto_tac;
-qed "NSDERIV_inf_close";
+qed "NSDERIV_approx";
 
 (*--------------------------------------------------------------- 
    from one version of differentiability 
  
                 f(x) - f(a)

  ------------------------------------------------------*)
 Goal "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] \
 \     ==> NSDERIV (f o g) x :> Da * Db";
 by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
     NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
-by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
+by (forw_inst_tac [("f","g")] NSDERIV_approx 1);
 by (auto_tac (claset(),
               simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym]));
 by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
 by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
 by (auto_tac (claset(),
     simpset() addsimps [hypreal_divide_def, hypreal_of_real_zero]));
 by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
     ("y1","inverse xa")] (lemma_chain RS ssubst) 1);
 by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
-by (rtac inf_close_mult_hypreal_of_real 1);
+by (rtac approx_mult_hypreal_of_real 1);
 by (fold_tac [hypreal_divide_def]);
 by (blast_tac (claset() addIs [NSDERIVD1,
-    inf_close_minus_iff RS iffD2]) 1);
+    approx_minus_iff RS iffD2]) 1);
 by (blast_tac (claset() addIs [NSDERIVD2]) 1);
 qed "NSDERIV_chain";
 
 (* standard version *)
 Goal "[| DERIV f (g x) :> Da; \

 Goal "NSDERIV (op * c) x :> c";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff]) 1);
 qed "NSDERIV_cmult_Id";
 Addsimps [NSDERIV_cmult_Id];
 
-Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
 by (induct_tac "n" 1);
 by (dtac (DERIV_Id RS DERIV_mult) 2);
 by (auto_tac (claset(), 
               simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib]));
 by (case_tac "0 < n" 1);

 by (auto_tac (claset(), 
               simpset() addsimps [real_mult_assoc, real_add_commute]));
 qed "DERIV_pow";
 
 (* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
 qed "NSDERIV_pow";
 
 (*---------------------------------------------------------------
                     Power of -1 

 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
                                       hypreal_add_mult_distrib2] 
          delsimps [hypreal_minus_mult_eq1 RS sym, 
                    hypreal_minus_mult_eq2 RS sym]) 1);
 by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] 
-                 inf_close_trans 1);
-by (rtac inverse_add_Infinitesimal_inf_close2 1);
+                 approx_trans 1);
+by (rtac inverse_add_Infinitesimal_approx2 1);
 by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal], 
          simpset() addsimps [hypreal_minus_inverse RS sym,
                              HFinite_minus_iff]));
 by (rtac Infinitesimal_HFinite_mult2 1); 
 by Auto_tac;  

 
 (*---------------------------------------------------------------------------*)
 (* By bisection, function continuous on closed interval is bounded above     *)
 (*---------------------------------------------------------------------------*)
 
-Goal "abs (real_of_nat x) = real_of_nat x";
-by (auto_tac (claset() addIs [abs_eqI1],simpset()));
+Goal "abs (real x) = real (x::nat)";
+by (auto_tac (claset() addIs [abs_eqI1], simpset()));
 qed "abs_real_of_nat_cancel";
 Addsimps [abs_real_of_nat_cancel];
 
 Goal "~ abs(x) + 1r < x";
 by (rtac real_leD 1);