# HG changeset patch
# User haftmann
# Date 1272023894 -7200
# Node ID 72f4d079ebf82b1fa8555cd0370916af73eaef9d
# Parent  c805033ad0327d27f94635f97309594193401ec1
more localization; factored out lemmas for division_ring

diff -r c805033ad032 -r 72f4d079ebf8 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Apr 23 13:58:14 2010 +0200
+++ b/src/HOL/Fields.thy	Fri Apr 23 13:58:14 2010 +0200
@@ -31,34 +31,6 @@
 
 subclass idom ..
 
-lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
-proof
-  assume neq: "b \<noteq> 0"
-  {
-    hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
-    also assume "a / b = 1"
-    finally show "a = b" by simp
-  next
-    assume "a = b"
-    with neq show "a / b = 1" by (simp add: divide_inverse)
-  }
-qed
-
-lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
-by (simp add: divide_inverse)
-
-lemma divide_zero_left [simp]: "0 / a = 0"
-by (simp add: divide_inverse)
-
-lemma inverse_eq_divide: "inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
-by (simp add: divide_inverse algebra_simps)
-
 text{*There is no slick version using division by zero.*}
 lemma inverse_add:
   "[| a \<noteq> 0;  b \<noteq> 0 |]
@@ -80,14 +52,8 @@
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
 by (simp add: mult_commute [of _ c])
 
-lemma divide_1 [simp]: "a / 1 = a"
-by (simp add: divide_inverse)
-
-lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
-by (simp add: divide_inverse mult_assoc)
-
 lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
-by (simp add: divide_inverse mult_ac)
+  by (simp add: divide_inverse mult_ac)
 
 text {* These are later declared as simp rules. *}
 lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
@@ -108,7 +74,7 @@
 
 lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
   "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
-using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
+  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
 
 lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
   "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
@@ -130,58 +96,21 @@
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
 
-lemma minus_divide_left: "- (a / b) = (-a) / b"
-by (simp add: divide_inverse)
-
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
-by (simp add: divide_inverse)
-
-lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
-by (simp add: diff_minus add_divide_distrib)
-
 lemma add_divide_eq_iff:
   "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
-by (simp add: add_divide_distrib)
+  by (simp add: add_divide_distrib)
 
 lemma divide_add_eq_iff:
   "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
-by (simp add: add_divide_distrib)
+  by (simp add: add_divide_distrib)
 
 lemma diff_divide_eq_iff:
   "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
-by (simp add: diff_divide_distrib)
+  by (simp add: diff_divide_distrib)
 
 lemma divide_diff_eq_iff:
   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
-by (simp add: diff_divide_distrib)
-
-lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
-proof -
-  assume [simp]: "c \<noteq> 0"
-  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
-  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
-  finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
-proof -
-  assume [simp]: "c \<noteq> 0"
-  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
-  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
-by simp
-
-lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
-by (erule subst, simp)
+  by (simp add: diff_divide_distrib)
 
 lemmas field_eq_simps[no_atp] = algebra_simps
   (* pull / out*)
@@ -189,9 +118,7 @@
   diff_divide_eq_iff divide_diff_eq_iff
   (* multiply eqn *)
   nonzero_eq_divide_eq nonzero_divide_eq_eq
-(* is added later:
   times_divide_eq_left times_divide_eq_right
-*)
 
 text{*An example:*}
 lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
@@ -202,68 +129,21 @@
 
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
-by (simp add: field_eq_simps times_divide_eq)
+  by (simp add: field_eq_simps times_divide_eq)
 
 lemma frac_eq_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
-by (simp add: field_eq_simps times_divide_eq)
+  by (simp add: field_eq_simps times_divide_eq)
 
 end
 
-class division_by_zero = zero + inverse +
-  assumes inverse_zero [simp]: "inverse 0 = 0"
-
-lemma divide_zero [simp]:
-  "a / 0 = (0::'a::{field,division_by_zero})"
-by (simp add: divide_inverse)
-
-lemma divide_self_if [simp]:
-  "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
-by simp
-
-class linordered_field = field + linordered_idom
-
-lemma inverse_nonzero_iff_nonzero [simp]:
-   "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
-by (force dest: inverse_zero_imp_zero) 
-
-lemma inverse_minus_eq [simp]:
-   "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
-proof cases
-  assume "a=0" thus ?thesis by simp
-next
-  assume "a\<noteq>0" 
-  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
-qed
-
-lemma inverse_eq_imp_eq:
-  "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
-apply (cases "a=0 | b=0") 
- apply (force dest!: inverse_zero_imp_zero
-              simp add: eq_commute [of "0::'a"])
-apply (force dest!: nonzero_inverse_eq_imp_eq) 
-done
-
-lemma inverse_eq_iff_eq [simp]:
-  "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
-by (force dest!: inverse_eq_imp_eq)
-
-lemma inverse_inverse_eq [simp]:
-     "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
-  proof cases
-    assume "a=0" thus ?thesis by simp
-  next
-    assume "a\<noteq>0" 
-    thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
-  qed
-
 text{*This version builds in division by zero while also re-orienting
       the right-hand side.*}
 lemma inverse_mult_distrib [simp]:
      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
   proof cases
     assume "a \<noteq> 0 & b \<noteq> 0" 
-    thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
+    thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
   next
     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
     thus ?thesis by force
@@ -271,10 +151,10 @@
 
 lemma inverse_divide [simp]:
   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
-by (simp add: divide_inverse mult_commute)
+  by (simp add: divide_inverse mult_commute)
 
 
-subsection {* Calculations with fractions *}
+text {* Calculations with fractions *}
 
 text{* There is a whole bunch of simp-rules just for class @{text
 field} but none for class @{text field} and @{text nonzero_divides}
@@ -301,7 +181,7 @@
 by (simp add: divide_inverse mult_assoc)
 
 
-subsubsection{*Special Cancellation Simprules for Division*}
+text {*Special Cancellation Simprules for Division*}
 
 lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
 fixes c :: "'a :: {field,division_by_zero}"
@@ -309,7 +189,7 @@
 by (simp add: mult_divide_mult_cancel_left)
 
 
-subsection {* Division and Unary Minus *}
+text {* Division and Unary Minus *}
 
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
 by (simp add: divide_inverse)
@@ -332,40 +212,74 @@
   "(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 inverse_eq_1_iff [simp]:
+  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
+by (insert inverse_eq_iff_eq [of x 1], simp) 
 
-subsection {* Ordered Fields *}
+lemma divide_eq_0_iff [simp,no_atp]:
+     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
+by (simp add: divide_inverse)
+
+lemma divide_cancel_right [simp,no_atp]:
+     "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse)
+done
+
+lemma divide_cancel_left [simp,no_atp]:
+     "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse)
+done
+
+lemma divide_eq_1_iff [simp,no_atp]:
+     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+apply (cases "b=0", simp)
+apply (simp add: right_inverse_eq)
+done
+
+lemma one_eq_divide_iff [simp,no_atp]:
+     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+by (simp add: eq_commute [of 1])
+
+
+text {* Ordered Fields *}
+
+class linordered_field = field + linordered_idom
+begin
 
 lemma positive_imp_inverse_positive: 
-assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"
+  assumes a_gt_0: "0 < a" 
+  shows "0 < inverse a"
 proof -
   have "0 < a * inverse a" 
-    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2])
+    by (simp add: a_gt_0 [THEN less_imp_not_eq2])
   thus "0 < inverse a" 
-    by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
+    by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
 qed
 
 lemma negative_imp_inverse_negative:
-  "a < 0 ==> inverse a < (0::'a::linordered_field)"
-by (insert positive_imp_inverse_positive [of "-a"], 
-    simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
+  "a < 0 \<Longrightarrow> inverse a < 0"
+  by (insert positive_imp_inverse_positive [of "-a"], 
+    simp add: nonzero_inverse_minus_eq less_imp_not_eq)
 
 lemma inverse_le_imp_le:
-assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
-shows "b \<le> (a::'a::linordered_field)"
+  assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
+  shows "b \<le> a"
 proof (rule classical)
   assume "~ b \<le> a"
   hence "a < b"  by (simp add: linorder_not_le)
-  hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
+  hence bpos: "0 < b"  by (blast intro: apos less_trans)
   hence "a * inverse a \<le> a * inverse b"
-    by (simp add: apos invle order_less_imp_le mult_left_mono)
+    by (simp add: apos invle less_imp_le mult_left_mono)
   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
-    by (simp add: bpos order_less_imp_le mult_right_mono)
-  thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
+    by (simp add: bpos less_imp_le mult_right_mono)
+  thus "b \<le> a"  by (simp add: mult_assoc apos bpos less_imp_not_eq2)
 qed
 
 lemma inverse_positive_imp_positive:
-assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
-shows "0 < (a::'a::linordered_field)"
+  assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
+  shows "0 < a"
 proof -
   have "0 < inverse (inverse a)"
     using inv_gt_0 by (rule positive_imp_inverse_positive)
@@ -373,21 +287,397 @@
     using nz by (simp add: nonzero_inverse_inverse_eq)
 qed
 
+lemma inverse_negative_imp_negative:
+  assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
+  shows "a < 0"
+proof -
+  have "inverse (inverse a) < 0"
+    using inv_less_0 by (rule negative_imp_inverse_negative)
+  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma linordered_field_no_lb:
+  "\<forall>x. \<exists>y. y < x"
+proof
+  fix x::'a
+  have m1: "- (1::'a) < 0" by simp
+  from add_strict_right_mono[OF m1, where c=x] 
+  have "(- 1) + x < x" by simp
+  thus "\<exists>y. y < x" by blast
+qed
+
+lemma linordered_field_no_ub:
+  "\<forall> x. \<exists>y. y > x"
+proof
+  fix x::'a
+  have m1: " (1::'a) > 0" by simp
+  from add_strict_right_mono[OF m1, where c=x] 
+  have "1 + x > x" by simp
+  thus "\<exists>y. y > x" by blast
+qed
+
+lemma less_imp_inverse_less:
+  assumes less: "a < b" and apos:  "0 < a"
+  shows "inverse b < inverse a"
+proof (rule ccontr)
+  assume "~ inverse b < inverse a"
+  hence "inverse a \<le> inverse b" by simp
+  hence "~ (a < b)"
+    by (simp add: not_less inverse_le_imp_le [OF _ apos])
+  thus False by (rule notE [OF _ less])
+qed
+
+lemma inverse_less_imp_less:
+  "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
+apply (simp add: less_le [of "inverse a"] less_le [of "b"])
+apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
+done
+
+text{*Both premises are essential. Consider -1 and 1.*}
+lemma inverse_less_iff_less [simp,no_atp]:
+  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
+  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
+
+lemma le_imp_inverse_le:
+  "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
+  by (force simp add: le_less less_imp_inverse_less)
+
+lemma inverse_le_iff_le [simp,no_atp]:
+  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
+  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
+
+
+text{*These results refer to both operands being negative.  The opposite-sign
+case is trivial, since inverse preserves signs.*}
+lemma inverse_le_imp_le_neg:
+  "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
+apply (rule classical) 
+apply (subgoal_tac "a < 0") 
+ prefer 2 apply force
+apply (insert inverse_le_imp_le [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq) 
+done
+
+lemma less_imp_inverse_less_neg:
+   "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
+apply (subgoal_tac "a < 0") 
+ prefer 2 apply (blast intro: less_trans) 
+apply (insert less_imp_inverse_less [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq) 
+done
+
+lemma inverse_less_imp_less_neg:
+   "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
+apply (rule classical) 
+apply (subgoal_tac "a < 0") 
+ prefer 2
+ apply force
+apply (insert inverse_less_imp_less [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq) 
+done
+
+lemma inverse_less_iff_less_neg [simp,no_atp]:
+  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
+apply (insert inverse_less_iff_less [of "-b" "-a"])
+apply (simp del: inverse_less_iff_less 
+            add: nonzero_inverse_minus_eq)
+done
+
+lemma le_imp_inverse_le_neg:
+  "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
+  by (force simp add: le_less less_imp_inverse_less_neg)
+
+lemma inverse_le_iff_le_neg [simp,no_atp]:
+  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
+  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
+
+lemma pos_le_divide_eq: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
+proof -
+  assume less: "0<c"
+  hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
+    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+  also have "... = (a*c \<le> b)"
+    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma neg_le_divide_eq: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
+proof -
+  assume less: "c<0"
+  hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
+    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+  also have "... = (b \<le> a*c)"
+    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma pos_less_divide_eq:
+     "0 < c ==> (a < b/c) = (a*c < b)"
+proof -
+  assume less: "0<c"
+  hence "(a < b/c) = (a*c < (b/c)*c)"
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+  also have "... = (a*c < b)"
+    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma neg_less_divide_eq:
+ "c < 0 ==> (a < b/c) = (b < a*c)"
+proof -
+  assume less: "c<0"
+  hence "(a < b/c) = ((b/c)*c < a*c)"
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+  also have "... = (b < a*c)"
+    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma pos_divide_less_eq:
+     "0 < c ==> (b/c < a) = (b < a*c)"
+proof -
+  assume less: "0<c"
+  hence "(b/c < a) = ((b/c)*c < a*c)"
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+  also have "... = (b < a*c)"
+    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma neg_divide_less_eq:
+ "c < 0 ==> (b/c < a) = (a*c < b)"
+proof -
+  assume less: "c<0"
+  hence "(b/c < a) = (a*c < (b/c)*c)"
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+  also have "... = (a*c < b)"
+    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma pos_divide_le_eq: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
+proof -
+  assume less: "0<c"
+  hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
+    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+  also have "... = (b \<le> a*c)"
+    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma neg_divide_le_eq: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
+proof -
+  assume less: "c<0"
+  hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
+    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+  also have "... = (a*c \<le> b)"
+    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
+if they can be proved to be non-zero (for equations) or positive/negative
+(for inequations). Can be too aggressive and is therefore separate from the
+more benign @{text algebra_simps}. *}
+
+lemmas field_simps[no_atp] = field_eq_simps
+  (* multiply ineqn *)
+  pos_divide_less_eq neg_divide_less_eq
+  pos_less_divide_eq neg_less_divide_eq
+  pos_divide_le_eq neg_divide_le_eq
+  pos_le_divide_eq neg_le_divide_eq
+
+thm field_eq_simps
+
+text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
+of positivity/negativity needed for @{text field_simps}. Have not added @{text
+sign_simps} to @{text field_simps} because the former can lead to case
+explosions. *}
+
+lemmas sign_simps[no_atp] = group_simps
+  zero_less_mult_iff mult_less_0_iff
+
+(* Only works once linear arithmetic is installed:
+text{*An example:*}
+lemma fixes a b c d e f :: "'a::linordered_field"
+shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
+ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
+ ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(simp add:field_simps)
+done
+*)
+
+lemma divide_pos_pos:
+  "0 < x ==> 0 < y ==> 0 < x / y"
+by(simp add:field_simps)
+
+lemma divide_nonneg_pos:
+  "0 <= x ==> 0 < y ==> 0 <= x / y"
+by(simp add:field_simps)
+
+lemma divide_neg_pos:
+  "x < 0 ==> 0 < y ==> x / y < 0"
+by(simp add:field_simps)
+
+lemma divide_nonpos_pos:
+  "x <= 0 ==> 0 < y ==> x / y <= 0"
+by(simp add:field_simps)
+
+lemma divide_pos_neg:
+  "0 < x ==> y < 0 ==> x / y < 0"
+by(simp add:field_simps)
+
+lemma divide_nonneg_neg:
+  "0 <= x ==> y < 0 ==> x / y <= 0" 
+by(simp add:field_simps)
+
+lemma divide_neg_neg:
+  "x < 0 ==> y < 0 ==> 0 < x / y"
+by(simp add:field_simps)
+
+lemma divide_nonpos_neg:
+  "x <= 0 ==> y < 0 ==> 0 <= x / y"
+by(simp add:field_simps)
+
+lemma divide_strict_right_mono:
+     "[|a < b; 0 < c|] ==> a / c < b / c"
+by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono 
+              positive_imp_inverse_positive)
+
+
+lemma divide_strict_right_mono_neg:
+     "[|b < a; c < 0|] ==> a / c < b / c"
+apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
+apply (simp add: 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*}
+lemma divide_strict_left_mono:
+  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
+
+lemma divide_left_mono:
+  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
+
+lemma divide_strict_left_mono_neg:
+  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
+
+lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
+    x / y <= z"
+by (subst pos_divide_le_eq, assumption+)
+
+lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
+    z <= x / y"
+by(simp add:field_simps)
+
+lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
+    x / y < z"
+by(simp add:field_simps)
+
+lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
+    z < x / y"
+by(simp add:field_simps)
+
+lemma frac_le: "0 <= 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 <= 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 < 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
+
+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]
+
+lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
+by (simp add: field_simps zero_less_two)
+
+lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
+by (simp add: field_simps zero_less_two)
+
+subclass dense_linorder
+proof
+  fix x y :: 'a
+  from less_add_one show "\<exists>y. x < y" .. 
+  from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
+  then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
+  then have "x - 1 < x" by (simp add: algebra_simps)
+  then show "\<exists>y. y < x" ..
+  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
+qed
+
+lemma nonzero_abs_inverse:
+     "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
+apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq 
+                      negative_imp_inverse_negative)
+apply (blast intro: positive_imp_inverse_positive elim: less_asym) 
+done
+
+lemma nonzero_abs_divide:
+     "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+  by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
+
+lemma field_le_epsilon:
+  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
+  shows "x \<le> y"
+proof (rule dense_le)
+  fix t assume "t < x"
+  hence "0 < x - t" by (simp add: less_diff_eq)
+  from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
+  then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
+  then show "t \<le> y" by (simp add: algebra_simps)
+qed
+
+end
+
+lemma le_divide_eq:
+  "(a \<le> b/c) = 
+   (if 0 < c then a*c \<le> b
+             else if c < 0 then b \<le> a*c
+             else  a \<le> (0::'a::{linordered_field,division_by_zero}))"
+apply (cases "c=0", simp) 
+apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
+done
+
 lemma inverse_positive_iff_positive [simp]:
   "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"
 apply (cases "a = 0", simp)
 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
 done
 
-lemma inverse_negative_imp_negative:
-assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
-shows "a < (0::'a::linordered_field)"
-proof -
-  have "inverse (inverse a) < 0"
-    using inv_less_0 by (rule negative_imp_inverse_negative)
-  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
-qed
-
 lemma inverse_negative_iff_negative [simp]:
   "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"
 apply (cases "a = 0", simp)
@@ -402,104 +692,6 @@
   "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric])
 
-lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
-proof
-  fix x::'a
-  have m1: "- (1::'a) < 0" by simp
-  from add_strict_right_mono[OF m1, where c=x] 
-  have "(- 1) + x < x" by simp
-  thus "\<exists>y. y < x" by blast
-qed
-
-lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
-proof
-  fix x::'a
-  have m1: " (1::'a) > 0" by simp
-  from add_strict_right_mono[OF m1, where c=x] 
-  have "1 + x > x" by simp
-  thus "\<exists>y. y > x" by blast
-qed
-
-subsection{*Anti-Monotonicity of @{term inverse}*}
-
-lemma less_imp_inverse_less:
-assumes less: "a < b" and apos:  "0 < a"
-shows "inverse b < inverse (a::'a::linordered_field)"
-proof (rule ccontr)
-  assume "~ inverse b < inverse a"
-  hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
-  hence "~ (a < b)"
-    by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
-  thus False by (rule notE [OF _ less])
-qed
-
-lemma inverse_less_imp_less:
-  "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)"
-apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
-apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
-done
-
-text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,no_atp]:
-  "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
-by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
-
-lemma le_imp_inverse_le:
-  "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
-by (force simp add: order_le_less less_imp_inverse_less)
-
-lemma inverse_le_iff_le [simp,no_atp]:
- "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
-by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
-
-
-text{*These results refer to both operands being negative.  The opposite-sign
-case is trivial, since inverse preserves signs.*}
-lemma inverse_le_imp_le_neg:
-  "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::linordered_field)"
-apply (rule classical) 
-apply (subgoal_tac "a < 0") 
- prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
-apply (insert inverse_le_imp_le [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-done
-
-lemma less_imp_inverse_less_neg:
-   "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)"
-apply (subgoal_tac "a < 0") 
- prefer 2 apply (blast intro: order_less_trans) 
-apply (insert less_imp_inverse_less [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-done
-
-lemma inverse_less_imp_less_neg:
-   "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)"
-apply (rule classical) 
-apply (subgoal_tac "a < 0") 
- prefer 2
- apply (force simp add: linorder_not_less intro: order_le_less_trans) 
-apply (insert inverse_less_imp_less [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-done
-
-lemma inverse_less_iff_less_neg [simp,no_atp]:
-  "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
-apply (insert inverse_less_iff_less [of "-b" "-a"])
-apply (simp del: inverse_less_iff_less 
-            add: order_less_imp_not_eq nonzero_inverse_minus_eq)
-done
-
-lemma le_imp_inverse_le_neg:
-  "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
-by (force simp add: order_le_less less_imp_inverse_less_neg)
-
-lemma inverse_le_iff_le_neg [simp,no_atp]:
- "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
-by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
-
-
-subsection{*Inverses and the Number One*}
-
 lemma one_less_inverse_iff:
   "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))"
 proof cases
@@ -518,10 +710,6 @@
   with notless show ?thesis by simp
 qed
 
-lemma inverse_eq_1_iff [simp]:
-  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
-by (insert inverse_eq_iff_eq [of x 1], simp) 
-
 lemma one_le_inverse_iff:
   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
 by (force simp add: order_le_less one_less_inverse_iff)
@@ -534,58 +722,6 @@
   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
 
-
-subsection{*Simplification of Inequalities Involving Literal Divisors*}
-
-lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
-proof -
-  assume less: "0<c"
-  hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
-    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
-  also have "... = (a*c \<le> b)"
-    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
-proof -
-  assume less: "c<0"
-  hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
-    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
-  also have "... = (b \<le> a*c)"
-    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma le_divide_eq:
-  "(a \<le> b/c) = 
-   (if 0 < c then a*c \<le> b
-             else if c < 0 then b \<le> a*c
-             else  a \<le> (0::'a::{linordered_field,division_by_zero}))"
-apply (cases "c=0", simp) 
-apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
-done
-
-lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
-proof -
-  assume less: "0<c"
-  hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
-    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
-  also have "... = (b \<le> a*c)"
-    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
-proof -
-  assume less: "c<0"
-  hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
-    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
-  also have "... = (a*c \<le> b)"
-    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
 lemma divide_le_eq:
   "(b/c \<le> a) = 
    (if 0 < c then b \<le> a*c
@@ -595,28 +731,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::linordered_field) ==> (a < b/c) = (a*c < b)"
-proof -
-  assume less: "0<c"
-  hence "(a < b/c) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
-  also have "... = (a*c < b)"
-    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma neg_less_divide_eq:
- "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)"
-proof -
-  assume less: "c<0"
-  hence "(a < b/c) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
-  also have "... = (b < a*c)"
-    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
 lemma less_divide_eq:
   "(a < b/c) = 
    (if 0 < c then a*c < b
@@ -626,28 +740,6 @@
 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
 done
 
-lemma pos_divide_less_eq:
-     "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)"
-proof -
-  assume less: "0<c"
-  hence "(b/c < a) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
-  also have "... = (b < a*c)"
-    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
-lemma neg_divide_less_eq:
- "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)"
-proof -
-  assume less: "c<0"
-  hence "(b/c < a) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
-  also have "... = (a*c < b)"
-    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
-
 lemma divide_less_eq:
   "(b/c < a) = 
    (if 0 < c then b < a*c
@@ -657,45 +749,7 @@
 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
 done
 
-
-subsection{*Field simplification*}
-
-text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
-if they can be proved to be non-zero (for equations) or positive/negative
-(for inequations). Can be too aggressive and is therefore separate from the
-more benign @{text algebra_simps}. *}
-
-lemmas field_simps[no_atp] = field_eq_simps
-  (* multiply ineqn *)
-  pos_divide_less_eq neg_divide_less_eq
-  pos_less_divide_eq neg_less_divide_eq
-  pos_divide_le_eq neg_divide_le_eq
-  pos_le_divide_eq neg_le_divide_eq
-
-text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
-of positivity/negativity needed for @{text field_simps}. Have not added @{text
-sign_simps} to @{text field_simps} because the former can lead to case
-explosions. *}
-
-lemmas sign_simps[no_atp] = group_simps
-  zero_less_mult_iff  mult_less_0_iff
-
-(* Only works once linear arithmetic is installed:
-text{*An example:*}
-lemma fixes a b c d e f :: "'a::linordered_field"
-shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
- ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
- ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(simp add:field_simps)
-done
-*)
-
-
-subsection{*Division and Signs*}
+text {*Division and Signs*}
 
 lemma zero_less_divide_iff:
      "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
@@ -716,71 +770,9 @@
       (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,no_atp]:
-     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse)
-
-lemma divide_pos_pos:
-  "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y"
-by(simp add:field_simps)
-
-
-lemma divide_nonneg_pos:
-  "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y"
-by(simp add:field_simps)
-
-lemma divide_neg_pos:
-  "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0"
-by(simp add:field_simps)
-
-lemma divide_nonpos_pos:
-  "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
-by(simp add:field_simps)
-
-lemma divide_pos_neg:
-  "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0"
-by(simp add:field_simps)
-
-lemma divide_nonneg_neg:
-  "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" 
-by(simp add:field_simps)
-
-lemma divide_neg_neg:
-  "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y"
-by(simp add:field_simps)
-
-lemma divide_nonpos_neg:
-  "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
-by(simp add:field_simps)
-
-
-subsection{*Cancellation Laws for Division*}
-
-lemma divide_cancel_right [simp,no_atp]:
-     "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
-apply (cases "c=0", simp)
-apply (simp add: divide_inverse)
-done
-
-lemma divide_cancel_left [simp,no_atp]:
-     "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
-apply (cases "c=0", simp)
-apply (simp add: divide_inverse)
-done
-
-
-subsection {* Division and the Number One *}
+text {* Division and the Number One *}
 
 text{*Simplify expressions equated with 1*}
-lemma divide_eq_1_iff [simp,no_atp]:
-     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-apply (cases "b=0", simp)
-apply (simp add: right_inverse_eq)
-done
-
-lemma one_eq_divide_iff [simp,no_atp]:
-     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-by (simp add: eq_commute [of 1])
 
 lemma zero_eq_1_divide_iff [simp,no_atp]:
      "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
@@ -806,49 +798,22 @@
 declare zero_le_divide_1_iff [simp,no_atp]
 declare divide_le_0_1_iff [simp,no_atp]
 
-
-subsection {* Ordering Rules for Division *}
-
-lemma divide_strict_right_mono:
-     "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)"
-by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
-              positive_imp_inverse_positive)
-
 lemma divide_right_mono:
      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_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,linordered_field}) <= b 
+lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= 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::linordered_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*}
-lemma divide_strict_left_mono:
-  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
-
-lemma divide_left_mono:
-  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
-
-lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b 
+lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= 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::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
 
 
 text{*Simplify quotients that are compared with the value 1.*}
@@ -874,7 +839,7 @@
 by (auto simp add: divide_less_eq)
 
 
-subsection{*Conditional Simplification Rules: No Case Splits*}
+text {*Conditional Simplification Rules: No Case Splits*}
 
 lemma le_divide_eq_1_pos [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
@@ -926,125 +891,25 @@
   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
 
-
-subsection {* Reasoning about inequalities with division *}
-
-lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==>
-    x / y <= z"
-by (subst pos_divide_le_eq, assumption+)
-
-lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==>
-    z <= x / y"
-by(simp add:field_simps)
-
-lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==>
-    x / y < z"
-by(simp add:field_simps)
-
-lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==>
-    z < x / y"
-by(simp add:field_simps)
-
-lemma frac_le: "(0::'a::linordered_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::linordered_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::linordered_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
-
-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 *}
-
-lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)"
-by (simp add: field_simps zero_less_two)
-
-lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b"
-by (simp add: field_simps zero_less_two)
-
-instance linordered_field < dense_linorder
-proof
-  fix x y :: 'a
-  have "x < x + 1" by simp
-  then show "\<exists>y. x < y" .. 
-  have "x - 1 < x" by simp
-  then show "\<exists>y. y < x" ..
-  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
-qed
-
-
-subsection {* Absolute Value *}
-
-lemma nonzero_abs_inverse:
-     "a \<noteq> 0 ==> abs (inverse (a::'a::linordered_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::{linordered_field,division_by_zero})) = 
-      inverse (abs a)"
+     "\<bar>inverse (a::'a::{linordered_field,division_by_zero})\<bar> = 
+      inverse \<bar>a\<bar>"
 apply (cases "a=0", simp) 
 apply (simp add: nonzero_abs_inverse) 
 done
 
-lemma nonzero_abs_divide:
-     "b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b"
-by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
-
 lemma abs_divide [simp]:
-     "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b"
+     "\<bar>a / (b::'a::{linordered_field,division_by_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
 apply (cases "b=0", simp) 
 apply (simp add: nonzero_abs_divide) 
 done
 
-lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> 
-    abs x / y = abs (x / y)"
+lemma abs_div_pos: "(0::'a::{linordered_field,division_by_zero}) < y ==> 
+    \<bar>x\<bar> / y = \<bar>x / y\<bar>"
   apply (subst abs_divide)
   apply (simp add: order_less_imp_le)
 done
 
-lemma field_le_epsilon:
-  fixes x y :: "'a\<Colon>linordered_field"
-  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
-  shows "x \<le> y"
-proof (rule dense_le)
-  fix t assume "t < x"
-  hence "0 < x - t" by (simp add: less_diff_eq)
-  from e[OF this]
-  show "t \<le> y" by (simp add: field_simps)
-qed
-
 lemma field_le_mult_one_interval:
   fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
diff -r c805033ad032 -r 72f4d079ebf8 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Apr 23 13:58:14 2010 +0200
+++ b/src/HOL/Rings.thy	Fri Apr 23 13:58:14 2010 +0200
@@ -487,6 +487,125 @@
   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
 by (simp add: algebra_simps)
 
+lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
+proof
+  assume neq: "b \<noteq> 0"
+  {
+    hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
+    also assume "a / b = 1"
+    finally show "a = b" by simp
+  next
+    assume "a = b"
+    with neq show "a / b = 1" by (simp add: divide_inverse)
+  }
+qed
+
+lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
+by (simp add: divide_inverse)
+
+lemma divide_zero_left [simp]: "0 / a = 0"
+by (simp add: divide_inverse)
+
+lemma inverse_eq_divide: "inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
+by (simp add: divide_inverse algebra_simps)
+
+lemma divide_1 [simp]: "a / 1 = a"
+  by (simp add: divide_inverse)
+
+lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
+  by (simp add: divide_inverse mult_assoc)
+
+lemma minus_divide_left: "- (a / b) = (-a) / b"
+  by (simp add: divide_inverse)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+  by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+  by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
+  by (simp add: divide_inverse)
+
+lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
+  by (simp add: diff_minus add_divide_distrib)
+
+lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+  assume [simp]: "c \<noteq> 0"
+  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+  finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+  assume [simp]: "c \<noteq> 0"
+  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+  by (simp add: divide_inverse mult_assoc)
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+  by (drule sym) (simp add: divide_inverse mult_assoc)
+
+end
+
+class division_by_zero = division_ring +
+  assumes inverse_zero [simp]: "inverse 0 = 0"
+begin
+
+lemma divide_zero [simp]:
+  "a / 0 = 0"
+  by (simp add: divide_inverse)
+
+lemma divide_self_if [simp]:
+  "a / a = (if a = 0 then 0 else 1)"
+  by simp
+
+lemma inverse_nonzero_iff_nonzero [simp]:
+  "inverse a = 0 \<longleftrightarrow> a = 0"
+  by rule (fact inverse_zero_imp_zero, simp)
+
+lemma inverse_minus_eq [simp]:
+  "inverse (- a) = - inverse a"
+proof cases
+  assume "a=0" thus ?thesis by simp
+next
+  assume "a\<noteq>0" 
+  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
+
+lemma inverse_eq_imp_eq:
+  "inverse a = inverse b \<Longrightarrow> a = b"
+apply (cases "a=0 | b=0") 
+ apply (force dest!: inverse_zero_imp_zero
+              simp add: eq_commute [of "0::'a"])
+apply (force dest!: nonzero_inverse_eq_imp_eq) 
+done
+
+lemma inverse_eq_iff_eq [simp]:
+  "inverse a = inverse b \<longleftrightarrow> a = b"
+  by (force dest!: inverse_eq_imp_eq)
+
+lemma inverse_inverse_eq [simp]:
+  "inverse (inverse a) = a"
+proof cases
+  assume "a=0" thus ?thesis by simp
+next
+  assume "a\<noteq>0" 
+  thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
+qed
+
 end
 
 class mult_mono = times + zero + ord +
@@ -533,17 +652,17 @@
 subclass ordered_semiring ..
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
-using mult_left_mono [of zero b a] by simp
+using mult_left_mono [of 0 b a] by simp
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
-using mult_left_mono [of b zero a] by simp
+using mult_left_mono [of b 0 a] by simp
 
 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
-using mult_right_mono [of a zero b] by simp
+using mult_right_mono [of a 0 b] by simp
 
 text {* Legacy - use @{text mult_nonpos_nonneg} *}
 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
-by (drule mult_right_mono [of b zero], auto)
+by (drule mult_right_mono [of b 0], auto)
 
 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
@@ -597,17 +716,17 @@
 by (force simp add: mult_strict_right_mono not_less [symmetric])
 
 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
-using mult_strict_left_mono [of zero b a] by simp
+using mult_strict_left_mono [of 0 b a] by simp
 
 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
-using mult_strict_left_mono [of b zero a] by simp
+using mult_strict_left_mono [of b 0 a] by simp
 
 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
-using mult_strict_right_mono [of a zero b] by simp
+using mult_strict_right_mono [of a 0 b] by simp
 
 text {* Legacy - use @{text mult_neg_pos} *}
 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
-by (drule mult_strict_right_mono [of b zero], auto)
+by (drule mult_strict_right_mono [of b 0], auto)
 
 lemma zero_less_mult_pos:
   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
@@ -763,18 +882,18 @@
 
 lemma mult_left_mono_neg:
   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
-  apply (drule mult_left_mono [of _ _ "uminus c"])
+  apply (drule mult_left_mono [of _ _ "- c"])
   apply simp_all
   done
 
 lemma mult_right_mono_neg:
   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
-  apply (drule mult_right_mono [of _ _ "uminus c"])
+  apply (drule mult_right_mono [of _ _ "- c"])
   apply simp_all
   done
 
 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
-using mult_right_mono_neg [of a zero b] by simp
+using mult_right_mono_neg [of a 0 b] by simp
 
 lemma split_mult_pos_le:
   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
@@ -821,7 +940,7 @@
 using mult_strict_right_mono [of b a "- c"] by simp
 
 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
-using mult_strict_right_mono_neg [of a zero b] by simp
+using mult_strict_right_mono_neg [of a 0 b] by simp
 
 subclass ring_no_zero_divisors
 proof
@@ -973,7 +1092,7 @@
 
 lemma pos_add_strict:
   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
-  using add_strict_mono [of zero a b c] by simp
+  using add_strict_mono [of 0 a b c] by simp
 
 lemma zero_le_one [simp]: "0 \<le> 1"
 by (rule zero_less_one [THEN less_imp_le]) 
@@ -1074,7 +1193,7 @@
   "sgn (a * b) = sgn a * sgn b"
 by (auto simp add: sgn_if zero_less_mult_iff)
 
-lemma abs_sgn: "abs k = k * sgn k"
+lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
 unfolding sgn_if abs_if by auto
 
 lemma sgn_greater [simp]:
@@ -1085,14 +1204,14 @@
   "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
-lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
-lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
 lemma dvd_if_abs_eq:
-  "abs l = abs (k) \<Longrightarrow> l dvd k"
+  "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
 by(subst abs_dvd_iff[symmetric]) simp
 
 end
@@ -1110,17 +1229,7 @@
     mult_cancel_right1 mult_cancel_right2
     mult_cancel_left1 mult_cancel_left2
 
--- {* FIXME continue localization here *}
-
-subsection {* Reasoning about inequalities with division *}
-
-lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
-    ==> x * y <= x"
-by (auto simp add: mult_le_cancel_left2)
-
-lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
-    ==> y * x <= x"
-by (auto simp add: mult_le_cancel_right2)
+text {* Reasoning about inequalities with division *}
 
 context linordered_semidom
 begin
@@ -1137,20 +1246,34 @@
 
 end
 
+context linordered_idom
+begin
 
-subsection {* Absolute Value *}
+lemma mult_right_le_one_le:
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
+  by (auto simp add: mult_le_cancel_left2)
+
+lemma mult_left_le_one_le:
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
+  by (auto simp add: mult_le_cancel_right2)
+
+end
+
+text {* Absolute Value *}
 
 context linordered_idom
 begin
 
-lemma mult_sgn_abs: "sgn x * abs x = x"
+lemma mult_sgn_abs:
+  "sgn x * \<bar>x\<bar> = x"
   unfolding abs_if sgn_if by auto
 
+lemma abs_one [simp]:
+  "\<bar>1\<bar> = 1"
+  by (simp add: abs_if zero_less_one [THEN less_not_sym])
+
 end
 
-lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
-by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
-
 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
   assumes abs_eq_mult:
     "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
@@ -1162,39 +1285,35 @@
 qed (auto simp add: abs_if not_less mult_less_0_iff)
 
 lemma abs_mult:
-  "abs (a * b) = abs a * abs b" 
+  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
   by (rule abs_eq_mult) auto
 
 lemma abs_mult_self:
-  "abs a * abs a = a * a"
+  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   by (simp add: abs_if) 
 
-end
-
 lemma abs_mult_less:
-     "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
+  "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
 proof -
-  assume ac: "abs a < c"
-  hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
-  assume "abs b < d"
+  assume ac: "\<bar>a\<bar> < c"
+  hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
+  assume "\<bar>b\<bar> < d"
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
-lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
-
-lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
-  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
+lemma less_minus_self_iff:
+  "a < - a \<longleftrightarrow> a < 0"
+  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
 
-lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
-apply (simp add: order_less_le abs_le_iff)  
-apply (auto simp add: abs_if)
-done
+lemma abs_less_iff:
+  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
+  by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
 
-lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
-    (abs y) * x = abs (y * x)"
-  apply (subst abs_mult)
-  apply simp
-done
+lemma abs_mult_pos:
+  "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
+  by (simp add: abs_mult)
+
+end
 
 code_modulename SML
   Rings Arith