src/HOL/Library/Float.thy
changeset 57862 8f074e6e22fc
parent 57512 cc97b347b301
child 58042 ffa9e39763e3
     1.1 --- a/src/HOL/Library/Float.thy	Tue Aug 05 12:42:38 2014 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Aug 05 12:56:15 2014 +0200
     1.3 @@ -610,8 +610,7 @@
     1.4      by (auto intro: exI[where x="m*2^nat (e+p)"]
     1.5               simp add: ac_simps powr_add[symmetric] r powr_realpow)
     1.6    with `\<not> p + e < 0` show ?thesis
     1.7 -    by transfer
     1.8 -       (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
     1.9 +    by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
    1.10  qed
    1.11  hide_fact (open) compute_float_down
    1.12  
    1.13 @@ -682,8 +681,7 @@
    1.14      by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
    1.15        intro: exI[where x="m*2^nat (e+p)"])
    1.16    then show ?thesis using `\<not> p + e < 0`
    1.17 -    by transfer
    1.18 -       (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
    1.19 +    by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
    1.20  qed
    1.21  hide_fact (open) compute_float_up
    1.22  
    1.23 @@ -840,7 +838,7 @@
    1.24      have "(1::int) < 2" by simp
    1.25      case False let ?S = "2^(nat (-e))"
    1.26      have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
    1.27 -      by (auto simp: powr_minus field_simps inverse_eq_divide)
    1.28 +      by (auto simp: powr_minus field_simps)
    1.29      hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
    1.30        by (auto simp: powr_minus)
    1.31      hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
    1.32 @@ -940,7 +938,7 @@
    1.33      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
    1.34      moreover have "real x * real (2::int) powr real l / real y = x / real y'"
    1.35        using `\<not> 0 \<le> l`
    1.36 -      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
    1.37 +      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
    1.38      ultimately show ?thesis
    1.39        unfolding normfloat_def
    1.40        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
    1.41 @@ -993,7 +991,7 @@
    1.42      using rat_precision_pos[OF assms] by (rule power_aux)
    1.43    finally show ?thesis
    1.44      apply (transfer fixing: n x y)
    1.45 -    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
    1.46 +    apply (simp add: round_up_def field_simps powr_minus powr1)
    1.47      unfolding int_of_reals real_of_int_less_iff
    1.48      apply (simp add: ceiling_less_eq)
    1.49      done
    1.50 @@ -1415,7 +1413,7 @@
    1.51      by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
    1.52    also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
    1.53      using `0 < x`
    1.54 -    by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
    1.55 +    by (auto simp: field_simps powr_add powr_divide2[symmetric])
    1.56    also have "\<dots> < 2 powr 0"
    1.57      using real_of_int_floor_add_one_gt
    1.58      unfolding neg_less_iff_less