src/HOL/Library/Float.thy
changeset 32960 69916a850301
parent 32069 6d28bbd33e2c
child 33555 a0a8a40385a2
     1.1 --- a/src/HOL/Library/Float.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4        fix x y z :: real
     1.5        assume "y \<noteq> 0"
     1.6        then have "(x * inverse y = z) = (x = z * y)"
     1.7 -	by auto
     1.8 +        by auto
     1.9      }
    1.10      note inverse = this
    1.11      have eq': "real a * (pow2 (b - b')) = real a'"
    1.12 @@ -551,9 +551,9 @@
    1.13      } moreover
    1.14      { have "x + 1 \<le> x - x mod 2 + 2"
    1.15        proof -
    1.16 -	have "x mod 2 < 2" using `0 < x` by auto
    1.17 - 	hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
    1.18 -	thus ?thesis by auto
    1.19 +        have "x mod 2 < 2" using `0 < x` by auto
    1.20 +        hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
    1.21 +        thus ?thesis by auto
    1.22        qed
    1.23        also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto
    1.24        also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
    1.25 @@ -839,7 +839,7 @@
    1.26      have "0 < ?X div y"
    1.27      proof -
    1.28        have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)"
    1.29 -	using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto
    1.30 +        using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto
    1.31        hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans)
    1.32        hence "bitlen x \<le> bitlen y" by auto
    1.33        hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto
    1.34 @@ -847,16 +847,16 @@
    1.35        have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto
    1.36  
    1.37        have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l"
    1.38 -	using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto
    1.39 +        using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto
    1.40  
    1.41        have "y * 2^nat (bitlen x - 1) \<le> y * x" 
    1.42 -	using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono)
    1.43 +        using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono)
    1.44        also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono)
    1.45        also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`)
    1.46        finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))"
    1.47 -	unfolding real_of_int_le_iff[symmetric] by auto
    1.48 +        unfolding real_of_int_le_iff[symmetric] by auto
    1.49        hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" 
    1.50 -	unfolding real_mult_assoc real_divide_def by auto
    1.51 +        unfolding real_mult_assoc real_divide_def by auto
    1.52        also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto
    1.53        finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
    1.54        thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
    1.55 @@ -1194,19 +1194,19 @@
    1.56        case True
    1.57        have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
    1.58        have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
    1.59 -	by (auto simp add: pow2_add `0 < ?d` pow_d)
    1.60 +        by (auto simp add: pow2_add `0 < ?d` pow_d)
    1.61        thus ?thesis
    1.62 -	unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
    1.63 -	by auto
    1.64 +        unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
    1.65 +        by auto
    1.66      next
    1.67        case False
    1.68        have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    1.69        also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    1.70        finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
    1.71 -	unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    1.72 -	by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
    1.73 +        unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    1.74 +        by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
    1.75        thus ?thesis
    1.76 -	unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] .
    1.77 +        unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] .
    1.78      qed
    1.79    next
    1.80      case False
    1.81 @@ -1264,7 +1264,7 @@
    1.82      have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
    1.83      proof -
    1.84        have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power[symmetric] real_number_of unfolding pow2_int[symmetric] 
    1.85 -	using `?l > 0` by auto
    1.86 +        using `?l > 0` by auto
    1.87        also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
    1.88        also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
    1.89        finally show ?thesis by auto