# HG changeset patch
# User paulson
# Date 977418490 -3600
# Node ID 1ce5a189f672e4fa166340b51d6c3ac36d0a4c19
# Parent  8666477dd9a2bf7edc722f24d6417554a2218ed1
further tidying of NSA proofs

diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -707,19 +707,6 @@
               simpset()));
 qed "hypreal_mult_zero_disj";
 
-Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
-by (case_tac "x=0 | y=0" 1);
-by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1); 
-by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),
-        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),
-        simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
-by (auto_tac (claset(),
-        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-qed "inverse_mult_eq";
-
 Goal "inverse(-x) = -inverse(x::hypreal)";
 by (hypreal_div_undefined_case_tac "x=0" 1);
 by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
@@ -1052,21 +1039,20 @@
 
 Goal "(0 < -R) = (R < (0::hypreal))";
 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
-    hypreal_less,hypreal_minus]));
+by (auto_tac (claset(),
+       simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
 qed "hypreal_minus_zero_less_iff";
 Addsimps [hypreal_minus_zero_less_iff];
 
 Goal "(-R < 0) = ((0::hypreal) < R)";
 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
-    hypreal_less,hypreal_minus]));
+by (auto_tac (claset(),
+         simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
 by (ALLGOALS(Ultra_tac));
 qed "hypreal_minus_zero_less_iff2";
 
 Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))";
-by (simp_tac (simpset() addsimps 
-    [hypreal_minus_zero_less_iff2]) 1);
+by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1);
 qed "hypreal_minus_zero_le_iff";
 Addsimps [hypreal_minus_zero_le_iff];
 
@@ -1074,20 +1060,19 @@
   hypreal_of_real preserves field and order properties
  -----------------------------------------------------------*)
 Goalw [hypreal_of_real_def] 
-     "hypreal_of_real (z1 + z2) = \
-\     hypreal_of_real z1 + hypreal_of_real z2";
-by (asm_simp_tac (simpset() addsimps [hypreal_add,
-       hypreal_add_mult_distrib]) 1);
+     "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2";
+by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1);
 qed "hypreal_of_real_add";
+Addsimps [hypreal_of_real_add];
 
 Goalw [hypreal_of_real_def] 
      "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2";
-by (full_simp_tac (simpset() addsimps [hypreal_mult,
-        hypreal_add_mult_distrib2]) 1);
+by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1);
 qed "hypreal_of_real_mult";
+Addsimps [hypreal_of_real_mult];
 
 Goalw [hypreal_less_def,hypreal_of_real_def] 
-            "(z1 < z2) = (hypreal_of_real z1 <  hypreal_of_real z2)";
+     "(z1 < z2) = (hypreal_of_real z1 <  hypreal_of_real z2)";
 by Auto_tac;
 by (res_inst_tac [("x","%n. z1")] exI 1);
 by (Step_tac 1); 
@@ -1125,28 +1110,24 @@
     simpset() addsimps [hypreal_of_real_def,
                         hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
 qed "hypreal_of_real_zero_iff";
+AddIffs [hypreal_of_real_zero_iff];
 
-(*FIXME: delete*)
-Goal "(hypreal_of_real r ~= 0) = (r ~= #0)";
-by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
-qed "hypreal_of_real_not_zero_iff";
 
-Goal "inverse (hypreal_of_real r) = hypreal_of_real (inverse r)";
+Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)";
 by (case_tac "r=#0" 1);
 by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, 
                               HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1);
 by (res_inst_tac [("c1","hypreal_of_real r")] 
     (hypreal_mult_left_cancel RS iffD1) 1);
-by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
-by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
-by (auto_tac (claset(),
-      simpset() addsimps [hypreal_of_real_one, hypreal_of_real_mult RS sym]));
+by (stac (hypreal_of_real_mult RS sym) 2); 
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_one]));
 qed "hypreal_of_real_inverse";
+Addsimps [hypreal_of_real_inverse];
 
 Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def, 
-                          hypreal_of_real_mult, hypreal_of_real_inverse]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1);
 qed "hypreal_of_real_divide"; 
+Addsimps [hypreal_of_real_divide];
 
 
 (*** Division lemmas ***)
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/HyperOrd.ML
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -501,10 +501,11 @@
 		    pnat_add_ac) 1);
 qed "hypreal_of_posnat_two";
 
+(*FIXME: delete this and all posnat*)
 Goalw [hypreal_of_posnat_def]
-          "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
-\          hypreal_of_posnat (n1 + n2) + 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
+     "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
+\     hypreal_of_posnat (n1 + n2) + 1hr";
+by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym,
     hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
     preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
 qed "hypreal_of_posnat_add";
@@ -617,11 +618,10 @@
 qed "hypreal_of_nat_one";
 
 Goalw [hypreal_of_nat_def]
-      "hypreal_of_nat n1 + hypreal_of_nat n2 = \
-\      hypreal_of_nat (n1 + n2)";
+     "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
-    hypreal_add_assoc RS sym]) 1);
+                                  hypreal_add_assoc RS sym]) 1);
 qed "hypreal_of_nat_add";
 
 Goal "hypreal_of_nat 2 = 1hr + 1hr";
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/HyperPow.ML
--- a/src/HOL/Real/Hyperreal/HyperPow.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -20,7 +20,7 @@
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset(), simpset() addsimps [inverse_mult_eq]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib]));
 qed_spec_mp "hrealpow_inverse";
 
 Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/Lim.ML
--- a/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -10,7 +10,6 @@
                       (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
 
 
-
 (*---------------------------------------------------------------
    Theory of limits, continuity and differentiation of 
    real=>real functions 
@@ -80,19 +79,18 @@
  --------------------------*)
 Goalw [LIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
 by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1);
-by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
-by (dtac (rename_numerals (real_minus_zero_less_iff RS iffD2)) 1);
+by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
 by (res_inst_tac [("x","-k")] exI 1);
 by (res_inst_tac [("x","k")] exI 2);
 by Auto_tac;
 by (ALLGOALS(dres_inst_tac [("y","s")] real_dense));
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS(res_inst_tac [("x","r + x")] exI));
-by (auto_tac (claset(),simpset() addsimps [real_add_assoc,abs_eqI2]));
+by Auto_tac;  
 qed "LIM_not_zero";
 
 (* [| k ~= #0; (%x. k) -- x --> #0 |] ==> R *)
-bind_thm("LIM_not_zeroE", (LIM_not_zero RS notE));
+bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
 
 Goal "(%x. k) -- x --> L ==> k = L";
 by (rtac ccontr 1);
@@ -193,7 +191,8 @@
 \     ==> ALL n::nat. EX xa.  xa ~= x & \
 \             abs(xa + -x) < inverse(real_of_posnat n) & r <= abs(f xa + -L)";
 by (Step_tac 1);
-by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
+by (cut_inst_tac [("n1","n")]
+    (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIM = result();
 
@@ -260,8 +259,7 @@
 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() addsimps [hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite],  simpset()));
 qed "NSLIM_mult";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
@@ -276,8 +274,7 @@
 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() addsimps [hypreal_of_real_add]));
+by (auto_tac (claset() addSIs [inf_close_add], simpset()));
 qed "NSLIM_add";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
@@ -332,45 +329,35 @@
 \     ==> (%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_not_zero_iff RS sym,
-                                  hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
-by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (auto_tac (claset() addSEs [inf_close_inverse],
-              simpset() addsimps [hypreal_of_real_zero_iff]));
+by (auto_tac (claset(), 
+              simpset() addsimps [hypreal_of_real_inf_close_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);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);
 qed "LIM_inverse";
 
 (*------------------------------
     NSLIM_zero
  ------------------------------*)
 Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> #0";
-by (res_inst_tac [("z1","l")] (rename_numerals 
-    (real_add_minus RS subst)) 1);
+by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
 by (rtac NSLIM_add_minus 1 THEN Auto_tac);
 qed "NSLIM_zero";
 
 Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_zero]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1);
 qed "LIM_zero2";
 
 Goal "(%x. f(x) - l) -- x --NS> #0 ==> f -- x --NS> l";
 by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1);
-by (auto_tac (claset(),simpset() addsimps [real_diff_def,
-    real_add_assoc]));
+by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
 qed "NSLIM_zero_cancel";
 
 Goal "(%x. f(x) - l) -- x --> #0 ==> f -- x --> l";
 by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1);
-by (auto_tac (claset(),simpset() addsimps [real_diff_def,
-    real_add_assoc]));
+by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
 qed "LIM_zero_cancel";
 
 (*--------------------------
@@ -381,17 +368,17 @@
 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],simpset()));
-by (dres_inst_tac [("x1","-hypreal_of_real x")] (hypreal_add_left_cancel RS iffD2) 1);
+by (dres_inst_tac [("x1","-hypreal_of_real x")]
+    (hypreal_add_left_cancel RS iffD2) 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym,
-    hypreal_epsilon_not_zero]) 1);
+                                           hypreal_epsilon_not_zero]) 1);
 qed "NSLIM_not_zero";
 
 (* [| k ~= #0; (%x. k) -- x --NS> #0 |] ==> R *)
-bind_thm("NSLIM_not_zeroE", (NSLIM_not_zero RS notE));
+bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
 
 Goal "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_not_zero]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
 qed "LIM_not_zero2";
 
 (*-------------------------------------
@@ -416,13 +403,11 @@
 Goal "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M";
 by (dtac NSLIM_minus 1);
 by (dtac NSLIM_add 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym],
-    simpset() addsimps [real_add_minus]));
+by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym], simpset()));
 qed "NSLIM_unique";
 
 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_unique]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_unique]) 1);
 qed "LIM_unique2";
 
 (*--------------------
@@ -560,8 +545,7 @@
  ------------------------*)
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
 by (auto_tac (claset() addIs [inf_close_add],
-              simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def,
-                             hypreal_of_real_add]));
+              simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
 qed "isCont_add";
 
 (*------------------------
@@ -570,7 +554,7 @@
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
 by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
               simpset() delsimps [starfun_mult RS sym]
-			addsimps [isNSCont_isCont_iff RS sym, isNSCont_def, hypreal_of_real_mult]));
+			addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
 qed "isCont_mult";
 
 (*-------------------------------------------
@@ -714,21 +698,17 @@
 by (Ultra_tac 1);
 qed "isUCont_isNSUCont";
 
-Goal "ALL s. #0 < s --> \
-\              (EX xa y. abs (xa + - y) < s  & \
-\              r <= abs (f xa + -f y)) ==> \
-\              ALL n::nat. EX xa y.  \
-\              abs(xa + -y) < inverse(real_of_posnat n) & \
-\              r <= abs(f xa + -f y)";
+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_posnat n) & \
+\              r <= abs(f z + -f y)";
 by (Step_tac 1);
 by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIMu = result();
 
-Goal "ALL s. #0 < s --> \
-\              (EX xa y. abs (xa + - y) < s  & \
-\              r <= abs (f xa + -f y)) ==> \
-\              EX X Y. ALL n::nat. \
+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_posnat n) & \
 \              r <= abs(f (X n) + -f (Y n))";
 by (dtac lemma_LIMu 1);
@@ -744,30 +724,22 @@
 by (Auto_tac );
 val lemma_simpu = result();
 
-Goal "{n. f (X n) + - f(Y n) = Ya n} Int \
-\         {n. abs (X n + - Y n) < inverse (real_of_posnat  n) & \
-\             r <= abs (f (X n) + - f(Y n))} <= \
-\         {n. r <= abs (Ya n)}";
-by Auto_tac;
-val lemma_Intu = result ();
-
 Goalw [isNSUCont_def,isUCont_def,inf_close_def] 
      "isNSUCont f ==> isUCont f";
 by (asm_full_simp_tac (simpset() addsimps 
-    [Infinitesimal_FreeUltrafilterNat_iff]) 1);
+                       [Infinitesimal_FreeUltrafilterNat_iff]) 1);
 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
 by (fold_tac [real_le_def]);
 by (dtac lemma_skolemize_LIM2u 1);
 by (Step_tac 1);
 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [starfun,
-    hypreal_minus,hypreal_add]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1);
 by Auto_tac;
 by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1);
 by (asm_full_simp_tac (simpset() addsimps 
-    [Infinitesimal_FreeUltrafilterNat_iff,
-     hypreal_minus,hypreal_add]) 1);
+     [Infinitesimal_FreeUltrafilterNat_iff, hypreal_minus,hypreal_add]) 1);
 by (Blast_tac 1);
 by (rotate_tac 2 1);
 by (dres_inst_tac [("x","r")] spec 1);
@@ -808,10 +780,11 @@
 
 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 [bspec] addSIs 
-   [inj_hypreal_of_real RS injD] addDs [inf_close_trans3],simpset()));
+by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1);
+by (auto_tac (claset() addSDs [inst "x" "ehr" bspec] 
+                       addSIs [inj_hypreal_of_real RS injD] 
+                       addDs [inf_close_trans3],
+              simpset()));
 qed "NSDeriv_unique";
 
 (*------------------------------------------------------------------------
@@ -1016,8 +989,7 @@
 
 (* use simple constant nslimit theorem *)
 Goal "(NSDERIV (%x. k) x :> #0)";
-by (simp_tac (simpset() addsimps 
-    [NSDERIV_NSLIM_iff,real_add_minus]) 1);
+by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
 qed "NSDERIV_const";
 Addsimps [NSDERIV_const];
 
@@ -1036,9 +1008,7 @@
 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_of_real_add, 
-                           hypreal_of_real_divide,
-                           hypreal_add_divide_distrib]));
+       simpset() addsimps [hypreal_add_divide_distrib]));
 by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1);
 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
 qed "NSDERIV_add";
@@ -1089,16 +1059,15 @@
 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],
-    simpset() addsimps [hypreal_of_real_add,hypreal_add_mult_distrib,
-         hypreal_add_mult_distrib2,hypreal_of_real_mult,hypreal_mult_commute,
-         hypreal_add_assoc]));
+      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,Infinitesimal_add,Infinitesimal_mult,
-                 Infinitesimal_hypreal_of_real_mult,
-                 Infinitesimal_hypreal_of_real_mult2 ],
-      simpset() addsimps [hypreal_add_assoc RS sym]));
+by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS inf_close_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";
 
 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \
@@ -1289,18 +1258,16 @@
 		hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
 qed "NSDERIVD2";
 
-(*---------------------------------------------
-  This proof uses both possible definitions
-  for differentiability.
- --------------------------------------------*)
+(*------------------------------------------------------
+  This proof uses both definitions of differentiability.
+ ------------------------------------------------------*)
 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 (auto_tac (claset(),
-    simpset() addsimps [hypreal_of_real_mult,
-              starfun_lambda_cancel2, starfun_o RS sym]));
+              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(),
@@ -1386,16 +1353,12 @@
 by (forward_tac [Infinitesimal_add_not_zero] 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); 
 by (auto_tac (claset(),
-     simpset() addsimps [starfun_inverse_inverse,
-         hypreal_of_real_inverse RS sym, realpow_two,
-         hypreal_of_real_mult,
-         hypreal_of_real_divide] 
+     simpset() addsimps [starfun_inverse_inverse, realpow_two] 
                delsimps [hypreal_minus_mult_eq1 RS sym,
                          hypreal_minus_mult_eq2 RS sym]));
-by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
 by (asm_full_simp_tac
      (simpset() addsimps [hypreal_inverse_add,
-          inverse_mult_eq RS sym, hypreal_minus_inverse RS sym] 
+          hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] 
           @ hypreal_add_ac @ hypreal_mult_ac 
        delsimps [hypreal_minus_mult_eq1 RS sym,
                  hypreal_minus_mult_eq2 RS sym] ) 1);
@@ -1403,22 +1366,18 @@
                                       hypreal_add_mult_distrib2] 
          delsimps [hypreal_minus_mult_eq1 RS sym, 
                    hypreal_minus_mult_eq2 RS sym]) 1);
-by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
-         (2,Infinitesimal_HFinite_mult2)) RS  
-          (Infinitesimal_minus_iff RS iffD1)) 1); 
-by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")]
-       hypreal_mult_not_0 1);
 by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] 
-                 inf_close_trans 2);
-by (rtac inverse_add_Infinitesimal_inf_close2 2);
-by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1]
-         addSDs [Infinitesimal_minus_iff RS iffD2,
-         hypreal_of_real_HFinite_diff_Infinitesimal], simpset() addsimps 
-         [hypreal_minus_inverse RS sym,hypreal_of_real_mult RS sym]));
+                 inf_close_trans 1);
+by (rtac inverse_add_Infinitesimal_inf_close2 1);
+by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal], 
+         simpset() addsimps [hypreal_minus_inverse RS sym,
+                             HFinite_minus_iff RS sym, 
+                             Infinitesimal_minus_iff RS sym]));
+by (rtac Infinitesimal_HFinite_mult2 1); 
+by Auto_tac;  
 qed "NSDERIV_inverse";
 
 
-
 Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
          NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
@@ -1777,9 +1736,9 @@
 by (blast_tac (claset() addIs [IVT2]) 1);
 qed "IVT2_objl";
 
-(*----------------------------------------------------------------------------*)
-(* By bisection, function continuous on closed interval is bounded above      *)
-(*----------------------------------------------------------------------------*)
+(*---------------------------------------------------------------------------*)
+(* 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()));
@@ -2009,7 +1968,7 @@
 by (Step_tac 1);
 by (dres_inst_tac [("x","x - e")] spec 1);
 by (dres_inst_tac [("x","x + e")] spec 2);
-by (auto_tac (claset(), simpset() addsimps [abs_eqI2]));
+by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
 qed "DERIV_local_max";
 
 (*----------------------------------------------------------------------------*)
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/NSA.ML
--- a/src/HOL/Real/Hyperreal/NSA.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -18,7 +18,7 @@
 Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x + y: SReal";
 by (Step_tac 1);
 by (res_inst_tac [("x","r + ra")] exI 1);
-by (simp_tac (simpset() addsimps [hypreal_of_real_add]) 1);
+by (Simp_tac 1);
 qed "SReal_add";
 
 Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x * y: SReal";
@@ -28,7 +28,7 @@
 qed "SReal_mult";
 
 Goalw [SReal_def] "x: SReal ==> inverse x : SReal";
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_inverse]));
+by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1); 
 qed "SReal_inverse";
 
 Goalw [SReal_def] "x: SReal ==> -x : SReal";
@@ -215,7 +215,7 @@
 by (blast_tac (claset() addSIs [SReal_add,hrabs_add_less]) 1);
 qed "HFinite_add";
 
-Goalw [HFinite_def] "[|x : HFinite;y : HFinite|] ==> (x*y) : HFinite";
+Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> (x*y) : HFinite";
 by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
 qed "HFinite_mult";
 
@@ -224,15 +224,18 @@
 qed "HFinite_minus_iff";
 
 Goal "[| x: HFinite; y: HFinite|] ==> (x + -y): HFinite";
-by (blast_tac (claset() addDs [HFinite_minus_iff RS iffD1] addIs [HFinite_add]) 1);
+by (blast_tac (claset() addDs [HFinite_minus_iff RS iffD1] 
+                        addIs [HFinite_add]) 1);
 qed "HFinite_add_minus";
 
 Goalw [SReal_def,HFinite_def] "SReal <= HFinite";
 by Auto_tac;
 by (res_inst_tac [("x","1hr + abs(hypreal_of_real r)")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_hrabs,
-    hypreal_of_real_one RS sym,hypreal_of_real_add RS sym,
-    hypreal_of_real_zero RS sym]));
+by (auto_tac (claset(),
+      simpset() addsimps [hypreal_of_real_hrabs, hypreal_zero_less_one]));
+by (res_inst_tac [("x","#1 + abs r")] exI 1);
+by (simp_tac (simpset() addsimps [hypreal_of_real_one,  
+                                  hypreal_of_real_zero]) 1);
 qed "SReal_subset_HFinite";
 
 Goal "hypreal_of_real x : HFinite";
@@ -285,7 +288,7 @@
 Goalw [Infinitesimal_def] "0 : Infinitesimal";
 by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
 qed "Infinitesimal_zero";
-Addsimps [Infinitesimal_zero];
+AddIffs [Infinitesimal_zero];
 
 Goalw [Infinitesimal_def] 
       "[| x : Infinitesimal; y : Infinitesimal |] ==> (x + y) : Infinitesimal";
@@ -466,7 +469,7 @@
 qed "Infinitesimal_interval2";
 
 Goalw [Infinitesimal_def] 
-      "!! x y. [| x ~: Infinitesimal; \
+      "[| x ~: Infinitesimal; \
 \                 y ~: Infinitesimal|] \
 \               ==> (x*y) ~:Infinitesimal";
 by (Clarify_tac 1);
@@ -480,17 +483,17 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
 qed "not_Infinitesimal_mult";
 
-Goal "!! x. x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
+Goal "x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
 by (rtac ccontr 1);
 by (dtac (de_Morgan_disj RS iffD1) 1);
 by (fast_tac (claset() addDs [not_Infinitesimal_mult]) 1);
 qed "Infinitesimal_mult_disj";
 
-Goal "!! x. x: HFinite-Infinitesimal ==> x ~= 0";
-by (fast_tac (claset() addIs [Infinitesimal_zero]) 1);
+Goal "x: HFinite-Infinitesimal ==> x ~= 0";
+by (Blast_tac 1);
 qed "HFinite_Infinitesimal_not_zero";
 
-Goal "!! x. [| x : HFinite - Infinitesimal; \
+Goal "[| x : HFinite - Infinitesimal; \
 \                  y : HFinite - Infinitesimal \
 \               |] ==> (x*y) : HFinite - Infinitesimal";
 by (Clarify_tac 1);
@@ -534,7 +537,7 @@
 by (Simp_tac 1);
 qed "inf_close_refl";
 
-Goalw [inf_close_def]  "!! x y. x @= y ==> y @= x";
+Goalw [inf_close_def]  "x @= y ==> y @= x";
 by (rtac (hypreal_minus_distrib1 RS subst) 1);
 by (etac (Infinitesimal_minus_iff RS iffD1) 1);
 qed "inf_close_sym";
@@ -570,7 +573,7 @@
     simpset() addsimps [inf_close_refl]));
 qed "inf_close_monad_iff";
 
-Goal "!!x y. [| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
+Goal "[| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
 by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
 by (fast_tac (claset() addIs [inf_close_trans2]) 1);
 qed "Infinitesimal_inf_close";
@@ -847,13 +850,12 @@
 
 Goal "[| x: SReal; x: Infinitesimal|] ==> x = 0";
 by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "SReal_Infinitesimal_zero";
 
-Goal "[| x : SReal; x ~= 0 |] \
-\              ==> x : HFinite - Infinitesimal";
+Goal "[| x : SReal; x ~= 0 |] ==> x : HFinite - Infinitesimal";
 by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
-          SReal_subset_HFinite RS subsetD],simpset()));
+                              SReal_subset_HFinite RS subsetD], simpset()));
 qed "SReal_HFinite_diff_Infinitesimal";
 
 Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
@@ -861,6 +863,14 @@
 by Auto_tac;
 qed "hypreal_of_real_HFinite_diff_Infinitesimal";
 
+Goal "(hypreal_of_real x : Infinitesimal) = (x=0)";
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));  
+by (rtac ccontr 1); 
+by (rtac (hypreal_of_real_HFinite_diff_Infinitesimal RS DiffD2) 1); 
+by Auto_tac;  
+qed "hypreal_of_real_Infinitesimal_iff_0";
+AddIffs [hypreal_of_real_Infinitesimal_iff_0];
+
 Goal "1hr+1hr ~: Infinitesimal";
 by (fast_tac (claset() addDs [SReal_two RS SReal_Infinitesimal_zero]
                        addSEs [hypreal_two_not_zero RS notE]) 1);
@@ -1220,10 +1230,15 @@
     simpset() addsimps [hypreal_mult_assoc]));
 qed "inf_close_inverse";
 
+(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
+bind_thm ("hypreal_of_real_inf_close_inverse",
+       hypreal_of_real_HFinite_diff_Infinitesimal RSN (2, inf_close_inverse));
+
 Goal "[| x: HFinite - Infinitesimal; \
-\                     h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
-by (auto_tac (claset() addIs [inf_close_inverse,
-    Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
+\        h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
+by (auto_tac (claset() addIs [inf_close_inverse, inf_close_sym, 
+                              Infinitesimal_add_inf_close_self], 
+              simpset()));
 qed "inverse_add_Infinitesimal_inf_close";
 
 Goal "[| x: HFinite - Infinitesimal; \
@@ -1293,7 +1308,7 @@
 by Auto_tac;
 qed "monad_hrabs_Un_subset";
 
-Goal "!! e. e : Infinitesimal ==> monad (x+e) = monad x";
+Goal "e : Infinitesimal ==> monad (x+e) = monad x";
 by (fast_tac (claset() addSIs [Infinitesimal_add_inf_close_self RS inf_close_sym,
     inf_close_monad_iff RS iffD1]) 1);
 qed "Infinitesimal_monad_eq";
@@ -1348,25 +1363,25 @@
 by (blast_tac (claset() addSIs [inf_close_sym]) 1);
 qed "inf_close_mem_monad2";
 
-Goal "!! x y. [| x @= y;x:monad 0 |] ==> y:monad 0";
+Goal "[| x @= y;x:monad 0 |] ==> y:monad 0";
 by (dtac mem_monad_inf_close 1);
 by (fast_tac (claset() addIs [inf_close_mem_monad,inf_close_trans]) 1);
 qed "inf_close_mem_monad_zero";
 
-Goal "!! x y. [| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
+Goal "[| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
 by (fast_tac (claset() addIs [(Infinitesimal_monad_zero_iff RS iffD1), 
     inf_close_mem_monad_zero,(monad_zero_hrabs_iff RS iffD1),
     mem_monad_inf_close,inf_close_trans3]) 1);
 qed "Infinitesimal_inf_close_hrabs";
 
-Goal "!! x. [| 0 < x; x ~:Infinitesimal |] \
+Goal "[| 0 < x; x ~:Infinitesimal |] \
 \     ==> ALL e: Infinitesimal. e < x";
 by (Step_tac 1 THEN rtac ccontr 1);
 by (auto_tac (claset() addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)] 
     addSDs [hypreal_leI RS hypreal_le_imp_less_or_eq],simpset()));
 qed "Ball_Infinitesimal_less";
 
-Goal "!! x. [| 0 < x; x ~: Infinitesimal|] \
+Goal "[| 0 < x; x ~: Infinitesimal|] \
 \     ==> ALL u: monad x. 0 < u";
 by (Step_tac 1);
 by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
@@ -1376,7 +1391,7 @@
 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
 qed "Ball_mem_monad_gt_zero";
 
-Goal "!! x. [| x < 0; x ~: Infinitesimal|] \
+Goal "[| x < 0; x ~: Infinitesimal|] \
 \     ==> ALL u: monad x. u < 0";
 by (Step_tac 1);
 by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
@@ -1460,12 +1475,11 @@
 by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_add_commute, 
-                                  hypreal_of_real_add, hrabs_interval_iff,
+                                  hrabs_interval_iff,
                                   SReal_add, SReal_minus]));
 by (dres_inst_tac [("x1","xa")] (hypreal_less_minus_iff RS iffD1) 1);
 by (auto_tac (claset(),
-        simpset() addsimps [hypreal_minus_add_distrib,hypreal_of_real_add] @ 
-                           hypreal_add_ac));
+        simpset() addsimps [hypreal_minus_add_distrib] @ hypreal_add_ac));
 qed "Infinitesimal_add_hypreal_of_real_less";
 
 Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
@@ -1501,51 +1515,49 @@
 qed "Infinitesimal_add_cancel_real_le";
 
 Goalw [hypreal_le_def]
-      "[| xa: Infinitesimal; ya: Infinitesimal; \
-\               hypreal_of_real x + xa <= hypreal_of_real y + ya \
-\            |] ==> hypreal_of_real x <= hypreal_of_real y";
+     "[| xa: Infinitesimal; ya: Infinitesimal; \
+\        hypreal_of_real x + xa <= hypreal_of_real y + ya |] \
+\     ==> hypreal_of_real x <= hypreal_of_real y";
 by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
 by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
 by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
 by (dtac Infinitesimal_add 1 THEN assume_tac 1);
 by (auto_tac (claset() addIs [Infinitesimal_add_hypreal_of_real_less],
-    simpset() addsimps [hypreal_add_assoc]));
+              simpset() addsimps [hypreal_add_assoc]));
 qed "hypreal_of_real_le_add_Infininitesimal_cancel";
 
 Goal "[| xa: Infinitesimal; ya: Infinitesimal; \
-\               hypreal_of_real x + xa <= hypreal_of_real y + ya \
-\            |] ==> x <= y";
+\        hypreal_of_real x + xa <= hypreal_of_real y + ya |] \
+\     ==> x <= y";
 by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
-               hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
+                          hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
 qed "hypreal_of_real_le_add_Infininitesimal_cancel2";
 
 Goal "[| hypreal_of_real x < e; e: Infinitesimal |] ==> hypreal_of_real x <= 0";
 by (rtac hypreal_leI 1 THEN Step_tac 1);
 by (dtac Infinitesimal_interval 1);
 by (dtac (SReal_hypreal_of_real RS SReal_Infinitesimal_zero) 4);
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
+by (auto_tac (claset(), 
+           simpset() addsimps [hypreal_of_real_zero, hypreal_less_not_refl]));
 qed "hypreal_of_real_less_Infinitesimal_le_zero";
 
-Goal "[| h: Infinitesimal; x ~= 0 |] \
-\                  ==> hypreal_of_real x + h ~= 0";
+(*used once, in NSDERIV_inverse*)
+Goal "[| h: Infinitesimal; x ~= 0 |] ==> hypreal_of_real x + h ~= 0";
 by (res_inst_tac [("t","h")] (hypreal_minus_minus RS subst) 1);
 by (rtac (not_sym RS (hypreal_not_eq_minus_iff RS iffD1)) 1);
 by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
-by (auto_tac (claset() addDs [((hypreal_of_real_not_zero_iff RS iffD2) RS
-          hypreal_of_real_HFinite_diff_Infinitesimal)],simpset()));
+by Auto_tac;  
 qed "Infinitesimal_add_not_zero";
 
 Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
 by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
-    Infinitesimal_interval2,hypreal_le_square,
-    Infinitesimal_zero]) 1);
+                 Infinitesimal_interval2, hypreal_le_square]) 1);
 qed "Infinitesimal_square_cancel";
 Addsimps [Infinitesimal_square_cancel];
 
 Goal "x*x + y*y : HFinite ==> x*x : HFinite";
 by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
-    HFinite_bounded,hypreal_le_square,
-    HFinite_zero]) 1);
+            HFinite_bounded,hypreal_le_square, HFinite_zero]) 1);
 qed "HFinite_square_cancel";
 Addsimps [HFinite_square_cancel];
 
@@ -1565,8 +1577,7 @@
 
 Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal";
 by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
-    Infinitesimal_interval2,hypreal_le_square,
-    Infinitesimal_zero]) 1);
+    Infinitesimal_interval2,hypreal_le_square]) 1);
 qed "Infinitesimal_sum_square_cancel";
 Addsimps [Infinitesimal_sum_square_cancel];
 
@@ -1654,7 +1665,7 @@
               addSEs [inf_close_trans3],simpset()));
 qed "st_eq_inf_close";
 
-Goal "!! x. [| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
+Goal "[| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
 by (EVERY1 [forward_tac [st_inf_close_self],
     forw_inst_tac [("x","y")] st_inf_close_self,
     dtac st_SReal,dtac st_SReal]);
@@ -1662,7 +1673,7 @@
     inf_close_trans2,SReal_inf_close_iff RS iffD1]) 1);
 qed "inf_close_st_eq";
 
-Goal "!! x y.  [| x: HFinite; y: HFinite|] \
+Goal "[| x: HFinite; y: HFinite|] \
 \                  ==> (x @= y) = (st x = st y)";
 by (blast_tac (claset() addIs [inf_close_st_eq,
                st_eq_inf_close]) 1);
@@ -1765,7 +1776,7 @@
 by (blast_tac (claset() addSIs [lemma_st_mult]) 1);
 qed "st_mult";
 
-Goal "!! x. st(x) ~= 0 ==> x ~=0";
+Goal "st(x) ~= 0 ==> x ~=0";
 by (fast_tac (claset() addIs [st_zero]) 1);
 qed "st_not_zero";
 
@@ -1776,7 +1787,7 @@
     RS subsetD],simpset() addsimps [mem_infmal_iff RS sym]));
 qed "st_Infinitesimal";
 
-Goal "!! x. st(x) ~= 0 ==> x ~: Infinitesimal";
+Goal "st(x) ~= 0 ==> x ~: Infinitesimal";
 by (fast_tac (claset() addIs [st_Infinitesimal]) 1);
 qed "st_not_Infinitesimal";
 
@@ -2050,27 +2061,26 @@
 Goal "(ALL r: SReal. 0 < r --> x < r) = \
 \     (ALL n. x < inverse(hypreal_of_posnat n))";
 by (Step_tac 1);
-by (dres_inst_tac [("x","hypreal_of_real (inverse(real_of_posnat n))")] bspec 1);
-by (Full_simp_tac 1);
+by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_posnat n))")] 
+    bspec 1);
+by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1); 
 by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS 
           (hypreal_of_real_less_iff RS iffD1) RSN(2,impE)) 1);
 by (assume_tac 2);
 by (asm_full_simp_tac (simpset() addsimps 
-       [hypreal_of_real_inverse RS sym,
-        rename_numerals real_of_posnat_gt_zero,hypreal_of_real_zero,
+       [rename_numerals real_of_posnat_gt_zero, hypreal_of_real_zero,
         hypreal_of_real_of_posnat]) 1);
 by (auto_tac (claset() addSDs [reals_Archimedean],
               simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
 by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
 by (asm_full_simp_tac (simpset() addsimps 
-       [hypreal_of_real_inverse RS sym,
-        rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
+       [rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
 by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
 qed "lemma_Infinitesimal2";
 
 Goalw [Infinitesimal_def] 
-      "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
-by (auto_tac (claset(),simpset() addsimps [lemma_Infinitesimal2]));
+     "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
+by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
 qed "Infinitesimal_hypreal_of_posnat_iff";
 
 (*-----------------------------------------------------------------------------
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/SEQ.ML
--- a/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -205,12 +205,12 @@
 Goalw [NSLIMSEQ_def]
       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
 by (auto_tac (claset() addIs [inf_close_add],
-    simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
+    simpset() addsimps [starfunNat_add RS sym]));
 qed "NSLIMSEQ_add";
 
 Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
 by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_add]) 1);
+                                           NSLIMSEQ_add]) 1);
 qed "LIMSEQ_add";
 
 Goalw [NSLIMSEQ_def]
@@ -273,14 +273,9 @@
      "[| X ----NS> a;  a ~= #0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
 by (Clarify_tac 1);
 by (dtac bspec 1);
-by (auto_tac (claset(),
-              simpset() addsimps [hypreal_of_real_not_zero_iff RS sym,
-                                  hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
-by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (stac (starfunNat_inverse RS sym) 1);
-by (auto_tac (claset() addSEs [inf_close_inverse],
-              simpset() addsimps [hypreal_of_real_zero_iff]));
+by (auto_tac (claset(), 
+              simpset() addsimps [starfunNat_inverse RS sym, 
+                                  hypreal_of_real_inf_close_inverse]));  
 qed "NSLIMSEQ_inverse";
 
 
@@ -1289,6 +1284,7 @@
 
 (* We now use NS criterion to bring proof of theorem through *)
 
+
 Goalw [NSLIMSEQ_def]
      "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
 by (auto_tac (claset() addSDs [convergent_realpow],
@@ -1305,7 +1301,8 @@
 by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
 by (dtac inf_close_trans3 1 THEN assume_tac 1);
 by (auto_tac (claset(),
-              simpset() addsimps [hypreal_of_real_mult RS sym]));
+              simpset() delsimps [hypreal_of_real_mult]
+			addsimps [hypreal_of_real_mult RS sym]));
 qed "NSLIMSEQ_realpow_zero";
 
 (*---------------  standard version ---------------*)
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -313,12 +313,17 @@
 
 Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)";
 by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], 
-    simpset() addsimps [sumr_mult RS sym]));
+              simpset() addsimps [sumr_mult RS sym]));
 qed "sums_mult";
 
-Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)";
+Goal "x sums x' ==> (%n. x(n)/c) sums (x'/c)";
+by (asm_simp_tac (simpset() addsimps [real_divide_def, sums_mult,
+                              inst "w" "inverse c" real_mult_commute]) 1); 
+qed "sums_divide";
+
+Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)";
 by (auto_tac (claset() addIs [LIMSEQ_diff],
-    simpset() addsimps [sumr_diff RS sym]));
+              simpset() addsimps [sumr_diff RS sym]));
 qed "sums_diff";
 
 Goal "summable f ==> suminf f * c = suminf(%n. f n * c)";
@@ -415,7 +420,7 @@
                     sum of geometric progression                 
  -------------------------------------------------------------------*)
 
-Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
+Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) / (x - #1)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
@@ -426,17 +431,18 @@
                            real_diff_def, real_mult_commute]));
 qed "sumr_geometric";
 
-Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)";
+Goal "abs(x) < #1 ==> (%n. x ^ n) sums (#1/(#1 - x))";
 by (case_tac "x = #1" 1);
 by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
-    simpset() addsimps [sumr_geometric,abs_one,sums_def,
-    real_diff_def,real_add_mult_distrib]));
-by (rtac (real_add_zero_left RS subst) 1);
-by (rtac (real_mult_0 RS subst) 1);
-by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
-by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps 
-    [real_minus_inverse RS sym,real_diff_def,real_add_commute,
-     rename_numerals LIMSEQ_rabs_realpow_zero2]));
+             simpset() addsimps [sumr_geometric ,abs_one, sums_def,
+                                 real_diff_def, real_add_divide_distrib]));
+by (subgoal_tac "#1 / (#1 + - x) = #0/(x-#1) + - #1/(x-#1)" 1);
+by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
+                 real_divide_minus_eq RS sym, real_diff_def]) 2); 
+by (etac ssubst 1); 
+by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
+by (auto_tac (claset() addIs [LIMSEQ_const], 
+              simpset() addsimps [real_diff_def, LIMSEQ_rabs_realpow_zero2]));
 qed "geometric_sums";
 
 (*-------------------------------------------------------------------
@@ -547,18 +553,6 @@
 qed "rabs_ratiotest_lemma";
 
 (* lemmas *)
-Goal "#0 < (r::real) ==> (x * r ^ n) * inverse (r ^ n) = x";
-by (auto_tac (claset(),simpset() addsimps 
-    [real_mult_assoc,rename_numerals realpow_not_zero]));
-val lemma_inverse_realpow = result();
-
-Goal "[| (c::real) ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\  ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (inverse(c ^ n)*abs(f n))";
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
-by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [rename_numerals  
-    realpow_not_zero]));
-val lemma_inverse_realpow2 = result();
 
 Goal "(k::nat) <= l ==> (EX n. l = k + n)";
 by (dtac le_imp_less_or_eq 1);
@@ -569,29 +563,38 @@
 by (auto_tac (claset(),simpset() addsimps [le_Suc_ex]));
 qed "le_Suc_ex_iff";
 
-Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\     ==> summable f";
-by (subgoal_tac "c <= #0 | #0 < c" 1 THEN Auto_tac);
+(*All this trouble just to get #0<c *)
+Goal "[| ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\     ==> #0 < c | summable f";
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 
 by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
 by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
 by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
 by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
 by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
-by (res_inst_tac [("g","%n. (abs (f N)* inverse(c ^ N))*c ^ n")] 
+qed "ratio_test_lemma2";
+
+
+Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\     ==> summable f";
+by (forward_tac [ratio_test_lemma2] 1);
+by Auto_tac;  
+by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")] 
     summable_comparison_test 1);
 by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
 by (dtac (le_Suc_ex_iff RS iffD1) 1);
 by (auto_tac (claset(),simpset() addsimps [realpow_add,
-    CLAIM_SIMP "(a * b) * (c * d) = (a * d) * (b * (c::real))" real_mult_ac,
     rename_numerals realpow_not_zero]));
 by (induct_tac "na" 1 THEN Auto_tac);
 by (res_inst_tac [("j","c*abs(f(N + n))")] real_le_trans 1);
 by (auto_tac (claset() addIs [real_mult_le_le_mono1],
-    simpset() addsimps [summable_def, CLAIM_SIMP 
-    "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
-by (res_inst_tac [("x","(abs(f N)*inverse(c ^ N))*inverse(#1 - c)")] exI 1);
-by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps 
-    [abs_eqI2]));
+    simpset() addsimps [summable_def]));
+by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
+by (res_inst_tac [("x","abs(f N) * (#1/(#1 - c)) / (c ^ N)")] exI 1);
+by (rtac sums_divide 1); 
+by (rtac sums_mult 1); 
+by (auto_tac (claset() addSIs [sums_mult,geometric_sums], 
+              simpset() addsimps [real_abs_def]));
 qed "ratio_test";
 
 
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/Hyperreal/Star.ML
--- a/src/HOL/Real/Hyperreal/Star.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -376,11 +376,7 @@
 by (auto_tac (claset(),
             simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
 qed "starfun_inverse_inverse";
-
-(* more specifically *)
-Goal "(*f* inverse) ehr = inverse (ehr)";
-by (rtac starfun_inverse_inverse 1);
-qed "starfun_inverse_epsilon";
+Addsimps [starfun_inverse_inverse];
 
 Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -457,13 +453,14 @@
    In this theory since hypreal_hrabs proved here. (To Check:) Maybe 
    move both if possible? 
  -------------------------------------------------------------------*)
-Goal "(x:Infinitesimal) = (EX X:Rep_hypreal(x). \
-\              ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
+Goal "(x:Infinitesimal) = \
+\     (EX X:Rep_hypreal(x). \
+\       ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
-    simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
-    hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
-    hypreal_hrabs,hypreal_less])); 
+	simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
+	    hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
+	    hypreal_hrabs,hypreal_less])); 
 by (dres_inst_tac [("x","n")] spec 1);
 by (Fuf_tac 1);
 qed  "Infinitesimal_FreeUltrafilterNat_iff2";
@@ -473,8 +470,9 @@
 \                 inverse(real_of_posnat m)} : FreeUltrafilterNat)";
 by (rtac (inf_close_minus_iff RS ssubst) 1);
 by (rtac (mem_infmal_iff RS subst) 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
-              hypreal_add,Infinitesimal_FreeUltrafilterNat_iff2]));
+by (auto_tac (claset(), 
+              simpset() addsimps [hypreal_minus, hypreal_add,
+                                  Infinitesimal_FreeUltrafilterNat_iff2]));
 by (dres_inst_tac [("x","m")] spec 1);
 by (Fuf_tac 1);
 qed "inf_close_FreeUltrafilterNat_iff";
diff -r 8666477dd9a2 -r 1ce5a189f672 src/HOL/Real/RealArith.ML
--- a/src/HOL/Real/RealArith.ML	Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/RealArith.ML	Thu Dec 21 18:08:10 2000 +0100
@@ -519,6 +519,11 @@
 qed "real_divide_minus1";
 Addsimps [real_divide_minus1];
 
+Goal "#-1/(x::real) = - (#1/x)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1); 
+qed "real_minus1_divide";
+Addsimps [real_minus1_divide];
+
 Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
 by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1); 
 by (asm_simp_tac (simpset() addsimps [min_def]) 1);