src/HOL/Library/Float.thy
changeset 56777 9c3f0ae99532
parent 56571 f4635657d66f
child 57492 74bf65a1910a
     1.1 --- a/src/HOL/Library/Float.thy	Mon Apr 28 17:48:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Mon Apr 28 17:50:03 2014 +0200
     1.3 @@ -919,7 +919,7 @@
     1.4    show ?thesis
     1.5    proof (cases "0 \<le> l")
     1.6      assume "0 \<le> l"
     1.7 -    def x' == "x * 2 ^ nat l"
     1.8 +    def x' \<equiv> "x * 2 ^ nat l"
     1.9      have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power)
    1.10      moreover have "real x * 2 powr real l = real x'"
    1.11        by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
    1.12 @@ -931,7 +931,7 @@
    1.13           (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
    1.14     next
    1.15      assume "\<not> 0 \<le> l"
    1.16 -    def y' == "y * 2 ^ nat (- l)"
    1.17 +    def y' \<equiv> "y * 2 ^ nat (- l)"
    1.18      from `y \<noteq> 0` have "y' \<noteq> 0" by (simp add: y'_def)
    1.19      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
    1.20      moreover have "real x * real (2::int) powr real l / real y = x / real y'"
    1.21 @@ -959,9 +959,12 @@
    1.22      using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
    1.23  qed
    1.24  
    1.25 -lemma power_aux: assumes "x > 0" shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
    1.26 +lemma power_aux:
    1.27 +  assumes "x > 0"
    1.28 +  shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
    1.29  proof -
    1.30 -  def y \<equiv> "nat (x - 1)" moreover
    1.31 +  def y \<equiv> "nat (x - 1)"
    1.32 +  moreover
    1.33    have "(2::int) ^ y \<le> (2 ^ (y + 1)) - 1" by simp
    1.34    ultimately show ?thesis using assms by simp
    1.35  qed
    1.36 @@ -1103,8 +1106,8 @@
    1.37  
    1.38  lemma lapprox_rat_nonneg:
    1.39    fixes n x y
    1.40 -  defines "p == int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
    1.41 -  assumes "0 \<le> x" "0 < y"
    1.42 +  defines "p \<equiv> int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
    1.43 +  assumes "0 \<le> x" and "0 < y"
    1.44    shows "0 \<le> real (lapprox_rat n x y)"
    1.45  using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    1.46     powr_int[of 2, simplified]