src/HOL/Real.thy
changeset 58983 9c390032e4eb
parent 58889 5b7a9633cfa8
child 59000 6eb0725503fc
     1.1 --- a/src/HOL/Real.thy	Wed Nov 12 17:36:29 2014 +0100
     1.2 +++ b/src/HOL/Real.thy	Wed Nov 12 17:36:32 2014 +0100
     1.3 @@ -1550,6 +1550,25 @@
     1.4  by (auto simp add: power2_eq_square)
     1.5  
     1.6  
     1.7 +lemma numeral_power_eq_real_of_int_cancel_iff[simp]:
     1.8 +  "numeral x ^ n = real (y::int) \<longleftrightarrow> numeral x ^ n = y"
     1.9 +  by (metis real_numeral(1) real_of_int_inject real_of_int_power)
    1.10 +
    1.11 +lemma real_of_int_eq_numeral_power_cancel_iff[simp]:
    1.12 +  "real (y::int) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
    1.13 +  using numeral_power_eq_real_of_int_cancel_iff[of x n y]
    1.14 +  by metis
    1.15 +
    1.16 +lemma numeral_power_eq_real_of_nat_cancel_iff[simp]:
    1.17 +  "numeral x ^ n = real (y::nat) \<longleftrightarrow> numeral x ^ n = y"
    1.18 +  by (metis of_nat_eq_iff of_nat_numeral real_of_int_eq_numeral_power_cancel_iff
    1.19 +    real_of_int_of_nat_eq zpower_int)
    1.20 +
    1.21 +lemma real_of_nat_eq_numeral_power_cancel_iff[simp]:
    1.22 +  "real (y::nat) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
    1.23 +  using numeral_power_eq_real_of_nat_cancel_iff[of x n y]
    1.24 +  by metis
    1.25 +
    1.26  lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
    1.27    "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
    1.28    unfolding real_of_nat_le_iff[symmetric] by simp
    1.29 @@ -1566,6 +1585,22 @@
    1.30    "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
    1.31    unfolding real_of_int_le_iff[symmetric] by simp
    1.32  
    1.33 +lemma numeral_power_less_real_of_nat_cancel_iff[simp]:
    1.34 +  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
    1.35 +  unfolding real_of_nat_less_iff[symmetric] by simp
    1.36 +
    1.37 +lemma real_of_nat_less_numeral_power_cancel_iff[simp]:
    1.38 +  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
    1.39 +  unfolding real_of_nat_less_iff[symmetric] by simp
    1.40 +
    1.41 +lemma numeral_power_less_real_of_int_cancel_iff[simp]:
    1.42 +  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::int) ^ n < a"
    1.43 +  unfolding real_of_int_less_iff[symmetric] by simp
    1.44 +
    1.45 +lemma real_of_int_less_numeral_power_cancel_iff[simp]:
    1.46 +  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
    1.47 +  unfolding real_of_int_less_iff[symmetric] by simp
    1.48 +
    1.49  lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
    1.50    "(- numeral x::real) ^ n \<le> real a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
    1.51    unfolding real_of_int_le_iff[symmetric] by simp
    1.52 @@ -1719,9 +1754,15 @@
    1.53  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
    1.54    by linarith
    1.55  
    1.56 +lemma floor_eq_iff: "floor x = b \<longleftrightarrow> real b \<le> x \<and> x < real (b + 1)"
    1.57 +  by linarith
    1.58 +
    1.59  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
    1.60    by linarith
    1.61  
    1.62 +lemma floor_add2[simp]: "floor (real a + x) = a + floor x"
    1.63 +  by linarith
    1.64 +
    1.65  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
    1.66    by linarith
    1.67  
    1.68 @@ -2015,6 +2056,14 @@
    1.69      by simp
    1.70  qed
    1.71  
    1.72 +lemma floor_numeral_power[simp]:
    1.73 +  "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
    1.74 +  by (metis floor_of_int of_int_numeral of_int_power)
    1.75 +
    1.76 +lemma ceiling_numeral_power[simp]:
    1.77 +  "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n"
    1.78 +  by (metis ceiling_of_int of_int_numeral of_int_power)
    1.79 +
    1.80  
    1.81  subsection {* Implementation of rational real numbers *}
    1.82