src/HOL/Real.thy
 changeset 61694 6571c78c9667 parent 61649 268d88ec9087 child 61799 4cf66f21b764
```     1.1 --- a/src/HOL/Real.thy	Tue Nov 17 12:01:19 2015 +0100
1.2 +++ b/src/HOL/Real.thy	Tue Nov 17 12:32:08 2015 +0000
1.3 @@ -1044,7 +1044,7 @@
1.4    have "(0::real) \<le> 1"
1.5      by (metis less_eq_real_def zero_less_one)
1.6    thus ?thesis
1.7 -    by (metis floor_unique less_add_one less_imp_le not_less of_int_le_iff order_trans)
1.8 +    by (metis floor_of_int less_floor_iff)
1.9  qed
1.10
1.11  lemma int_le_real_less: "(n \<le> m) = (real_of_int n < real_of_int m + 1)"
1.12 @@ -1509,29 +1509,23 @@
1.13  lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
1.14    by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
1.15
1.16 -lemma real_of_int_ceiling_cancel [simp]:
1.17 -     "(real_of_int (ceiling x) = x) = (\<exists>n::int. x = real_of_int n)"
1.18 +lemma of_int_ceiling_cancel [simp]:
1.19 +     "(of_int (ceiling x) = x) = (\<exists>n::int. x = of_int n)"
1.20    using ceiling_of_int by metis
1.21
1.22 -lemma ceiling_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> ceiling x = n + 1"
1.23 -  by linarith
1.24 +lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> ceiling x = n + 1"
1.25 +  by (simp add: ceiling_unique)
1.26
1.27 -lemma ceiling_eq2: "[| real_of_int n < x; x \<le> real_of_int n + 1 |] ==> ceiling x = n + 1"
1.28 +lemma of_int_ceiling_diff_one_le [simp]: "of_int (ceiling r) - 1 \<le> r"
1.29    by linarith
1.30
1.31 -lemma real_of_int_ceiling_diff_one_le [simp]: "real_of_int (ceiling r) - 1 \<le> r"
1.32 -  by linarith
1.33 -
1.34 -lemma real_of_int_ceiling_le_add_one [simp]: "real_of_int (ceiling r) \<le> r + 1"
1.35 +lemma of_int_ceiling_le_add_one [simp]: "of_int (ceiling r) \<le> r + 1"
1.36    by linarith
1.37
1.38 -lemma ceiling_le: "x <= real_of_int a ==> ceiling x <= a"
1.39 -  by linarith
1.40 +lemma ceiling_le: "x <= of_int a ==> ceiling x <= a"
1.41 +  by (simp add: ceiling_le_iff)
1.42
1.43 -lemma ceiling_le_real: "ceiling x <= a ==> x <= real_of_int a"
1.44 -  by linarith
1.45 -
1.46 -lemma ceiling_divide_eq_div: "\<lceil>real_of_int a / real_of_int b\<rceil> = - (- a div b)"
1.47 +lemma ceiling_divide_eq_div: "\<lceil>of_int a / of_int b\<rceil> = - (- a div b)"
1.48    by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus)
1.49
1.50  lemma ceiling_divide_eq_div_numeral [simp]:
1.51 @@ -1574,25 +1568,13 @@
1.52  subsection \<open>Exponentiation with floor\<close>
1.53
1.54  lemma floor_power:
1.55 -  assumes "x = real_of_int (floor x)"
1.56 +  assumes "x = of_int (floor x)"
1.57    shows "floor (x ^ n) = floor x ^ n"
1.58  proof -
1.59 -  have "x ^ n = real_of_int (floor x ^ n)"
1.60 +  have "x ^ n = of_int (floor x ^ n)"
1.61      using assms by (induct n arbitrary: x) simp_all
1.62 -  then show ?thesis  by linarith
1.63 +  then show ?thesis by (metis floor_of_int)
1.64  qed
1.65 -(*
1.66 -lemma natfloor_power:
1.67 -  assumes "x = real (natfloor x)"
1.68 -  shows "natfloor (x ^ n) = natfloor x ^ n"
1.69 -proof -
1.70 -  from assms have "0 \<le> floor x" by auto
1.71 -  note assms[unfolded natfloor_def of_nat_nat[OF `0 \<le> floor x`]]
1.72 -  from floor_power[OF this]
1.73 -  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
1.74 -    by simp
1.75 -qed
1.76 -*)
1.77
1.78  lemma floor_numeral_power[simp]:
1.79    "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
```