src/HOL/Ring_and_Field.thy
changeset 15229 1eb23f805c06
parent 15228 4d332d10fa3d
child 15234 ec91a90c604e
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:28:03 2004 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Oct 05 15:30:50 2004 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header {* (Ordered) Rings and Fields *}
     1.6  
     1.7 -theory Ring_and_Field 
     1.8 +theory Ring_and_Field
     1.9  imports OrderedGroup
    1.10  begin
    1.11  
    1.12 @@ -1371,6 +1371,12 @@
    1.13  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
    1.14    by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
    1.15  
    1.16 +lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
    1.17 +by (simp add: abs_if linorder_not_less [symmetric]) 
    1.18 +
    1.19 +lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
    1.20 +by (simp add: abs_if linorder_not_less [symmetric])
    1.21 +
    1.22  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
    1.23  proof -
    1.24    let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"