src/HOL/Ring_and_Field.thy
changeset 24506 020db6ec334a
parent 24491 8d194c9198ae
child 24515 d4dc5dc2db98
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Aug 31 23:17:25 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Sep 01 01:21:48 2007 +0200
     1.3 @@ -299,6 +299,9 @@
     1.4  class abs_if = minus + ord + zero + abs +
     1.5    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
     1.6  
     1.7 +class sgn_if = sgn + zero + one + minus + ord +
     1.8 +assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
     1.9 +
    1.10  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    1.11     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
    1.12   *)
    1.13 @@ -311,7 +314,8 @@
    1.14      by (simp only: abs_if sup_eq_if)
    1.15  qed
    1.16  
    1.17 -class ordered_ring_strict = ring + ordered_semiring_strict + lordered_ab_group + abs_if
    1.18 +class ordered_ring_strict =
    1.19 +  ring + ordered_semiring_strict + lordered_ab_group + abs_if
    1.20  
    1.21  instance ordered_ring_strict \<subseteq> ordered_ring ..
    1.22  
    1.23 @@ -330,12 +334,13 @@
    1.24    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    1.25    using add_strict_mono [of 0 a b c] by simp
    1.26  
    1.27 -class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
    1.28 +class ordered_idom =
    1.29 +  comm_ring_1 +
    1.30 +  ordered_comm_semiring_strict +
    1.31 +  lordered_ab_group +
    1.32 +  abs_if + sgn_if
    1.33    (*previously ordered_ring*)
    1.34  
    1.35 -definition (in ordered_idom) sgn where
    1.36 -"sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<sqsubset> x then \<^loc>1 else uminus \<^loc>1)"
    1.37 -
    1.38  instance ordered_idom \<subseteq> ordered_ring_strict ..
    1.39  
    1.40  instance ordered_idom \<subseteq> pordered_comm_ring ..
    1.41 @@ -1901,7 +1906,7 @@
    1.42  
    1.43  lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
    1.44  using less_linear[of x 0]
    1.45 -by(auto simp: sgn_def abs_if)
    1.46 +by(auto simp: sgn_if abs_if)
    1.47  
    1.48  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
    1.49  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])