src/HOL/Ring_and_Field.thy

   using add_strict_mono [of 0 a b c] by simp
 
 class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
   (*previously ordered_ring*)
 
+definition (in ordered_idom) sgn where
+"sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<sqsubset> x then \<^loc>1 else uminus \<^loc>1)"
+
 instance ordered_idom \<subseteq> ordered_ring_strict ..
 
 instance ordered_idom \<subseteq> pordered_comm_ring ..
 
 class ordered_field = field + ordered_idom

   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
 qed
 
 
 subsection {* Absolute Value *}
+
+lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
+using less_linear[of x 0]
+by(auto simp: sgn_def abs_if)
 
 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_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"