1.1 --- a/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -25,48 +25,54 @@
     1.4    real_of_preal :: "preal => real" where
     1.5    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
     1.6  
     1.7 -instance real :: zero
     1.8 -  real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
     1.9 -lemmas [code func del] = real_zero_def
    1.10 +instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
    1.11 +begin
    1.12  
    1.13 -instance real :: one
    1.14 -  real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
    1.15 -lemmas [code func del] = real_one_def
    1.16 +definition
    1.17 +  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
    1.18 +
    1.19 +definition
    1.20 +  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
    1.21  
    1.22 -instance real :: plus
    1.23 -  real_add_def: "z + w ==
    1.24 +definition
    1.25 +  real_add_def [code func del]: "z + w =
    1.26         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.27 -		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
    1.28 -lemmas [code func del] = real_add_def
    1.29 +		 { Abs_Real(realrel``{(x+u, y+v)}) })"
    1.30  
    1.31 -instance real :: minus
    1.32 -  real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.33 -  real_diff_def: "r - (s::real) == r + - s" ..
    1.34 -lemmas [code func del] = real_minus_def real_diff_def
    1.35 +definition
    1.36 +  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.37 +
    1.38 +definition
    1.39 +  real_diff_def [code func del]: "r - (s::real) = r + - s"
    1.40  
    1.41 -instance real :: times
    1.42 -  real_mult_def:
    1.43 -    "z * w ==
    1.44 +definition
    1.45 +  real_mult_def [code func del]:
    1.46 +    "z * w =
    1.47         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.48 -		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
    1.49 -lemmas [code func del] = real_mult_def
    1.50 +		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    1.51  
    1.52 -instance real :: inverse
    1.53 -  real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    1.54 -  real_divide_def: "R / (S::real) == R * inverse S" ..
    1.55 -lemmas [code func del] = real_inverse_def real_divide_def
    1.56 +definition
    1.57 +  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
    1.58 +
    1.59 +definition
    1.60 +  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
    1.61  
    1.62 -instance real :: ord
    1.63 -  real_le_def: "z \<le> (w::real) == 
    1.64 -    \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
    1.65 -  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
    1.66 -lemmas [code func del] = real_le_def real_less_def
    1.67 +definition
    1.68 +  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
    1.69 +    (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
    1.70 +
    1.71 +definition
    1.72 +  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.73  
    1.74 -instance real :: abs
    1.75 -  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
    1.76 +definition
    1.77 +  real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
    1.78  
    1.79 -instance real :: sgn
    1.80 -  real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
    1.81 +definition
    1.82 +  real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
    1.83 +
    1.84 +instance ..
    1.85 +
    1.86 +end
    1.87  
    1.88  subsection {* Equivalence relation over positive reals *}
    1.89  
    1.90 @@ -400,11 +406,20 @@
    1.91  apply (simp add: right_distrib)
    1.92  done
    1.93  
    1.94 -instance real :: distrib_lattice
    1.95 -  "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
    1.96 -  "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
    1.97 +instantiation real :: distrib_lattice
    1.98 +begin
    1.99 +
   1.100 +definition
   1.101 +  "(inf \<Colon> real \<Rightarrow> real \<Rightarrow> real) = min"
   1.102 +
   1.103 +definition
   1.104 +  "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
   1.105 +
   1.106 +instance
   1.107    by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
   1.108  
   1.109 +end
   1.110 +
   1.111  
   1.112  subsection{*The Reals Form an Ordered Field*}
   1.113  
   1.114 @@ -833,10 +848,17 @@
   1.115  
   1.116  subsection{*Numerals and Arithmetic*}
   1.117  
   1.118 -instance real :: number_ring
   1.119 -  real_number_of_def: "number_of w \<equiv> real_of_int w"
   1.120 +instantiation real :: number_ring
   1.121 +begin
   1.122 +
   1.123 +definition
   1.124 +  real_number_of_def: "number_of w = real_of_int w"
   1.125 +
   1.126 +instance
   1.127    by intro_classes (simp add: real_number_of_def)
   1.128  
   1.129 +end
   1.130 +
   1.131  lemma [code, code unfold]:
   1.132    "number_of k = real_of_int (number_of k)"
   1.133    unfolding number_of_is_id real_number_of_def ..