src/HOL/Real/RealDef.thy
changeset 26732 6ea9de67e576
parent 26513 6f306c8c2c54
child 27106 ff27dc6e7d05
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:13 2008 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:16 2008 +0200
     1.3 @@ -950,6 +950,13 @@
     1.4  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
     1.5  by simp
     1.6  
     1.7 +instance real :: lordered_ring
     1.8 +proof
     1.9 +  fix a::real
    1.10 +  show "abs a = sup a (-a)"
    1.11 +    by (auto simp add: real_abs_def sup_real_def)
    1.12 +qed
    1.13 +
    1.14  
    1.15  subsection {* Implementation of rational real numbers as pairs of integers *}
    1.16  
    1.17 @@ -981,11 +988,11 @@
    1.18  instantiation real :: eq
    1.19  begin
    1.20  
    1.21 -definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
    1.22 +definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x = y"
    1.23  
    1.24  instance by default (simp add: eq_real_def)
    1.25  
    1.26 -lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
    1.27 +lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
    1.28    unfolding Ratreal_def INum_normNum_iff eq ..
    1.29  
    1.30  end
    1.31 @@ -1024,13 +1031,6 @@
    1.32  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
    1.33    unfolding Ratreal_def by simp
    1.34  
    1.35 -instance real :: lordered_ring
    1.36 -proof
    1.37 -  fix a::real
    1.38 -  show "abs a = sup a (-a)"
    1.39 -    by (auto simp add: real_abs_def sup_real_def)
    1.40 -qed
    1.41 -
    1.42  text {* Setup for SML code generator *}
    1.43  
    1.44  types_code