# HG changeset patch
# User paulson
# Date 1073142579 -3600
# Node ID 8f731d3cd65b2357ad753467c95aedcc9864f744
# Parent  9c0b5e081037edd90a8117dcc6a7cf0223c00cd5
Deleting more redundant theorems

diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Complex/ComplexArith0.ML
--- a/src/HOL/Complex/ComplexArith0.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Complex/ComplexArith0.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -5,66 +5,6 @@
 		 Also, common factor cancellation (see e.g. HyperArith0)
 *)
 
-(** Division and inverse **)
-
-Goal "0/x = (0::complex)";
-by (simp_tac (simpset() addsimps [complex_divide_def]) 1); 
-qed "complex_0_divide";
-Addsimps [complex_0_divide];
-
-Goalw [complex_divide_def] "x/(0::complex) = 0";
-by (stac COMPLEX_INVERSE_ZERO 1); 
-by (Simp_tac 1); 
-qed "COMPLEX_DIVIDE_ZERO";
-
-Goal "inverse (x::complex) = 1/x";
-by (simp_tac (simpset() addsimps [complex_divide_def]) 1); 
-qed "complex_inverse_eq_divide";
-
-Goal "(inverse(x::complex) = 0) = (x = 0)";
-by (auto_tac (claset(), 
-              simpset() addsimps [COMPLEX_INVERSE_ZERO]));  
-qed "complex_inverse_zero_iff";
-Addsimps [complex_inverse_zero_iff];
-
-Goal "(x/y = 0) = (x=0 | y=(0::complex))";
-by (auto_tac (claset(), simpset() addsimps [complex_divide_def]));  
-qed "complex_divide_eq_0_iff";
-Addsimps [complex_divide_eq_0_iff];
-
-Goal "h ~= (0::complex) ==> h/h = 1";
-by (asm_simp_tac 
-    (simpset() addsimps [complex_divide_def]) 1);
-qed "complex_divide_self_eq"; 
-Addsimps [complex_divide_self_eq];
-
-bind_thm ("complex_mult_minus_right", complex_minus_mult_eq2 RS sym);
-
-Goal "!!k::complex. (k*m = k*n) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [complex_mult_left_cancel]));  
-qed "complex_mult_eq_cancel1";
-
-Goal "!!k::complex. (m*k = n*k) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [complex_mult_right_cancel]));  
-qed "complex_mult_eq_cancel2";
-
-Goal "!!k::complex. k~=0 ==> (k*m) / (k*n) = (m/n)";
-by (asm_simp_tac
-    (simpset() addsimps [complex_divide_def, complex_inverse_distrib]) 1); 
-by (subgoal_tac "k * m * (inverse k * inverse n) = \
-\                (k * inverse k) * (m * inverse n)" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (HOL_ss addsimps complex_mult_ac) 1); 
-qed "complex_mult_div_cancel1";
-
-(*For ExtractCommonTerm*)
-Goal "(k*m) / (k*n) = (if k = (0::complex) then 0 else m/n)";
-by (simp_tac (simpset() addsimps [complex_mult_div_cancel1]) 1); 
-qed "complex_mult_div_cancel_disj";
-
-
 local
   open Complex_Numeral_Simprocs
 in
@@ -90,7 +30,7 @@
   val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   val dest_bal = HOLogic.dest_bin "HOL.divide" complexT
-  val cancel = complex_mult_div_cancel1 RS trans
+  val cancel = mult_divide_cancel_left RS trans
   val neg_exchanges = false
 )
 
@@ -100,7 +40,7 @@
   val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" complexT
-  val cancel = complex_mult_eq_cancel1 RS trans
+  val cancel = field_mult_cancel_left RS trans
   val neg_exchanges = false
 )
 
@@ -174,7 +114,7 @@
   val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" complexT
-  val simplify_meta_eq  = cancel_simplify_meta_eq complex_mult_eq_cancel1
+  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
 );
 
 
@@ -183,7 +123,7 @@
   val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   val dest_bal = HOLogic.dest_bin "HOL.divide" complexT
-  val simplify_meta_eq  = cancel_simplify_meta_eq complex_mult_div_cancel_disj
+  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
 );
 
 val complex_cancel_factor = 
@@ -220,45 +160,8 @@
 *)
 
 
-Goal "z~=0 ==> ((x::complex) = y/z) = (x*z = y)";
-by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [complex_divide_def, complex_mult_assoc]) 2); 
-by (etac ssubst 1);
-by (stac complex_mult_eq_cancel2 1); 
-by (Asm_simp_tac 1); 
-qed "complex_eq_divide_eq";
-Addsimps [inst "z" "number_of ?w" complex_eq_divide_eq];
-
-Goal "z~=0 ==> (y/z = (x::complex)) = (y = x*z)";
-by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [complex_divide_def, complex_mult_assoc]) 2); 
-by (etac ssubst 1);
-by (stac complex_mult_eq_cancel2 1); 
-by (Asm_simp_tac 1); 
-qed "complex_divide_eq_eq";
-Addsimps [inst "z" "number_of ?w" complex_divide_eq_eq];
-
-Goal "(m/k = n/k) = (k = 0 | m = (n::complex))";
-by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [COMPLEX_DIVIDE_ZERO]) 1); 
-by (asm_simp_tac (simpset() addsimps [complex_divide_eq_eq, complex_eq_divide_eq, 
-                                      complex_mult_eq_cancel2]) 1); 
-qed "complex_divide_eq_cancel2";
-
-Goal "(k/m = k/n) = (k = 0 | m = (n::complex))";
-by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [COMPLEX_DIVIDE_ZERO, complex_divide_eq_eq, 
-                                  complex_eq_divide_eq, complex_mult_eq_cancel1]));  
-qed "complex_divide_eq_cancel1";
-
 (** Division by 1, -1 **)
 
-Goal "(x::complex)/1 = x";
-by (simp_tac (simpset() addsimps [complex_divide_def]) 1); 
-qed "complex_divide_1";
-Addsimps [complex_divide_1];
-
 Goal "x/-1 = -(x::complex)";
 by (Simp_tac 1); 
 qed "complex_divide_minus1";
@@ -269,34 +172,11 @@
 qed "complex_minus1_divide";
 Addsimps [complex_minus1_divide];
 
-
-Goal "(x = - y) = (y = - (x::complex))";
-by Auto_tac;
-qed "complex_equation_minus";
-
-Goal "(- x = y) = (- (y::complex) = x)";
-by Auto_tac;
-qed "complex_minus_equation";
-
 Goal "(x + - a = (0::complex)) = (x=a)";
 by (simp_tac (simpset() addsimps [complex_diff_eq_eq,symmetric complex_diff_def]) 1);
 qed "complex_add_minus_iff";
 Addsimps [complex_add_minus_iff];
 
-Goal "(-b = -a) = (b = (a::complex))";
-by Auto_tac;
-qed "complex_minus_eq_cancel";
-Addsimps [complex_minus_eq_cancel];
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
-	  [complex_add_mult_distrib, complex_add_mult_distrib2,
-	   complex_diff_mult_distrib, complex_diff_mult_distrib2]);
-
-Addsimps [inst "x" "number_of ?v" complex_equation_minus];
-
-Addsimps [inst "y" "number_of ?v" complex_minus_equation];
-
 Goal "(x+y = (0::complex)) = (y = -x)";
 by Auto_tac;
 by (dtac (sym RS (complex_diff_eq_eq RS iffD2)) 1);
@@ -304,10 +184,4 @@
 qed "complex_add_eq_0_iff";
 AddIffs [complex_add_eq_0_iff];
 
-Goalw [complex_diff_def]"-(x-y) = y - (x::complex)";
-by (auto_tac (claset(),simpset() addsimps [complex_add_commute]));
-qed "complex_minus_diff_eq";
-Addsimps [complex_minus_diff_eq];
 
-Addsimps [inst "x" "number_of ?w" complex_inverse_eq_divide];
-
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Sat Jan 03 16:09:39 2004 +0100
@@ -1733,11 +1733,12 @@
 lemma hcomplex_of_complex_inverse:
      "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
 apply (case_tac "r=0")
-apply (simp (no_asm_simp) add: COMPLEX_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO hcomplex_of_complex_zero COMPLEX_DIVIDE_ZERO)
-apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1])
+apply (simp add: hcomplex_of_complex_zero)
+apply (rule_tac c1 = "hcomplex_of_complex r" 
+       in hcomplex_mult_left_cancel [THEN iffD1])
 apply (force simp add: hcomplex_of_complex_zero_iff)
 apply (subst hcomplex_of_complex_mult [symmetric])
-apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff); 
+apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
 done
 declare hcomplex_of_complex_inverse [simp]
 
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Hyperreal/HRealAbs.ML
--- a/src/HOL/Hyperreal/HRealAbs.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -23,16 +23,6 @@
    (adapted version of previously proved theorems about abs)
  ------------------------------------------------------------*)
 
-Goal "abs (0::hypreal) = 0";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
-qed "hrabs_zero";
-Addsimps [hrabs_zero];
-
-Goal "abs (1::hypreal) = 1";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
-qed "hrabs_one";
-Addsimps [hrabs_one];
-
 Goal "(0::hypreal)<=x ==> abs x = x";
 by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); 
 qed "hrabs_eqI1";
@@ -48,78 +38,14 @@
 Goal "x<=(0::hypreal) ==> abs x = -x";
 by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def]));qed "hrabs_minus_eqI1";
 
-Goal "(0::hypreal)<= abs x";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
-qed "hrabs_ge_zero";
-
-Goal "abs(abs x) = abs (x::hypreal)";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
-qed "hrabs_idempotent";
-Addsimps [hrabs_idempotent];
-
-Goalw [hrabs_def] "(abs x = (0::hypreal)) = (x=0)";
-by (Simp_tac 1);
-qed "hrabs_zero_iff";
-AddIffs [hrabs_zero_iff];
-
-Goalw [hrabs_def] "(x::hypreal) <= abs x";
-by (Simp_tac 1); 
-qed "hrabs_ge_self";
-
-Goalw [hrabs_def] "-(x::hypreal) <= abs x";
-by (Simp_tac 1);
-qed "hrabs_ge_minus_self";
-
-(* proof by "transfer" *)
-Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)";  
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult]));
-qed "hrabs_mult";
-Addsimps [hrabs_mult];
-
-Goal "abs(inverse(x)) = inverse(abs(x::hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_minus_inverse, hrabs_def]) 1);  
-qed "hrabs_inverse";
-
-Goalw [hrabs_def] "abs(x+(y::hypreal)) <= abs x + abs y"; 
-by (Simp_tac 1);
-qed "hrabs_triangle_ineq";
-
-Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)";
-by (simp_tac (simpset() addsimps [hrabs_triangle_ineq RS order_trans]) 1);
-qed "hrabs_triangle_ineq_three";
-
-Goalw [hrabs_def] "abs(-x) = abs((x::hypreal))";
-by (Simp_tac 1);
-qed "hrabs_minus_cancel";
-Addsimps [hrabs_minus_cancel];
+Addsimps [abs_mult];
 
 Goalw [hrabs_def] "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)";
 by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); 
 qed "hrabs_add_less";
 
-Goal "[| abs x<r;  abs y<s |] ==> abs x * abs y < r * (s::hypreal)";
-by (subgoal_tac "0 < r" 1);
-by (asm_full_simp_tac (simpset() addsimps [hrabs_def] 
-                                 addsplits [split_if_asm]) 2); 
-by (case_tac "y = 0" 1);
-by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); 
-by (rtac hypreal_mult_less_mono 1); 
-by (auto_tac (claset(), 
-              simpset() addsimps [hrabs_def, linorder_neq_iff] 
-                        addsplits [split_if_asm])); 
-qed "hrabs_mult_less";
-
-Goal "((0::hypreal) < abs x) = (x ~= 0)";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1);
-by (arith_tac 1);
-qed "hypreal_0_less_abs_iff";
-Addsimps [hypreal_0_less_abs_iff];
-
 Goal "abs x < r ==> (0::hypreal) < r";
-by (blast_tac (claset() addSIs [order_le_less_trans, hrabs_ge_zero]) 1);
+by (blast_tac (claset() addSIs [order_le_less_trans, abs_ge_zero]) 1);
 qed "hrabs_less_gt_zero";
 
 Goal "abs x = (x::hypreal) | abs x = -x";
@@ -131,25 +57,12 @@
                                  addsplits [split_if_asm]) 1); 
 qed "hrabs_eq_disj";
 
-Goalw [hrabs_def] "(abs x < (r::hypreal)) = (-r < x & x < r)";
-by Auto_tac; 
-qed "hrabs_interval_iff";
-
-Goal "(abs x < (r::hypreal)) = (- x < r & x < r)";
-by (auto_tac (claset(),  simpset() addsimps [hrabs_interval_iff]));
-qed "hrabs_interval_iff2";
-
-
 (* Needed in Geom.ML *)
 Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y";
 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] 
                                  addsplits [split_if_asm]) 1); 
 qed "hrabs_add_lemma_disj";
 
-Goal "abs((x::hypreal) + -y) = abs (y + -x)";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
-qed "hrabs_minus_add_cancel";
-
 (* Needed in Geom.ML?? *)
 Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y";
 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] 
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Hyperreal/HyperPow.ML
--- a/src/HOL/Hyperreal/HyperPow.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -23,7 +23,7 @@
 
 Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [hrabs_mult]));
+by Auto_tac;
 qed "hrealpow_hrabs";
 
 Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
@@ -507,7 +507,7 @@
      "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
 by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
               simpset() addsimps [hyperpow_hrabs RS sym,
-                                  hypnat_gt_zero_iff2, hrabs_ge_zero]));
+                                  hypnat_gt_zero_iff2, abs_ge_zero]));
 qed "lemma_Infinitesimal_hyperpow";
 
 Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Hyperreal/Integration.ML
--- a/src/HOL/Hyperreal/Integration.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/Integration.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -474,7 +474,7 @@
          (real_mult_le_cancel_iff2 RS iffD1) 2);
 by (Asm_full_simp_tac 2);
 by (asm_full_simp_tac (simpset() 
-     delsimps [abs_inverse]
+     delsimps [abs_inverse, abs_mult]
      addsimps [abs_mult RS sym, real_mult_assoc RS sym]) 2);
 by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \
 \                (f z - f x)/(z - x) - f' x" 2);
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Hyperreal/NSA.ML
--- a/src/HOL/Hyperreal/NSA.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -216,7 +216,7 @@
 
 Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> x*y : HFinite";
 by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
+by (blast_tac (claset() addSIs [SReal_mult,abs_mult_less]) 1);
 qed "HFinite_mult";
 
 Goalw [HFinite_def] "(-x : HFinite) = (x : HFinite)";
@@ -243,7 +243,7 @@
 qed "HFiniteD";
 
 Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)";
-by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
+by Auto_tac;
 qed "HFinite_hrabs_iff";
 AddIffs [HFinite_hrabs_iff];
 
@@ -284,7 +284,7 @@
 qed "InfinitesimalD";
 
 Goalw [Infinitesimal_def] "0 : Infinitesimal";
-by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
+by (Simp_tac 1);
 qed "Infinitesimal_zero";
 AddIffs [Infinitesimal_zero];
 
@@ -424,9 +424,7 @@
 
 Goalw [Infinitesimal_def]
       "[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
-by (auto_tac (claset() addSDs [bspec], simpset()));
-by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
-by (fast_tac (claset() addIs [order_less_trans]) 1);
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
 qed "hrabs_less_Infinitesimal";
 
 Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
@@ -438,10 +436,7 @@
       "[| e : Infinitesimal; \
 \         e' : Infinitesimal; \
 \         e' < x ; x < e |] ==> x : Infinitesimal";
-by (auto_tac (claset() addSDs [bspec], simpset()));
-by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
-by (dtac (hrabs_interval_iff RS iffD1) 1);
-by (fast_tac(claset() addIs [order_less_trans,hrabs_interval_iff RS iffD2]) 1);
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
 qed "Infinitesimal_interval";
 
 Goal "[| e : Infinitesimal; e' : Infinitesimal; \
@@ -819,7 +814,7 @@
 
 Goalw [Infinitesimal_def]
      "[| x: Reals; y: Infinitesimal; 0 < x |] ==> y < x";
-by (rtac (hrabs_ge_self RS order_le_less_trans) 1);
+by (rtac (abs_ge_self RS order_le_less_trans) 1);
 by Auto_tac;
 qed "Infinitesimal_less_SReal";
 
@@ -991,15 +986,14 @@
 Goal "x: HFinite ==> EX u. isUb Reals {s. s: Reals & s < x} u";
 by (dtac HFiniteD 1 THEN Step_tac 1);
 by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
-by (auto_tac (claset() addIs [order_less_imp_le,setleI,isUbI,
-    order_less_trans], simpset() addsimps [hrabs_interval_iff]));
+by (auto_tac (claset() addIs [setleI,isUbI], simpset() addsimps [abs_less_iff]));
 qed "lemma_st_part_ub";
 
 Goal "x: HFinite ==> EX y. y: {s. s: Reals & s < x}";
 by (dtac HFiniteD 1 THEN Step_tac 1);
 by (dtac SReal_minus 1);
 by (res_inst_tac [("x","-t")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
 qed "lemma_st_part_nonempty";
 
 Goal "{s. s: Reals & s < x} <= Reals";
@@ -1135,8 +1129,8 @@
 by (ftac lemma_st_part2a 4);
 by Auto_tac;
 by (REPEAT(dtac order_le_imp_less_or_eq 1));
-by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
-    lemma_st_part_not_eq2], simpset() addsimps [hrabs_interval_iff2]));
+by (auto_tac (claset() addDs [lemma_st_part_not_eq1, lemma_st_part_not_eq2],
+         simpset() addsimps [abs_less_iff]));
 qed "lemma_st_part_major";
 
 Goal "[| x: HFinite; \
@@ -1490,7 +1484,7 @@
 by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_add_commute,
-                                  hrabs_interval_iff,
+                                  abs_less_iff,
                                   SReal_add, SReal_minus]));
 qed "Infinitesimal_add_hypreal_of_real_less";
 
@@ -1900,28 +1894,27 @@
 Goalw [HFinite_def]
     "x : HFinite ==> EX X: Rep_hypreal x. \
 \    EX u. {n. abs (X n) < u}:  FreeUltrafilterNat";
-by (auto_tac (claset(), simpset() addsimps
-    [hrabs_interval_iff]));
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
 by (auto_tac (claset(), simpset() addsimps
     [hypreal_less_def,SReal_iff,hypreal_minus,
      hypreal_of_real_def]));
 by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
-by (res_inst_tac [("x","Y")] bexI 1 THEN assume_tac 2);
+by (rename_tac "Z" 1);
+by (res_inst_tac [("x","Z")] bexI 1 THEN assume_tac 2);
 by (res_inst_tac [("x","y")] exI 1);
-by (Ultra_tac 1 THEN arith_tac 1);
+by (Ultra_tac 1);
 qed "HFinite_FreeUltrafilterNat";
 
 Goalw [HFinite_def]
      "EX X: Rep_hypreal x. \
 \      EX u. {n. abs (X n) < u}: FreeUltrafilterNat\
 \      ==>  x : HFinite";
-by (auto_tac (claset(), simpset() addsimps
-    [hrabs_interval_iff]));
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
 by (res_inst_tac [("x","hypreal_of_real u")] bexI 1);
-by (auto_tac (claset() addSIs [exI], simpset() addsimps
-    [hypreal_less_def,SReal_iff,hypreal_minus,
-     hypreal_of_real_def]));
-by (ALLGOALS(Ultra_tac THEN' arith_tac));
+by (auto_tac (claset() addSIs [exI], 
+   simpset() addsimps
+    [hypreal_less_def,SReal_iff,hypreal_minus, hypreal_of_real_def]));
+by (ALLGOALS Ultra_tac);
 qed "FreeUltrafilterNat_HFinite";
 
 Goal "(x : HFinite) = (EX X: Rep_hypreal x. \
@@ -2026,7 +2019,7 @@
 Goalw [Infinitesimal_def]
           "x : Infinitesimal ==> EX X: Rep_hypreal x. \
 \          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat";
-by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
+by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (EVERY[Auto_tac, rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
 by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
@@ -2035,7 +2028,7 @@
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_less_def, hypreal_minus,
                                   hypreal_of_real_def]));
-by (Ultra_tac 1 THEN arith_tac 1);
+by (Ultra_tac 1);
 qed "Infinitesimal_FreeUltrafilterNat";
 
 Goalw [Infinitesimal_def]
@@ -2043,7 +2036,7 @@
 \           ALL u. 0 < u --> {n. abs (X n) < u} : FreeUltrafilterNat \
 \     ==> x : Infinitesimal";
 by (auto_tac (claset(),
-              simpset() addsimps [hrabs_interval_iff,abs_interval_iff]));
+              simpset() addsimps [abs_less_iff,abs_interval_iff, inst "a" "x" minus_less_iff]));
 by (auto_tac (claset(),
               simpset() addsimps [SReal_iff]));
 by (auto_tac (claset() addSIs [exI]
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -439,10 +439,6 @@
 (* i.e. if it sums for x, then it sums absolutely for z with |z| < |x|.     *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [real_divide_def] "1/(x::real) = inverse x";
-by (Simp_tac 1);
-qed "real_divide_eq_inverse";
-
 Goal "[| summable (%n. f(n) * (x ^ n)); abs(z) < abs(x) |] \
 \     ==> summable (%n. abs(f(n)) * (z ^ n))";
 by (dtac summable_LIMSEQ_zero 1);
@@ -458,7 +454,7 @@
 by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP 
     "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [mult_le_cancel_left]) 1);
 by (auto_tac (claset(),
-    simpset() addsimps [real_mult_assoc,realpow_abs]));
+    simpset() addsimps [mult_assoc,realpow_abs]));
 by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); 
 by (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ mult_ac));
 by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
@@ -466,29 +462,28 @@
 by (auto_tac (claset() addSIs [mult_right_mono],
     simpset() addsimps [mult_assoc RS sym, realpow_abs,summable_def]));
 by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1);
-by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [real_mult_assoc]));
+by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [mult_assoc]));
 by (subgoal_tac 
     "abs(z ^ n) * inverse(abs x ^ n) = (abs(z) * inverse(abs x)) ^ n" 1);
 by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym]));
 by (subgoal_tac "x ~= 0" 1);
 by (subgoal_tac "x ~= 0" 3);
 by (auto_tac (claset(),
-     simpset() delsimps [abs_inverse]
+     simpset() delsimps [abs_inverse, abs_mult]
       addsimps [abs_inverse RS sym, realpow_not_zero, abs_mult RS sym,
     realpow_inverse, realpow_mult RS sym]));
 by (auto_tac (claset() addSIs [geometric_sums],
-   simpset() addsimps
-    [realpow_abs,real_divide_eq_inverse RS sym]));
+       simpset() addsimps [realpow_abs, inverse_eq_divide]));
 by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP 
     "[|(0::real)<z; x*z<y*z |] ==> x<y" [mult_less_cancel_left]) 1);
-by (auto_tac (claset(),simpset() addsimps [abs_mult RS sym,real_mult_assoc]));
+by (auto_tac (claset(),simpset() addsimps [abs_mult RS sym,mult_assoc]));
 qed "powser_insidea";
 
 Goal "[| summable (%n. f(n) * (x ^ n)); abs(z) < abs(x) |] \
 \     ==> summable (%n. f(n) * (z ^ n))";
 by (dres_inst_tac [("z","abs z")] powser_insidea 1);
 by (auto_tac (claset() addIs [summable_rabs_cancel],
-    simpset() addsimps [realpow_abs RS sym,abs_mult RS sym]));
+    simpset() addsimps [realpow_abs RS sym]));
 qed "powser_inside";
 
 (* ------------------------------------------------------------------------ *)
diff -r 9c0b5e081037 -r 8f731d3cd65b src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -217,8 +217,7 @@
              inst "a" "(number_of ?v)::real" right_distrib,
              divide_1,times_divide_eq_right,times_divide_eq_left];
 
-val simprocs = [real_cancel_numeral_factors_divide,
-                real_cancel_numeral_factors_divide];
+val simprocs = [real_cancel_numeral_factors_divide];
 
 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;