src/HOL/Real/RealDef.thy
changeset 24198 4031da6d8ba3
parent 24075 366d4d234814
child 24506 020db6ec334a
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:49 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Aug 09 15:52:53 2007 +0200
     1.3 @@ -25,39 +25,42 @@
     1.4    real_of_preal :: "preal => real" where
     1.5    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
     1.6  
     1.7 -consts
     1.8 -   (*overloaded constant for injecting other types into "real"*)
     1.9 -   real :: "'a => real"
    1.10 -
    1.11  instance real :: zero
    1.12    real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
    1.13 +lemmas [code func del] = real_zero_def
    1.14  
    1.15  instance real :: one
    1.16    real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
    1.17 +lemmas [code func del] = real_one_def
    1.18  
    1.19  instance real :: plus
    1.20    real_add_def: "z + w ==
    1.21         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.22  		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
    1.23 +lemmas [code func del] = real_add_def
    1.24  
    1.25  instance real :: minus
    1.26    real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.27    real_diff_def: "r - (s::real) == r + - s" ..
    1.28 +lemmas [code func del] = real_minus_def real_diff_def
    1.29  
    1.30  instance real :: times
    1.31    real_mult_def:
    1.32      "z * w ==
    1.33         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.34  		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
    1.35 +lemmas [code func del] = real_mult_def
    1.36  
    1.37  instance real :: inverse
    1.38    real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    1.39    real_divide_def: "R / (S::real) == R * inverse S" ..
    1.40 +lemmas [code func del] = real_inverse_def real_divide_def
    1.41  
    1.42  instance real :: ord
    1.43    real_le_def: "z \<le> (w::real) == 
    1.44      \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
    1.45    real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
    1.46 +lemmas [code func del] = real_le_def real_less_def
    1.47  
    1.48  instance real :: abs
    1.49    real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
    1.50 @@ -520,23 +523,36 @@
    1.51  by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
    1.52  
    1.53  
    1.54 -subsection{*Embedding the Integers into the Reals*}
    1.55 +subsection {* Embedding numbers into the Reals *}
    1.56 +
    1.57 +abbreviation
    1.58 +  real_of_nat :: "nat \<Rightarrow> real"
    1.59 +where
    1.60 +  "real_of_nat \<equiv> of_nat"
    1.61 +
    1.62 +abbreviation
    1.63 +  real_of_int :: "int \<Rightarrow> real"
    1.64 +where
    1.65 +  "real_of_int \<equiv> of_int"
    1.66 +
    1.67 +abbreviation
    1.68 +  real_of_rat :: "rat \<Rightarrow> real"
    1.69 +where
    1.70 +  "real_of_rat \<equiv> of_rat"
    1.71 +
    1.72 +consts
    1.73 +  (*overloaded constant for injecting other types into "real"*)
    1.74 +  real :: "'a => real"
    1.75  
    1.76  defs (overloaded)
    1.77 -  real_of_nat_def: "real z == of_nat z"
    1.78 -  real_of_int_def: "real z == of_int z"
    1.79 +  real_of_nat_def [code unfold]: "real == real_of_nat"
    1.80 +  real_of_int_def [code unfold]: "real == real_of_int"
    1.81  
    1.82  lemma real_eq_of_nat: "real = of_nat"
    1.83 -  apply (rule ext)
    1.84 -  apply (unfold real_of_nat_def)
    1.85 -  apply (rule refl)
    1.86 -  done
    1.87 +  unfolding real_of_nat_def ..
    1.88  
    1.89  lemma real_eq_of_int: "real = of_int"
    1.90 -  apply (rule ext)
    1.91 -  apply (unfold real_of_int_def)
    1.92 -  apply (rule refl)
    1.93 -  done
    1.94 +  unfolding real_of_int_def ..
    1.95  
    1.96  lemma real_of_int_zero [simp]: "real (0::int) = 0"  
    1.97  by (simp add: real_of_int_def) 
    1.98 @@ -811,14 +827,14 @@
    1.99  
   1.100  subsection{*Numerals and Arithmetic*}
   1.101  
   1.102 -instance real :: number ..
   1.103 +instance real :: number_ring
   1.104 +  real_number_of_def: "number_of w \<equiv> real_of_int w"
   1.105 +  by intro_classes (simp add: real_number_of_def)
   1.106  
   1.107 -defs (overloaded)
   1.108 -  real_number_of_def: "(number_of w :: real) == of_int w"
   1.109 -    --{*the type constraint is essential!*}
   1.110 +lemma [code, code unfold]:
   1.111 +  "number_of k = real_of_int (number_of k)"
   1.112 +  unfolding number_of_is_id real_number_of_def ..
   1.113  
   1.114 -instance real :: number_ring
   1.115 -by (intro_classes, simp add: real_number_of_def) 
   1.116  
   1.117  text{*Collapse applications of @{term real} to @{term number_of}*}
   1.118  lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   1.119 @@ -940,8 +956,4 @@
   1.120    "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
   1.121    "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
   1.122  
   1.123 -lemma [code, code unfold]:
   1.124 -  "number_of k = real (number_of k :: int)"
   1.125 -  by simp
   1.126 -
   1.127  end