author immler Wed Nov 12 17:37:43 2014 +0100 (2014-11-12) changeset 58989 99831590def5 parent 58988 6ebf918128b9 child 58990 b66788d19c0f
tuned proofs
```     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.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.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)