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))"
```