src/HOL/Ring_and_Field.thy
changeset 24491 8d194c9198ae
parent 24427 bc5cf3b09ff3
child 24506 020db6ec334a
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Aug 30 21:43:08 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Aug 30 21:43:31 2007 +0200
     1.3 @@ -333,6 +333,9 @@
     1.4  class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
     1.5    (*previously ordered_ring*)
     1.6  
     1.7 +definition (in ordered_idom) sgn where
     1.8 +"sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<sqsubset> x then \<^loc>1 else uminus \<^loc>1)"
     1.9 +
    1.10  instance ordered_idom \<subseteq> ordered_ring_strict ..
    1.11  
    1.12  instance ordered_idom \<subseteq> pordered_comm_ring ..
    1.13 @@ -1896,6 +1899,10 @@
    1.14  
    1.15  subsection {* Absolute Value *}
    1.16  
    1.17 +lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
    1.18 +using less_linear[of x 0]
    1.19 +by(auto simp: sgn_def abs_if)
    1.20 +
    1.21  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
    1.22  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
    1.23