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"