--- a/src/HOL/Ring_and_Field.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Tue Oct 05 15:30:50 2004 +0200
@@ -5,7 +5,7 @@
header {* (Ordered) Rings and Fields *}
-theory Ring_and_Field
+theory Ring_and_Field
imports OrderedGroup
begin
@@ -1371,6 +1371,12 @@
lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
+by (simp add: abs_if linorder_not_less [symmetric])
+
+lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
+by (simp add: abs_if linorder_not_less [symmetric])
+
lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
proof -
let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"