more localisation
authorhaftmann
Wed Apr 22 19:09:22 2009 +0200 (2009-04-22)
changeset 30961541bfff659af
parent 30960 fec1a04b7220
child 30962 f5fd07c558f9
more localisation
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Wed Apr 22 19:09:21 2009 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Apr 22 19:09:22 2009 +0200
     1.3 @@ -2226,15 +2226,21 @@
     1.4  qed
     1.5  qed
     1.6  
     1.7 -instance ordered_idom \<subseteq> pordered_ring_abs
     1.8 -by default (auto simp add: abs_if not_less
     1.9 -  equal_neg_zero neg_equal_zero mult_less_0_iff)
    1.10 -
    1.11 -lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
    1.12 -by (simp add: abs_eq_mult linorder_linear)
    1.13 -
    1.14 -lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
    1.15 -by (simp add: abs_if) 
    1.16 +context ordered_idom
    1.17 +begin
    1.18 +
    1.19 +subclass pordered_ring_abs proof
    1.20 +qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
    1.21 +
    1.22 +lemma abs_mult:
    1.23 +  "abs (a * b) = abs a * abs b" 
    1.24 +  by (rule abs_eq_mult) auto
    1.25 +
    1.26 +lemma abs_mult_self:
    1.27 +  "abs a * abs a = a * a"
    1.28 +  by (simp add: abs_if) 
    1.29 +
    1.30 +end
    1.31  
    1.32  lemma nonzero_abs_inverse:
    1.33       "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"