--- a/src/HOL/Library/Float.thy Mon May 11 08:29:28 2009 -0700
+++ b/src/HOL/Library/Float.thy Wed Apr 29 20:19:50 2009 +0200
@@ -15,8 +15,17 @@
datatype float = Float int int
-primrec Ifloat :: "float \<Rightarrow> real" where
- "Ifloat (Float a b) = real a * pow2 b"
+primrec of_float :: "float \<Rightarrow> real" where
+ "of_float (Float a b) = real a * pow2 b"
+
+defs (overloaded)
+ real_of_float_def [code unfold]: "real == of_float"
+
+primrec mantissa :: "float \<Rightarrow> int" where
+ "mantissa (Float a b) = a"
+
+primrec scale :: "float \<Rightarrow> int" where
+ "scale (Float a b) = b"
instantiation float :: zero begin
definition zero_float where "0 = Float 0 0"
@@ -33,20 +42,17 @@
instance ..
end
-primrec mantissa :: "float \<Rightarrow> int" where
- "mantissa (Float a b) = a"
+lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
+ unfolding real_of_float_def using of_float.simps .
-primrec scale :: "float \<Rightarrow> int" where
- "scale (Float a b) = b"
-
-lemma Ifloat_neg_exp: "e < 0 \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
-lemma Ifloat_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
-lemma Ifloat_ge0_exp: "0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * (2^nat e)" by auto
+lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
+lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
+lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
lemma Float_num[simp]: shows
- "Ifloat (Float 1 0) = 1" and "Ifloat (Float 1 1) = 2" and "Ifloat (Float 1 2) = 4" and
- "Ifloat (Float 1 -1) = 1/2" and "Ifloat (Float 1 -2) = 1/4" and "Ifloat (Float 1 -3) = 1/8" and
- "Ifloat (Float -1 0) = -1" and "Ifloat (Float (number_of n) 0) = number_of n"
+ "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
+ "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
+ "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
by auto
lemma pow2_0[simp]: "pow2 0 = 1" by simp
@@ -131,7 +137,7 @@
lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
-lemma float_zero[simp]: "Ifloat (Float 0 e) = 0" by simp
+lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
by arith
@@ -142,7 +148,7 @@
termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
declare normfloat.simps[simp del]
-theorem normfloat[symmetric, simp]: "Ifloat f = Ifloat (normfloat f)"
+theorem normfloat[symmetric, simp]: "real f = real (normfloat f)"
proof (induct f rule: normfloat.induct)
case (1 a b)
have real2: "2 = real (2::int)"
@@ -217,7 +223,7 @@
lemma float_eq_odd_helper:
assumes odd: "odd a'"
- and floateq: "Ifloat (Float a b) = Ifloat (Float a' b')"
+ and floateq: "real (Float a b) = real (Float a' b')"
shows "b \<le> b'"
proof -
{
@@ -267,7 +273,7 @@
lemma float_eq_odd:
assumes odd1: "odd a"
and odd2: "odd a'"
- and floateq: "Ifloat (Float a b) = Ifloat (Float a' b')"
+ and floateq: "real (Float a b) = real (Float a' b')"
shows "a = a' \<and> b = b'"
proof -
from
@@ -278,14 +284,14 @@
qed
theorem normfloat_unique:
- assumes Ifloat_eq: "Ifloat f = Ifloat g"
+ assumes real_of_float_eq: "real f = real g"
shows "normfloat f = normfloat g"
proof -
from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto
from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto
- have "Ifloat (normfloat f) = Ifloat (normfloat g)"
- by (simp add: Ifloat_eq)
- then have float_eq: "Ifloat (Float a b) = Ifloat (Float a' b')"
+ have "real (normfloat f) = real (normfloat g)"
+ by (simp add: real_of_float_eq)
+ then have float_eq: "real (Float a b) = real (Float a' b')"
by (simp add: normf normg)
have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf])
have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
@@ -341,32 +347,32 @@
"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
instantiation float :: ord begin
-definition le_float_def: "z \<le> w \<equiv> Ifloat z \<le> Ifloat w"
-definition less_float_def: "z < w \<equiv> Ifloat z < Ifloat w"
+definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
+definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
instance ..
end
-lemma Ifloat_add[simp]: "Ifloat (a + b) = Ifloat a + Ifloat b"
+lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
by (cases a, cases b, simp add: algebra_simps plus_float.simps,
auto simp add: pow2_int[symmetric] pow2_add[symmetric])
-lemma Ifloat_minus[simp]: "Ifloat (- a) = - Ifloat a"
+lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
by (cases a, simp add: uminus_float.simps)
-lemma Ifloat_sub[simp]: "Ifloat (a - b) = Ifloat a - Ifloat b"
+lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
by (cases a, cases b, simp add: minus_float_def)
-lemma Ifloat_mult[simp]: "Ifloat (a*b) = Ifloat a * Ifloat b"
+lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
by (cases a, cases b, simp add: times_float.simps pow2_add)
-lemma Ifloat_0[simp]: "Ifloat 0 = 0"
+lemma real_of_float_0[simp]: "real (0 :: float) = 0"
by (auto simp add: zero_float_def float_zero)
-lemma Ifloat_1[simp]: "Ifloat 1 = 1"
+lemma real_of_float_1[simp]: "real (1 :: float) = 1"
by (auto simp add: one_float_def)
lemma zero_le_float:
- "(0 <= Ifloat (Float a b)) = (0 <= a)"
+ "(0 <= real (Float a b)) = (0 <= a)"
apply auto
apply (auto simp add: zero_le_mult_iff)
apply (insert zero_less_pow2[of b])
@@ -374,19 +380,19 @@
done
lemma float_le_zero:
- "(Ifloat (Float a b) <= 0) = (a <= 0)"
+ "(real (Float a b) <= 0) = (a <= 0)"
apply auto
apply (auto simp add: mult_le_0_iff)
apply (insert zero_less_pow2[of b])
apply auto
done
-declare Ifloat.simps[simp del]
+declare real_of_float_simp[simp del]
-lemma Ifloat_pprt[simp]: "Ifloat (float_pprt a) = pprt (Ifloat a)"
+lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero)
-lemma Ifloat_nprt[simp]: "Ifloat (float_nprt a) = nprt (Ifloat a)"
+lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
by (cases a, auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero)
instance float :: ab_semigroup_add
@@ -440,10 +446,10 @@
lemma float_less_simp: "((x::float) < y) = (0 < y - x)"
by (auto simp add: less_float_def)
-lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
-lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
+lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto
+lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto
-lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
+lemma float_power: "real (x ^ n :: float) = real x ^ n"
by (induct n) simp_all
lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
@@ -467,7 +473,7 @@
done
lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m"
- unfolding less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff
+ unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff
by auto
lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0"
@@ -480,7 +486,7 @@
assume "\<not> e < 0" hence "0 \<le> e" by auto
hence "1 \<le> pow2 e" unfolding pow2_def by auto
from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`]
- have "1 \<le> Float m e" by (simp add: le_float_def Ifloat.simps)
+ have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp)
thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto
qed
qed
@@ -490,7 +496,7 @@
have "e < 0" using float_pos_less1_e_neg assms by auto
have "\<And>x. (0::real) < 2^x" by auto
have "real m < 2^(nat (-e))" using `Float m e < 1`
- unfolding less_float_def Ifloat_neg_exp[OF `e < 0`] Ifloat_1
+ unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric]
real_mult_assoc by auto
thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
@@ -588,7 +594,7 @@
hence "0 < m" using float_pos_m_pos by auto
hence "m \<noteq> 0" and "1 < (2::int)" by auto
case False let ?S = "2^(nat (-e))"
- have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def Ifloat_nge0_exp[OF False] by auto
+ have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto
hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
hence "?S \<le> real m" unfolding mult_assoc by auto
hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
@@ -598,12 +604,12 @@
thus ?thesis by auto
qed
-lemma normalized_float: assumes "m \<noteq> 0" shows "Ifloat (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)"
+lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)"
proof (cases "- (bitlen m - 1) = 0")
- case True show ?thesis unfolding Ifloat.simps pow2_def using True by auto
+ case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
next
case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
- show ?thesis unfolding Ifloat_nge0_exp[OF P] real_divide_def by auto
+ show ?thesis unfolding real_of_float_nge0_exp[OF P] real_divide_def by auto
qed
lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
@@ -660,7 +666,7 @@
lemma lapprox_posrat:
assumes x: "0 \<le> x"
and y: "0 < y"
- shows "Ifloat (lapprox_posrat prec x y) \<le> real x / real y"
+ shows "real (lapprox_posrat prec x y) \<le> real x / real y"
proof -
let ?l = "nat (int prec + bitlen y - bitlen x)"
@@ -668,7 +674,7 @@
by (rule mult_right_mono, fact real_of_int_div4, simp)
also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto
- thus ?thesis unfolding lapprox_posrat_def Let_def normfloat Ifloat.simps
+ thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
unfolding pow2_minus pow2_int minus_minus .
qed
@@ -688,19 +694,19 @@
qed
lemma lapprox_posrat_bottom: assumes "0 < y"
- shows "real (x div y) \<le> Ifloat (lapprox_posrat n x y)"
+ shows "real (x div y) \<le> real (lapprox_posrat n x y)"
proof -
have pow: "\<And>x. (0::int) < 2^x" by auto
show ?thesis
- unfolding lapprox_posrat_def Let_def Ifloat_add normfloat Ifloat.simps pow2_minus pow2_int
+ unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
using real_of_int_div_mult[OF `0 < y` pow] by auto
qed
lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y"
- shows "0 \<le> Ifloat (lapprox_posrat n x y)"
+ shows "0 \<le> real (lapprox_posrat n x y)"
proof -
show ?thesis
- unfolding lapprox_posrat_def Let_def Ifloat_add normfloat Ifloat.simps pow2_minus pow2_int
+ unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg)
qed
@@ -716,7 +722,7 @@
lemma rapprox_posrat:
assumes x: "0 \<le> x"
and y: "0 < y"
- shows "real x / real y \<le> Ifloat (rapprox_posrat prec x y)"
+ shows "real x / real y \<le> real (rapprox_posrat prec x y)"
proof -
let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
show ?thesis
@@ -727,7 +733,7 @@
also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
- unfolding Ifloat.simps pow2_minus pow2_int minus_minus by auto
+ unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
next
case False
have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto
@@ -742,13 +748,13 @@
also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`]
unfolding real_divide_def ..
- finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False]
+ finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
unfolding pow2_minus pow2_int minus_minus by auto
qed
qed
lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
- shows "Ifloat (rapprox_posrat n x y) \<le> 1"
+ shows "real (rapprox_posrat n x y) \<le> 1"
proof -
let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
show ?thesis
@@ -760,7 +766,7 @@
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
- unfolding Ifloat.simps pow2_minus pow2_int minus_minus by auto
+ unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
next
case False
have "x \<noteq> y"
@@ -781,7 +787,7 @@
unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
by (rule mult_right_mono, auto)
hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
- thus ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False]
+ thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
unfolding pow2_minus pow2_int minus_minus by auto
qed
qed
@@ -798,9 +804,9 @@
qed
lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
- shows "Ifloat (rapprox_posrat n x y) < 1"
+ shows "real (rapprox_posrat n x y) < 1"
proof (cases "x = 0")
- case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat Ifloat.simps by auto
+ case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto
next
case False hence "0 < x" using `0 \<le> x` by auto
hence "x < y" using assms by auto
@@ -814,7 +820,7 @@
also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto
- finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_P[OF True]
+ finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True]
unfolding pow2_minus pow2_int minus_minus by auto
next
case False
@@ -855,7 +861,7 @@
unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
by (rule mult_strict_right_mono, auto)
hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
- thus ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False]
+ thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
unfolding pow2_minus pow2_int minus_minus by auto
qed
qed
@@ -890,7 +896,7 @@
else (if 0 < y then - (rapprox_posrat prec (-x) y) else lapprox_posrat prec (-x) (-y)))"
by auto
-lemma lapprox_rat: "Ifloat (lapprox_rat prec x y) \<le> real x / real y"
+lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y"
proof -
have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
show ?thesis
@@ -917,7 +923,7 @@
qed
lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y"
- shows "real (x div y) \<le> Ifloat (lapprox_rat n x y)"
+ shows "real (x div y) \<le> real (lapprox_rat n x y)"
unfolding lapprox_rat.simps(2)[OF assms] using lapprox_posrat_bottom[OF `0<y`] .
function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
@@ -935,7 +941,7 @@
(if 0 < y then - (lapprox_posrat prec (-x) y) else rapprox_posrat prec (-x) (-y)))"
by auto
-lemma rapprox_rat: "real x / real y \<le> Ifloat (rapprox_rat prec x y)"
+lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
proof -
have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
show ?thesis
@@ -962,19 +968,19 @@
qed
lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
- shows "Ifloat (rapprox_rat n x y) \<le> 1"
+ shows "real (rapprox_rat n x y) \<le> 1"
unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] .
lemma rapprox_rat_neg: assumes "x < 0" and "0 < y"
- shows "Ifloat (rapprox_rat n x y) \<le> 0"
+ shows "real (rapprox_rat n x y) \<le> 0"
unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "-x" y n] assms by auto
lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0"
- shows "Ifloat (rapprox_rat n x y) \<le> 0"
+ shows "real (rapprox_rat n x y) \<le> 0"
unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "-y" n] assms by auto
lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
- shows "Ifloat (rapprox_rat n x y) \<le> 0"
+ shows "real (rapprox_rat n x y) \<le> 0"
proof (cases "x = 0")
case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
unfolding True rapprox_posrat_def Let_def by auto
@@ -992,7 +998,7 @@
in
f * l)"
-lemma float_divl: "Ifloat (float_divl prec x y) \<le> Ifloat x / Ifloat y"
+lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
proof -
from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
@@ -1013,29 +1019,29 @@
apply (subst pow2_add[symmetric])
apply (simp add: field_simps)
done
- then have "Ifloat (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
+ then have "real (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
by (rule order_trans[OF lapprox_rat])
- then have "Ifloat (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)"
+ then have "real (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)"
apply (subst pos_le_divide_eq[symmetric])
apply simp_all
done
- then have "pow2 (sx - sy) * Ifloat (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)"
+ then have "pow2 (sx - sy) * real (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)"
by (simp add: algebra_simps)
then show ?thesis
- by (simp add: x y Let_def Ifloat.simps)
+ by (simp add: x y Let_def real_of_float_simp)
qed
lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y"
proof (cases x, cases y)
fix xm xe ym ye :: int
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
- have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 zero_le_mult_iff] by auto
- have "0 < ym" using `0 < y`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff] by auto
+ have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
+ have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
- have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto
- moreover have "0 \<le> Ifloat (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
+ have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
+ moreover have "0 \<le> real (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
ultimately show "0 \<le> float_divl prec x y"
- unfolding x_eq y_eq float_divl.simps Let_def le_float_def Ifloat_0 by (auto intro!: mult_nonneg_nonneg)
+ unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 by (auto intro!: mult_nonneg_nonneg)
qed
lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x"
@@ -1076,7 +1082,7 @@
show ?thesis
unfolding one_float_def Float float_divl.simps Let_def lapprox_rat.simps(2)[OF zero_le_one `0 < m`] lapprox_posrat_def `bitlen 1 = 1`
- unfolding le_float_def Ifloat_mult normfloat Ifloat.simps pow2_minus pow2_int e_nat
+ unfolding le_float_def real_of_float_mult normfloat real_of_float_simp pow2_minus pow2_int e_nat
using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
qed
@@ -1089,7 +1095,7 @@
in
f * r)"
-lemma float_divr: "Ifloat x / Ifloat y \<le> Ifloat (float_divr prec x y)"
+lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
proof -
from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
@@ -1109,20 +1115,20 @@
apply (subst pow2_add[symmetric])
apply (simp add: field_simps)
done
- then have "Ifloat (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
+ then have "real (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
by (rule order_trans[OF _ rapprox_rat])
- then have "Ifloat (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)"
+ then have "real (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)"
apply (subst pos_divide_le_eq[symmetric])
apply simp_all
done
then show ?thesis
- by (simp add: x y Let_def algebra_simps Ifloat.simps)
+ by (simp add: x y Let_def algebra_simps real_of_float_simp)
qed
lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
proof -
- have "1 \<le> 1 / Ifloat x" using `0 < x` and `x < 1` unfolding less_float_def by auto
- also have "\<dots> \<le> Ifloat (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
+ have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
+ also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
finally show ?thesis unfolding le_float_def by auto
qed
@@ -1130,27 +1136,27 @@
proof (cases x, cases y)
fix xm xe ym ye :: int
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
- have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 mult_le_0_iff] by auto
- have "0 < ym" using `0 < y`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff] by auto
+ have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 mult_le_0_iff] by auto
+ have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
- have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto
- moreover have "Ifloat (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] .
+ have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
+ moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] .
ultimately show "float_divr prec x y \<le> 0"
- unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos)
+ unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
qed
lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0"
proof (cases x, cases y)
fix xm xe ym ye :: int
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
- have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 zero_le_mult_iff] by auto
- have "ym < 0" using `y < 0`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 mult_less_0_iff] by auto
+ have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
+ have "ym < 0" using `y < 0`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 mult_less_0_iff] by auto
hence "0 < - ym" by auto
- have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto
- moreover have "Ifloat (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] .
+ have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
+ moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] .
ultimately show "float_divr prec x y \<le> 0"
- unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos)
+ unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
qed
primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
@@ -1163,7 +1169,7 @@
if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d)
else Float m e)"
-lemma round_up: "Ifloat x \<le> Ifloat (round_up prec x)"
+lemma round_up: "real x \<le> real (round_up prec x)"
proof (cases x)
case (Float m e)
let ?d = "bitlen m - int prec"
@@ -1177,7 +1183,7 @@
proof (cases "m mod ?p = 0")
case True
have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
- have "Ifloat (Float m e) = Ifloat (Float (m div ?p) (e + ?d))" unfolding Ifloat.simps arg_cong[OF m, of real]
+ have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
by (auto simp add: pow2_add `0 < ?d` pow_d)
thus ?thesis
unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
@@ -1186,7 +1192,7 @@
case False
have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
- finally have "Ifloat (Float m e) \<le> Ifloat (Float (m div ?p + 1) (e + ?d))" unfolding Ifloat.simps add_commute[of e]
+ finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
thus ?thesis
@@ -1199,7 +1205,7 @@
qed
qed
-lemma round_down: "Ifloat (round_down prec x) \<le> Ifloat x"
+lemma round_down: "real (round_down prec x) \<le> real x"
proof (cases x)
case (Float m e)
let ?d = "bitlen m - int prec"
@@ -1211,7 +1217,7 @@
hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
- finally have "Ifloat (Float (m div ?p) (e + ?d)) \<le> Ifloat (Float m e)" unfolding Ifloat.simps add_commute[of e]
+ finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
thus ?thesis
@@ -1235,12 +1241,12 @@
in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
else Float m e)"
-lemma lb_mult: "Ifloat (lb_mult prec x y) \<le> Ifloat (x * y)"
+lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
proof (cases "normfloat (x * y)")
case (Float m e)
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
let ?l = "bitlen m - int prec"
- have "Ifloat (lb_mult prec x y) \<le> Ifloat (normfloat (x * y))"
+ have "real (lb_mult prec x y) \<le> real (normfloat (x * y))"
proof (cases "?l > 0")
case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto
next
@@ -1253,19 +1259,19 @@
also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
finally show ?thesis by auto
qed
- thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] Ifloat.simps pow2_add real_mult_commute real_mult_assoc by auto
+ thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
qed
- also have "\<dots> = Ifloat (x * y)" unfolding normfloat ..
+ also have "\<dots> = real (x * y)" unfolding normfloat ..
finally show ?thesis .
qed
-lemma ub_mult: "Ifloat (x * y) \<le> Ifloat (ub_mult prec x y)"
+lemma ub_mult: "real (x * y) \<le> real (ub_mult prec x y)"
proof (cases "normfloat (x * y)")
case (Float m e)
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
let ?l = "bitlen m - int prec"
- have "Ifloat (x * y) = Ifloat (normfloat (x * y))" unfolding normfloat ..
- also have "\<dots> \<le> Ifloat (ub_mult prec x y)"
+ have "real (x * y) = real (normfloat (x * y))" unfolding normfloat ..
+ also have "\<dots> \<le> real (ub_mult prec x y)"
proof (cases "?l > 0")
case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto
next
@@ -1280,7 +1286,7 @@
also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto
finally show ?thesis unfolding pow2_int[symmetric] using True by auto
qed
- thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] Ifloat.simps pow2_add real_mult_commute real_mult_assoc by auto
+ thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
qed
finally show ?thesis .
qed
@@ -1293,28 +1299,28 @@
instance ..
end
-lemma Ifloat_abs: "Ifloat \<bar>x\<bar> = \<bar>Ifloat x\<bar>"
+lemma real_of_float_abs: "real \<bar>x :: float\<bar> = \<bar>real x\<bar>"
proof (cases x)
case (Float m e)
have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto
- thus ?thesis unfolding Float abs_float_def float_abs.simps Ifloat.simps by auto
+ thus ?thesis unfolding Float abs_float_def float_abs.simps real_of_float_simp by auto
qed
primrec floor_fl :: "float \<Rightarrow> float" where
"floor_fl (Float m e) = (if 0 \<le> e then Float m e
else Float (m div (2 ^ (nat (-e)))) 0)"
-lemma floor_fl: "Ifloat (floor_fl x) \<le> Ifloat x"
+lemma floor_fl: "real (floor_fl x) \<le> real x"
proof (cases x)
case (Float m e)
show ?thesis
proof (cases "0 \<le> e")
case False
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
- have "Ifloat (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding Ifloat.simps by auto
+ have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
- also have "\<dots> = Ifloat (Float m e)" unfolding Ifloat.simps me_eq pow2_int pow2_neg[of e] ..
+ also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
next
case True thus ?thesis unfolding Float by auto
@@ -1333,17 +1339,17 @@
"ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
else Float (m div (2 ^ (nat (-e))) + 1) 0)"
-lemma ceiling_fl: "Ifloat x \<le> Ifloat (ceiling_fl x)"
+lemma ceiling_fl: "real x \<le> real (ceiling_fl x)"
proof (cases x)
case (Float m e)
show ?thesis
proof (cases "0 \<le> e")
case False
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
- have "Ifloat (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding Ifloat.simps me_eq pow2_int pow2_neg[of e] ..
+ have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
- also have "\<dots> = Ifloat (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding Ifloat.simps by auto
+ also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
next
case True thus ?thesis unfolding Float by auto
@@ -1358,48 +1364,48 @@
definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
-lemma lb_mod: fixes k :: int assumes "0 \<le> Ifloat x" and "real k * y \<le> Ifloat x" (is "?k * y \<le> ?x")
- assumes "0 < Ifloat lb" "Ifloat lb \<le> y" (is "?lb \<le> y") "y \<le> Ifloat ub" (is "y \<le> ?ub")
- shows "Ifloat (lb_mod prec x ub lb) \<le> ?x - ?k * y"
+lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
+ assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
+ shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
proof -
have "?lb \<le> ?ub" by (auto!)
have "0 \<le> ?lb" and "?lb \<noteq> 0" by (auto!)
have "?k * y \<le> ?x" using assms by auto
also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`])
- also have "\<dots> \<le> Ifloat (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
- finally show ?thesis unfolding lb_mod_def Ifloat_sub Ifloat_mult by auto
+ also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
+ finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
qed
-lemma ub_mod: fixes k :: int assumes "0 \<le> Ifloat x" and "Ifloat x \<le> real k * y" (is "?x \<le> ?k * y")
- assumes "0 < Ifloat lb" "Ifloat lb \<le> y" (is "?lb \<le> y") "y \<le> Ifloat ub" (is "y \<le> ?ub")
- shows "?x - ?k * y \<le> Ifloat (ub_mod prec x ub lb)"
+lemma ub_mod: fixes k :: int and x :: float assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
+ assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
+ shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
proof -
have "?lb \<le> ?ub" by (auto!)
hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" by (auto!)
- have "Ifloat (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
+ have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`])
also have "\<dots> \<le> ?k * y" using assms by auto
- finally show ?thesis unfolding ub_mod_def Ifloat_sub Ifloat_mult by auto
+ finally show ?thesis unfolding ub_mod_def real_of_float_sub real_of_float_mult by auto
qed
lemma le_float_def': "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)"
proof -
- have le_transfer: "(f \<le> g) = (Ifloat (f - g) \<le> 0)" by (auto simp add: le_float_def)
+ have le_transfer: "(f \<le> g) = (real (f - g) \<le> 0)" by (auto simp add: le_float_def)
from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
- with le_transfer have le_transfer': "f \<le> g = (Ifloat (Float a b) \<le> 0)" by simp
+ with le_transfer have le_transfer': "f \<le> g = (real (Float a b) \<le> 0)" by simp
show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero)
qed
lemma float_less_zero:
- "(Ifloat (Float a b) < 0) = (a < 0)"
- apply (auto simp add: mult_less_0_iff Ifloat.simps)
+ "(real (Float a b) < 0) = (a < 0)"
+ apply (auto simp add: mult_less_0_iff real_of_float_simp)
done
lemma less_float_def': "f < g = (case f - g of Float a b \<Rightarrow> a < 0)"
proof -
- have less_transfer: "(f < g) = (Ifloat (f - g) < 0)" by (auto simp add: less_float_def)
+ have less_transfer: "(f < g) = (real (f - g) < 0)" by (auto simp add: less_float_def)
from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
- with less_transfer have less_transfer': "f < g = (Ifloat (Float a b) < 0)" by simp
+ with less_transfer have less_transfer': "f < g = (real (Float a b) < 0)" by simp
show ?thesis by (simp add: less_transfer' f_diff_g float_less_zero)
qed