use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 18 14:29:22 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 19 11:55:30 2012 +0200
@@ -634,7 +634,7 @@
have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
- have "arctan (1 / x) \<le> arctan ?invx" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divr)
+ have "arctan (1 / x) \<le> arctan ?invx" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divr)
also have "\<dots> \<le> (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
finally have "pi / 2 - (?ub_horner ?invx) \<le> arctan x"
using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
@@ -726,7 +726,7 @@
have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
have "(?lb_horner ?invx) \<le> arctan (?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
- also have "\<dots> \<le> arctan (1 / x)" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divl)
+ also have "\<dots> \<le> arctan (1 / x)" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divl)
finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
@@ -749,8 +749,8 @@
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`]
- unfolding atLeastAtMost_iff using bounds[unfolded real_of_float_minus arctan_minus]
+ show ?thesis unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
+ unfolding atLeastAtMost_iff using bounds[unfolded minus_float.rep_eq arctan_minus]
by (simp add: arctan_minus)
qed
@@ -783,6 +783,7 @@
| "lb_sin_cos_aux prec 0 i k x = 0"
| "lb_sin_cos_aux prec (Suc n) i k x =
(lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
+
lemma cos_aux:
shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
@@ -880,7 +881,7 @@
hence "get_even n = 0" by auto
have "- (pi / 2) \<le> x" by (rule order_trans[OF _ `0 < real x`[THEN less_imp_le]], auto)
with `x \<le> pi / 2`
- show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps real_of_float_minus real_of_float_zero using cos_ge_zero by auto
+ show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps minus_float.rep_eq zero_float.rep_eq using cos_ge_zero by auto
qed
ultimately show ?thesis by auto
next
@@ -995,7 +996,7 @@
case False
hence "get_even n = 0" by auto
with `x \<le> pi / 2` `0 \<le> real x`
- show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps real_of_float_minus using sin_ge_zero by auto
+ show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps minus_float.rep_eq using sin_ge_zero by auto
qed
ultimately show ?thesis by auto
next
@@ -1214,7 +1215,7 @@
using lb_cos_minus[OF pi_lx lx_0] by simp
also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
- by (simp only: real_of_float_uminus real_of_int_minus
+ by (simp only: uminus_float.rep_eq real_of_int_minus
cos_minus diff_minus mult_minus_left)
finally have "(lb_cos prec (- ?lx)) \<le> cos x"
unfolding cos_periodic_int . }
@@ -1242,7 +1243,7 @@
have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
- by (simp only: real_of_float_uminus real_of_int_minus
+ by (simp only: uminus_float.rep_eq real_of_int_minus
cos_minus diff_minus mult_minus_left)
also have "\<dots> \<le> (ub_cos prec (- ?ux))"
using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
@@ -1334,10 +1335,10 @@
unfolding cos_periodic_int ..
also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
- by (simp only: real_of_float_minus real_of_int_minus real_of_one minus_one[symmetric]
+ by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
diff_minus mult_minus_left mult_1_left)
also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
- unfolding real_of_float_uminus cos_minus ..
+ unfolding uminus_float.rep_eq cos_minus ..
also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
using lb_cos_minus[OF pi_ux ux_0] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -1378,7 +1379,7 @@
unfolding cos_periodic_int ..
also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
- by (simp only: real_of_float_minus real_of_int_minus real_of_one
+ by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
minus_one[symmetric] diff_minus mult_minus_left mult_1_left)
also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
using lb_cos[OF lx_0 pi_lx] by simp
@@ -1534,7 +1535,7 @@
proof -
have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
- unfolding less_eq_float_def real_of_float_zero .
+ unfolding less_eq_float_def zero_float.rep_eq .
have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
@@ -1562,7 +1563,7 @@
exp (float_divl prec x (- floor_fl x)) ^ ?num"
using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
- using float_divl by (auto intro!: power_mono simp del: real_of_float_uminus)
+ using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
finally show ?thesis
@@ -1571,7 +1572,7 @@
case True
have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
- have "- 1 \<le> x / (- floor_fl x)" unfolding real_of_float_minus by auto
+ have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
@@ -1597,7 +1598,7 @@
have "lb_exp prec x \<le> exp x"
proof -
from exp_boundaries'[OF `-x \<le> 0`]
- have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
+ have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
have "float_divl prec 1 (ub_exp prec (-x)) \<le> 1 / ub_exp prec (-x)" using float_divl[where x=1] by auto
also have "\<dots> \<le> exp x"
@@ -1611,7 +1612,7 @@
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 lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
@@ -1686,7 +1687,7 @@
let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
- have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
+ have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
by (rule mult_right_mono)
@@ -1694,7 +1695,7 @@
finally show "?lb \<le> ?ln" .
have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
- also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
+ also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
by (rule mult_right_mono)
@@ -1743,14 +1744,14 @@
have uthird_gt0: "0 < real ?uthird + 1" using ub3_lb by auto
have lthird_gt0: "0 < real ?lthird + 1" using lb3_lb by auto
- show ?ub_ln2 unfolding ub_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
+ show ?ub_ln2 unfolding ub_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
proof (rule add_mono, fact ln_float_bounds(2)[OF lb2 ub2])
have "ln (1 / 3 + 1) \<le> ln (real ?uthird + 1)" unfolding ln_le_cancel_iff[OF third_gt0 uthird_gt0] using ub3 by auto
also have "\<dots> \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird"
using ln_float_bounds(2)[OF ub3_lb ub3_ub] .
finally show "ln (1 / 3 + 1) \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird" .
qed
- show ?lb_ln2 unfolding lb_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
+ show ?lb_ln2 unfolding lb_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
proof (rule add_mono, fact ln_float_bounds(1)[OF lb2 ub2])
have "?lthird * lb_ln_horner prec (get_even prec) 1 ?lthird \<le> ln (real ?lthird + 1)"
using ln_float_bounds(1)[OF lb3_lb lb3_ub] .
@@ -1993,7 +1994,7 @@
{
have "lb_ln2 prec * ?s \<le> ln 2 * (e + (bitlen m - 1))" (is "?lb2 \<le> _")
- unfolding nat_0 power_0 mult_1_right real_of_float_times
+ unfolding nat_0 power_0 mult_1_right times_float.rep_eq
using lb_ln2[of prec]
proof (rule mult_mono)
from float_gt1_scale[OF `1 \<le> Float m e`]
@@ -2011,7 +2012,7 @@
have "ln ?x \<le> (?x - 1) * ub_ln_horner prec (get_odd prec) 1 (?x - 1)" (is "_ \<le> ?ub_horner") by auto
moreover
have "ln 2 * (e + (bitlen m - 1)) \<le> ub_ln2 prec * ?s" (is "_ \<le> ?ub2")
- unfolding nat_0 power_0 mult_1_right real_of_float_times
+ unfolding nat_0 power_0 mult_1_right times_float.rep_eq
using ub_ln2[of prec]
proof (rule mult_mono)
from float_gt1_scale[OF `1 \<le> Float m e`]
@@ -2025,7 +2026,7 @@
}
ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
- unfolding real_of_float_plus e_def[symmetric] m_def[symmetric] by simp
+ unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
qed
qed
@@ -2049,7 +2050,7 @@
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
from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
- have "?ln \<le> - the (lb_ln prec ?divl)" unfolding real_of_float_uminus by (rule order_trans)
+ have "?ln \<le> - the (lb_ln prec ?divl)" unfolding uminus_float.rep_eq by (rule order_trans)
} moreover
{
let ?divr = "float_divr prec 1 x"
@@ -2059,7 +2060,7 @@
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
from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
- have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding real_of_float_uminus by (rule order_trans)
+ have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding uminus_float.rep_eq by (rule order_trans)
}
ultimately show ?thesis unfolding lb_ln.simps[where x=x] ub_ln.simps[where x=x]
unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
@@ -2447,7 +2448,7 @@
from lift_un'[OF Minus.prems[unfolded approx.simps]] Minus.hyps
obtain l1 u1 where "l = -u1" and "u = -l1"
"l1 \<le> interpret_floatarith a xs" and "interpret_floatarith a xs \<le> u1" unfolding fst_conv snd_conv by blast
- thus ?case unfolding interpret_floatarith.simps using real_of_float_minus by auto
+ thus ?case unfolding interpret_floatarith.simps using minus_float.rep_eq by auto
next
case (Mult a b)
from lift_bin'[OF Mult.prems[unfolded approx.simps]] Mult.hyps
--- a/src/HOL/Library/Float.thy Wed Apr 18 14:29:22 2012 +0200
+++ b/src/HOL/Library/Float.thy Thu Apr 19 11:55:30 2012 +0200
@@ -8,13 +8,16 @@
morphisms real_of_float float_of
by auto
-setup_lifting type_definition_float
+defs (overloaded)
+ real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
+
+lemma type_definition_float': "type_definition real float_of float"
+ using type_definition_float unfolding real_of_float_def .
+
+setup_lifting (no_code) type_definition_float'
lemmas float_of_inject[simp]
-defs (overloaded)
- real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
-
declare [[coercion "real :: float \<Rightarrow> real"]]
lemma real_of_float_eq:
@@ -27,10 +30,6 @@
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"
@@ -124,6 +123,9 @@
qed
lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
+declare Float.rep_eq[simp]
+
+code_datatype Float
subsection {* Arithmetic operations on floating point numbers *}
@@ -131,41 +133,34 @@
begin
lift_definition zero_float :: float is 0 by simp
+declare zero_float.rep_eq[simp]
lift_definition one_float :: float is 1 by simp
+declare one_float.rep_eq[simp]
lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
+declare plus_float.rep_eq[simp]
lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
+declare times_float.rep_eq[simp]
lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
+declare minus_float.rep_eq[simp]
lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
+declare uminus_float.rep_eq[simp]
lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
+declare abs_float.rep_eq[simp]
lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
+declare sgn_float.rep_eq[simp]
lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
+declare less_eq_float.rep_eq[simp]
lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
+declare less_float.rep_eq[simp]
instance
proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
end
-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
@@ -213,7 +208,7 @@
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)
+ plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
done
lemma transfer_numeral [transfer_rule]:
@@ -366,12 +361,9 @@
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)
+by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
unfolding real_of_float_eq mantissa_exponent[of f] by simp
@@ -537,9 +529,7 @@
subsection {* Rounding Floats *}
lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up 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)
+declare float_up.rep_eq[simp]
lemma float_up_correct:
shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
@@ -552,9 +542,7 @@
qed (simp add: algebra_simps round_up)
lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down 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)
+declare float_down.rep_eq[simp]
lemma float_down_correct:
shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
@@ -929,7 +917,8 @@
ultimately show ?thesis using assms by simp
qed
-lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
+lemma rapprox_posrat_less1:
+ assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
shows "real (rapprox_posrat n x y) < 1"
proof -
have powr1: "2 powr real (rat_precision n (int x) (int y)) =
@@ -947,14 +936,10 @@
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
- apply (simp add: round_up_def)
- apply (simp add: field_simps powr_minus inverse_eq_divide)
- unfolding powr1
+ apply (transfer fixing: n x y)
+ apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide 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
+ apply (simp add: ceiling_less_eq)
done
qed
@@ -970,12 +955,7 @@
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 (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
+ by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
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
@@ -989,12 +969,7 @@
else (if 0 < y
then - (lapprox_posrat prec (nat (-x)) (nat y))
else rapprox_posrat prec (nat (-x)) (nat (-y))))"
- 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
+ by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
subsection {* Division *}
@@ -1004,23 +979,17 @@
lemma compute_float_divl[code]:
"float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
proof cases
- 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)"
+ 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)"
+ assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ then 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)"
+ by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+ 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 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
+ show ?thesis
+ using not_0
+ by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
qed (transfer, auto)
lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
@@ -1029,23 +998,17 @@
lemma compute_float_divr[code]:
"float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
proof cases
- 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)"
+ 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)"
+ assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+ then 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)"
+ by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+ 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 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
+ show ?thesis
+ using not_0
+ by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
qed (transfer, auto)
subsection {* Lemmas needed by Approximate *}
@@ -1242,12 +1205,9 @@
"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)"
+ using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
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
+ by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
lemma compute_float_round_up[code]:
"float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
@@ -1256,10 +1216,7 @@
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
+ by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
apply (auto simp: zero_float_def mult_le_0_iff)
@@ -1282,15 +1239,13 @@
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))))"
+ "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
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)"
+ "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
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 transfer simp
@@ -1305,7 +1260,5 @@
thus ?thesis by simp
qed (simp add: floor_fl_def)
-code_datatype Float
-
end