# HG changeset patch
# User immler
# Date 1415810192 -3600
# Node ID 9c390032e4eb01f148b2c233b38975e56afa0d61
# Parent  27e7e3f9e665bb2fd22c48f79506e07c92244f00
cancel real of power of numeral also for equality and strict inequality;
simplify floor of power of numeral;
lemmas about real/floor

diff -r 27e7e3f9e665 -r 9c390032e4eb src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Nov 12 17:36:29 2014 +0100
+++ b/src/HOL/Real.thy	Wed Nov 12 17:36:32 2014 +0100
@@ -1550,6 +1550,25 @@
 by (auto simp add: power2_eq_square)
 
 
+lemma numeral_power_eq_real_of_int_cancel_iff[simp]:
+  "numeral x ^ n = real (y::int) \<longleftrightarrow> numeral x ^ n = y"
+  by (metis real_numeral(1) real_of_int_inject real_of_int_power)
+
+lemma real_of_int_eq_numeral_power_cancel_iff[simp]:
+  "real (y::int) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_real_of_int_cancel_iff[of x n y]
+  by metis
+
+lemma numeral_power_eq_real_of_nat_cancel_iff[simp]:
+  "numeral x ^ n = real (y::nat) \<longleftrightarrow> numeral x ^ n = y"
+  by (metis of_nat_eq_iff of_nat_numeral real_of_int_eq_numeral_power_cancel_iff
+    real_of_int_of_nat_eq zpower_int)
+
+lemma real_of_nat_eq_numeral_power_cancel_iff[simp]:
+  "real (y::nat) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_real_of_nat_cancel_iff[of x n y]
+  by metis
+
 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
@@ -1566,6 +1585,22 @@
   "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
   unfolding real_of_int_le_iff[symmetric] by simp
 
+lemma numeral_power_less_real_of_nat_cancel_iff[simp]:
+  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
+  unfolding real_of_nat_less_iff[symmetric] by simp
+
+lemma real_of_nat_less_numeral_power_cancel_iff[simp]:
+  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
+  unfolding real_of_nat_less_iff[symmetric] by simp
+
+lemma numeral_power_less_real_of_int_cancel_iff[simp]:
+  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::int) ^ n < a"
+  unfolding real_of_int_less_iff[symmetric] by simp
+
+lemma real_of_int_less_numeral_power_cancel_iff[simp]:
+  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
+  unfolding real_of_int_less_iff[symmetric] by simp
+
 lemma neg_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
@@ -1719,9 +1754,15 @@
 lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   by linarith
 
+lemma floor_eq_iff: "floor x = b \<longleftrightarrow> real b \<le> x \<and> x < real (b + 1)"
+  by linarith
+
 lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   by linarith
 
+lemma floor_add2[simp]: "floor (real a + x) = a + floor x"
+  by linarith
+
 lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   by linarith
 
@@ -2015,6 +2056,14 @@
     by simp
 qed
 
+lemma floor_numeral_power[simp]:
+  "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
+  by (metis floor_of_int of_int_numeral of_int_power)
+
+lemma ceiling_numeral_power[simp]:
+  "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n"
+  by (metis ceiling_of_int of_int_numeral of_int_power)
+
 
 subsection {* Implementation of rational real numbers *}