src/HOL/Real.thy
changeset 66912 a99a7cbf0fb5
parent 66793 deabce3ccf1f
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Real.thy	Tue Oct 24 10:59:15 2017 +0200
     1.2 +++ b/src/HOL/Real.thy	Tue Oct 24 18:48:21 2017 +0200
     1.3 @@ -1378,62 +1378,6 @@
     1.4    for u x :: real
     1.5    by (auto simp add: power2_eq_square)
     1.6  
     1.7 -lemma numeral_power_eq_real_of_int_cancel_iff [simp]:
     1.8 -  "numeral x ^ n = real_of_int y \<longleftrightarrow> numeral x ^ n = y"
     1.9 -  by (metis of_int_eq_iff of_int_numeral of_int_power)
    1.10 -
    1.11 -lemma real_of_int_eq_numeral_power_cancel_iff [simp]:
    1.12 -  "real_of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
    1.13 -  using numeral_power_eq_real_of_int_cancel_iff [of x n y] by metis
    1.14 -
    1.15 -lemma numeral_power_eq_real_of_nat_cancel_iff [simp]:
    1.16 -  "numeral x ^ n = real y \<longleftrightarrow> numeral x ^ n = y"
    1.17 -  using of_nat_eq_iff by fastforce
    1.18 -
    1.19 -lemma real_of_nat_eq_numeral_power_cancel_iff [simp]:
    1.20 -  "real y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
    1.21 -  using numeral_power_eq_real_of_nat_cancel_iff [of x n y] by metis
    1.22 -
    1.23 -lemma numeral_power_le_real_of_nat_cancel_iff [simp]:
    1.24 -  "(numeral x :: real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
    1.25 -  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
    1.26 -
    1.27 -lemma real_of_nat_le_numeral_power_cancel_iff [simp]:
    1.28 -  "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
    1.29 -  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
    1.30 -
    1.31 -lemma numeral_power_le_real_of_int_cancel_iff [simp]:
    1.32 -  "(numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
    1.33 -  by (metis ceiling_le_iff ceiling_of_int of_int_numeral of_int_power)
    1.34 -
    1.35 -lemma real_of_int_le_numeral_power_cancel_iff [simp]:
    1.36 -  "real_of_int a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
    1.37 -  by (metis floor_of_int le_floor_iff of_int_numeral of_int_power)
    1.38 -
    1.39 -lemma numeral_power_less_real_of_nat_cancel_iff [simp]:
    1.40 -  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
    1.41 -  by (metis of_nat_less_iff of_nat_numeral of_nat_power)
    1.42 -
    1.43 -lemma real_of_nat_less_numeral_power_cancel_iff [simp]:
    1.44 -  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
    1.45 -  by (metis of_nat_less_iff of_nat_numeral of_nat_power)
    1.46 -
    1.47 -lemma numeral_power_less_real_of_int_cancel_iff [simp]:
    1.48 -  "(numeral x::real) ^ n < real_of_int a \<longleftrightarrow> (numeral x::int) ^ n < a"
    1.49 -  by (meson not_less real_of_int_le_numeral_power_cancel_iff)
    1.50 -
    1.51 -lemma real_of_int_less_numeral_power_cancel_iff [simp]:
    1.52 -  "real_of_int a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
    1.53 -  by (meson not_less numeral_power_le_real_of_int_cancel_iff)
    1.54 -
    1.55 -lemma neg_numeral_power_le_real_of_int_cancel_iff [simp]:
    1.56 -  "(- numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
    1.57 -  by (metis of_int_le_iff of_int_neg_numeral of_int_power)
    1.58 -
    1.59 -lemma real_of_int_le_neg_numeral_power_cancel_iff [simp]:
    1.60 -  "real_of_int a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
    1.61 -  by (metis of_int_le_iff of_int_neg_numeral of_int_power)
    1.62 -
    1.63  
    1.64  subsection \<open>Density of the Reals\<close>
    1.65