src/HOL/Real/Float.thy
changeset 21404 eb85850d3eb7
parent 21256 47195501ecf7
child 22964 2284e0d02e7f
     1.1 --- a/src/HOL/Real/Float.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Real/Float.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -11,9 +11,11 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  pow2 :: "int \<Rightarrow> real"
     1.8 +  pow2 :: "int \<Rightarrow> real" where
     1.9    "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
    1.10 -  float :: "int * int \<Rightarrow> real"
    1.11 +
    1.12 +definition
    1.13 +  float :: "int * int \<Rightarrow> real" where
    1.14    "float x = real (fst x) * pow2 (snd x)"
    1.15  
    1.16  lemma pow2_0[simp]: "pow2 0 = 1"
    1.17 @@ -99,9 +101,11 @@
    1.18  by (simp add: float_def ring_eq_simps)
    1.19  
    1.20  definition
    1.21 -  int_of_real :: "real \<Rightarrow> int"
    1.22 +  int_of_real :: "real \<Rightarrow> int" where
    1.23    "int_of_real x = (SOME y. real y = x)"
    1.24 -  real_is_int :: "real \<Rightarrow> bool"
    1.25 +
    1.26 +definition
    1.27 +  real_is_int :: "real \<Rightarrow> bool" where
    1.28    "real_is_int x = (EX (u::int). x = real u)"
    1.29  
    1.30  lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"