# HG changeset patch
# User hoelzl
# Date 1334752160 -7200
# Node ID d20bdee675dc201baa43502e30569de124c80a3a
# Parent  5e7e394f78d467e6c0c7ddda49a67d53b444ad47
add lemmas to remove real conversions when compared to power of numerals

diff -r 5e7e394f78d4 -r d20bdee675dc 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: