--- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 18 14:29:21 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 18 14:29:22 2012 +0200
@@ -12,6 +12,9 @@
"~~/src/HOL/Library/Efficient_Nat"
begin
+declare powr_numeral[simp]
+declare powr_neg_numeral[simp]
+
section "Horner Scheme"
subsection {* Define auxiliary helper @{text horner} function *}
@@ -148,7 +151,7 @@
case True
show ?thesis
proof (cases "0 < l")
- case True hence "odd n \<or> 0 < l" and "0 \<le> real l" unfolding less_float_def by auto
+ case True hence "odd n \<or> 0 < l" and "0 \<le> real l" by auto
have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms
unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
have "real l ^ n \<le> x ^ n" and "x ^ n \<le> real u ^ n " using `0 \<le> real l` assms
@@ -158,7 +161,7 @@
case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
show ?thesis
proof (cases "u < 0")
- case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms unfolding less_float_def by auto
+ case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms by auto
hence "real u ^ n \<le> x ^ n" and "x ^ n \<le> real l ^ n" using power_mono[of "-x" "-real l" n] power_mono[of "-real u" "-x" n]
unfolding power_minus_even[OF `even n`] by auto
moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
@@ -167,9 +170,9 @@
case False
have "\<bar>x\<bar> \<le> real (max (-l) u)"
proof (cases "-l \<le> u")
- case True thus ?thesis unfolding max_def if_P[OF True] using assms unfolding less_eq_float_def by auto
+ case True thus ?thesis unfolding max_def if_P[OF True] using assms by auto
next
- case False thus ?thesis unfolding max_def if_not_P[OF False] using assms unfolding less_eq_float_def by auto
+ case False thus ?thesis unfolding max_def if_not_P[OF False] using assms by auto
qed
hence x_abs: "\<bar>x\<bar> \<le> \<bar>real (max (-l) u)\<bar>" by auto
have u1: "u1 = (max (-l) u) ^ n" and l1: "l1 = 0" using assms unfolding float_power_bnds_def if_not_P[OF P] if_not_P[OF False] by auto
@@ -215,7 +218,7 @@
else if x < 0 then - ub_sqrt prec (- x)
else 0)"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
+termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
declare lb_sqrt.simps[simp del]
declare ub_sqrt.simps[simp del]
@@ -284,7 +287,7 @@
qed
finally show ?thesis using `0 < m`
unfolding Float
- by (subst compute_sqrt_iteration_base) (simp add: ac_simps real_Float del: Float_def)
+ by (subst compute_sqrt_iteration_base) (simp add: ac_simps)
qed
next
case (Suc n)
@@ -308,20 +311,20 @@
lemma lb_sqrt_lower_bound: assumes "0 \<le> real x"
shows "0 \<le> real (lb_sqrt prec x)"
proof (cases "0 < x")
- case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` unfolding less_float_def less_eq_float_def by auto
- hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto
+ case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` by auto
+ hence "0 < sqrt_iteration prec prec x" using sqrt_iteration_lower_bound by auto
hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \<le> x`] unfolding less_eq_float_def by auto
thus ?thesis unfolding lb_sqrt.simps using True by auto
next
- case False with `0 \<le> real x` have "real x = 0" unfolding less_float_def by auto
- thus ?thesis unfolding lb_sqrt.simps less_float_def by auto
+ case False with `0 \<le> real x` have "real x = 0" by auto
+ thus ?thesis unfolding lb_sqrt.simps by auto
qed
lemma bnds_sqrt':
shows "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x) }"
proof -
{ fix x :: float assume "0 < x"
- hence "0 < real x" and "0 \<le> real x" unfolding less_float_def by auto
+ hence "0 < real x" and "0 \<le> real x" by auto
hence sqrt_gt0: "0 < sqrt x" by auto
hence sqrt_ub: "sqrt x < sqrt_iteration prec prec x" using sqrt_iteration_bound by auto
@@ -338,7 +341,7 @@
note lb = this
{ fix x :: float assume "0 < x"
- hence "0 < real x" unfolding less_float_def by auto
+ hence "0 < real x" by auto
hence "0 < sqrt x" by auto
hence "sqrt x < sqrt_iteration prec prec x"
using sqrt_iteration_bound by auto
@@ -352,10 +355,10 @@
next case False show ?thesis
proof (cases "real x = 0")
case True thus ?thesis
- by (auto simp add: less_float_def lb_sqrt.simps ub_sqrt.simps)
+ by (auto simp add: lb_sqrt.simps ub_sqrt.simps)
next
case False with `\<not> 0 < x` have "x < 0" and "0 < -x"
- by (auto simp add: less_float_def)
+ by auto
with `\<not> 0 < x`
show ?thesis using lb[OF `0 < -x`] ub[OF `0 < -x`]
@@ -553,7 +556,7 @@
else Float 1 1 * ub_horner y
else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
+termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
declare ub_arctan_horner.simps[simp del]
declare lb_arctan_horner.simps[simp del]
@@ -561,17 +564,17 @@
lemma lb_arctan_bound': assumes "0 \<le> real x"
shows "lb_arctan prec x \<le> arctan x"
proof -
- have "\<not> x < 0" and "0 \<le> x" unfolding less_float_def less_eq_float_def using `0 \<le> real x` by auto
+ have "\<not> x < 0" and "0 \<le> x" using `0 \<le> real x` by auto
let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)"
and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
show ?thesis
proof (cases "x \<le> Float 1 -1")
- case True hence "real x \<le> 1" unfolding less_eq_float_def Float_num by auto
+ case True hence "real x \<le> 1" by auto
show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
next
- case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto
+ case False hence "0 < real x" by auto
let ?R = "1 + sqrt (1 + real x * real x)"
let ?fR = "1 + ub_sqrt prec (1 + x * x)"
let ?DIV = "float_divl prec x ?fR"
@@ -583,7 +586,7 @@
using bnds_sqrt'[of "1 + x * x"] by auto
hence "?R \<le> ?fR" by auto
- hence "0 < ?fR" and "0 < real ?fR" unfolding less_float_def using `0 < ?R` by auto
+ hence "0 < ?fR" and "0 < real ?fR" using `0 < ?R` by auto
have monotone: "(float_divl prec x ?fR) \<le> x / ?R"
proof -
@@ -613,7 +616,7 @@
finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
next
case False
- hence "2 < real x" unfolding less_eq_float_def Float_num by auto
+ hence "2 < real x" by auto
hence "1 \<le> real x" by auto
let "?invx" = "float_divr prec 1 x"
@@ -626,7 +629,7 @@
using `0 \<le> arctan x` by auto
next
case False
- hence "real ?invx \<le> 1" unfolding less_float_def by auto
+ hence "real ?invx \<le> 1" by auto
have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
@@ -650,18 +653,18 @@
lemma ub_arctan_bound': assumes "0 \<le> real x"
shows "arctan x \<le> ub_arctan prec x"
proof -
- have "\<not> x < 0" and "0 \<le> x" unfolding less_float_def less_eq_float_def using `0 \<le> real x` by auto
+ have "\<not> x < 0" and "0 \<le> x" using `0 \<le> real x` by auto
let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)"
and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
show ?thesis
proof (cases "x \<le> Float 1 -1")
- case True hence "real x \<le> 1" unfolding less_eq_float_def Float_num by auto
+ case True hence "real x \<le> 1" by auto
show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
next
- case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto
+ case False hence "0 < real x" by auto
let ?R = "1 + sqrt (1 + real x * real x)"
let ?fR = "1 + lb_sqrt prec (1 + x * x)"
let ?DIV = "float_divr prec x ?fR"
@@ -695,7 +698,7 @@
show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
next
case False
- hence "real ?DIV \<le> 1" unfolding less_float_def by auto
+ hence "real ?DIV \<le> 1" by auto
have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
@@ -709,16 +712,16 @@
qed
next
case False
- hence "2 < real x" unfolding less_eq_float_def Float_num by auto
+ hence "2 < real x" by auto
hence "1 \<le> real x" by auto
hence "0 < real x" by auto
- hence "0 < x" unfolding less_float_def by auto
+ hence "0 < x" by auto
let "?invx" = "float_divl prec 1 x"
have "0 \<le> arctan x" using arctan_monotone'[OF `0 \<le> real x`] using arctan_tan[of 0, unfolded tan_zero] by auto
have "real ?invx \<le> 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: `1 \<le> real x` divide_le_eq_1_pos[OF `0 < real x`])
- have "0 \<le> real ?invx" by (rule float_divl_lower_bound[unfolded less_eq_float_def], auto simp add: `0 < x`)
+ have "0 \<le> real ?invx" using `0 < x` by (intro float_divl_lower_bound) auto
have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
@@ -739,11 +742,11 @@
lemma arctan_boundaries:
"arctan x \<in> {(lb_arctan prec x) .. (ub_arctan prec x)}"
proof (cases "0 \<le> x")
- case True hence "0 \<le> real x" unfolding less_eq_float_def by auto
+ case True hence "0 \<le> real x" by auto
show ?thesis using ub_arctan_bound'[OF `0 \<le> real x`] lb_arctan_bound'[OF `0 \<le> real x`] unfolding atLeastAtMost_iff by auto
next
let ?mx = "-x"
- case False hence "x < 0" and "0 \<le> real ?mx" unfolding less_eq_float_def less_float_def by auto
+ case False hence "x < 0" and "0 \<le> real ?mx" by auto
hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx"
using ub_arctan_bound'[OF `0 \<le> real ?mx`] lb_arctan_bound'[OF `0 \<le> real ?mx`] by auto
show ?thesis unfolding real_of_float_minus arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
@@ -801,8 +804,8 @@
shows "cos x \<in> {(lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) .. (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))}"
proof (cases "real x = 0")
case False hence "real x \<noteq> 0" by auto
- hence "0 < x" and "0 < real x" using `0 \<le> real x` unfolding less_float_def by auto
- have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero
+ hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
+ have "0 < x * x" using `0 < x`
using mult_pos_pos[where a="real x" and b="real x"] by auto
{ fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
@@ -918,8 +921,8 @@
shows "sin x \<in> {(x * lb_sin_cos_aux prec (get_even n) 2 1 (x * x)) .. (x * ub_sin_cos_aux prec (get_odd n) 2 1 (x * x))}"
proof (cases "real x = 0")
case False hence "real x \<noteq> 0" by auto
- hence "0 < x" and "0 < real x" using `0 \<le> real x` unfolding less_float_def by auto
- have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero
+ hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
+ have "0 < x * x" using `0 < x`
using mult_pos_pos[where a="real x" and b="real x"] by auto
{ fix x n have "(\<Sum> j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
@@ -1036,7 +1039,7 @@
finally have "cos x = 2 * cos (x / 2) * cos (x / 2) - 1" .
} note x_half = this[symmetric]
- have "\<not> x < 0" using `0 \<le> real x` unfolding less_float_def by auto
+ have "\<not> x < 0" using `0 \<le> real x` by auto
let "?ub_horner x" = "ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x)"
let "?lb_horner x" = "lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x)"
let "?ub_half x" = "Float 1 1 * x * x - 1"
@@ -1044,7 +1047,7 @@
show ?thesis
proof (cases "x < Float 1 -1")
- case True hence "x \<le> pi / 2" unfolding less_float_def using pi_ge_two by auto
+ case True hence "x \<le> pi / 2" using pi_ge_two by auto
show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 -1`] Let_def
using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
next
@@ -1059,7 +1062,7 @@
case True show ?thesis using cos_ge_minus_one unfolding if_P[OF True] by auto
next
case False
- hence "0 \<le> real y" unfolding less_float_def by auto
+ hence "0 \<le> real y" by auto
from mult_mono[OF `y \<le> cos ?x2` `y \<le> cos ?x2` `0 \<le> cos ?x2` this]
have "real y * real y \<le> cos ?x2 * cos ?x2" .
hence "2 * real y * real y \<le> 2 * cos ?x2 * cos ?x2" by auto
@@ -1091,7 +1094,7 @@
show ?thesis
proof (cases "x < 1")
- case True hence "real x \<le> 1" unfolding less_float_def by auto
+ case True hence "real x \<le> 1" by auto
have "0 \<le> real ?x2" and "?x2 \<le> pi / 2" using pi_ge_two `0 \<le> real x` using assms by auto
from cos_boundaries[OF this]
have lb: "(?lb_horner ?x2) \<le> ?cos ?x2" and ub: "?cos ?x2 \<le> (?ub_horner ?x2)" by auto
@@ -1113,7 +1116,7 @@
from cos_boundaries[OF this]
have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
- have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by simp
+ have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by transfer simp
have "(?lb x) \<le> ?cos x"
proof -
@@ -1197,7 +1200,7 @@
using x unfolding k[symmetric]
by (cases "k = 0")
(auto intro!: add_mono
- simp add: diff_minus k[symmetric] less_float_def
+ simp add: diff_minus k[symmetric]
simp del: float_of_numeral)
note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
hence lx_less_ux: "?lx \<le> real ?ux" by (rule order_trans)
@@ -1205,7 +1208,7 @@
{ assume "- ?lpi \<le> ?lx" and x_le_0: "x - k * (2 * pi) \<le> 0"
with lpi[THEN le_imp_neg_le] lx
have pi_lx: "- pi \<le> ?lx" and lx_0: "real ?lx \<le> 0"
- by (simp_all add: less_eq_float_def)
+ by simp_all
have "(lb_cos prec (- ?lx)) \<le> cos (real (- ?lx))"
using lb_cos_minus[OF pi_lx lx_0] by simp
@@ -1220,7 +1223,7 @@
{ assume "0 \<le> ?lx" and pi_x: "x - k * (2 * pi) \<le> pi"
with lx
have pi_lx: "?lx \<le> pi" and lx_0: "0 \<le> real ?lx"
- by (auto simp add: less_eq_float_def)
+ by auto
have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
using cos_monotone_0_pi'[OF lx_0 lx pi_x]
@@ -1235,7 +1238,7 @@
{ assume pi_x: "- pi \<le> x - k * (2 * pi)" and "?ux \<le> 0"
with ux
have pi_ux: "- pi \<le> ?ux" and ux_0: "real ?ux \<le> 0"
- by (simp_all add: less_eq_float_def)
+ by simp_all
have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
@@ -1250,7 +1253,7 @@
{ assume "?ux \<le> ?lpi" and x_ge_0: "0 \<le> x - k * (2 * pi)"
with lpi ux
have pi_ux: "?ux \<le> pi" and ux_0: "0 \<le> real ?ux"
- by (simp_all add: less_eq_float_def)
+ by simp_all
have "(lb_cos prec ?ux) \<le> cos ?ux"
using lb_cos[OF ux_0 pi_ux] by simp
@@ -1272,7 +1275,7 @@
from True lpi[THEN le_imp_neg_le] lx ux
have "- pi \<le> x - k * (2 * pi)"
and "x - k * (2 * pi) \<le> 0"
- by (auto simp add: less_eq_float_def)
+ by auto
with True negative_ux negative_lx
show ?thesis unfolding l u by simp
next case False note 1 = this show ?thesis
@@ -1285,7 +1288,7 @@
from True lpi lx ux
have "0 \<le> x - k * (2 * pi)"
and "x - k * (2 * pi) \<le> pi"
- by (auto simp add: less_eq_float_def)
+ by auto
with True positive_ux positive_lx
show ?thesis unfolding l u by simp
next case False note 2 = this show ?thesis
@@ -1314,16 +1317,16 @@
case False hence "pi \<le> x - k * (2 * pi)" by simp
hence pi_x: "- pi \<le> x - k * (2 * pi) - 2 * pi" by simp
- have "?ux \<le> 2 * pi" using Cond lpi by (auto simp add: less_eq_float_def)
+ have "?ux \<le> 2 * pi" using Cond lpi by auto
hence "x - k * (2 * pi) - 2 * pi \<le> 0" using ux by simp
have ux_0: "real (?ux - 2 * ?lpi) \<le> 0"
- using Cond by (auto simp add: less_eq_float_def)
+ using Cond by auto
from 2 and Cond have "\<not> ?ux \<le> ?lpi" by auto
- hence "- ?lpi \<le> ?ux - 2 * ?lpi" by (auto simp add: less_eq_float_def)
+ hence "- ?lpi \<le> ?ux - 2 * ?lpi" by auto
hence pi_ux: "- pi \<le> (?ux - 2 * ?lpi)"
- using lpi[THEN le_imp_neg_le] by (auto simp add: less_eq_float_def)
+ using lpi[THEN le_imp_neg_le] by auto
have x_le_ux: "x - k * (2 * pi) - 2 * pi \<le> (?ux - 2 * ?lpi)"
using ux lpi by auto
@@ -1345,7 +1348,7 @@
case True note Cond = this with bnds 1 2 3 4
have l: "l = Float -1 0"
and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
- by (auto simp add: bnds_cos_def Let_def simp del: neg_numeral_float_Float)
+ by (auto simp add: bnds_cos_def Let_def)
have "cos x \<le> u"
proof (cases "-pi < x - k * (2 * pi)")
@@ -1356,17 +1359,17 @@
case False hence "x - k * (2 * pi) \<le> -pi" by simp
hence pi_x: "x - k * (2 * pi) + 2 * pi \<le> pi" by simp
- have "-2 * pi \<le> ?lx" using Cond lpi by (auto simp add: less_eq_float_def)
+ have "-2 * pi \<le> ?lx" using Cond lpi by auto
hence "0 \<le> x - k * (2 * pi) + 2 * pi" using lx by simp
have lx_0: "0 \<le> real (?lx + 2 * ?lpi)"
- using Cond lpi by (auto simp add: less_eq_float_def)
+ using Cond lpi by auto
from 1 and Cond have "\<not> -?lpi \<le> ?lx" by auto
- hence "?lx + 2 * ?lpi \<le> ?lpi" by (auto simp add: less_eq_float_def)
+ hence "?lx + 2 * ?lpi \<le> ?lpi" by auto
hence pi_lx: "(?lx + 2 * ?lpi) \<le> pi"
- using lpi[THEN le_imp_neg_le] by (auto simp add: less_eq_float_def)
+ using lpi[THEN le_imp_neg_le] by auto
have lx_le_x: "(?lx + 2 * ?lpi) \<le> x - k * (2 * pi) + 2 * pi"
using lx lpi by auto
@@ -1455,7 +1458,7 @@
else if x < - 1 then ub_exp_horner prec (get_odd (prec + 2)) 1 1 (float_divr prec x (- floor_fl x)) ^ (nat (- int_floor_fl x))
else ub_exp_horner prec (get_odd (prec + 2)) 1 1 x)"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto simp add: less_float_def)
+termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto)
lemma exp_m1_ge_quarter: "(1 / 4 :: real) \<le> exp (- 1)"
proof -
@@ -1466,22 +1469,22 @@
unfolding get_even_def eq4
by (auto simp add: compute_lapprox_rat compute_rapprox_rat compute_lapprox_posrat compute_rapprox_posrat rat_precision_def compute_bitlen)
also have "\<dots> \<le> exp (- 1 :: float)" using bnds_exp_horner[where x="- 1"] by auto
- finally show ?thesis unfolding real_of_float_minus real_of_float_one by simp
+ finally show ?thesis by simp
qed
lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
proof -
let "?lb_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
let "?horner x" = "let y = ?lb_horner x in if y \<le> 0 then Float 1 -2 else y"
- have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto simp add: less_eq_float_def less_float_def)
+ have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
moreover { fix x :: float fix num :: nat
- have "0 < real (?horner x) ^ num" using `0 < ?horner x`[unfolded less_float_def real_of_float_zero] by (rule zero_less_power)
+ have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
also have "\<dots> = (?horner x) ^ num" by auto
finally have "0 < real ((?horner x) ^ num)" .
}
ultimately show ?thesis
unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
- by (cases "floor_fl x", cases "x < - 1", auto simp add: less_eq_float_def less_float_def)
+ by (cases "floor_fl x", cases "x < - 1", auto)
qed
lemma exp_boundaries': assumes "x \<le> 0"
@@ -1490,13 +1493,13 @@
let "?lb_exp_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
let "?ub_exp_horner x" = "ub_exp_horner prec (get_odd (prec + 2)) 1 1 x"
- have "real x \<le> 0" and "\<not> x > 0" using `x \<le> 0` unfolding less_eq_float_def less_float_def by auto
+ have "real x \<le> 0" and "\<not> x > 0" using `x \<le> 0` by auto
show ?thesis
proof (cases "x < - 1")
- case False hence "- 1 \<le> real x" unfolding less_float_def by auto
+ case False hence "- 1 \<le> real x" by auto
show ?thesis
proof (cases "?lb_exp_horner x \<le> 0")
- from `\<not> x < - 1` have "- 1 \<le> real x" unfolding less_float_def by auto
+ from `\<not> x < - 1` have "- 1 \<le> real x" by auto
hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
from order_trans[OF exp_m1_ge_quarter this]
have "Float 1 -2 \<le> exp x" unfolding Float_num .
@@ -1510,8 +1513,8 @@
let ?num = "nat (- int_floor_fl x)"
- have "real (int_floor_fl x) < - 1" using int_floor_fl `x < - 1` unfolding less_eq_float_def less_float_def real_of_float_uminus real_of_float_one
- by (rule order_le_less_trans)
+ have "real (int_floor_fl x) < - 1" using int_floor_fl[of x] `x < - 1`
+ by simp
hence "real (int_floor_fl x) < 0" by simp
hence "int_floor_fl x < 0" by auto
hence "1 \<le> - int_floor_fl x" by auto
@@ -1550,7 +1553,7 @@
show ?thesis
proof (cases "?horner \<le> 0")
- case False hence "0 \<le> real ?horner" unfolding less_eq_float_def by auto
+ case False hence "0 \<le> real ?horner" by auto
have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
@@ -1586,10 +1589,10 @@
proof -
show ?thesis
proof (cases "0 < x")
- case False hence "x \<le> 0" unfolding less_float_def less_eq_float_def by auto
+ case False hence "x \<le> 0" by auto
from exp_boundaries'[OF this] show ?thesis .
next
- case True hence "-x \<le> 0" unfolding less_float_def less_eq_float_def by auto
+ case True hence "-x \<le> 0" by auto
have "lb_exp prec x \<le> exp x"
proof -
@@ -1605,15 +1608,14 @@
moreover
have "exp x \<le> ub_exp prec x"
proof -
- have "\<not> 0 < -x" using `0 < x` unfolding less_float_def by auto
+ have "\<not> 0 < -x" using `0 < x` by auto
from exp_boundaries'[OF `-x \<le> 0`]
have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
- using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_zero],
- symmetric]]
- unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide real_of_float_one by auto
+ using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
+ by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))" using float_divr .
finally show ?thesis unfolding ub_exp.simps if_P[OF True] .
qed
@@ -1778,16 +1780,15 @@
by pat_completeness auto
termination proof (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 1 then 1 else 0))", auto)
- fix prec x assume "\<not> x \<le> 0" and "x < 1" and "float_divl (max prec (Suc 0)) 1 x < 1"
- hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1"
- unfolding less_float_def less_eq_float_def by auto
+ fix prec and x :: float assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divl (max prec (Suc 0)) 1 x) < 1"
+ hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1` `1 \<le> max prec (Suc 0)`]
- show False using `float_divl (max prec (Suc 0)) 1 x < 1` unfolding less_float_def less_eq_float_def by auto
+ show False using `real (float_divl (max prec (Suc 0)) 1 x) < 1` by auto
next
- fix prec x assume "\<not> x \<le> 0" and "x < 1" and "float_divr prec 1 x < 1"
- hence "0 < x" unfolding less_float_def less_eq_float_def by auto
- from float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`, of prec]
- show False using `float_divr prec 1 x < 1` unfolding less_float_def less_eq_float_def by auto
+ fix prec x assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divr prec 1 x) < 1"
+ hence "0 < x" by auto
+ from float_divr_pos_less1_lower_bound[OF `0 < x`, of prec] `real x < 1`
+ show False using `real (float_divr prec 1 x) < 1` by auto
qed
lemma float_pos_eq_mantissa_pos: "x > 0 \<longleftrightarrow> mantissa x > 0"
@@ -1811,24 +1812,20 @@
and "Float (mantissa x) (- (bitlen (mantissa x) - 1)) = Float m ( - (bitlen m - 1))" (is ?th2)
proof -
from assms have mantissa_pos: "m > 0" "mantissa x > 0"
- using Float_pos_eq_mantissa_pos float_pos_eq_mantissa_pos by simp_all
- thus ?th1 using bitlen_Float[of m e] assms by (simp add: less_float_def zero_less_mult_iff)
- from assms have "x \<noteq> float_of 0" by (auto simp add: zero_float_def zero_less_mult_iff)
+ using Float_pos_eq_mantissa_pos[of m e] float_pos_eq_mantissa_pos[of x] by simp_all
+ thus ?th1 using bitlen_Float[of m e] assms by (auto simp add: zero_less_mult_iff intro!: arg_cong2[where f=Float])
+ have "x \<noteq> float_of 0"
+ unfolding zero_float_def[symmetric] using `0 < x` by auto
from denormalize_shift[OF assms(1) this] guess i . note i = this
- from `x \<noteq> float_of 0` have "mantissa x \<noteq> 0" by (simp add: mantissa_noteq_0)
- from assms
- have "real (mantissa x) * 2 powr (1 - real (bitlen (mantissa x))) \<in> float"
- using two_powr_int_float[of "1 - bitlen (mantissa x)"] by simp
- moreover
+
have "2 powr (1 - (real (bitlen (mantissa x)) + real i)) =
2 powr (1 - (real (bitlen (mantissa x)))) * inverse (2 powr (real i))"
by (simp add: powr_minus[symmetric] powr_add[symmetric] field_simps)
hence "real (mantissa x) * 2 powr (1 - real (bitlen (mantissa x))) =
(real (mantissa x) * 2 ^ i) * 2 powr (1 - real (bitlen (mantissa x * 2 ^ i)))"
using `mantissa x > 0` by (simp add: powr_realpow)
- ultimately
- show ?th2
- using two_powr_int_float[of "1 - bitlen (mantissa x)"] by (simp add: i)
+ then show ?th2
+ unfolding i by transfer auto
qed
lemma compute_ln[code]:
@@ -1854,7 +1851,7 @@
proof -
from assms Float_pos_eq_mantissa_pos have "x > 0 \<Longrightarrow> m > 0" by simp
thus ?th1 ?th2 using Float_representation_aux[of m e] unfolding x_def[symmetric]
- by (auto simp add: simp del: Float_def dest: not_leE)
+ by (auto dest: not_leE)
qed
lemma ln_shifted_float: assumes "0 < m" shows "ln (Float m e) = ln 2 * (e + (bitlen m - 1)) + ln (Float m (- (bitlen m - 1)))"
@@ -1893,9 +1890,9 @@
(is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
proof (cases "x < Float 1 1")
case True
- hence "real (x - 1) < 1" and "real x < 2" unfolding less_float_def Float_num by auto
- have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` unfolding less_float_def less_eq_float_def by auto
- hence "0 \<le> real (x - 1)" using `1 \<le> x` unfolding less_float_def Float_num by auto
+ hence "real (x - 1) < 1" and "real x < 2" by auto
+ have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
+ hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
have [simp]: "(Float 3 -1) = 3 / 2" by simp
@@ -1906,7 +1903,7 @@
using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
by auto
next
- case False hence *: "3 / 2 < x" by (auto simp add: less_eq_float_def)
+ case False hence *: "3 / 2 < x" by auto
with ln_add[of "3 / 2" "x - 3 / 2"]
have add: "ln x = ln (3 / 2) + ln (real x * 2 / 3)"
@@ -1975,8 +1972,7 @@
next
case False
hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
- using `1 \<le> x` unfolding less_float_def less_eq_float_def
- by auto
+ using `1 \<le> x` by auto
show ?thesis
proof -
def m \<equiv> "mantissa x"
@@ -1986,7 +1982,7 @@
let ?x = "Float m (- (bitlen m - 1))"
have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
- by (auto simp: less_float_def less_eq_float_def zero_less_mult_iff)
+ by (auto simp: zero_less_mult_iff)
def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
@@ -2040,15 +2036,15 @@
case False hence "1 \<le> x" unfolding less_float_def less_eq_float_def by auto
show ?thesis using ub_ln_lb_ln_bounds'[OF `1 \<le> x`] .
next
- case True have "\<not> x \<le> 0" using `0 < x` unfolding less_float_def less_eq_float_def by auto
- from True have "real x < 1" by (simp add: less_float_def)
- have "0 < real x" and "real x \<noteq> 0" using `0 < x` unfolding less_float_def by auto
+ case True have "\<not> x \<le> 0" using `0 < x` by auto
+ from True have "real x < 1" by simp
+ have "0 < real x" and "real x \<noteq> 0" using `0 < x` by auto
hence A: "0 < 1 / real x" by auto
{
let ?divl = "float_divl (max prec 1) 1 x"
- have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`] unfolding less_eq_float_def less_float_def by auto
- hence B: "0 < real ?divl" unfolding less_eq_float_def by auto
+ have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`] by auto
+ hence B: "0 < real ?divl" by auto
have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
@@ -2058,7 +2054,7 @@
{
let ?divr = "float_divr prec 1 x"
have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`] unfolding less_eq_float_def less_float_def by auto
- hence B: "0 < real ?divr" unfolding less_eq_float_def by auto
+ hence B: "0 < real ?divr" by auto
have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
@@ -2077,7 +2073,7 @@
assume "\<not> 0 < x" hence "x \<le> 0" unfolding less_eq_float_def less_float_def by auto
thus False using assms by auto
qed
- thus "0 < real x" unfolding less_float_def by auto
+ thus "0 < real x" by auto
have "the (lb_ln prec x) \<le> ln x" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
thus "y \<le> ln x" unfolding assms[symmetric] by auto
qed
@@ -2087,10 +2083,10 @@
proof -
have "0 < x"
proof (rule ccontr)
- assume "\<not> 0 < x" hence "x \<le> 0" unfolding less_eq_float_def less_float_def by auto
+ assume "\<not> 0 < x" hence "x \<le> 0" by auto
thus False using assms by auto
qed
- thus "0 < real x" unfolding less_float_def by auto
+ thus "0 < real x" by auto
have "ln x \<le> the (ub_ln prec x)" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
thus "ln x \<le> y" unfolding assms[symmetric] by auto
qed
@@ -2470,13 +2466,13 @@
and l1: "l1 \<le> interpret_floatarith a xs" and u1: "interpret_floatarith a xs \<le> u1" by blast
have either: "0 < l1 \<or> u1 < 0" proof (rule ccontr) assume P: "\<not> (0 < l1 \<or> u1 < 0)" show False using l' unfolding if_not_P[OF P] by auto qed
moreover have l1_le_u1: "real l1 \<le> real u1" using l1 u1 by auto
- ultimately have "real l1 \<noteq> 0" and "real u1 \<noteq> 0" unfolding less_float_def by auto
+ ultimately have "real l1 \<noteq> 0" and "real u1 \<noteq> 0" by auto
have inv: "inverse u1 \<le> inverse (interpret_floatarith a xs)
\<and> inverse (interpret_floatarith a xs) \<le> inverse l1"
proof (cases "0 < l1")
case True hence "0 < real u1" and "0 < real l1" "0 < interpret_floatarith a xs"
- unfolding less_float_def using l1_le_u1 l1 by auto
+ using l1_le_u1 l1 by auto
show ?thesis
unfolding inverse_le_iff_le[OF `0 < real u1` `0 < interpret_floatarith a xs`]
inverse_le_iff_le[OF `0 < interpret_floatarith a xs` `0 < real l1`]
@@ -2484,7 +2480,7 @@
next
case False hence "u1 < 0" using either by blast
hence "real u1 < 0" and "real l1 < 0" "interpret_floatarith a xs < 0"
- unfolding less_float_def using l1_le_u1 u1 by auto
+ using l1_le_u1 u1 by auto
show ?thesis
unfolding inverse_le_iff_le_neg[OF `real u1 < 0` `interpret_floatarith a xs < 0`]
inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
@@ -2505,7 +2501,7 @@
from lift_un'[OF Abs.prems[unfolded approx.simps], unfolded fst_conv snd_conv] Abs.hyps
obtain l1 u1 where l': "l = (if l1 < 0 \<and> 0 < u1 then 0 else min \<bar>l1\<bar> \<bar>u1\<bar>)" and u': "u = max \<bar>l1\<bar> \<bar>u1\<bar>"
and l1: "l1 \<le> interpret_floatarith x xs" and u1: "interpret_floatarith x xs \<le> u1" by blast
- thus ?case unfolding l' u' by (cases "l1 < 0 \<and> 0 < u1", auto simp add: real_of_float_min real_of_float_max less_float_def)
+ thus ?case unfolding l' u' by (cases "l1 < 0 \<and> 0 < u1", auto simp add: real_of_float_min real_of_float_max)
next
case (Min a b)
from lift_bin'[OF Min.prems[unfolded approx.simps], unfolded fst_conv snd_conv] Min.hyps
@@ -2664,7 +2660,7 @@
and inequality: "u < l'"
by (cases "approx prec a vs", auto,
cases "approx prec b vs", auto)
- from inequality[unfolded less_float_def] approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
+ from inequality approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
show ?case by auto
next
case (LessEqual a b)
@@ -2674,7 +2670,7 @@
and inequality: "u \<le> l'"
by (cases "approx prec a vs", auto,
cases "approx prec b vs", auto)
- from inequality[unfolded less_eq_float_def] approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
+ from inequality approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
show ?case by auto
next
case (AtLeastAtMost x a b)
@@ -2686,7 +2682,7 @@
by (cases "approx prec x vs", auto,
cases "approx prec a vs", auto,
cases "approx prec b vs", auto, blast)
- from inequality[unfolded less_eq_float_def] approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
+ from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
show ?case by auto
qed
@@ -2750,7 +2746,6 @@
apply (auto intro!: DERIV_intros
simp del: interpret_floatarith.simps(5)
simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
- apply (simp add: cos_sin_eq)
done
next case (Power a n) thus ?case
by (cases n, auto intro!: DERIV_intros
@@ -2794,7 +2789,7 @@
and *: "0 < l \<or> u < 0"
by (cases "approx prec a vs", auto)
with approx[OF `bounded_by xs vs` approx_Some]
- have "interpret_floatarith a xs \<noteq> 0" unfolding less_float_def by auto
+ have "interpret_floatarith a xs \<noteq> 0" by auto
thus ?case using Inverse by auto
next
case (Ln a)
@@ -2802,7 +2797,7 @@
and *: "0 < l"
by (cases "approx prec a vs", auto)
with approx[OF `bounded_by xs vs` approx_Some]
- have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+ have "0 < interpret_floatarith a xs" by auto
thus ?case using Ln by auto
next
case (Sqrt a)
@@ -2810,7 +2805,7 @@
and *: "0 < l"
by (cases "approx prec a vs", auto)
with approx[OF `bounded_by xs vs` approx_Some]
- have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+ have "0 < interpret_floatarith a xs" by auto
thus ?case using Sqrt by auto
next
case (Power a n) thus ?case by (cases n, auto)
@@ -3160,7 +3155,7 @@
from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
by (auto simp add: diff_minus)
- from order_less_le_trans[OF `0 < ly`[unfolded less_float_def] this]
+ from order_less_le_trans[OF _ this, of 0] `0 < ly`
show ?thesis by auto
qed
@@ -3182,7 +3177,7 @@
from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
by (auto simp add: diff_minus)
- from order_trans[OF `0 \<le> ly`[unfolded less_eq_float_def] this]
+ from order_trans[OF _ this, of 0] `0 \<le> ly`
show ?thesis by auto
qed
--- a/src/HOL/Library/Float.thy Wed Apr 18 14:29:21 2012 +0200
+++ b/src/HOL/Library/Float.thy Wed Apr 18 14:29:22 2012 +0200
@@ -8,17 +8,17 @@
morphisms real_of_float float_of
by auto
-declare [[coercion "real::float\<Rightarrow>real"]]
+setup_lifting type_definition_float
lemmas float_of_inject[simp]
-lemmas float_of_cases2 = float_of_cases[case_product float_of_cases]
-lemmas float_of_cases3 = float_of_cases2[case_product float_of_cases]
defs (overloaded)
- real_of_float_def[code_unfold]: "real == real_of_float"
+ real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
-lemma real_of_float_eq[simp]:
- fixes f1 f2 :: float shows "real f1 = real f2 \<longleftrightarrow> f1 = f2"
+declare [[coercion "real :: float \<Rightarrow> real"]]
+
+lemma real_of_float_eq:
+ fixes f1 f2 :: float shows "f1 = f2 \<longleftrightarrow> real f1 = real f2"
unfolding real_of_float_def real_of_float_inject ..
lemma float_of_real[simp]: "float_of (real x) = x"
@@ -27,6 +27,10 @@
lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
unfolding real_of_float_def by (rule float_of_inverse)
+lemma transfer_real_of_float [transfer_rule]:
+ "(fun_rel cr_float op =) (\<lambda>x. x) real"
+ unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def)
+
subsection {* Real operations preserving the representation as floating point number *}
lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
@@ -37,7 +41,7 @@
lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
-lemma real_of_nat_float[simp]: "real (x ::nat) \<in> float" by (intro floatI[of x 0]) simp
+lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float" by (intro floatI[of 1 i]) simp
lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
@@ -119,232 +123,117 @@
finally show ?thesis .
qed
+lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
+
subsection {* Arithmetic operations on floating point numbers *}
-instantiation float :: ring_1
+instantiation float :: "{ring_1, linorder, linordered_ring, linordered_idom, numeral, equal}"
begin
-definition [simp]: "(0::float) = float_of 0"
-
-definition [simp]: "(1::float) = float_of 1"
-
-definition "(x + y::float) = float_of (real x + real y)"
-
-lemma float_plus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x + float_of y = float_of (x + y)"
- by (simp add: plus_float_def)
-
-definition "(-x::float) = float_of (- real x)"
+lift_definition zero_float :: float is 0 by simp
+lift_definition one_float :: float is 1 by simp
+lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
+lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
+lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
+lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
-lemma uminus_of_float[simp]: "x \<in> float \<Longrightarrow> - float_of x = float_of (- x)"
- by (simp add: uminus_float_def)
-
-definition "(x - y::float) = float_of (real x - real y)"
+lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
+lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
-lemma float_minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x - float_of y = float_of (x - y)"
- by (simp add: minus_float_def)
+lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
-definition "(x * y::float) = float_of (real x * real y)"
-
-lemma float_times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x * float_of y = float_of (x * y)"
- by (simp add: times_float_def)
+lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
+lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
instance
-proof
- fix a b c :: float
- show "0 + a = a"
- by (cases a rule: float_of_cases) simp
- show "1 * a = a"
- by (cases a rule: float_of_cases) simp
- show "a * 1 = a"
- by (cases a rule: float_of_cases) simp
- show "-a + a = 0"
- by (cases a rule: float_of_cases) simp
- show "a + b = b + a"
- by (cases a b rule: float_of_cases2) (simp add: ac_simps)
- show "a - b = a + -b"
- by (cases a b rule: float_of_cases2) (simp add: field_simps)
- show "a + b + c = a + (b + c)"
- by (cases a b c rule: float_of_cases3) (simp add: ac_simps)
- show "a * b * c = a * (b * c)"
- by (cases a b c rule: float_of_cases3) (simp add: ac_simps)
- show "(a + b) * c = a * c + b * c"
- by (cases a b c rule: float_of_cases3) (simp add: field_simps)
- show "a * (b + c) = a * b + a * c"
- by (cases a b c rule: float_of_cases3) (simp add: field_simps)
- show "0 \<noteq> (1::float)" by simp
-qed
+ proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
end
-lemma real_of_float_uminus[simp]:
- fixes f g::float shows "real (- g) = - real g"
- by (simp add: uminus_float_def)
-
-lemma real_of_float_plus[simp]:
- fixes f g::float shows "real (f + g) = real f + real g"
- by (simp add: plus_float_def)
-
-lemma real_of_float_minus[simp]:
- fixes f g::float shows "real (f - g) = real f - real g"
- by (simp add: minus_float_def)
-
-lemma real_of_float_times[simp]:
- fixes f g::float shows "real (f * g) = real f * real g"
- by (simp add: times_float_def)
-
-lemma real_of_float_zero[simp]: "real (0::float) = 0" by simp
-lemma real_of_float_one[simp]: "real (1::float) = 1" by simp
+lemma
+ fixes x y :: float
+ shows real_of_float_uminus[simp]: "real (- x) = - real x"
+ and real_of_float_plus[simp]: "real (y + x) = real y + real x"
+ and real_of_float_minus[simp]: "real (y - x) = real y - real x"
+ and real_of_float_times[simp]: "real (y * x) = real y * real x"
+ and real_of_float_zero[simp]: "real (0::float) = 0"
+ and real_of_float_one[simp]: "real (1::float) = 1"
+ and real_of_float_le[simp]: "x \<le> y \<longleftrightarrow> real x \<le> real y"
+ and real_of_float_less[simp]: "x < y \<longleftrightarrow> real x < real y"
+ and real_of_float_abs[simp]: "real (abs x) = abs (real x)"
+ and real_of_float_sgn[simp]: "real (sgn x) = sgn (real x)"
+ using uminus_float.rep_eq plus_float.rep_eq minus_float.rep_eq times_float.rep_eq
+ zero_float.rep_eq one_float.rep_eq less_eq_float.rep_eq less_float.rep_eq
+ abs_float.rep_eq sgn_float.rep_eq
+ by (simp_all add: real_of_float_def)
lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
by (induct n) simp_all
-instantiation float :: linorder
-begin
-
-definition "x \<le> (y::float) \<longleftrightarrow> real x \<le> real y"
-
-lemma float_le_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x \<le> float_of y \<longleftrightarrow> x \<le> y"
- by (simp add: less_eq_float_def)
-
-definition "x < (y::float) \<longleftrightarrow> real x < real y"
-
-lemma float_less_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x < float_of y \<longleftrightarrow> x < y"
- by (simp add: less_float_def)
-
-instance
-proof
- fix a b c :: float
- show "a \<le> a"
- by (cases a rule: float_of_cases) simp
- show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
- by (cases a b rule: float_of_cases2) auto
- show "a \<le> b \<or> b \<le> a"
- by (cases a b rule: float_of_cases2) auto
- { assume "a \<le> b" "b \<le> a" then show "a = b"
- by (cases a b rule: float_of_cases2) auto }
- { assume "a \<le> b" "b \<le> c" then show "a \<le> c"
- by (cases a b c rule: float_of_cases3) auto }
-qed
-end
-
-lemma real_of_float_min: fixes a b::float shows "real (min a b) = min (real a) (real b)"
- by (simp add: min_def less_eq_float_def)
-
-lemma real_of_float_max: fixes a b::float shows "real (max a b) = max (real a) (real b)"
- by (simp add: max_def less_eq_float_def)
-
-instantiation float :: linordered_ring
-begin
-
-definition "(abs x :: float) = float_of (abs (real x))"
-
-lemma float_abs[simp]: "x \<in> float \<Longrightarrow> abs (float_of x) = float_of (abs x)"
- by (simp add: abs_float_def)
-
-instance
-proof
- fix a b c :: float
- show "\<bar>a\<bar> = (if a < 0 then - a else a)"
- by (cases a rule: float_of_cases) simp
- assume "a \<le> b"
- then show "c + a \<le> c + b"
- by (cases a b c rule: float_of_cases3) simp
- assume "0 \<le> c"
- with `a \<le> b` show "c * a \<le> c * b"
- by (cases a b c rule: float_of_cases3) (auto intro: mult_left_mono)
- from `0 \<le> c` `a \<le> b` show "a * c \<le> b * c"
- by (cases a b c rule: float_of_cases3) (auto intro: mult_right_mono)
-qed
-end
-
-lemma real_of_abs_float[simp]: fixes f::float shows "real (abs f) = abs (real f)"
- unfolding abs_float_def by simp
+lemma fixes x y::float
+ shows real_of_float_min: "real (min x y) = min (real x) (real y)"
+ and real_of_float_max: "real (max x y) = max (real x) (real y)"
+ by (simp_all add: min_def max_def)
instance float :: dense_linorder
proof
fix a b :: float
show "\<exists>c. a < c"
apply (intro exI[of _ "a + 1"])
- apply (cases a rule: float_of_cases)
+ apply transfer
apply simp
done
show "\<exists>c. c < a"
apply (intro exI[of _ "a - 1"])
- apply (cases a rule: float_of_cases)
+ apply transfer
apply simp
done
assume "a < b"
then show "\<exists>c. a < c \<and> c < b"
- apply (intro exI[of _ "(b + a) * float_of (1/2)"])
- apply (cases a b rule: float_of_cases2)
- apply simp
+ apply (intro exI[of _ "(a + b) * Float 1 -1"])
+ apply transfer
+ apply (simp add: powr_neg_numeral)
done
qed
-instantiation float :: linordered_idom
+instantiation float :: lattice_ab_group_add
begin
-definition "sgn x = float_of (sgn (real x))"
+definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
+where "inf_float a b = min a b"
-lemma sgn_float[simp]: "x \<in> float \<Longrightarrow> sgn (float_of x) = float_of (sgn x)"
- by (simp add: sgn_float_def)
+definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
+where "sup_float a b = max a b"
instance
-proof
- fix a b c :: float
- show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
- by (cases a rule: float_of_cases) simp
- show "a * b = b * a"
- by (cases a b rule: float_of_cases2) (simp add: field_simps)
- show "1 * a = a" "(a + b) * c = a * c + b * c"
- by (simp_all add: field_simps del: one_float_def)
- assume "a < b" "0 < c" then show "c * a < c * b"
- by (cases a b c rule: float_of_cases3) (simp add: field_simps)
-qed
+ by default
+ (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
end
-definition Float :: "int \<Rightarrow> int \<Rightarrow> float" where
- [simp, code del]: "Float m e = float_of (m * 2 powr e)"
-
-lemma real_of_float_Float[code]: "real_of_float (Float m e) =
- (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
-by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
-
-code_datatype Float
-
-lemma real_Float: "real (Float m e) = m * 2 powr e" by simp
-
-definition normfloat :: "float \<Rightarrow> float" where
- [simp]: "normfloat x = x"
+lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
+ apply (induct x)
+ apply simp
+ apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
+ real_of_float_plus real_of_float_one plus_float numeral_float one_float)
+ done
-lemma compute_normfloat[code]: "normfloat (Float m e) =
- (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
- else if m = 0 then 0 else Float m e)"
- by (simp del: real_of_int_add split: prod.split)
- (auto simp add: powr_add zmod_eq_0_iff)
-
-lemma compute_zero[code_unfold, code]: "0 = Float 0 0"
- by simp
+lemma transfer_numeral [transfer_rule]:
+ "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
+ unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
-lemma compute_one[code_unfold, code]: "1 = Float 1 0"
- by simp
-
-instance float :: numeral ..
-
-lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)"
- by (induct k)
- (simp_all only: numeral.simps one_float_def float_plus_float numeral_float one_float plus_float)
-
-lemma float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
+lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
by (simp add: minus_numeral[symmetric] del: minus_numeral)
+lemma transfer_neg_numeral [transfer_rule]:
+ "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
+ unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
+
lemma
- shows float_numeral[simp]: "real (numeral x :: float) = numeral x"
- and float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
- by simp_all
+ shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
+ and float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
+ unfolding real_of_float_eq by simp_all
subsection {* Represent floats as unique mantissa and exponent *}
-
lemma int_induct_abs[case_names less]:
fixes j :: int
assumes H: "\<And>n. (\<And>i. \<bar>i\<bar> < \<bar>n\<bar> \<Longrightarrow> P i) \<Longrightarrow> P n"
@@ -415,7 +304,7 @@
| (powr) m e :: int where "real f = m * 2 powr e" "\<not> 2 dvd m" "f \<noteq> 0"
proof (atomize_elim, induct f)
case (float_of y) then show ?case
- by (cases rule: floatE_normed) auto
+ by (cases rule: floatE_normed) (auto simp: zero_float_def)
qed
definition mantissa :: "float \<Rightarrow> int" where
@@ -432,7 +321,7 @@
proof -
have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)" by auto
then show ?E ?M
- by (auto simp add: mantissa_def exponent_def)
+ by (auto simp add: mantissa_def exponent_def zero_float_def)
qed
lemma
@@ -448,23 +337,14 @@
by auto
then show ?thesis
unfolding exponent_def mantissa_def
- by (rule someI2_ex) simp
- qed simp
+ by (rule someI2_ex) (simp add: zero_float_def)
+ qed (simp add: zero_float_def)
then show ?E ?D by auto
qed simp
lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
using mantissa_not_dvd[of f] by auto
-lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
- unfolding real_of_float_eq[symmetric] mantissa_exponent[of f] by simp
-
-lemma Float_cases[case_names Float, cases type: float]:
- fixes f :: float
- obtains (Float) m e :: int where "f = Float m e"
- using Float_mantissa_exponent[symmetric]
- by (atomize_elim) auto
-
lemma
fixes m e :: int
defines "f \<equiv> float_of (m * 2 powr e)"
@@ -484,6 +364,24 @@
by (auto simp: mult_powr_eq_mult_powr_iff)
qed
+subsection {* Compute arithmetic operations *}
+
+lemma real_Float[simp]: "real (Float m e) = m * 2 powr e"
+ using Float.rep_eq by (simp add: real_of_float_def)
+
+lemma real_of_float_Float[code]: "real_of_float (Float m e) =
+ (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
+by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric] Float_def)
+
+lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
+ unfolding real_of_float_eq mantissa_exponent[of f] by simp
+
+lemma Float_cases[case_names Float, cases type: float]:
+ fixes f :: float
+ obtains (Float) m e :: int where "f = Float m e"
+ using Float_mantissa_exponent[symmetric]
+ by (atomize_elim) auto
+
lemma denormalize_shift:
assumes f_def: "f \<equiv> Float m e" and not_0: "f \<noteq> float_of 0"
obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
@@ -520,64 +418,70 @@
unfolding real_of_int_inject by auto
qed
-subsection {* Compute arithmetic operations *}
+lemma compute_zero[code_unfold, code]: "0 = Float 0 0"
+ by transfer simp
+
+lemma compute_one[code_unfold, code]: "1 = Float 1 0"
+ by transfer simp
+
+definition normfloat :: "float \<Rightarrow> float" where
+ [simp]: "normfloat x = x"
+
+lemma compute_normfloat[code]: "normfloat (Float m e) =
+ (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
+ else if m = 0 then 0 else Float m e)"
+ unfolding normfloat_def
+ by transfer (auto simp add: powr_add zmod_eq_0_iff)
lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
- by simp
+ by transfer simp
lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
- by simp
+ by transfer simp
lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
- by simp
+ by transfer simp
lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
- by (simp add: field_simps powr_add)
+ by transfer (simp add: field_simps powr_add)
lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
(if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
- by (simp add: field_simps)
- (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
+ by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
-lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)" by simp
+lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
+ by simp
lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
- by (simp add: sgn_times)
+ by transfer (simp add: sgn_times)
-definition is_float_pos :: "float \<Rightarrow> bool" where
- "is_float_pos f \<longleftrightarrow> 0 < f"
+lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
- by (auto simp add: is_float_pos_def zero_less_mult_iff) (simp add: not_le[symmetric])
+ by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
- by (simp add: is_float_pos_def field_simps del: zero_float_def)
+ by transfer (simp add: field_simps)
-definition is_float_nonneg :: "float \<Rightarrow> bool" where
- "is_float_nonneg f \<longleftrightarrow> 0 \<le> f"
+lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
- by (auto simp add: is_float_nonneg_def zero_le_mult_iff) (simp add: not_less[symmetric])
+ by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
- by (simp add: is_float_nonneg_def field_simps del: zero_float_def)
+ by transfer (simp add: field_simps)
-definition is_float_zero :: "float \<Rightarrow> bool" where
- "is_float_zero f \<longleftrightarrow> 0 = f"
+lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" by simp
lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
- by (auto simp add: is_float_zero_def)
-
-lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e" by (simp add: abs_mult)
+ by transfer (auto simp add: is_float_zero_def)
-instantiation float :: equal
-begin
+lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
+ by transfer (simp add: abs_mult)
-definition "equal_float (f1 :: float) f2 \<longleftrightarrow> is_float_zero (f1 - f2)"
-
-instance proof qed (auto simp: equal_float_def is_float_zero_def simp del: zero_float_def)
-end
+lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
+ by transfer simp
subsection {* Rounding Real numbers *}
@@ -632,12 +536,10 @@
subsection {* Rounding Floats *}
-definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" where
- "float_up prec x = float_of (round_up prec (real x))"
+lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
-lemma float_up_float:
- "x \<in> float \<Longrightarrow> float_up prec (float_of x) = float_of (round_up prec x)"
- unfolding float_up_def by simp
+lemma real_of_float_float_up[simp]: "real (float_up e f) = round_up e (real f)"
+ using float_up.rep_eq by (simp add: real_of_float_def)
lemma float_up_correct:
shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
@@ -646,15 +548,13 @@
have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
finally show "real (float_up e f) - real f \<le> 2 powr real (- e)"
- by (simp add: float_up_def)
-qed (simp add: algebra_simps float_up_def round_up)
+ by simp
+qed (simp add: algebra_simps round_up)
-definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" where
- "float_down prec x = float_of (round_down prec (real x))"
+lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
-lemma float_down_float:
- "x \<in> float \<Longrightarrow> float_down prec (float_of x) = float_of (round_down prec x)"
- unfolding float_down_def by simp
+lemma real_of_float_float_down[simp]: "real (float_down e f) = round_down e (real f)"
+ using float_down.rep_eq by (simp add: real_of_float_def)
lemma float_down_correct:
shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
@@ -663,21 +563,8 @@
have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
finally show "real f - real (float_down e f) \<le> 2 powr real (- e)"
- by (simp add: float_down_def)
-qed (simp add: algebra_simps float_down_def round_down)
-
-lemma round_down_Float_id:
- assumes "p + e \<ge> 0"
- shows "round_down p (Float m e) = Float m e"
-proof -
- from assms have r: "real e + real p = real (nat (e + p))" by simp
- have r: "\<lfloor>real (Float m e) * 2 powr real p\<rfloor> = real (Float m e) * 2 powr real p"
- by (auto intro: exI[where x="m*2^nat (e+p)"]
- simp add: ac_simps powr_add[symmetric] r powr_realpow)
- show ?thesis using assms
- unfolding round_down_def floor_divide_eq_div r
- by (simp add: ac_simps powr_add[symmetric])
-qed
+ by simp
+qed (simp add: algebra_simps round_down)
lemma compute_float_down[code]:
"float_down p (Float m e) =
@@ -687,12 +574,19 @@
hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
using powr_realpow[of 2 "nat (-(p + e))"] by simp
also have "... = 1 / 2 powr p / 2 powr e"
- unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
+ unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
finally show ?thesis
- unfolding float_down_def round_down_def floor_divide_eq_div[symmetric]
- using `p + e < 0` by (simp add: ac_simps)
+ using `p + e < 0`
+ by transfer (simp add: ac_simps round_down_def floor_divide_eq_div[symmetric])
next
- assume "\<not> p + e < 0" with round_down_Float_id show ?thesis by (simp add: float_down_def)
+ assume "\<not> p + e < 0"
+ then have r: "real e + real p = real (nat (e + p))" by simp
+ have r: "\<lfloor>(m * 2 powr e) * 2 powr real p\<rfloor> = (m * 2 powr e) * 2 powr real p"
+ by (auto intro: exI[where x="m*2^nat (e+p)"]
+ simp add: ac_simps powr_add[symmetric] r powr_realpow)
+ with `\<not> p + e < 0` show ?thesis
+ by transfer
+ (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
qed
lemma ceil_divide_floor_conv:
@@ -714,19 +608,6 @@
qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
-lemma round_up_Float_id:
- assumes "p + e \<ge> 0"
- shows "round_up p (Float m e) = Float m e"
-proof -
- from assms have r1: "real e + real p = real (nat (e + p))" by simp
- have r: "\<lceil>real (Float m e) * 2 powr real p\<rceil> = real (Float m e) * 2 powr real p"
- by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
- intro: exI[where x="m*2^nat (e+p)"])
- show ?thesis using assms
- unfolding float_up_def round_up_def floor_divide_eq_div Let_def r
- by (simp add: ac_simps powr_add[symmetric])
-qed
-
lemma compute_float_up[code]:
"float_up p (Float m e) =
(let P = 2^nat (-(p + e)); r = m mod P in
@@ -745,8 +626,8 @@
show ?thesis
proof cases
assume "2^nat (-(p + e)) dvd m"
- with `p + e < 0` twopow_rewrite show ?thesis
- by (auto simp: ac_simps float_up_def round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
+ with `p + e < 0` twopow_rewrite show ?thesis unfolding Let_def
+ by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
next
assume ndvd: "\<not> 2 ^ nat (- (p + e)) dvd m"
have one_div: "real m * (1 / real ((2::int) ^ nat (- (p + e)))) =
@@ -757,10 +638,19 @@
using ndvd unfolding powr_rewrite one_div
by (subst ceil_divide_floor_conv) (auto simp: field_simps)
thus ?thesis using `p + e < 0` twopow_rewrite
- by (auto simp: ac_simps Let_def float_up_def round_up_def floor_divide_eq_div[symmetric])
+ unfolding Let_def
+ by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div[symmetric])
qed
next
- assume "\<not> p + e < 0" with round_up_Float_id show ?thesis by (simp add: float_up_def)
+ assume "\<not> p + e < 0"
+ then have r1: "real e + real p = real (nat (e + p))" by simp
+ have r: "\<lceil>(m * 2 powr e) * 2 powr real p\<rceil> = (m * 2 powr e) * 2 powr real p"
+ by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
+ intro: exI[where x="m*2^nat (e+p)"])
+ then show ?thesis using `\<not> p + e < 0`
+ unfolding Let_def
+ by transfer
+ (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
qed
lemmas real_of_ints =
@@ -790,8 +680,8 @@
subsection {* Compute bitlen of integers *}
-definition bitlen::"int => int"
-where "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
+definition bitlen :: "int \<Rightarrow> int" where
+ "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
lemma bitlen_nonneg: "0 \<le> bitlen x"
proof -
@@ -842,12 +732,15 @@
defines "f \<equiv> Float m e"
shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
proof cases
- assume "m \<noteq> 0" hence "f \<noteq> float_of 0" by (simp add: f_def) hence "mantissa f \<noteq> 0"
+ assume "m \<noteq> 0"
+ hence "f \<noteq> float_of 0"
+ unfolding real_of_float_eq by (simp add: f_def)
+ hence "mantissa f \<noteq> 0"
by (simp add: mantissa_noteq_0)
moreover
from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
ultimately show ?thesis by (simp add: abs_mult)
-qed (simp add: f_def bitlen_def)
+qed (simp add: f_def bitlen_def Float_def)
lemma compute_bitlen[code]:
shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
@@ -899,7 +792,7 @@
proof -
have "0 < Float m e" using assms by auto
hence "0 < m" using powr_gt_zero[of 2 e]
- by (auto simp: less_float_def less_eq_float_def zero_less_mult_iff)
+ by (auto simp: zero_less_mult_iff)
hence "m \<noteq> 0" by auto
show ?thesis
proof (cases "0 \<le> e")
@@ -955,8 +848,8 @@
definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
-definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where
- "lapprox_posrat prec x y = float_of (round_down (rat_precision prec x y) (x / y))"
+lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
+ is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
lemma compute_lapprox_posrat[code]:
fixes prec x y
@@ -965,13 +858,13 @@
l = rat_precision prec x y;
d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
in normfloat (Float d (- l)))"
- unfolding lapprox_posrat_def div_mult_twopow_eq
- by (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide
- field_simps Let_def
+ unfolding div_mult_twopow_eq Let_def normfloat_def
+ by transfer
+ (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps
del: two_powr_minus_int_float)
-definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where
- "rapprox_posrat prec x y = float_of (round_up (rat_precision prec x y) (x / y))"
+lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
+ is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
(* TODO: optimize using zmod_zmult2_eq, pdivmod ? *)
lemma compute_rapprox_posrat[code]:
@@ -984,7 +877,7 @@
m = fst X mod snd X
in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
proof (cases "y = 0")
- assume "y = 0" thus ?thesis by (simp add: rapprox_posrat_def Let_def)
+ assume "y = 0" thus ?thesis unfolding Let_def normfloat_def by transfer simp
next
assume "y \<noteq> 0"
show ?thesis
@@ -995,10 +888,11 @@
moreover have "real x * 2 powr real l = real x'"
by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
ultimately show ?thesis
- unfolding rapprox_posrat_def round_up_def l_def[symmetric]
+ unfolding Let_def normfloat_def
using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
- by (simp add: Let_def floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals
- del: real_of_ints)
+ l_def[symmetric, THEN meta_eq_to_obj_eq]
+ by transfer
+ (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
next
assume "\<not> 0 \<le> l"
def y' == "y * 2 ^ nat (- l)"
@@ -1008,14 +902,14 @@
using `\<not> 0 \<le> l`
by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
ultimately show ?thesis
+ unfolding Let_def normfloat_def
using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
- by (simp add: rapprox_posrat_def l_def round_up_def ceil_divide_floor_conv
- floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals
- del: real_of_ints)
+ l_def[symmetric, THEN meta_eq_to_obj_eq]
+ by transfer
+ (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
qed
qed
-
lemma rat_precision_pos:
assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
shows "rat_precision n (int x) (int y) > 0"
@@ -1052,16 +946,20 @@
also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
unfolding int_of_reals real_of_int_le_iff
using rat_precision_pos[OF assms] by (rule power_aux)
- finally show ?thesis unfolding rapprox_posrat_def
+ finally show ?thesis
+ unfolding rapprox_posrat_def
apply (simp add: round_up_def)
- apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide)
+ apply (simp add: field_simps powr_minus inverse_eq_divide)
unfolding powr1
unfolding int_of_reals real_of_int_less_iff
- unfolding ceiling_less_eq using rat_precision_pos[of x y n] assms apply simp done
+ unfolding ceiling_less_eq
+ using rat_precision_pos[of x y n] assms
+ apply simp
+ done
qed
-definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where
- "lapprox_rat prec x y = float_of (round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))"
+lift_definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
+ "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
lemma compute_lapprox_rat[code]:
"lapprox_rat prec x y =
@@ -1072,15 +970,15 @@
else (if 0 < y
then - (rapprox_posrat prec (nat (-x)) (nat y))
else lapprox_posrat prec (nat (-x)) (nat (-y))))"
+ apply transfer
apply (cases "y = 0")
- apply (simp add: lapprox_posrat_def rapprox_posrat_def round_down_def lapprox_rat_def)
- apply (auto simp: lapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def
- ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints)
+ apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
+ int_of_reals simp del: real_of_ints)
apply (auto simp: ac_simps)
done
-definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where
- "rapprox_rat prec x y = float_of (round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))"
+lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
+ "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
lemma compute_rapprox_rat[code]:
"rapprox_rat prec x y =
@@ -1091,94 +989,67 @@
else (if 0 < y
then - (lapprox_posrat prec (nat (-x)) (nat y))
else rapprox_posrat prec (nat (-x)) (nat (-y))))"
- apply (cases "y = 0", simp add: lapprox_posrat_def rapprox_posrat_def round_up_def rapprox_rat_def)
- apply (auto simp: rapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def
- ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints)
+ apply transfer
+ apply (cases "y = 0")
+ apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
+ int_of_reals simp del: real_of_ints)
apply (auto simp: ac_simps)
done
subsection {* Division *}
-definition div_precision
-where "div_precision prec x y =
- rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y"
-
-definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
-where "float_divl prec a b =
- float_of (round_down (div_precision prec a b) (a / b))"
+lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
+ "\<lambda>(prec::nat) a b. round_down (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
lemma compute_float_divl[code]:
- fixes m1 s1 m2 s2
- defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2"
- shows "float_divl prec f1 f2 = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
+ "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
proof cases
- assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0"
- then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto
- with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2]
- have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0"
- by (auto simp add: dvd_def)
- then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>"
- by simp_all
- moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this
- moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this
- moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j))
- = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)"
- by (simp add: powr_divide2[symmetric] powr_realpow)
- moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)"
- unfolding mantissa_exponent by (simp add: powr_divide2[symmetric])
- moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) =
- rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i"
- using pos by (simp add: rat_precision_def)
- ultimately show ?thesis
- unfolding float_divl_def lapprox_rat_def div_precision_def
- by (simp add: abs_mult round_down_shift powr_divide2[symmetric]
- del: int_nat_eq real_of_int_diff times_divide_eq_left )
- (simp add: field_simps powr_divide2[symmetric] powr_add)
-next
- assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis
- by (auto simp add: float_divl_def f1_def f2_def lapprox_rat_def)
-qed
+ assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ then show ?thesis
+ proof transfer
+ fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
+ let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
-definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
-where "float_divr prec a b =
- float_of (round_up (div_precision prec a b) (a / b))"
+ have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
+ by (simp add: field_simps powr_divide2[symmetric])
+ have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
+ rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
+ using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+
+ show "round_down (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
+ round_down (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
+ using not_0 unfolding eq1 eq2 round_down_shift by (simp add: field_simps)
+ qed
+qed (transfer, auto)
+
+lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
+ "\<lambda>(prec::nat) a b. round_up (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
lemma compute_float_divr[code]:
- fixes m1 s1 m2 s2
- defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2"
- shows "float_divr prec f1 f2 = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
+ "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
proof cases
- assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0"
- then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto
- with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2]
- have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0"
- by (auto simp add: dvd_def)
- then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>"
- by simp_all
- moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this
- moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this
- moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j))
- = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)"
- by (simp add: powr_divide2[symmetric] powr_realpow)
- moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)"
- unfolding mantissa_exponent by (simp add: powr_divide2[symmetric])
- moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) =
- rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i"
- using pos by (simp add: rat_precision_def)
- ultimately show ?thesis
- unfolding float_divr_def rapprox_rat_def div_precision_def
- by (simp add: abs_mult round_up_shift powr_divide2[symmetric]
- del: int_nat_eq real_of_int_diff times_divide_eq_left)
- (simp add: field_simps powr_divide2[symmetric] powr_add)
-next
- assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis
- by (auto simp add: float_divr_def f1_def f2_def rapprox_rat_def)
-qed
+ assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ then show ?thesis
+ proof transfer
+ fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
+ let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
+
+ have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
+ by (simp add: field_simps powr_divide2[symmetric])
+ have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
+ rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
+ using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+
+ show "round_up (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
+ round_up (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
+ using not_0 unfolding eq1 eq2 round_up_shift by (simp add: field_simps)
+ qed
+qed (transfer, auto)
subsection {* Lemmas needed by Approximate *}
-declare one_float_def[simp del] zero_float_def[simp del]
-
lemma Float_num[simp]: shows
"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
@@ -1255,14 +1126,11 @@
by (auto simp: field_simps mult_le_0_iff)
lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
- using round_down by (simp add: float_divl_def)
+ by transfer (simp add: round_down)
lemma float_divl_lower_bound:
- fixes x y prec
- defines "p == rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y"
- assumes xy: "0 \<le> x" "0 < y" shows "0 \<le> real (float_divl prec x y)"
- using xy unfolding float_divl_def p_def[symmetric] round_down_def
- by (simp add: zero_le_mult_iff zero_le_divide_iff less_eq_float_def less_float_def)
+ "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
+ by transfer (simp add: round_down_def zero_le_mult_iff zero_le_divide_iff)
lemma exponent_1: "exponent 1 = 0"
using exponent_float[of 1 0] by (simp add: one_float_def)
@@ -1292,138 +1160,106 @@
qed
lemma float_divl_pos_less1_bound:
- assumes "0 < real x" and "real x < 1" and "prec \<ge> 1"
- shows "1 \<le> real (float_divl prec 1 x)"
-proof cases
- assume nonneg: "div_precision prec 1 x \<ge> 0"
- hence "2 powr real (div_precision prec 1 x) =
- floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1::real)"
- by (simp add: powr_int del: real_of_int_power) simp
- also have "floor (1::real) \<le> floor (1 / x)" using assms by simp
- also have "floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1 / x) \<le>
- floor (real ((2::int) ^ nat (div_precision prec 1 x)) * (1 / x))"
- by (rule le_mult_floor) (auto simp: assms less_imp_le)
- finally have "2 powr real (div_precision prec 1 x) <=
- floor (2 powr nat (div_precision prec 1 x) / x)" by (simp add: powr_realpow)
- thus ?thesis
- using assms nonneg
- unfolding float_divl_def round_down_def
- by simp (simp add: powr_minus inverse_eq_divide)
-next
- assume neg: "\<not> 0 \<le> div_precision prec 1 x"
- have "1 \<le> 1 * 2 powr (prec - 1)" using assms by (simp add: powr_realpow)
- also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1)"
- apply (rule mult_mono) using assms float_upper_bound
- by (auto intro!: divide_nonneg_pos)
- also have "2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1) =
- 2 powr real (div_precision prec 1 x) / real x"
- using assms
- apply (simp add: div_precision_def rat_precision_def diff_diff_eq2
- mantissa_1 exponent_1 bitlen_1 powr_add powr_minus real_of_nat_diff)
- apply (simp only: diff_def powr_add)
- apply simp
- done
- finally have "1 \<le> \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>"
- using floor_mono[of "1::real"] by simp thm mult_mono
- hence "1 \<le> real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>"
- by (metis floor_real_of_int one_le_floor)
- hence "1 * 1 \<le>
- real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor> * 2 powr - real (div_precision prec 1 x)"
- apply (rule mult_mono)
- using assms neg
- by (auto intro: divide_nonneg_pos mult_nonneg_nonneg simp: real_of_int_minus[symmetric] powr_int simp del: real_of_int_minus) find_theorems "real (- _)"
- thus ?thesis
- using assms neg
- unfolding float_divl_def round_down_def
- by simp
+ "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
+proof transfer
+ fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
+ def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
+ show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
+ proof cases
+ assume nonneg: "0 \<le> p"
+ hence "2 powr real (p) = floor (real ((2::int) ^ nat p)) * floor (1::real)"
+ by (simp add: powr_int del: real_of_int_power) simp
+ also have "floor (1::real) \<le> floor (1 / x)" using x prec by simp
+ also have "floor (real ((2::int) ^ nat p)) * floor (1 / x) \<le>
+ floor (real ((2::int) ^ nat p) * (1 / x))"
+ by (rule le_mult_floor) (auto simp: x prec less_imp_le)
+ finally have "2 powr real p \<le> floor (2 powr nat p / x)" by (simp add: powr_realpow)
+ thus ?thesis unfolding p_def[symmetric]
+ using x prec nonneg by (simp add: powr_minus inverse_eq_divide round_down_def)
+ next
+ assume neg: "\<not> 0 \<le> p"
+
+ have "x = 2 powr (log 2 x)"
+ using x by simp
+ also have "2 powr (log 2 x) \<le> 2 powr p"
+ proof (rule powr_mono)
+ have "log 2 x \<le> \<lceil>log 2 x\<rceil>"
+ by simp
+ also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + 1"
+ using ceiling_diff_floor_le_1[of "log 2 x"] by simp
+ also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + prec"
+ using prec by simp
+ finally show "log 2 x \<le> real p"
+ using x by (simp add: p_def)
+ qed simp
+ finally have x_le: "x \<le> 2 powr p" .
+
+ from neg have "2 powr real p \<le> 2 powr 0"
+ by (intro powr_mono) auto
+ also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
+ also have "\<dots> \<le> \<lfloor>2 powr real p / x\<rfloor>" unfolding real_of_int_le_iff
+ using x x_le by (intro floor_mono) (simp add: pos_le_divide_eq mult_pos_pos)
+ finally show ?thesis
+ using prec x unfolding p_def[symmetric]
+ by (simp add: round_down_def powr_minus_divide pos_le_divide_eq mult_pos_pos)
+ qed
qed
lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
- using round_up by (simp add: float_divr_def)
+ using round_up by transfer simp
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 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
+ have "1 \<le> 1 / real x" using `0 < x` and `x < 1` 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 less_eq_float_def by auto
+ finally show ?thesis by auto
qed
lemma float_divr_nonpos_pos_upper_bound:
- assumes "real x \<le> 0" and "0 < real y"
- shows "real (float_divr prec x y) \<le> 0"
-using assms
-unfolding float_divr_def round_up_def
-by (auto simp: field_simps mult_le_0_iff divide_le_0_iff)
+ "real x \<le> 0 \<Longrightarrow> 0 < real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
+ by transfer (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def)
lemma float_divr_nonneg_neg_upper_bound:
- assumes "0 \<le> real x" and "real y < 0"
- shows "real (float_divr prec x y) \<le> 0"
-using assms
-unfolding float_divr_def round_up_def
-by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff)
+ "0 \<le> real x \<Longrightarrow> real y < 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
+ by transfer (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def)
+
+lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is
+ "\<lambda>(prec::nat) x. round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
+
+lemma float_round_up: "real x \<le> real (float_round_up prec x)"
+ using round_up by transfer simp
-definition "round_prec p f = int p - (bitlen \<bar>mantissa f\<bar> + exponent f)"
+lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is
+ "\<lambda>(prec::nat) x. round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
-definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
-"float_round_down prec f = float_of (round_down (round_prec prec f) f)"
+lemma float_round_down: "real (float_round_down prec x) \<le> real x"
+ using round_down by transfer simp
-definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
-"float_round_up prec f = float_of (round_up (round_prec prec f) f)"
+lemma floor_add2[simp]: "\<lfloor> real i + x \<rfloor> = i + \<lfloor> x \<rfloor>"
+ using floor_add[of x i] by (simp del: floor_add add: ac_simps)
lemma compute_float_round_down[code]:
-fixes prec m e
-defines "d == bitlen (abs m) - int prec"
-defines "P == 2^nat d"
-defines "f == Float m e"
-shows "float_round_down prec f = (let d = d in
- if 0 < d then let P = P ; n = m div P in Float n (e + d)
- else f)"
- unfolding float_round_down_def float_down_def[symmetric]
- compute_float_down f_def Let_def P_def round_prec_def d_def bitlen_Float
- by (simp add: field_simps)
-
-lemma compute_float_round_up[code]:
-fixes prec m e
-defines "d == bitlen (abs m) - int prec"
-defines "P == 2^nat d"
-defines "f == Float m e"
-shows "float_round_up prec f = (let d = d in
- if 0 < d then let P = P ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d)
- else f)"
- unfolding float_round_up_def float_up_def[symmetric]
- compute_float_up f_def Let_def P_def round_prec_def d_def bitlen_Float
- by (simp add: field_simps)
-
-lemma float_round_up: "real x \<le> real (float_round_up prec x)"
- using round_up
- by (simp add: float_round_up_def)
+ "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
+ if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
+ else Float m e)"
+ unfolding Let_def
+ using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
+ apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
+ apply (cases "m = 0")
+ apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
+ done
-lemma float_round_down: "real (float_round_down prec x) \<le> real x"
- using round_down
- by (simp add: float_round_down_def)
-
-instantiation float :: lattice_ab_group_add
-begin
-
-definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
-where "inf_float a b = min a b"
-
-definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
-where "sup_float a b = max a b"
-
-instance
-proof
- fix x y :: float show "inf x y \<le> x" unfolding inf_float_def by simp
- show "inf x y \<le> y" unfolding inf_float_def by simp
- show "x \<le> sup x y" unfolding sup_float_def by simp
- show "y \<le> sup x y" unfolding sup_float_def by simp
- fix z::float
- assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z" unfolding inf_float_def by simp
- next fix x y z :: float
- assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x" unfolding sup_float_def by simp
-qed
-
-end
+lemma compute_float_round_up[code]:
+ "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
+ 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)"
+ using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
+ unfolding Let_def
+ apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
+ apply (cases "m = 0")
+ apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
+ done
lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
apply (auto simp: zero_float_def mult_le_0_iff)
@@ -1438,63 +1274,38 @@
unfolding nprt_def inf_float_def min_def Float_le_zero_iff ..
lemma of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
- unfolding pprt_def sup_float_def max_def sup_real_def by (auto simp: less_eq_float_def)
+ unfolding pprt_def sup_float_def max_def sup_real_def by auto
lemma of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
- unfolding nprt_def inf_float_def min_def inf_real_def by (auto simp: less_eq_float_def)
+ unfolding nprt_def inf_float_def min_def inf_real_def by auto
-definition int_floor_fl :: "float \<Rightarrow> int" where
- "int_floor_fl f = floor f"
+lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
lemma compute_int_floor_fl[code]:
shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e
else m div (2 ^ (nat (-e))))"
- by (simp add: int_floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
+ by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
-definition floor_fl :: "float \<Rightarrow> float" where
- "floor_fl f = float_of (floor f)"
+lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
lemma compute_floor_fl[code]:
shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e
else Float (m div (2 ^ (nat (-e)))) 0)"
- by (simp add: floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
+ by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
-lemma floor_fl: "real (floor_fl x) \<le> real x" by (simp add: floor_fl_def)
-lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by (simp add: int_floor_fl_def)
+lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
+
+lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
proof cases
assume nzero: "floor_fl x \<noteq> float_of 0"
- have "floor_fl x \<equiv> Float \<lfloor>real x\<rfloor> 0" by (simp add: floor_fl_def)
- from denormalize_shift[OF this nzero] guess i . note i = this
+ have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
+ from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
thus ?thesis by simp
qed (simp add: floor_fl_def)
-(* TODO: not used in approximation
-definition ceiling_fl :: "float_of \<Rightarrow> float" where
- "ceiling_fl f = float_of (ceiling f)"
-
-lemma compute_ceiling_fl:
- "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: "real x \<le> real (ceiling_fl x)"
-
-definition lb_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float" where
-"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
-
-definition ub_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<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> 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"
-
-lemma ub_mod: fixes k :: int and x :: float_of 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)"
-
-*)
+code_datatype Float
end