diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Jul 12 12:49:46 2005 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue Jul 12 17:56:03 2005 +0200
@@ -1,6 +1,7 @@
 (*  Title:   HOL/Ring_and_Field.thy
     ID:      $Id$
-    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel
+    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
+             with contributions by Jeremy Avigad
 *)
 
 header {* (Ordered) Rings and Fields *}
@@ -330,28 +331,28 @@
 
 subsection{* Products of Signs *}
 
-lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
+lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
 by (drule mult_strict_left_mono [of 0 b], auto)
 
-lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
+lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
 by (drule mult_left_mono [of 0 b], auto)
 
 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"
 by (drule mult_strict_left_mono [of b 0], auto)
 
-lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
+lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
 by (drule mult_left_mono [of b 0], auto)
 
 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" 
 by (drule mult_strict_right_mono[of b 0], auto)
 
-lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 
+lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 
 by (drule mult_right_mono[of b 0], auto)
 
-lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
+lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
 by (drule mult_strict_right_mono_neg, auto)
 
-lemma mult_neg_le: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
+lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
 by (drule mult_right_mono_neg[of a 0 b ], auto)
 
 lemma zero_less_mult_pos:
@@ -372,7 +373,8 @@
 
 lemma zero_less_mult_iff:
      "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
-apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
+apply (auto simp add: order_le_less linorder_not_less mult_pos_pos 
+  mult_neg_neg)
 apply (blast dest: zero_less_mult_pos) 
 apply (blast dest: zero_less_mult_pos2)
 done
@@ -403,10 +405,10 @@
 done
 
 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"
-by (auto simp add: mult_pos_le mult_neg_le)
+by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
 
 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" 
-by (auto simp add: mult_pos_neg_le mult_pos_neg2_le)
+by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 lemma zero_le_square: "(0::'a::ordered_ring_strict) \<le> a*a"
 by (simp add: zero_le_mult_iff linorder_linear) 
@@ -444,7 +446,7 @@
 lemma mult_strict_mono:
      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
 apply (case_tac "c=0")
- apply (simp add: mult_pos) 
+ apply (simp add: mult_pos_pos) 
 apply (erule mult_strict_right_mono [THEN order_less_trans])
  apply (force simp add: order_le_less) 
 apply (erule mult_strict_left_mono, assumption)
@@ -469,6 +471,26 @@
 apply (simp add:  order_less_trans [OF zero_less_one]) 
 done
 
+lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==>
+    c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d"
+  apply (subgoal_tac "a * c < b * c")
+  apply (erule order_less_le_trans)
+  apply (erule mult_left_mono)
+  apply simp
+  apply (erule mult_strict_right_mono)
+  apply assumption
+done
+
+lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==>
+    c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d"
+  apply (subgoal_tac "a * c <= b * c")
+  apply (erule order_le_less_trans)
+  apply (erule mult_strict_left_mono)
+  apply simp
+  apply (erule mult_right_mono)
+  apply simp
+done
+
 subsection{*Cancellation Laws for Relationships With a Common Factor*}
 
 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
@@ -774,7 +796,7 @@
 qed
 
 lemma inverse_minus_eq [simp]:
-   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
+   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"
 proof cases
   assume "a=0" thus ?thesis by (simp add: inverse_zero)
 next
@@ -882,6 +904,8 @@
       "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
   by (simp add: divide_inverse mult_commute)
 
+subsection {* Calculations with fractions *}
+
 lemma nonzero_mult_divide_cancel_left:
   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
     shows "(c*a)/(c*b) = a/(b::'a::field)"
@@ -936,6 +960,19 @@
      "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
 by (simp add: divide_inverse mult_assoc)
 
+lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
+    x / y + w / z = (x * z + w * y) / (y * z)"
+  apply (subgoal_tac "x / y = (x * z) / (y * z)")
+  apply (erule ssubst)
+  apply (subgoal_tac "w / z = (w * y) / (y * z)")
+  apply (erule ssubst)
+  apply (rule add_divide_distrib [THEN sym])
+  apply (subst mult_commute)
+  apply (erule nonzero_mult_divide_cancel_left [THEN sym])
+  apply assumption
+  apply (erule nonzero_mult_divide_cancel_right [THEN sym])
+  apply assumption
+done
 
 subsubsection{*Special Cancellation Simprules for Division*}
 
@@ -1025,6 +1062,13 @@
 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
 by (simp add: diff_minus add_divide_distrib) 
 
+lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
+    x / y - w / z = (x * z - w * y) / (y * z)"
+  apply (subst diff_def)+
+  apply (subst minus_divide_left)
+  apply (subst add_frac_eq)
+  apply simp_all
+done
 
 subsection {* Ordered Fields *}
 
@@ -1224,33 +1268,6 @@
    "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
 
-
-subsection{*Division and Signs*}
-
-lemma zero_less_divide_iff:
-     "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
-by (simp add: divide_inverse zero_less_mult_iff)
-
-lemma divide_less_0_iff:
-     "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
-      (0 < a & b < 0 | a < 0 & 0 < b)"
-by (simp add: divide_inverse mult_less_0_iff)
-
-lemma zero_le_divide_iff:
-     "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
-      (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse zero_le_mult_iff)
-
-lemma divide_le_0_iff:
-     "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
-      (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
-by (simp add: divide_inverse mult_le_0_iff)
-
-lemma divide_eq_0_iff [simp]:
-     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse field_mult_eq_0_iff)
-
-
 subsection{*Simplification of Inequalities Involving Literal Divisors*}
 
 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
@@ -1263,7 +1280,6 @@
   finally show ?thesis .
 qed
 
-
 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
 proof -
   assume less: "c<0"
@@ -1312,7 +1328,6 @@
 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
 done
 
-
 lemma pos_less_divide_eq:
      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
 proof -
@@ -1403,6 +1418,99 @@
   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
 by (force simp add: nonzero_divide_eq_eq) 
 
+lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
+    b = a * c ==> b / c = a"
+  by (subst divide_eq_eq, simp)
+
+lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
+    a * c = b ==> a = b / c"
+  by (subst eq_divide_eq, simp)
+
+lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
+    (x / y = w / z) = (x * z = w * y)"
+  apply (subst nonzero_eq_divide_eq)
+  apply assumption
+  apply (subst times_divide_eq_left)
+  apply (erule nonzero_divide_eq_eq) 
+done
+
+subsection{*Division and Signs*}
+
+lemma zero_less_divide_iff:
+     "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
+by (simp add: divide_inverse zero_less_mult_iff)
+
+lemma divide_less_0_iff:
+     "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
+      (0 < a & b < 0 | a < 0 & 0 < b)"
+by (simp add: divide_inverse mult_less_0_iff)
+
+lemma zero_le_divide_iff:
+     "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
+      (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
+by (simp add: divide_inverse zero_le_mult_iff)
+
+lemma divide_le_0_iff:
+     "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
+      (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
+by (simp add: divide_inverse mult_le_0_iff)
+
+lemma divide_eq_0_iff [simp]:
+     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
+by (simp add: divide_inverse field_mult_eq_0_iff)
+
+lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==> 
+    0 < y ==> 0 < x / y"
+  apply (subst pos_less_divide_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==> 
+    0 <= x / y"
+  apply (subst pos_le_divide_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
+  apply (subst pos_divide_less_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==> 
+    0 < y ==> x / y <= 0"
+  apply (subst pos_divide_le_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
+  apply (subst neg_divide_less_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==> 
+    y < 0 ==> x / y <= 0"
+  apply (subst neg_divide_le_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
+  apply (subst neg_less_divide_eq)
+  apply assumption
+  apply simp
+done
+
+lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 
+    0 <= x / y"
+  apply (subst neg_le_divide_eq)
+  apply assumption
+  apply simp
+done
 
 subsection{*Cancellation Laws for Division*}
 
@@ -1427,7 +1535,6 @@
 apply (simp add: right_inverse_eq) 
 done
 
-
 lemma one_eq_divide_iff [simp]:
      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
 by (simp add: eq_commute [of 1])  
@@ -1451,7 +1558,6 @@
 declare zero_le_divide_iff [of "1", simp]
 declare divide_le_0_iff [of "1", simp]
 
-
 subsection {* Ordering Rules for Division *}
 
 lemma divide_strict_right_mono:
@@ -1463,6 +1569,17 @@
      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
   by (force simp add: divide_strict_right_mono order_le_less) 
 
+lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
+    ==> c <= 0 ==> b / c <= a / c"
+  apply (drule divide_right_mono [of _ _ "- c"])
+  apply auto
+done
+
+lemma divide_strict_right_mono_neg:
+     "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
+apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
+apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
+done
 
 text{*The last premise ensures that @{term a} and @{term b} 
       have the same sign*}
@@ -1481,6 +1598,12 @@
   apply (force simp add: divide_strict_left_mono order_le_less) 
   done
 
+lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
+    ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
+  apply (drule divide_left_mono [of _ _ "- c"])
+  apply (auto simp add: mult_commute)
+done
+
 lemma divide_strict_left_mono_neg:
      "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
   apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
@@ -1490,12 +1613,139 @@
    apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) 
   done
 
-lemma divide_strict_right_mono_neg:
-     "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
-apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
-apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
+text{*Simplify quotients that are compared with the value 1.*}
+
+lemma le_divide_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
+by (auto simp add: le_divide_eq)
+
+lemma divide_le_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
+by (auto simp add: divide_le_eq)
+
+lemma less_divide_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
+by (auto simp add: less_divide_eq)
+
+lemma divide_less_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
+by (auto simp add: divide_less_eq)
+
+subsection{*Conditional Simplification Rules: No Case Splits*}
+
+lemma le_divide_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
+by (auto simp add: le_divide_eq)
+
+lemma le_divide_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
+by (auto simp add: le_divide_eq)
+
+lemma divide_le_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
+by (auto simp add: divide_le_eq)
+
+lemma divide_le_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
+by (auto simp add: divide_le_eq)
+
+lemma less_divide_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
+by (auto simp add: less_divide_eq)
+
+lemma less_divide_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
+by (auto simp add: less_divide_eq)
+
+lemma divide_less_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
+by (auto simp add: divide_less_eq)
+
+lemma eq_divide_eq_1 [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
+by (auto simp add: eq_divide_eq)
+
+lemma divide_eq_eq_1 [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
+by (auto simp add: divide_eq_eq)
+
+subsection {* Reasoning about inequalities with division *}
+
+lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
+    ==> x * y <= x"
+  by (auto simp add: mult_compare_simps);
+
+lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
+    ==> y * x <= x"
+  by (auto simp add: mult_compare_simps);
+
+lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
+    x / y <= z";
+  by (subst pos_divide_le_eq, assumption+);
+
+lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
+    z <= x / y";
+  by (subst pos_le_divide_eq, assumption+)
+
+lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
+    x / y < z"
+  by (subst pos_divide_less_eq, assumption+)
+
+lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
+    z < x / y"
+  by (subst pos_less_divide_eq, assumption+)
+
+lemma frac_le: "(0::'a::ordered_field) <= x ==> 
+    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
+  apply (rule mult_imp_div_pos_le)
+  apply simp;
+  apply (subst times_divide_eq_left);
+  apply (rule mult_imp_le_div_pos, assumption)
+  apply (rule mult_mono)
+  apply simp_all
 done
 
+lemma frac_less: "(0::'a::ordered_field) <= x ==> 
+    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
+  apply (rule mult_imp_div_pos_less)
+  apply simp;
+  apply (subst times_divide_eq_left);
+  apply (rule mult_imp_less_div_pos, assumption)
+  apply (erule mult_less_le_imp_less)
+  apply simp_all
+done
+
+lemma frac_less2: "(0::'a::ordered_field) < x ==> 
+    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
+  apply (rule mult_imp_div_pos_less)
+  apply simp_all
+  apply (subst times_divide_eq_left);
+  apply (rule mult_imp_less_div_pos, assumption)
+  apply (erule mult_le_less_imp_less)
+  apply simp_all
+done
+
+lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+
+text{*It's not obvious whether these should be simprules or not. 
+  Their effect is to gather terms into one big fraction, like
+  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
+  seem to need them.*}
+
+declare times_divide_eq [simp]
 
 subsection {* Ordered Fields are Dense *}
 
@@ -1519,16 +1769,6 @@
 by (blast intro!: less_half_sum gt_half_sum)
 
 
-lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
-
-text{*It's not obvious whether these should be simprules or not. 
-  Their effect is to gather terms into one big fraction, like
-  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
-  seem to need them.*}
-
-declare times_divide_eq [simp]
-
-
 subsection {* Absolute Value *}
 
 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
@@ -1556,15 +1796,15 @@
     apply (simp)
     apply (rule_tac y="0::'a" in order_trans)
     apply (rule addm2)
-    apply (simp_all add: mult_pos_le mult_neg_le)
+    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
     apply (rule addm)
-    apply (simp_all add: mult_pos_le mult_neg_le)
+    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
     done
   have yx: "?y <= ?x"
     apply (simp add:diff_def)
     apply (rule_tac y=0 in order_trans)
-    apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
-    apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
+    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
+    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
     done
   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
@@ -1600,8 +1840,8 @@
 	ring_eq_simps 
 	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
-	apply(drule (1) mult_pos_neg_le[of a b], simp)
-	apply(drule (1) mult_pos_neg2_le[of b a], simp)
+	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
+	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
       done
   next
     assume "~(0 <= a*b)"
@@ -1610,8 +1850,8 @@
       apply (simp_all add: mulprts abs_prts)
       apply (insert prems)
       apply (auto simp add: ring_eq_simps)
-      apply(drule (1) mult_pos_le[of a b],simp)
-      apply(drule (1) mult_neg_le[of a b],simp)
+      apply(drule (1) mult_nonneg_nonneg[of a b],simp)
+      apply(drule (1) mult_nonpos_nonpos[of a b],simp)
       done
   qed
 qed
@@ -1667,6 +1907,20 @@
 apply (simp add: le_minus_self_iff linorder_neq_iff) 
 done
 
+lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
+    (abs y) * x = abs (y * x)";
+  apply (subst abs_mult);
+  apply simp;
+done;
+
+lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
+    abs x / y = abs (x / y)";
+  apply (subst abs_divide);
+  apply (simp add: order_less_imp_le);
+done;
+
+subsection {* Miscellaneous *}
+
 lemma linprog_dual_estimate:
   assumes
   "A * x \<le> (b::'a::lordered_ring)"
@@ -1712,7 +1966,7 @@
     by (simp)
   show ?thesis 
     apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
-    apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
+    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
     done
 qed
 
@@ -1727,7 +1981,7 @@
     have 1: "A - A1 = A + (- A1)" by simp
     show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
   qed
-  then have "abs (A-A1) = A-A1" by (rule abs_of_ge_0)
+  then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
   with prems show "abs (A-A1) <= (A2-A1)" by simp
 qed
 
@@ -1856,6 +2110,7 @@
 val mult_left_mono_neg = thm "mult_left_mono_neg";
 val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
 val mult_right_mono_neg = thm "mult_right_mono_neg";
+(*
 val mult_pos = thm "mult_pos";
 val mult_pos_le = thm "mult_pos_le";
 val mult_pos_neg = thm "mult_pos_neg";
@@ -1864,6 +2119,7 @@
 val mult_pos_neg2_le = thm "mult_pos_neg2_le";
 val mult_neg = thm "mult_neg";
 val mult_neg_le = thm "mult_neg_le";
+*)
 val zero_less_mult_pos = thm "zero_less_mult_pos";
 val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
 val zero_less_mult_iff = thm "zero_less_mult_iff";