add lemmas to remove real conversions when compared to power of numerals
authorhoelzl
Wed, 18 Apr 2012 14:29:20 +0200
changeset 47598 d20bdee675dc
parent 47597 5e7e394f78d4
child 47599 400b158f1589
add lemmas to remove real conversions when compared to power of numerals
src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Apr 18 14:29:20 2012 +0200
+++ b/src/HOL/RealDef.thy	Wed Apr 18 14:29:20 2012 +0200
@@ -1567,6 +1567,30 @@
 by (auto simp add: power2_eq_square)
 
 
+lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
+  "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
+  unfolding real_of_nat_le_iff[symmetric] by simp
+
+lemma real_of_nat_le_numeral_power_cancel_iff[simp]:
+  "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
+  unfolding real_of_nat_le_iff[symmetric] by simp
+
+lemma numeral_power_le_real_of_int_cancel_iff[simp]:
+  "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
+  unfolding real_of_int_le_iff[symmetric] by simp
+
+lemma real_of_int_le_numeral_power_cancel_iff[simp]:
+  "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
+  unfolding real_of_int_le_iff[symmetric] by simp
+
+lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
+  "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
+  unfolding real_of_int_le_iff[symmetric] by simp
+
+lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
+  "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
+  unfolding real_of_int_le_iff[symmetric] by simp
+
 subsection{*Density of the Reals*}
 
 lemma real_lbound_gt_zero: