instance int,real :: lordered_ring
authorobua
Wed Dec 05 16:54:50 2007 +0100 (2007-12-05)
changeset 255464f8d7ac83c0b
parent 25545 21cd20c1ce98
child 25547 ffa6e91b7add
instance int,real :: lordered_ring
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Dec 05 14:36:58 2007 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Dec 05 16:54:50 2007 +0100
     1.3 @@ -993,6 +993,20 @@
     1.4  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
     1.5    unfolding Ratreal_def by simp
     1.6  
     1.7 +instance int :: lordered_ring
     1.8 +proof  
     1.9 +  fix a::int
    1.10 +  show "abs a = sup a (- a)"
    1.11 +    by (auto simp add: zabs_def sup_int_def)
    1.12 +qed
    1.13 +
    1.14 +instance real :: lordered_ring
    1.15 +proof
    1.16 +  fix a::real
    1.17 +  show "abs a = sup a (-a)"
    1.18 +    by (auto simp add: real_abs_def sup_real_def)
    1.19 +qed
    1.20 +
    1.21  text {* Setup for SML code generator *}
    1.22  
    1.23  types_code