# HG changeset patch
# User paulson
# Date 1071304432 -3600
# Node ID f4d806fd72ced144042d764b310159118845c2f1
# Parent  22542982bffd1e0ca0d74786fa2f5bc7bb03c06c
absolute value theorems moved to HOL/Ring_and_Field

diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/HyperNat.ML
--- a/src/HOL/Hyperreal/HyperNat.ML	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML	Sat Dec 13 09:33:52 2003 +0100
@@ -1317,8 +1317,6 @@
 by Auto_tac;
 by (dres_inst_tac [("x","m + 1")] spec 1);
 by (Ultra_tac 1);
-by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
-by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
 qed "HNatInfinite_inverse_Infinitesimal";
 Addsimps [HNatInfinite_inverse_Infinitesimal];
 
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Integration.ML
--- a/src/HOL/Hyperreal/Integration.ML	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Hyperreal/Integration.ML	Sat Dec 13 09:33:52 2003 +0100
@@ -398,7 +398,7 @@
     simpset()));
 by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def,
     sumr_mult RS sym,real_mult_assoc]));
-by (res_inst_tac [("x2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq)
+by (res_inst_tac [("a2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq)
     RS disjE) 1);
 by (dtac sym 2);
 by (Asm_full_simp_tac 2 THEN Blast_tac 2);
@@ -470,8 +470,9 @@
 by (res_inst_tac [("z1","abs(inverse(z - x))")] 
          (real_mult_le_cancel_iff2 RS iffD1) 2);
 by (Asm_full_simp_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym,
-    real_mult_assoc RS sym]) 2);
+by (asm_full_simp_tac (simpset() 
+     delsimps [abs_inverse]
+     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);
 by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ real_mult_ac) 2);
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Sat Dec 13 09:33:52 2003 +0100
@@ -132,7 +132,7 @@
 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) 
     THEN step_tac (claset() addSEs [order_less_trans]) 3);
 by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst)));
-by (ALLGOALS(rtac abs_mult_less2));
+by (ALLGOALS(rtac abs_mult_less));
 by Auto_tac;
 qed "LIM_mult_zero";
 
@@ -1665,7 +1665,7 @@
 by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1);
 by Safe_tac;
 by (dres_inst_tac [("x","ba - x")] spec 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [thm"abs_if"])));
 by (dres_inst_tac [("x","aa - x")] spec 1);
 by (case_tac "x \\<le> aa" 1);
 by (ALLGOALS Asm_full_simp_tac);
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Sat Dec 13 09:33:52 2003 +0100
@@ -461,7 +461,7 @@
     simpset() addsimps [real_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] @ real_mult_ac));
-by (res_inst_tac [("x2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
+by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
     RS disjE) 1 THEN dtac sym 2);
 by (auto_tac (claset() addSIs [real_mult_le_le_mono2],
     simpset() addsimps [real_mult_assoc RS sym,
@@ -473,10 +473,12 @@
 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() 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
+by (auto_tac (claset(),
+     simpset() delsimps [abs_inverse]
+      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]));
 by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP 
     "[|(0::real)<z; x*z<y*z |] ==> x<y" [real_mult_less_cancel1]) 1);
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Integ/Int.thy	Sat Dec 13 09:33:52 2003 +0100
@@ -243,6 +243,12 @@
 lemma abs_int_eq [simp]: "abs (int m) = int m"
 by (simp add: zabs_def)
 
+text{*This version is proved for all ordered rings, not just integers!
+      But is it really better than just rewriting with @{text abs_if}?*}
+lemma abs_split [arith_split]:
+     "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
 
 subsection{*Misc Results*}
 
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Real/RealArith.thy
--- a/src/HOL/Real/RealArith.thy	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Real/RealArith.thy	Sat Dec 13 09:33:52 2003 +0100
@@ -9,7 +9,7 @@
 
 text{*Needed in this non-standard form by Hyperreal/Transcendental*}
 lemma real_0_le_divide_iff:
-     "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"
+     "((0::real) \<le> x/y) = ((x \<le> 0 | 0 \<le> y) & (0 \<le> x | y \<le> 0))"
 by (simp add: real_divide_def zero_le_mult_iff, auto)
 
 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
@@ -76,8 +76,6 @@
 
 subsection{*Absolute Value Function for the Reals*}
 
-(** abs (absolute value) **)
-
 lemma abs_nat_number_of: 
      "abs (number_of v :: real) =  
         (if neg (number_of v) then number_of (bin_minus v)  
@@ -87,30 +85,14 @@
 
 declare abs_nat_number_of [simp]
 
-lemma abs_split [arith_split]: 
-  "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))"
-apply (unfold real_abs_def, auto)
-done
-
 
 (*----------------------------------------------------------------------------
        Properties of the absolute value function over the reals
        (adapted version of previously proved theorems about abs)
  ----------------------------------------------------------------------------*)
 
-lemma abs_iff: "abs (r::real) = (if 0<=r then r else -r)"
-apply (unfold real_abs_def, auto)
-done
-
-lemma abs_zero: "abs 0 = (0::real)"
-by (unfold real_abs_def, auto)
-declare abs_zero [simp]
-
-lemma abs_one: "abs (1::real) = 1"
-by (unfold real_abs_def, simp)
-declare abs_one [simp]
-
-lemma abs_eqI1: "(0::real)<=x ==> abs x = x"
+text{*FIXME: these should go!*}
+lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
 by (unfold real_abs_def, simp)
 
 lemma abs_eqI2: "(0::real) < x ==> abs x = x"
@@ -119,103 +101,37 @@
 lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
 by (unfold real_abs_def real_le_def, simp)
 
-lemma abs_minus_eqI1: "x<=(0::real) ==> abs x = -x"
-by (unfold real_abs_def, simp)
-
-lemma abs_ge_zero: "(0::real)<= abs x"
-by (unfold real_abs_def, simp)
-declare abs_ge_zero [simp]
-
-lemma abs_idempotent: "abs(abs x)=abs (x::real)"
-by (unfold real_abs_def, simp)
-declare abs_idempotent [simp]
-
-lemma abs_zero_iff: "(abs x = 0) = (x=(0::real))"
-by (unfold real_abs_def, simp)
-declare abs_zero_iff [iff]
-
-lemma abs_ge_self: "x<=abs (x::real)"
-by (unfold real_abs_def, simp)
-
-lemma abs_ge_minus_self: "-x<=abs (x::real)"
-by (unfold real_abs_def, simp)
-
-lemma abs_mult: "abs (x * y) = abs x * abs (y::real)"
-apply (unfold real_abs_def)
-apply (auto dest!: order_antisym simp add: real_0_le_mult_iff)
-done
-
-lemma abs_inverse: "abs(inverse(x::real)) = inverse(abs(x))"
-apply (unfold real_abs_def)
-apply (case_tac "x=0")
-apply (auto simp add: real_minus_inverse real_le_less INVERSE_ZERO real_inverse_gt_0)
-done
-
 lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"
 by (simp add: abs_mult abs_inverse)
 
-lemma abs_triangle_ineq: "abs(x+y) <= abs x + abs (y::real)"
+text{*Much easier to prove using arithmetic than abstractly!!*}
+lemma abs_triangle_ineq: "abs(x+y) \<le> abs x + abs (y::real)"
 by (unfold real_abs_def, simp)
 
 (*Unused, but perhaps interesting as an example*)
-lemma abs_triangle_ineq_four: "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"
+lemma abs_triangle_ineq_four: "abs(w + x + y + z) \<le> abs(w) + abs(x) + abs(y) + abs(z::real)"
 by (simp add: abs_triangle_ineq [THEN order_trans])
 
-lemma abs_minus_cancel: "abs(-x)=abs(x::real)"
-by (unfold real_abs_def, simp)
-declare abs_minus_cancel [simp]
-
 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
 by (unfold real_abs_def, simp)
 
-lemma abs_triangle_minus_ineq: "abs(x + (-y)) <= abs x + abs (y::real)"
+lemma abs_triangle_minus_ineq: "abs(x + (-y)) \<le> abs x + abs (y::real)"
 by (unfold real_abs_def, simp)
 
 lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"
 by (unfold real_abs_def, simp)
 
-lemma abs_add_minus_less: "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
+lemma abs_add_minus_less:
+     "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
 by (unfold real_abs_def, simp)
 
-(* lemmas manipulating terms *)
-lemma real_mult_0_less: "((0::real)*x < r)=(0 < r)"
-by simp
-
-lemma real_mult_less_trans: "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s"
-by (blast intro!: real_mult_less_mono2 intro: order_less_trans)
-
-(*USED ONLY IN NEXT THM*)
-lemma real_mult_le_less_trans:
-     "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s"
-apply (drule order_le_imp_less_or_eq)
-apply (fast  elim: real_mult_0_less [THEN iffD2] real_mult_less_trans) 
-done
-
-lemma abs_mult_less: "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)"
-apply (simp add: abs_mult)
-apply (rule real_mult_le_less_trans)
-apply (rule abs_ge_zero, assumption)
-apply (rule_tac [2] real_mult_order)
-apply (auto intro!: real_mult_less_mono1 abs_ge_zero intro: order_le_less_trans)
-done
-
-lemma abs_mult_less2: "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)"
-by (auto intro: abs_mult_less simp add: abs_mult [symmetric])
-
-lemma abs_less_gt_zero: "abs(x) < r ==> (0::real) < r"
-by (blast intro!: order_le_less_trans abs_ge_zero)
-
-lemma abs_minus_one: "abs (-1) = (1::real)"
+lemma abs_minus_one [simp]: "abs (-1) = (1::real)"
 by (unfold real_abs_def, simp)
-declare abs_minus_one [simp]
-
-lemma abs_disj: "abs x =x | abs x = -(x::real)"
-by (unfold real_abs_def, auto)
 
 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
 by (unfold real_abs_def, auto)
 
-lemma abs_le_interval_iff: "(abs x <= r) = (-r<=x & x<=(r::real))"
+lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
 by (unfold real_abs_def, auto)
 
 lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)"
@@ -225,21 +141,9 @@
 by (unfold real_abs_def, auto)
 declare abs_add_one_gt_zero [simp]
 
-lemma abs_not_less_zero: "~ abs x < (0::real)"
-by (unfold real_abs_def, auto)
-declare abs_not_less_zero [simp]
-
 lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"
 by (auto intro: abs_triangle_ineq [THEN order_le_less_trans])
 
-lemma abs_le_zero_iff: "(abs x <= (0::real)) = (x = 0)"
-by (unfold real_abs_def, auto)
-declare abs_le_zero_iff [simp]
-
-lemma real_0_less_abs_iff: "((0::real) < abs x) = (x ~= 0)"
-by (simp add: real_abs_def, arith)
-declare real_0_less_abs_iff [simp]
-
 lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)"
 by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
 declare abs_real_of_nat_cancel [simp]
@@ -251,18 +155,18 @@
 declare abs_add_one_not_less_self [simp]
  
 (* used in vector theory *)
-lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"
+lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) \<le> abs(w) + abs(x) + abs(y)"
 by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono
                  simp add: real_add_assoc)
 
 lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y"
 apply (unfold real_abs_def)
-apply (case_tac "0 <= x - y", auto)
+apply (case_tac "0 \<le> x - y", auto)
 done
 
 lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x"
 apply (unfold real_abs_def)
-apply (case_tac "0 <= x - y", auto)
+apply (case_tac "0 \<le> x - y", auto)
 done
 
 lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x"
@@ -272,11 +176,11 @@
 by (auto simp add: abs_interval_iff)
 
 lemma abs_triangle_ineq_minus_cancel: 
-     "abs(x) <= abs(x + (-y)) + abs((y::real))"
+     "abs(x) \<le> abs(x + (-y)) + abs((y::real))"
 apply (unfold real_abs_def, auto)
 done
 
-lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"
+lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 apply (simp add: real_add_assoc)
 apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst])
 apply (rule real_add_assoc [THEN subst])
@@ -305,13 +209,10 @@
 
 val abs_nat_number_of = thm"abs_nat_number_of";
 val abs_split = thm"abs_split";
-val abs_iff = thm"abs_iff";
 val abs_zero = thm"abs_zero";
-val abs_one = thm"abs_one";
 val abs_eqI1 = thm"abs_eqI1";
 val abs_eqI2 = thm"abs_eqI2";
 val abs_minus_eqI2 = thm"abs_minus_eqI2";
-val abs_minus_eqI1 = thm"abs_minus_eqI1";
 val abs_ge_zero = thm"abs_ge_zero";
 val abs_idempotent = thm"abs_idempotent";
 val abs_zero_iff = thm"abs_zero_iff";
@@ -327,22 +228,13 @@
 val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq";
 val abs_add_less = thm"abs_add_less";
 val abs_add_minus_less = thm"abs_add_minus_less";
-val real_mult_0_less = thm"real_mult_0_less";
-val real_mult_less_trans = thm"real_mult_less_trans";
-val real_mult_le_less_trans = thm"real_mult_le_less_trans";
-val abs_mult_less = thm"abs_mult_less";
-val abs_mult_less2 = thm"abs_mult_less2";
-val abs_less_gt_zero = thm"abs_less_gt_zero";
 val abs_minus_one = thm"abs_minus_one";
-val abs_disj = thm"abs_disj";
 val abs_interval_iff = thm"abs_interval_iff";
 val abs_le_interval_iff = thm"abs_le_interval_iff";
 val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero";
 val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
-val abs_not_less_zero = thm"abs_not_less_zero";
 val abs_circle = thm"abs_circle";
 val abs_le_zero_iff = thm"abs_le_zero_iff";
-val real_0_less_abs_iff = thm"real_0_less_abs_iff";
 val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel";
 val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
 val abs_triangle_ineq_three = thm"abs_triangle_ineq_three";
@@ -352,6 +244,8 @@
 val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4";
 val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel";
 val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
+
+val abs_mult_less = thm"abs_mult_less";
 *}
 
 end
diff -r 22542982bffd -r f4d806fd72ce src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Dec 12 15:05:18 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sat Dec 13 09:33:52 2003 +0100
@@ -1360,26 +1360,94 @@
 
 subsection {* Absolute Value *}
 
-text{*But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split:
-     "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
-by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
 lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
 by (simp add: abs_if)
 
-lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" 
-apply (case_tac "x=0 | y=0", force) 
+lemma abs_one [simp]: "abs 1 = (1::'a::ordered_ring)"
+  by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
+
+lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_ring)" 
+apply (case_tac "a=0 | b=0", force) 
 apply (auto elim: order_less_asym
             simp add: abs_if mult_less_0_iff linorder_neq_iff
                   minus_mult_left [symmetric] minus_mult_right [symmetric])  
 done
 
-lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
+lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
+by (simp add: abs_if)
+
+lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::ordered_ring))"
+by (simp add: abs_if linorder_neq_iff)
+
+lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)"
+by (simp add: abs_if  order_less_not_sym [of a 0])
+
+lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" 
+by (simp add: order_le_less) 
+
+lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::ordered_ring)"
+apply (auto simp add: abs_if linorder_not_less order_less_not_sym [of 0 a])  
+apply (drule order_antisym, assumption, simp) 
+done
+
+lemma abs_ge_zero [simp]: "(0::'a::ordered_ring) \<le> abs a"
+apply (simp add: abs_if order_less_imp_le)
+apply (simp add: linorder_not_less) 
+done
+
+lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)"
+  by (force elim: order_less_asym simp add: abs_if)
+
+lemma abs_zero_iff [iff]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
 by (simp add: abs_if)
 
-lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
-by (simp add: abs_if linorder_neq_iff)
+lemma abs_ge_self: "a \<le> abs (a::'a::ordered_ring)"
+apply (simp add: abs_if)
+apply (simp add: order_less_imp_le order_trans [of _ 0])
+done
+
+lemma abs_ge_minus_self: "-a \<le> abs (a::'a::ordered_ring)"
+by (insert abs_ge_self [of "-a"], simp)
+
+lemma nonzero_abs_inverse:
+     "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
+apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
+                      negative_imp_inverse_negative)
+apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
+done
+
+lemma abs_inverse [simp]:
+     "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
+      inverse (abs a)"
+apply (case_tac "a=0", simp) 
+apply (simp add: nonzero_abs_inverse) 
+done
+
+
+lemma nonzero_abs_divide:
+     "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
+by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
+
+lemma abs_divide:
+     "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
+apply (case_tac "b=0", simp) 
+apply (simp add: nonzero_abs_divide) 
+done
+
+(*TOO DIFFICULT: 6 CASES
+lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
+apply (simp add: abs_if)
+apply (auto ); 
+*)
+
+lemma abs_mult_less:
+     "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"
+proof -
+  assume ac: "abs a < c"
+  hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
+  assume "abs b < d"
+  thus ?thesis by (simp add: ac cpos mult_strict_mono) 
+qed
 
 
 end