tuned proofs
authorimmler
Wed Nov 12 17:37:43 2014 +0100 (2014-11-12)
changeset 5898999831590def5
parent 58988 6ebf918128b9
child 58990 b66788d19c0f
tuned proofs
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Wed Nov 12 17:37:43 2014 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Nov 12 17:37:43 2014 +0100
     1.3 @@ -580,13 +580,11 @@
     1.4    real_of_nat_add
     1.5    real_of_nat_mult
     1.6    real_of_nat_power
     1.7 +  real_of_nat_numeral
     1.8  
     1.9  lemmas int_of_reals = real_of_ints[symmetric]
    1.10  lemmas nat_of_reals = real_of_nats[symmetric]
    1.11  
    1.12 -lemma two_real_int: "(2::real) = real (2::int)" by simp
    1.13 -lemma two_real_nat: "(2::real) = real (2::nat)" by simp
    1.14 -
    1.15  
    1.16  subsection {* Rounding Real Numbers *}
    1.17  
    1.18 @@ -661,23 +659,12 @@
    1.19    assumes "x < 1 / 2" "p > 0"
    1.20    shows "round_up p x < 1"
    1.21  proof -
    1.22 -  have powr1: "2 powr p = 2 ^ nat p"
    1.23 -    using `p > 0` by (simp add: powr_realpow[symmetric])
    1.24    have "x * 2 powr p < 1 / 2 * 2 powr p"
    1.25      using assms by simp
    1.26 -  also have "\<dots> = 2 powr (p - 1)"
    1.27 -    by (simp add: algebra_simps powr_mult_base)
    1.28 -  also have "\<dots> = 2 ^ nat (p - 1)"
    1.29 -    using `p > 0` by (simp add: powr_realpow[symmetric])
    1.30 -  also have "\<dots> \<le> 2 ^ nat p - 1"
    1.31 -    using `p > 0`
    1.32 -    unfolding int_of_reals real_of_int_le_iff
    1.33 -    by simp
    1.34 -  finally show ?thesis
    1.35 -    apply (simp add: round_up_def field_simps powr_minus powr1)
    1.36 -    unfolding int_of_reals real_of_int_less_iff
    1.37 -    apply (simp add: ceiling_less_eq)
    1.38 -    done
    1.39 +  also have "\<dots> \<le> 2 powr p - 1" using `p > 0`
    1.40 +    by (auto simp: powr_divide2[symmetric] powr_int field_simps self_le_power)
    1.41 +  finally show ?thesis using `p > 0`
    1.42 +    by (simp add: round_up_def field_simps powr_minus powr_int ceiling_less_eq)
    1.43  qed
    1.44  
    1.45  lemma round_down_ge1:
    1.46 @@ -856,7 +843,7 @@
    1.47      apply (simp add: powr_realpow[symmetric])
    1.48      using `x > 0` by simp
    1.49    finally show "x < 2 ^ nat (bitlen x)" using `x > 0`
    1.50 -    by (simp add: bitlen_def ac_simps int_of_reals del: real_of_ints)
    1.51 +    by (simp add: bitlen_def ac_simps)
    1.52  qed
    1.53  
    1.54  lemma bitlen_pow2[simp]:
    1.55 @@ -1810,8 +1797,7 @@
    1.56    also have "mantissa x \<le> \<bar>mantissa x\<bar>" by simp
    1.57    also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
    1.58      using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg `mantissa x \<noteq> 0`
    1.59 -    by (simp add: powr_int) (simp only: two_real_int int_of_reals real_of_int_abs[symmetric]
    1.60 -      real_of_int_le_iff less_imp_le)
    1.61 +    by (auto simp del: real_of_int_abs simp add: powr_int)
    1.62    finally show ?thesis by (simp add: powr_add)
    1.63  qed
    1.64