tuned
authorhaftmann
Sat Jun 22 06:25:34 2019 +0000 (4 weeks ago)
changeset 70355a80ad0ac0837
parent 70354 9497a6334a26
child 70356 4a327c061870
tuned
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Fri Jun 21 18:55:00 2019 +0000
     1.2 +++ b/src/HOL/Library/Float.thy	Sat Jun 22 06:25:34 2019 +0000
     1.3 @@ -831,19 +831,12 @@
     1.4    finally show ?thesis
     1.5      using \<open>p + e < 0\<close>
     1.6      apply transfer
     1.7 -    apply (simp add: ac_simps round_down_def flip: floor_divide_of_int_eq)
     1.8 -    proof - (*FIXME*)
     1.9 -      fix pa :: int and ea :: int and ma :: int
    1.10 -      assume a1: "2 ^ nat (- pa - ea) = 1 / (2 powr real_of_int pa * 2 powr real_of_int ea)"
    1.11 -      assume "pa + ea < 0"
    1.12 -      have "\<lfloor>real_of_int ma / real_of_int (int 2 ^ nat (- (pa + ea)))\<rfloor> =
    1.13 -          \<lfloor>real_of_float (Float ma (pa + ea))\<rfloor>"
    1.14 -        using a1 by (simp add: powr_add)
    1.15 -      then show "\<lfloor>real_of_int ma * (2 powr real_of_int pa * 2 powr real_of_int ea)\<rfloor> =
    1.16 -          ma div 2 ^ nat (- pa - ea)"
    1.17 -        by (metis Float.rep_eq add_uminus_conv_diff floor_divide_of_int_eq
    1.18 -            minus_add_distrib of_int_simps(3) of_nat_numeral powr_add)
    1.19 -    qed
    1.20 +    apply (simp add: round_down_def field_simps flip: floor_divide_of_int_eq)
    1.21 +    apply (metis (no_types, hide_lams) Float.rep_eq
    1.22 +      add.inverse_inverse compute_real_of_float diff_minus_eq_add
    1.23 +      floor_divide_of_int_eq int_of_reals(1) linorder_not_le
    1.24 +      minus_add_distrib of_int_eq_numeral_power_cancel_iff powr_add)
    1.25 +    done
    1.26  next
    1.27    case False
    1.28    then have r: "real_of_int e + real_of_int p = real (nat (e + p))"